quox/lib/Quox/Typing/Context.idr

387 lines
11 KiB
Idris
Raw Normal View History

2023-03-13 16:41:57 -04:00
module Quox.Typing.Context
import Quox.Syntax
import Quox.Context
2023-03-15 10:54:51 -04:00
import Quox.Pretty
import public Data.Singleton
2023-09-17 13:09:54 -04:00
import Derive.Prelude
2023-03-13 16:41:57 -04:00
%default total
2023-09-17 13:09:54 -04:00
%language ElabReflection
2023-03-13 16:41:57 -04:00
2023-03-15 10:54:51 -04:00
public export
2023-04-01 13:16:43 -04:00
QContext : Nat -> Type
QContext = Context' Qty
2023-03-15 10:54:51 -04:00
public export
record LocalVar d n where
constructor MkLocal
type : Term d n
term : Maybe (Term d n) -- if from a `let`
%runElab deriveIndexed "LocalVar" [Show]
export
CanShift (LocalVar d) where
l // by = {type $= (// by), term $= map (// by)} l
namespace LocalVar
export %inline
letVar : (type, term : Term d n) -> LocalVar d n
letVar type term = MkLocal {type, term = Just term}
export %inline
lamVar : (type : Term d n) -> LocalVar d n
lamVar type = MkLocal {type, term = Nothing}
subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
subD th = {type $= (// th), term $= map (// th)}
weakD : LocalVar d n -> LocalVar (S d) n
weakD = subD $ shift 1
2023-03-13 16:41:57 -04:00
public export
2023-04-01 13:16:43 -04:00
TContext : TermLike
TContext d = Context (\n => LocalVar d n)
2023-03-13 16:41:57 -04:00
public export
2023-04-01 13:16:43 -04:00
QOutput : Nat -> Type
QOutput = Context' Qty
2023-03-13 16:41:57 -04:00
public export
DimAssign : Nat -> Type
DimAssign = Context' DimConst
2023-03-13 16:41:57 -04:00
public export
2023-04-01 13:16:43 -04:00
record TyContext d n where
2023-03-13 16:41:57 -04:00
constructor MkTyContext
{auto dimLen : Singleton d}
{auto termLen : Singleton n}
dctx : DimEq d
2023-05-01 21:06:25 -04:00
dnames : BContext d
2023-04-01 13:16:43 -04:00
tctx : TContext d n
tnames : BContext n -- only used for printing
2023-04-01 13:16:43 -04:00
qtys : QContext n -- only used for printing
2023-03-13 16:41:57 -04:00
%name TyContext ctx
2023-09-17 13:09:54 -04:00
%runElab deriveIndexed "TyContext" [Show]
public export
2023-04-01 13:16:43 -04:00
record EqContext n where
constructor MkEqContext
2023-03-15 10:54:51 -04:00
{dimLen : Nat}
{auto termLen : Singleton n}
2023-03-15 10:54:51 -04:00
dassign : DimAssign dimLen -- only used for printing
2023-05-01 21:06:25 -04:00
dnames : BContext dimLen -- only used for printing
2023-04-01 13:16:43 -04:00
tctx : TContext 0 n
tnames : BContext n -- only used for printing
2023-04-01 13:16:43 -04:00
qtys : QContext n -- only used for printing
%name EqContext ctx
2023-09-17 13:09:54 -04:00
%runElab deriveIndexed "EqContext" [Show]
2023-04-15 09:13:01 -04:00
public export
record WhnfContext d n where
constructor MkWhnfContext
2023-10-15 10:23:38 -04:00
{auto dimLen : Singleton d}
{auto termLen : Singleton n}
2023-05-01 21:06:25 -04:00
dnames : BContext d
tnames : BContext n
2023-04-15 09:13:01 -04:00
tctx : TContext d n
%name WhnfContext ctx
2023-09-17 13:09:54 -04:00
%runElab deriveIndexed "WhnfContext" [Show]
2023-04-15 09:13:01 -04:00
namespace TContext
export %inline
2023-04-01 13:16:43 -04:00
zeroFor : Context tm n -> QOutput n
zeroFor ctx = Zero <$ ctx
2023-09-30 12:37:44 -04:00
public export
2023-06-23 12:32:05 -04:00
extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
extendLen [<] x = x
extendLen (tel :< _) x = [|S $ extendLen tel x|]
2023-04-03 11:46:23 -04:00
public export
CtxExtension : Nat -> Nat -> Nat -> Type
2023-05-01 21:06:25 -04:00
CtxExtension d = Telescope ((Qty, BindName,) . Term d)
2023-04-03 11:46:23 -04:00
public export
CtxExtension0 : Nat -> Nat -> Nat -> Type
CtxExtension0 d = Telescope ((BindName,) . Term d)
public export
CtxExtensionLet : Nat -> Nat -> Nat -> Type
CtxExtensionLet d = Telescope ((Qty, BindName,) . LocalVar d)
public export
CtxExtensionLet0 : Nat -> Nat -> Nat -> Type
CtxExtensionLet0 d = Telescope ((BindName,) . LocalVar d)
namespace TyContext
public export %inline
2023-04-01 13:16:43 -04:00
empty : TyContext 0 0
2023-03-15 10:54:51 -04:00
empty =
MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]}
2023-03-26 10:10:39 -04:00
public export %inline
2023-04-01 13:16:43 -04:00
null : TyContext d n -> Bool
2023-03-26 10:10:39 -04:00
null ctx = null ctx.dnames && null ctx.tnames
export %inline
extendTyLetN : CtxExtensionLet d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyLetN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
let (qs, xs, ls) = unzip3 xss in
MkTyContext {
dctx, dnames,
termLen = extendLen xss termLen,
tctx = tctx . ls,
tnames = tnames . xs,
qtys = qtys . qs
}
export %inline
extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
export %inline
extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyLetN0 xss = extendTyLetN (map (Zero,) xss)
export %inline
extendTyN0 : CtxExtension0 d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN0 xss = extendTyN (map (Zero,) xss)
export %inline
extendTyLet : Qty -> BindName -> Term d n -> Term d n ->
TyContext d n -> TyContext d (S n)
extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
export %inline
2023-05-01 21:06:25 -04:00
extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
2023-03-15 10:54:51 -04:00
extendTy q x s = extendTyN [< (q, x, s)]
export %inline
extendTy0 : BindName -> Term d n -> TyContext d n -> TyContext d (S n)
extendTy0 = extendTy Zero
export %inline
2023-05-01 21:06:25 -04:00
extendDim : BindName -> TyContext d n -> TyContext (S d) n
extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
MkTyContext {
dctx = dctx :<? Nothing,
dnames = dnames :< x,
dimLen = [|S dimLen|],
tctx = map weakD tctx,
tnames, qtys
}
export %inline
2023-04-01 13:16:43 -04:00
eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}
2023-04-15 09:13:01 -04:00
export
toWhnfContext : TyContext d n -> WhnfContext d n
toWhnfContext (MkTyContext {dnames, tnames, tctx, _}) =
MkWhnfContext {dnames, tnames, tctx}
namespace QOutput
2023-04-01 13:16:43 -04:00
export %inline
(+) : QOutput n -> QOutput n -> QOutput n
(+) = zipWith (+)
2023-04-01 13:16:43 -04:00
export %inline
(*) : Qty -> QOutput n -> QOutput n
(*) pi = map (pi *)
2023-04-01 13:16:43 -04:00
export %inline
zeroFor : TyContext _ n -> QOutput n
zeroFor ctx = zeroFor ctx.tctx
export
makeDAssign : DSubst d 0 -> DimAssign d
2023-05-01 21:06:25 -04:00
makeDAssign (Shift SZ) = [<]
makeDAssign (K e _ ::: th) = makeDAssign th :< e
export
2023-04-01 13:16:43 -04:00
makeEqContext' : {d : Nat} -> TyContext d n -> DSubst d 0 -> EqContext n
2023-03-15 10:54:51 -04:00
makeEqContext' ctx th = MkEqContext {
termLen = ctx.termLen,
dassign = makeDAssign th,
dnames = ctx.dnames,
tctx = map (subD th) ctx.tctx,
2023-03-15 10:54:51 -04:00
tnames = ctx.tnames,
qtys = ctx.qtys
}
2023-03-15 10:54:51 -04:00
export
2023-04-01 13:16:43 -04:00
makeEqContext : TyContext d n -> DSubst d 0 -> EqContext n
2023-03-15 10:54:51 -04:00
makeEqContext ctx@(MkTyContext {dnames, _}) th =
let Val d = lengthPrf0 dnames in makeEqContext' ctx th
2023-03-15 10:54:51 -04:00
namespace EqContext
public export %inline
2023-04-01 13:16:43 -04:00
empty : EqContext 0
2023-03-15 10:54:51 -04:00
empty = MkEqContext {
dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<]
}
2023-03-26 10:10:39 -04:00
public export %inline
2023-04-01 13:16:43 -04:00
null : EqContext n -> Bool
2023-03-26 10:10:39 -04:00
null ctx = null ctx.dnames && null ctx.tnames
export %inline
extendTyLetN : CtxExtensionLet 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyLetN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
let (qs, xs, ls) = unzip3 xss in
MkEqContext {
termLen = extendLen xss termLen,
tctx = tctx . ls,
tnames = tnames . xs,
qtys = qtys . qs,
dassign, dnames
}
export %inline
extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
export %inline
extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyLetN0 xss = extendTyLetN (map (Zero,) xss)
export %inline
extendTyN0 : CtxExtension0 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN0 xss = extendTyN (map (Zero,) xss)
export %inline
extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n ->
EqContext n -> EqContext (S n)
extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
export %inline
2023-05-01 21:06:25 -04:00
extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
2023-03-15 10:54:51 -04:00
extendTy q x s = extendTyN [< (q, x, s)]
export %inline
extendTy0 : BindName -> Term 0 n -> EqContext n -> EqContext (S n)
extendTy0 = extendTy Zero
export %inline
2023-05-01 21:06:25 -04:00
extendDim : BindName -> DimConst -> EqContext n -> EqContext n
extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
MkEqContext {dassign = dassign :< e, dnames = dnames :< x,
tctx, tnames, qtys}
export
2023-04-01 13:16:43 -04:00
toTyContext : (e : EqContext n) -> TyContext e.dimLen n
2023-03-15 10:54:51 -04:00
toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
MkTyContext {
2023-11-27 15:01:36 -05:00
dctx = fromGround dnames dassign,
tctx = map (subD $ shift0 dimLen) tctx,
2023-03-15 10:54:51 -04:00
dnames, tnames, qtys
}
2023-04-15 09:13:01 -04:00
export
toWhnfContext : (ectx : EqContext n) -> WhnfContext 0 n
toWhnfContext (MkEqContext {tnames, tctx, _}) =
MkWhnfContext {dnames = [<], tnames, tctx}
2023-10-15 10:23:38 -04:00
export
injElim : WhnfContext d n -> Elim 0 0 -> Elim d n
injElim ctx e =
let Val d = ctx.dimLen; Val n = ctx.termLen in
e // shift0 d // shift0 n
2023-04-15 09:13:01 -04:00
namespace WhnfContext
public export %inline
empty : WhnfContext 0 0
empty = MkWhnfContext [<] [<] [<]
export
extendTy' : BindName -> LocalVar d n -> WhnfContext d n -> WhnfContext d (S n)
extendTy' x var (MkWhnfContext {termLen, dnames, tnames, tctx}) =
MkWhnfContext {
dnames,
termLen = [|S termLen|],
tnames = tnames :< x,
tctx = tctx :< var
}
export %inline
extendTy : BindName -> Term d n -> WhnfContext d n -> WhnfContext d (S n)
extendTy x ty ctx = extendTy' x (lamVar ty) ctx
export %inline
extendTyLet : BindName -> (type, term : Term d n) ->
WhnfContext d n -> WhnfContext d (S n)
extendTyLet x type term ctx = extendTy' x (letVar {type, term}) ctx
2023-04-15 09:13:01 -04:00
export
2023-05-01 21:06:25 -04:00
extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
2023-04-15 09:13:01 -04:00
WhnfContext (s + d) n
2023-10-15 10:23:38 -04:00
extendDimN ns (MkWhnfContext {dnames, tnames, tctx, dimLen}) =
2023-04-15 09:13:01 -04:00
MkWhnfContext {
2023-10-15 10:23:38 -04:00
dimLen = [|Val s + dimLen|],
2023-04-15 09:13:01 -04:00
dnames = dnames ++ toSnocVect' ns,
tctx = map (subD $ shift s) tctx,
2023-04-15 09:13:01 -04:00
tnames
}
export
2023-05-01 21:06:25 -04:00
extendDim : BindName -> WhnfContext d n -> WhnfContext (S d) n
2023-04-15 09:13:01 -04:00
extendDim i = extendDimN [< i]
2023-03-15 10:54:51 -04:00
private
2023-05-14 13:58:46 -04:00
prettyTContextElt : {opts : _} ->
BContext d -> BContext n ->
Qty -> BindName -> LocalVar d n -> Eff Pretty (Doc opts)
prettyTContextElt dnames tnames q x s = do
q <- prettyQty q; dot <- dotD
x <- prettyTBind x; colon <- colonD
ty <- withPrec Outer $ prettyTerm dnames tnames s.type; eq <- cstD
tm <- traverse (withPrec Outer . prettyTerm dnames tnames) s.term
d <- askAt INDENT
let qx = hcat [q, dot, x]
pure $ case tm of
Nothing =>
ifMultiline (hsep [qx, colon, ty]) (vsep [qx, indent d $ colon <++> ty])
Just tm =>
ifMultiline (hsep [qx, colon, ty, eq, tm])
(vsep [qx, indent d $ colon <++> ty, indent d $ eq <++> tm])
2023-05-14 13:58:46 -04:00
private
prettyTContext' : {opts : _} ->
BContext d -> QContext n -> BContext n ->
TContext d n -> Eff Pretty (SnocList (Doc opts))
prettyTContext' _ [<] [<] [<] = pure [<]
prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) =
[|prettyTContext' dnames qtys tnames tys :<
prettyTContextElt dnames tnames q x t|]
export
prettyTContext : {opts : _} ->
BContext d -> QContext n -> BContext n ->
TContext d n -> Eff Pretty (Doc opts)
2023-12-21 12:03:57 -05:00
prettyTContext dnames qtys tnames tys = do
comma <- commaD
sepSingle . exceptLast (<+> comma) . toList <$>
prettyTContext' dnames qtys tnames tys
2023-05-14 13:58:46 -04:00
export
prettyTyContext : {opts : _} -> TyContext d n -> Eff Pretty (Doc opts)
prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
case dctx of
C [<] => prettyTContext dnames qtys tnames tctx
_ => pure $
2023-12-21 12:03:57 -05:00
sepSingle [!(prettyDimEq dnames dctx) <++> !pipeD,
!(prettyTContext dnames qtys tnames tctx)]
2023-05-14 13:58:46 -04:00
export
prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)
prettyEqContext ctx = prettyTyContext $ toTyContext ctx