Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Primitive.Cubical

Synopsis

- requireCubical :: Cubical -> String -> TCM ()
- primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type
- primINeg' :: TCM PrimitiveImpl
- primDepIMin' :: TCM PrimitiveImpl
- primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl
- primIMin' :: TCM PrimitiveImpl
- primIMax' :: TCM PrimitiveImpl
- imax :: HasBuiltins m => m Term -> m Term -> m Term
- imin :: HasBuiltins m => m Term -> m Term -> m Term
- primIdJ :: TCM PrimitiveImpl
- primIdElim' :: TCM PrimitiveImpl
- primPOr :: TCM PrimitiveImpl
- primPartial' :: TCM PrimitiveImpl
- primPartialP' :: TCM PrimitiveImpl
- primSubOut' :: TCM PrimitiveImpl
- primIdFace' :: TCM PrimitiveImpl
- primIdPath' :: TCM PrimitiveImpl
- primTrans' :: TCM PrimitiveImpl
- primHComp' :: TCM PrimitiveImpl
- data TranspOrHComp
  - = DoTransp
  - | DoHComp
- cmdToName :: TranspOrHComp -> String
- data FamilyOrNot a
  - = IsFam {
    - famThing :: a
    }
  - | IsNot {
    - famThing :: a
    }
- mkGComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
- unglueTranspGlue :: PureTCM m => Arg Term -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> m Term
- data TermPosition
  - = Head
  - | Eliminated
- headStop :: PureTCM m => TermPosition -> m Term -> m Bool
- compGlue :: PureTCM m => TranspOrHComp -> Arg Term -> Maybe (Arg Term) -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term)
- compHCompU :: PureTCM m => TranspOrHComp -> Arg Term -> Maybe (Arg Term) -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term)
- primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
- primComp :: TCM PrimitiveImpl
- prim_glueU' :: TCM PrimitiveImpl
- prim_unglueU' :: TCM PrimitiveImpl
- primGlue' :: TCM PrimitiveImpl
- prim_glue' :: TCM PrimitiveImpl
- prim_unglue' :: TCM PrimitiveImpl
- primFaceForall' :: TCM PrimitiveImpl
- decomposeInterval :: HasBuiltins m => Term -> m [(Map Int Bool, [Term])]
- decomposeInterval' :: HasBuiltins m => Term -> m [(Map Int (Set Bool), [Term])]
- transpTel :: Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args
- trFillTel :: Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) TCM Args

# Documentation

requireCubical Source #

Arguments

:: Cubical | Which variant of Cubical Agda is required?
-> String |
-> TCM () |

Checks that the correct variant of Cubical Agda is activated. Note that `--erased-cubical` "counts as" `--cubical` in erased contexts.

primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type Source #

primINeg' :: TCM PrimitiveImpl Source #

primDepIMin' :: TCM PrimitiveImpl Source #

primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl Source #

primIMin' :: TCM PrimitiveImpl Source #

primIMax' :: TCM PrimitiveImpl Source #

imax :: HasBuiltins m => m Term -> m Term -> m Term Source #

imin :: HasBuiltins m => m Term -> m Term -> m Term Source #

primIdJ :: TCM PrimitiveImpl Source #

primIdElim' :: TCM PrimitiveImpl Source #

primPOr :: TCM PrimitiveImpl Source #

primPartial' :: TCM PrimitiveImpl Source #

primPartialP' :: TCM PrimitiveImpl Source #

primSubOut' :: TCM PrimitiveImpl Source #

primIdFace' :: TCM PrimitiveImpl Source #

primIdPath' :: TCM PrimitiveImpl Source #

primTrans' :: TCM PrimitiveImpl Source #

primHComp' :: TCM PrimitiveImpl Source #

data TranspOrHComp Source #

Constructors

DoTransp |
DoHComp |

#### Instances

Instances details

Show TranspOrHComp Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TranspOrHComp -> ShowS Source # show :: TranspOrHComp -> String Source # showList :: [TranspOrHComp] -> ShowS Source #
Eq TranspOrHComp Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: TranspOrHComp -> TranspOrHComp -> Bool Source # (/=) :: TranspOrHComp -> TranspOrHComp -> Bool Source #

cmdToName :: TranspOrHComp -> String Source #

data FamilyOrNot a Source #

Constructors

IsFam |

Fields

- famThing :: a

IsNot |

Fields

- famThing :: a

#### Instances

Instances details

Foldable FamilyOrNot Source # |

Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

fold :: Monoid m => FamilyOrNot m -> m Source #

foldMap :: Monoid m => (a -> m) -> FamilyOrNot a -> m Source #

foldMap' :: Monoid m => (a -> m) -> FamilyOrNot a -> m Source #

foldr :: (a -> b -> b) -> b -> FamilyOrNot a -> b Source #

foldr' :: (a -> b -> b) -> b -> FamilyOrNot a -> b Source #

foldl :: (b -> a -> b) -> b -> FamilyOrNot a -> b Source #

foldl' :: (b -> a -> b) -> b -> FamilyOrNot a -> b Source #

foldr1 :: (a -> a -> a) -> FamilyOrNot a -> a Source #

foldl1 :: (a -> a -> a) -> FamilyOrNot a -> a Source #

toList :: FamilyOrNot a -> [a] Source #

null :: FamilyOrNot a -> Bool Source #

length :: FamilyOrNot a -> Int Source #

elem :: Eq a => a -> FamilyOrNot a -> Bool Source #

maximum :: Ord a => FamilyOrNot a -> a Source #

minimum :: Ord a => FamilyOrNot a -> a Source #

sum :: Num a => FamilyOrNot a -> a Source #

product :: Num a => FamilyOrNot a -> a Source #

Traversable FamilyOrNot Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods traverse :: Applicative f => (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b) Source # sequenceA :: Applicative f => FamilyOrNot (f a) -> f (FamilyOrNot a) Source # mapM :: Monad m => (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b) Source # sequence :: Monad m => FamilyOrNot (m a) -> m (FamilyOrNot a) Source #
Functor FamilyOrNot Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b Source # (<$) :: a -> FamilyOrNot b -> FamilyOrNot a Source #
Reduce a => Reduce (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a) Source # reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a)) Source #
Show a => Show (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> FamilyOrNot a -> ShowS Source # show :: FamilyOrNot a -> String Source # showList :: [FamilyOrNot a] -> ShowS Source #
Eq a => Eq (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: FamilyOrNot a -> FamilyOrNot a -> Bool Source # (/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool Source #

mkGComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term) Source #

Define a "ghcomp" version of gcomp. Normal comp looks like:

comp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u ] (forward A 0 u0)

So for "gcomp" we compute:

gcomp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u, ~ phi -> forward A 0 u0 ] (forward A 0 u0)

The point of this is that gcomp does not produce any empty systems (if phi = 0 it will reduce to "forward A 0 u".

unglueTranspGlue :: PureTCM m => Arg Term -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> m Term Source #

data TermPosition Source #

Constructors

Head |
Eliminated |

#### Instances

Instances details

Show TermPosition Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TermPosition -> ShowS Source # show :: TermPosition -> String Source # showList :: [TermPosition] -> ShowS Source #
Eq TermPosition Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: TermPosition -> TermPosition -> Bool Source # (/=) :: TermPosition -> TermPosition -> Bool Source #

headStop :: PureTCM m => TermPosition -> m Term -> m Bool Source #

compGlue :: PureTCM m => TranspOrHComp -> Arg Term -> Maybe (Arg Term) -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term) Source #

compHCompU :: PureTCM m => TranspOrHComp -> Arg Term -> Maybe (Arg Term) -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term) Source #

primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term) Source #

primComp :: TCM PrimitiveImpl Source #

prim_glueU' :: TCM PrimitiveImpl Source #

prim_unglueU' :: TCM PrimitiveImpl Source #

primGlue' :: TCM PrimitiveImpl Source #

prim_glue' :: TCM PrimitiveImpl Source #

prim_unglue' :: TCM PrimitiveImpl Source #

primFaceForall' :: TCM PrimitiveImpl Source #

decomposeInterval :: HasBuiltins m => Term -> m [(Map Int Bool, [Term])] Source #

decomposeInterval' :: HasBuiltins m => Term -> m [(Map Int (Set Bool), [Term])] Source #

transpTel :: Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args Source #

Tries to `primTransp` a whole telescope of arguments, following the rule for Σ types. If a type in the telescope does not support transp, `transpTel` throws it as an exception.

trFillTel :: Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) TCM Args Source #

Like `transpTel` but performing a transpFill.