Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Primitive.Cubical.Base

Contents

Helper functions for building terms

Description

Implementations of the basic primitives of Cubical Agda: The interval and its operations.

Synopsis

requireCubical :: Cubical -> String -> TCM ()
primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type
primIMin' :: TCM PrimitiveImpl
primIMax' :: TCM PrimitiveImpl
primDepIMin' :: TCM PrimitiveImpl
primINeg' :: TCM PrimitiveImpl
imax :: HasBuiltins m => m Term -> m Term -> m Term
imin :: HasBuiltins m => m Term -> m Term -> m Term
ineg :: HasBuiltins m => m Term -> m Term
data Command
- = DoTransp
- | DoHComp
data KanOperation
- = TranspOp {
  - kanOpCofib :: Blocked (Arg Term)
  - kanOpBase :: Arg Term
  }
- | HCompOp {
  - kanOpCofib :: Blocked (Arg Term)
  - kanOpSides :: Arg Term
  - kanOpBase :: Arg Term
  }
kanOpName :: KanOperation -> String
data TermPosition
- = Head
- | Eliminated
headStop :: PureTCM m => TermPosition -> m Term -> m Bool
data FamilyOrNot a
- = IsFam {
  - famThing :: a
  }
- | IsNot {
  - famThing :: a
  }
familyOrNot :: IsString p => FamilyOrNot a -> p
combineSys :: forall (m :: Type -> Type). HasBuiltins m => NamesT m Term -> NamesT m Term -> [(NamesT m Term, NamesT m Term)] -> NamesT m Term
combineSys' :: forall (m :: Type -> Type). HasBuiltins m => NamesT m Term -> NamesT m Term -> [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
fiber :: forall (m :: Type -> Type). (HasBuiltins m, HasConstInfo m) => NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
hfill :: forall (m :: Type -> Type). (HasBuiltins m, HasConstInfo m) => NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
decomposeInterval' :: HasBuiltins m => Term -> m [(IntMap BoolSet, [Term])]
decomposeInterval :: HasBuiltins m => Term -> m [(IntMap Bool, [Term])]
reduce2Lam :: Term -> ReduceM (Blocked Term)
isCubicalSubtype :: PureTCM m => Type -> m (Maybe (Term, Term, Term, Term))

Documentation

requireCubical Source #

Arguments

:: Cubical	Which variant of Cubical Agda is required?
-> String	Why, exactly, do we need Cubical to be enabled?
-> 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 #

Our good friend the interval type.

primIMin' :: TCM PrimitiveImpl Source #

Implements both the min connection and conjunction on the cofibration classifier.

primIMax' :: TCM PrimitiveImpl Source #

Implements both the max connection and disjunction on the cofibration classifier.

primDepIMin' :: TCM PrimitiveImpl Source #

primDepIMin expresses that cofibrations are closed under Σ. Thus, it serves as a dependent version of primIMin (which, recall, implements _∧_). This is required for the construction of the Kan operations in Id.

primINeg' :: TCM PrimitiveImpl Source #

Negation on the interval. Negation satisfies De Morgan's laws, and their implementation is handled here.

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

A helper for evaluating max on the interval in TCM&co.

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

A helper for evaluating min on the interval in TCM&co.

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

A helper for evaluating neg on the interval in TCM&co.

data Command Source #

Constructors

DoTransp
DoHComp

Instances

Instances details

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

data KanOperation Source #

Our Kan operations are transp and hcomp. The KanOperation record stores the data associated with a Kan operation on arbitrary types: A cofibration and an element of that type.

Constructors

TranspOp	A transport problem consists of a cofibration, marking where the transport is constant, and a term to move from the fibre over i0 to the fibre over i1.
Fields kanOpCofib :: Blocked (Arg Term) When this cofibration holds, the transport must definitionally be the identity. This is handled generically by `primTransHComp` but specific Kan operations may still need it. kanOpBase :: Arg Term This is the term in `A i0` which we are transporting.
HCompOp	A composition problem consists of a partial element and a base. Semantically, this is justified by the types being Kan fibrations, i.e., having the lifting property against trivial cofibrations. While the specified cofibration may not be trivial, (φ ∨ ~ r) for r ∉ φ is always a trivial cofibration.
Fields kanOpCofib :: Blocked (Arg Term) When this cofibration holds, the transport must definitionally be the identity. This is handled generically by `primTransHComp` but specific Kan operations may still need it. kanOpSides :: Arg Term The partial element itself kanOpBase :: Arg Term This is the term in `A i0` which we are transporting.

kanOpName :: KanOperation -> String Source #

The built-in name associated with a particular Kan operation.

data TermPosition Source #

For the Kan operations in Glue and hcomp {Type}, we optimise evaluation a tiny bit by differentiating the term produced when evaluating a Kan operation by itself vs evaluating it under unglue. (See headStop below.)

Constructors

Head
Eliminated

Instances

Instances details

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

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

Kan operations for the "unstable" type formers (Glue, hcomp {Type}) are computed "negatively": they never actually produce a glue φ t a term. Instead, we block the computation unless such a term would reduce further, which happens in two cases:

when the formula φ is i1, in which case we reduce to t;
when we're under an unglue, i.e. in Eliminated TermPosition, in which case we reduce to a.

data FamilyOrNot a Source #

Are we looking at a family of things, or at a single thing?

Constructors

IsFam
Fields famThing :: a
IsNot
Fields famThing :: a

Instances

Instances details

Functor FamilyOrNot Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b (<$) :: a -> FamilyOrNot b -> FamilyOrNot a #
Foldable FamilyOrNot Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods fold :: Monoid m => FamilyOrNot m -> m foldMap :: Monoid m => (a -> m) -> FamilyOrNot a -> m foldMap' :: Monoid m => (a -> m) -> FamilyOrNot a -> m foldr :: (a -> b -> b) -> b -> FamilyOrNot a -> b foldr' :: (a -> b -> b) -> b -> FamilyOrNot a -> b foldl :: (b -> a -> b) -> b -> FamilyOrNot a -> b foldl' :: (b -> a -> b) -> b -> FamilyOrNot a -> b foldr1 :: (a -> a -> a) -> FamilyOrNot a -> a foldl1 :: (a -> a -> a) -> FamilyOrNot a -> a toList :: FamilyOrNot a -> [a] null :: FamilyOrNot a -> Bool length :: FamilyOrNot a -> Int elem :: Eq a => a -> FamilyOrNot a -> Bool maximum :: Ord a => FamilyOrNot a -> a minimum :: Ord a => FamilyOrNot a -> a sum :: Num a => FamilyOrNot a -> a product :: Num a => FamilyOrNot a -> a
Traversable FamilyOrNot Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods traverse :: Applicative f => (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b) sequenceA :: Applicative f => FamilyOrNot (f a) -> f (FamilyOrNot a) mapM :: Monad m => (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b) sequence :: Monad m => FamilyOrNot (m a) -> m (FamilyOrNot a)
Reduce a => Reduce (FamilyOrNot a) Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base 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.Base Methods showsPrec :: Int -> FamilyOrNot a -> ShowS show :: FamilyOrNot a -> String showList :: [FamilyOrNot a] -> ShowS
Eq a => Eq (FamilyOrNot a) Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods (==) :: FamilyOrNot a -> FamilyOrNot a -> Bool (/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool

familyOrNot :: IsString p => FamilyOrNot a -> p Source #

Helper functions for building terms

combineSys Source #

Arguments

:: forall (m :: Type -> Type). HasBuiltins m
=> NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]	A list of `(ψ, PartialP ψ λ o → A (... o ...))` mappings. Note that by definitional proof-irrelevance of `IsOne`, the actual injection can not matter here.
-> NamesT m Term

Build a partial element. The type of the resulting partial element can depend on the computed extent, which we denote by φ here. Note that φ is the n-ary disjunction of all the ψs.

combineSys' :: forall (m :: Type -> Type). HasBuiltins m => NamesT m Term -> NamesT m Term -> [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term) Source #

Build a partial element, and compute its extent. See combineSys for the details.

fiber :: forall (m :: Type -> Type). (HasBuiltins m, HasConstInfo m) => NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term Source #

Helper function for constructing the type of fibres of a function over a given point.

hfill :: forall (m :: Type -> Type). (HasBuiltins m, HasConstInfo m) => NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term Source #

Helper function for constructing the filler of a given composition problem.

decomposeInterval' :: HasBuiltins m => Term -> m [(IntMap BoolSet, [Term])] Source #

Decompose an interval expression φ : I into a set of possible assignments for the variables mentioned in φ, together any leftover neutral terms that could not be put into IntervalView form.

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

Decompose an interval expression i : I as in decomposeInterval', but discard any inconsistent mappings.

reduce2Lam :: Term -> ReduceM (Blocked Term) Source #

isCubicalSubtype :: PureTCM m => Type -> m (Maybe (Term, Term, Term, Term)) Source #

Are we looking at an application of the Sub type? If so, return: * The type we're an extension of * The extent * The partial element.