Safe Haskell | None |
---|---|
Language | Haskell98 |
- class Apply t where
- apply1 :: Apply t => t -> Term -> t
- canProject :: QName -> Term -> Maybe (Arg Term)
- conApp :: ConHead -> Args -> Elims -> Term
- defApp :: QName -> Elims -> Elims -> Term
- argToDontCare :: Arg c Term -> Term
- piApply :: Type -> Args -> Type
- class Abstract t where
- telVars :: Telescope -> [Arg Pattern]
- namedTelVars :: Telescope -> [NamedArg Pattern]
- abstractArgs :: Abstract a => Args -> a -> a
- idS :: Substitution
- wkS :: Int -> Substitution -> Substitution
- raiseS :: Int -> Substitution
- consS :: Term -> Substitution -> Substitution
- singletonS :: Int -> Term -> Substitution
- liftS :: Int -> Substitution -> Substitution
- dropS :: Int -> Substitution -> Substitution
- composeS :: Substitution -> Substitution -> Substitution
- splitS :: Int -> Substitution -> (Substitution, Substitution)
- (++#) :: [Term] -> Substitution -> Substitution
- prependS :: Empty -> [Maybe Term] -> Substitution -> Substitution
- parallelS :: [Term] -> Substitution
- compactS :: Empty -> [Maybe Term] -> Substitution
- strengthenS :: Empty -> Int -> Substitution
- lookupS :: Substitution -> Nat -> Term
- class Subst t where
- applySubst :: Substitution -> t -> t
- raise :: Subst t => Nat -> t -> t
- raiseFrom :: Subst t => Nat -> Nat -> t -> t
- subst :: Subst t => Int -> Term -> t -> t
- strengthen :: Subst t => Empty -> t -> t
- substUnder :: Subst t => Nat -> Term -> t -> t
- 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 => Abs t -> Term -> t
- lazyAbsApp :: Subst t => Abs t -> Term -> t
- noabsApp :: Subst t => Empty -> Abs t -> t
- absBody :: Subst t => Abs t -> t
- mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a
- reAbs :: (Subst a, Free a) => Abs a -> Abs a
- underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b
- underLambdas :: Subst 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
Application
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
Nothing
Apply Permutation Source | |
Apply ClauseBody Source | |
Apply Clause Source | |
Apply Sort Source | |
Apply Type 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 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.
argToDontCare :: Arg c Term -> Term Source
piApply :: Type -> Args -> Type Source
The type must contain the right number of pis without have to perform any reduction.
Abstraction
(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 :: Telescope -> [NamedArg Pattern] Source
abstractArgs :: Abstract a => Args -> a -> a Source
Explicit substitutions
wkS :: Int -> Substitution -> Substitution Source
raiseS :: Int -> Substitution Source
consS :: Term -> Substitution -> Substitution Source
singletonS :: Int -> Term -> Substitution Source
To replace index n
by term u
, do applySubst (singletonS n u)
.
liftS :: Int -> Substitution -> Substitution Source
Lift a substitution under k binders.
dropS :: Int -> Substitution -> Substitution Source
composeS :: Substitution -> Substitution -> Substitution Source
applySubst (ρ composeS
σ) v == applySubst ρ (applySubst σ v)
splitS :: Int -> Substitution -> (Substitution, Substitution) Source
(++#) :: [Term] -> Substitution -> Substitution infixr 4 Source
prependS :: Empty -> [Maybe Term] -> Substitution -> Substitution Source
parallelS :: [Term] -> Substitution Source
strengthenS :: Empty -> Int -> Substitution Source
Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
lookupS :: Substitution -> Nat -> Term Source
Substitution and raisingshiftingweakening
Apply a substitution.
applySubst :: Substitution -> t -> t Source
strengthen :: Subst t => Empty -> t -> t Source
substUnder :: Subst t => Nat -> Term -> t -> t Source
Replace what is now de Bruijn index 0, but go under n binders.
substUnder n u == subst n (raise n u)
.
Telescopes
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope Source
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
.
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 => Abs t -> Term -> t 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 => Empty -> Abs t -> t Source
Instantiate an abstraction that doesn't use its argument.
underAbs :: Subst 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.
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 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.
|
Term :# Substitution infixr 4 | Substitution extension, ` |
Strengthen Empty Substitution | Strengthening substitution. First argument is |
Wk !Int Substitution | Weakning substitution, lifts to an extended context.
|
Lift !Int Substitution | Lifting substitution. Use this to go under a binder.
|