rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

minor tweaks in Q.Typing.Context

Browse source
This commit is contained in:
rhiannon morris 2024-04-14 15:48:10 +02:00
parent 95a0b38d74
commit 32b9fe124f
1 changed files with 17 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
lib/Quox/Typing/Context.idr
View file

@ -21,10 +21,6 @@ record LocalVar d n where
term : Maybe (Term d n) -- if from a `let` term : Maybe (Term d n) -- if from a `let`
%runElab deriveIndexed "LocalVar" [Show] %runElab deriveIndexed "LocalVar" [Show]
export
CanShift (LocalVar d) where
l // by = {type $= (// by), term $= map (// by)} l
namespace LocalVar namespace LocalVar
export %inline export %inline
letVar : (type, term : Term d n) -> LocalVar d n letVar : (type, term : Term d n) -> LocalVar d n
@ -34,15 +30,25 @@ namespace LocalVar
lamVar : (type : Term d n) -> LocalVar d n lamVar : (type : Term d n) -> LocalVar d n
lamVar type = MkLocal {type, term = Nothing} lamVar type = MkLocal {type, term = Nothing}
subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n export %inline
subD th = {type $= (// th), term $= map (// th)} mapVar : (Term d n -> Term d' n') -> LocalVar d n -> LocalVar d' n'
mapVar f = {type $= f, term $= map f}
export %inline
subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
subD th = mapVar (// th)
export %inline
weakD : LocalVar d n -> LocalVar (S d) n weakD : LocalVar d n -> LocalVar (S d) n
weakD = subD $ shift 1 weakD = subD $ shift 1
export %inline CanShift (LocalVar d) where l // by = mapVar (// by) l
export %inline CanDSubst LocalVar where l // by = mapVar (// by) l
export %inline CanTSubst LocalVar where l // by = mapVar (// by) l
public export public export
TContext : TermLike TContext : TermLike
TContext d = Context (\n => LocalVar d n) TContext d = Context (LocalVar d)
public export public export
QOutput : Nat -> Type QOutput : Nat -> Type
@ -59,7 +65,7 @@ record TyContext d n where
{auto dimLen : Singleton d} {auto dimLen : Singleton d}
{auto termLen : Singleton n} {auto termLen : Singleton n}
dctx : DimEq d dctx : DimEq d
dnames : BContext d dnames : BContext d -- only used for printing
tctx : TContext d n tctx : TContext d n
tnames : BContext n -- only used for printing tnames : BContext n -- only used for printing
qtys : QContext n -- only used for printing qtys : QContext n -- only used for printing
@ -122,8 +128,9 @@ CtxExtensionLet0 d = Telescope ((BindName,) . LocalVar d)
namespace TyContext namespace TyContext
public export %inline public export %inline
empty : TyContext 0 0 empty : TyContext 0 0
empty = empty = MkTyContext {
MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]} dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]
}
public export %inline public export %inline
null : TyContext d n -> Bool null : TyContext d n -> Bool