Safe Haskell | None |
---|---|
Language | Haskell98 |
- class Apply t where
- applys :: Apply t => t -> [Term] -> t
- apply1 :: Apply t => t -> Term -> t
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: ConHead -> Args -> Elims -> Term
- defApp :: QName -> Elims -> Elims -> Term
- argToDontCare :: Arg Term -> Term
- piApply :: Type -> Args -> Type
- class Abstract t where
- telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
- namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
- abstractArgs :: Abstract a => Args -> a -> a
- class DeBruijn a where
- idS :: Substitution' a
- wkS :: Int -> Substitution' a -> Substitution' a
- raiseS :: Int -> Substitution' a
- consS :: DeBruijn a => a -> Substitution' a -> Substitution' a
- singletonS :: DeBruijn a => Int -> a -> Substitution' a
- liftS :: Int -> Substitution' a -> Substitution' a
- dropS :: Int -> Substitution' a -> Substitution' a
- composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a
- splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
- (++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
- prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a
- parallelS :: DeBruijn a => [a] -> Substitution' a
- compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a
- strengthenS :: Empty -> Int -> Substitution' a
- lookupS :: Subst a a => Substitution' a -> Nat -> a
- class DeBruijn t => Subst t a | a -> t where
- raise :: Subst t a => Nat -> a -> a
- raiseFrom :: Subst t a => Nat -> Nat -> a -> a
- subst :: Subst t a => Int -> t -> a -> a
- strengthen :: Subst t a => Empty -> a -> a
- substUnder :: Subst t a => Nat -> t -> a -> a
- type TelView = TelV Type
- data TelV a = TelV {}
- type ListTel' a = [Dom (a, Type)]
- type ListTel = ListTel' ArgName
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- telToList :: Telescope -> ListTel
- telToArgs :: Telescope -> [Arg ArgName]
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a
- bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel
- telView' :: Type -> TelView
- telView'UpTo :: Int -> Type -> TelView
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- mkLam :: Arg ArgName -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePi_ :: Telescope -> Type -> Type
- teleLam :: Telescope -> Term -> Term
- class TeleNoAbs a where
- dLub :: Sort -> Abs Sort -> Sort
- absApp :: Subst t a => Abs a -> t -> a
- lazyAbsApp :: Subst t a => Abs a -> t -> a
- noabsApp :: Subst t a => Empty -> Abs a -> a
- absBody :: Subst t a => Abs a -> a
- mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a
- reAbs :: (Subst t a, Free a) => Abs a -> Abs a
- underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b
- underLambdas :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term
- class GetBody a where
- pts :: Sort -> Sort -> Sort
- sLub :: Sort -> Sort -> Sort
- lvlView :: Term -> Level
- levelMax :: [PlusLevel] -> Level
- sortTm :: Sort -> Term
- levelSort :: Level -> Sort
- levelTm :: Level -> Term
- unLevelAtom :: LevelAtom -> Term
- data Substitution' a
- = IdS
- | EmptyS
- | a :# (Substitution' a)
- | Strengthen Empty (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term
Application
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
Apply Permutation Source # | |
Apply ClauseBody Source # | |
Apply Clause Source # | |
Apply Sort Source # | |
Apply Term Source # | |
Apply CompiledClauses Source # | |
Apply FunctionInverse Source # | |
Apply PrimFun Source # | |
Apply Defn Source # | |
Apply Projection Source # | |
Apply Definition Source # | |
Apply RewriteRule Source # | |
Apply DisplayTerm Source # | |
Apply t => Apply [t] Source # | |
Apply [Occurrence] Source # | |
Apply [Polarity] Source # | |
Apply t => Apply (Maybe t) Source # | |
Apply a => Apply (Ptr a) Source # | |
DoDrop a => Apply (Drop a) Source # | |
Apply t => Apply (Blocked t) Source # | |
Subst Term a => Apply (Tele a) Source # | |
Apply a => Apply (Case a) Source # | |
Apply a => Apply (WithArity a) Source # | |
(Apply a, Apply b) => Apply (a, b) Source # | |
Apply v => Apply (Map k v) Source # | |
(Apply a, Apply b, Apply c) => Apply (a, b, c) Source # | |
canProject :: QName -> Term -> Maybe (Arg Term) Source #
If $v$ is a record value, canProject f v
returns its field f
.
defApp :: QName -> Elims -> Elims -> Term Source #
defApp f us vs
applies Def f us
to further arguments vs
,
eliminating top projection redexes.
If us
is not empty, we cannot have a projection redex, since
the record argument is the first one.
piApply :: Type -> Args -> Type Source #
(x:A)->B(x) piApply
[u] = B(u)
Precondition: The type must contain the right number of pis without having to perform any reduction.
piApply
is potentially unsafe, the monadic piApplyM
is preferable.
Abstraction
class Abstract t where Source #
(abstract args v)
.apply
args --> v[args]
Abstract Permutation Source # | |
Abstract ClauseBody Source # | |
Abstract Clause Source # | |
Abstract Sort Source # | |
Abstract Telescope Source # | |
Abstract Type Source # | |
Abstract Term Source # | |
Abstract CompiledClauses Source # | |
Abstract FunctionInverse Source # | |
Abstract PrimFun Source # | |
Abstract Defn Source # | |
Abstract Projection Source # | |
Abstract Definition Source # | |
Abstract RewriteRule Source # |
|
Abstract t => Abstract [t] Source # | |
Abstract [Occurrence] Source # | |
Abstract [Polarity] Source # | |
Abstract t => Abstract (Maybe t) Source # | |
DoDrop a => Abstract (Drop a) Source # | |
Abstract a => Abstract (Case a) Source # | |
Abstract a => Abstract (WithArity a) Source # | |
Abstract v => Abstract (Map k v) Source # | |
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #
abstractArgs :: Abstract a => Args -> a -> a Source #
Explicit substitutions
class DeBruijn a where Source #
debruijnVar :: Int -> a Source #
debruijnNamedVar :: String -> Int -> a Source #
debruijnView :: a -> Maybe Int Source #
idS :: Substitution' a Source #
wkS :: Int -> Substitution' a -> Substitution' a Source #
raiseS :: Int -> Substitution' a Source #
consS :: DeBruijn a => a -> Substitution' a -> Substitution' a Source #
singletonS :: DeBruijn a => Int -> a -> Substitution' a Source #
To replace index n
by term u
, do applySubst (singletonS n u)
.
liftS :: Int -> Substitution' a -> Substitution' a Source #
Lift a substitution under k binders.
dropS :: Int -> Substitution' a -> Substitution' a Source #
composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a Source #
applySubst (ρ composeS
σ) v == applySubst ρ (applySubst σ v)
splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a) Source #
(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4 Source #
prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a Source #
parallelS :: DeBruijn a => [a] -> Substitution' a Source #
strengthenS :: Empty -> Int -> Substitution' a Source #
Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
Substitution and raisingshiftingweakening
class DeBruijn t => Subst t a | a -> t where Source #
Apply a substitution.
applySubst :: Substitution' t -> a -> a Source #
strengthen :: Subst t a => Empty -> a -> a Source #
substUnder :: Subst t a => Nat -> t -> a -> a Source #
Replace what is now de Bruijn index 0, but go under n binders.
substUnder n u == subst n (raise n u)
.
Telescopes
telFromList :: ListTel -> Telescope Source #
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a Source #
Turn a typed binding (x1 .. xn : A)
into a telescope.
bindsWithHidingToTel' :: (Name -> a) -> [WithHiding Name] -> Dom Type -> ListTel' a Source #
Turn a typed binding (x1 .. xn : A)
into a telescope.
bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel Source #
telView' :: Type -> TelView Source #
Takes off all exposed function domains from the given type.
This means that it does not reduce to expose Pi
-types.
telView'UpTo :: Int -> Type -> TelView Source #
telView'UpTo n t
takes off the first n
exposed function types of t
.
Takes off all (exposed ones) if n < 0
.
telePi :: Telescope -> Type -> Type Source #
Uses free variable analysis to introduce noAbs
bindings.
dLub :: Sort -> Abs Sort -> Sort Source #
Dependent least upper bound, to assign a level to expressions
like forall i -> Set i
.
dLub s1 i.s2 = omega
if i
appears in the rigid variables of s2
.
Functions on abstractions
lazyAbsApp :: Subst t a => Abs a -> t -> a Source #
Instantiate an abstraction. Lazy in the term, which allow it to be
IMPOSSIBLE in the case where the variable shouldn't be used but we
cannot use noabsApp
. Used in Apply.
noabsApp :: Subst t a => Empty -> Abs a -> a Source #
Instantiate an abstraction that doesn't use its argument.
underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b Source #
underAbs k a b
applies k
to a
and the content of
abstraction b
and puts the abstraction back.
a
is raised if abstraction was proper such that
at point of application of k
and the content of b
are at the same context.
Precondition: a
and b
are at the same context at call time.
class GetBody a where Source #
Methods to retrieve the clauseBody
.
Syntactic equality and order
Level stuff
pts :: Sort -> Sort -> Sort Source #
The `rule'
, if Agda is considered as a functional
pure type system (pts).
TODO: This needs to be properly implemented, requiring
refactoring of Agda's handling of levels.
Without impredicativity or SizeUniv
, Agda's pts rule is
just the least upper bound, which is total and commutative.
The handling of levels relies on this simplification.
unLevelAtom :: LevelAtom -> Term Source #
data Substitution' a Source #
Substitutions.
IdS | Identity substitution.
|
EmptyS | Empty substitution, lifts from the empty context.
Apply this to closed terms you want to use in a non-empty context.
|
a :# (Substitution' a) infixr 4 | Substitution extension, ` |
Strengthen Empty (Substitution' a) | Strengthening substitution. First argument is |
Wk !Int (Substitution' a) | Weakning substitution, lifts to an extended context.
|
Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Functor Substitution' Source # | |
Foldable Substitution' Source # | |
Traversable Substitution' Source # | |
Pretty Substitution Source # | |
KillRange Substitution Source # | |
InstantiateFull Substitution Source # | |
Subst a a => Subst a (Substitution' a) Source # | |
Show a => Show (Substitution' a) Source # | |
TermSize a => TermSize (Substitution' a) Source # | |
(Show a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # | |
type Substitution = Substitution' Term Source #
Orphan instances
Eq NotBlocked Source # | |
Eq LevelAtom Source # | |
Eq PlusLevel Source # | |
Eq Level Source # | |
Eq Sort Source # | |
Eq Term Source # | Syntactic |
Eq Candidate Source # | |
Eq Section Source # | |
Eq Constraint Source # | |
Ord NotBlocked Source # | |
Ord LevelAtom Source # | |
Ord PlusLevel Source # | |
Ord Level Source # | |
Ord Sort Source # | |
Ord Term Source # | |
Eq (Substitution' Term) Source # | |
Eq t => Eq (Blocked t) Source # | |
(Subst t a, Eq a) => Eq (Tele a) Source # | |
Eq a => Eq (Type' a) Source # | Syntactic |
(Subst t a, Eq a) => Eq (Abs a) Source # | |
(Subst t a, Eq a) => Eq (Elim' a) Source # | |
Ord (Substitution' Term) Source # | |
Ord t => Ord (Blocked t) Source # | |
(Subst t a, Ord a) => Ord (Tele a) Source # | |
Ord a => Ord (Type' a) Source # | |
(Subst t a, Ord a) => Ord (Abs a) Source # | |
(Subst t a, Ord a) => Ord (Elim' a) Source # | |