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

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 -> TCM ()
- primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type
- primIMin' :: TCM PrimitiveImpl
- primIMax' :: 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?
-> 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.

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 Source # show :: Command -> String Source # showList :: [Command] -> ShowS Source #
Eq Command Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods (==) :: Command -> Command -> Bool Source # (/=) :: Command -> Command -> Bool Source #

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 Source # show :: TermPosition -> String Source # showList :: [TermPosition] -> ShowS Source #
Eq TermPosition Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical.Base Methods (==) :: TermPosition -> TermPosition -> Bool Source # (/=) :: TermPosition -> TermPosition -> Bool Source #

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 Source # (<$) :: a -> FamilyOrNot b -> FamilyOrNot a Source #
Foldable FamilyOrNot Source # |

Instance details

Defined in Agda.TypeChecking.Primitive.Cubical.Base

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.Base 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 #
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 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.Base Methods (==) :: FamilyOrNot a -> FamilyOrNot a -> Bool Source # (/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool Source #

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.