From fa14ce1a023e9ae91acc6c84b33111c7b8bbfa27 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 12 Sep 2023 09:56:49 +0200 Subject: [PATCH] add FreeVars, and split only on used dvars in Equal --- lib/Quox/Context.idr | 34 +++-- lib/Quox/Equal.idr | 25 ++-- lib/Quox/FreeVars.idr | 280 ++++++++++++++++++++++++++++++++++++ lib/Quox/Syntax/DimEq.idr | 27 ++-- lib/Quox/Syntax/Shift.idr | 32 ++++- lib/Quox/Syntax/Subst.idr | 7 + lib/Quox/Typing/Context.idr | 26 +++- lib/quox-lib.ipkg | 1 + 8 files changed, 399 insertions(+), 33 deletions(-) create mode 100644 lib/Quox/FreeVars.idr diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr index 0a923b3..91b3fcd 100644 --- a/lib/Quox/Context.idr +++ b/lib/Quox/Context.idr @@ -109,10 +109,17 @@ fromSnocVect [<] = [<] fromSnocVect (sx :< x) = fromSnocVect sx :< x +public export +tabulateLT : (n : Nat) -> ((i : Nat) -> (0 p : i `LT` n) => tm i) -> + Context tm n +tabulateLT 0 f = [<] +tabulateLT (S k) f = + tabulateLT k (\i => f i @{lteSuccRight %search}) :< f k @{reflexive} + public export tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n -tabulate f 0 = [<] -tabulate f (S k) = tabulate f k :< f k +tabulate f n = tabulateLT n (\i => f i) +-- [todo] fixup argument order lol public export replicate : (n : Nat) -> a -> Context' a n @@ -182,6 +189,12 @@ export %hint succGT = LTESucc reflexive +public export +drop : (m : Nat) -> Context term (m + n) -> Context term n +drop 0 ctx = ctx +drop (S m) (ctx :< _) = drop m ctx + + parameters {auto _ : Applicative f} export traverse : (forall n. tm1 n -> f (tm2 n)) -> @@ -260,16 +273,17 @@ unzip3 (tel :< (x, y, z)) = public export -lengthPrf : Telescope _ from to -> (len ** len + from = to) -lengthPrf [<] = (0 ** Refl) +lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to) +lengthPrf [<] = Element 0 Refl lengthPrf (tel :< _) = - let len = lengthPrf tel in (S len.fst ** cong S len.snd) + let len = lengthPrf tel in Element (S len.fst) (cong S len.snd) export -lengthPrf0 : Context _ to -> (len ** len = to) +lengthPrf0 : Context _ to -> Singleton to lengthPrf0 ctx = - let len = lengthPrf ctx in - (len.fst ** rewrite sym $ plusZeroRightNeutral len.fst in len.snd) + let Element len prf = lengthPrf ctx in + rewrite sym prf `trans` plusZeroRightNeutral len in + [|len|] public export %inline length : Telescope {} -> Nat @@ -288,6 +302,10 @@ foldl : {0 acc : Nat -> Type} -> foldl f z [<] = z foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t) +export %inline +foldl_ : (acc -> tm -> acc) -> acc -> Telescope' tm from to -> acc +foldl_ f z tel = foldl f z tel + export %inline foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a foldMap f = foldl (\acc, tm => acc <+> f tm) neutral diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index ea54e4f..82e7b22 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -4,6 +4,7 @@ import Quox.BoolExtra import public Quox.Typing import Data.Maybe import Quox.EffExtra +import Quox.FreeVars %default total @@ -673,9 +674,12 @@ parameters (loc : Loc) (ctx : TyContext d n) fromInner = lift . map fst . runState mode private - eachFace : Applicative f => (EqContext n -> DSubst d 0 -> f ()) -> f () - eachFace act = - for_ (splits loc ctx.dctx) $ \th => act (makeEqContext ctx th) th + eachFace : Applicative f => FreeVars d -> + (EqContext n -> DSubst d 0 -> f ()) -> f () + eachFace fvs act = + let Val d = ctx.dimLen in + for_ (splits loc ctx.dctx fvs) $ \th => + act (makeEqContext ctx th) th private CompareAction : Nat -> Nat -> Type @@ -683,18 +687,23 @@ parameters (loc : Loc) (ctx : TyContext d n) Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner () private - runCompare : CompareAction d n -> Eff Equal () - runCompare act = fromInner $ eachFace $ act !(askAt DEFS) + runCompare : FreeVars d -> CompareAction d n -> Eff Equal () + runCompare fvs act = fromInner $ eachFace fvs $ act !(askAt DEFS) + + private + fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d + fdvAll ts = + let Val d = ctx.dimLen; Val n = ctx.termLen in foldMap fdv ts namespace Term export covering compare : (ty, s, t : Term d n) -> Eff Equal () - compare ty s t = runCompare $ \defs, ectx, th => + compare ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th => compare0 defs ectx (ty // th) (s // th) (t // th) export covering compareType : (s, t : Term d n) -> Eff Equal () - compareType s t = runCompare $ \defs, ectx, th => + compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th => compareType defs ectx (s // th) (t // th) namespace Elim @@ -702,7 +711,7 @@ parameters (loc : Loc) (ctx : TyContext d n) ||| of the same type!! export covering compare : (e, f : Elim d n) -> Eff Equal () - compare e f = runCompare $ \defs, ectx, th => + compare e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th => ignore $ compare0 defs ectx (e // th) (f // th) namespace Term diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr new file mode 100644 index 0000000..acff6ae --- /dev/null +++ b/lib/Quox/FreeVars.idr @@ -0,0 +1,280 @@ +module Quox.FreeVars + +import Quox.Syntax.Term.Base +import Data.Maybe +import Data.Nat +import Data.Singleton +import Data.SortedSet + + +public export +record FreeVars n where + constructor FV + vars : Context' Bool n + + +export %inline +(||) : FreeVars n -> FreeVars n -> FreeVars n +FV s || FV t = FV $ zipWith (\x, y => x || y) s t + +export %inline +(&&) : FreeVars n -> FreeVars n -> FreeVars n +FV s && FV t = FV $ zipWith (\x, y => x && y) s t + +export %inline Semigroup (FreeVars n) where (<+>) = (||) + +export %inline [AndS] Semigroup (FreeVars n) where (<+>) = (&&) + +export +only : {n : Nat} -> Var n -> FreeVars n +only i = FV $ only' i where + only' : {n' : Nat} -> Var n' -> Context' Bool n' + only' VZ = replicate (pred n') False :< True + only' (VS i) = only' i :< False + +export %inline +all : {n : Nat} -> FreeVars n +all = FV $ replicate n True + +export %inline +none : {n : Nat} -> FreeVars n +none = FV $ replicate n False + + +export %inline +uncons : FreeVars (S n) -> (FreeVars n, Bool) +uncons (FV (xs :< x)) = (FV xs, x) + + +export %inline {n : Nat} -> Monoid (FreeVars n) where neutral = none +export %inline [AndM] {n : Nat} -> Monoid (FreeVars n) where neutral = all + + +private +self : {n : Nat} -> Context' (FreeVars n) n +self = tabulate (\i => FV $ tabulate (== i) n) n + +export +shift : forall from, to. Shift from to -> FreeVars from -> FreeVars to +shift by (FV xs) = FV $ shift' by xs where + shift' : Shift from' to' -> Context' Bool from' -> Context' Bool to' + shift' SZ ctx = ctx + shift' (SS by) ctx = shift' by ctx :< False + + +export +fromSet : {n : Nat} -> SortedSet (Var n) -> FreeVars n +fromSet vs = FV $ tabulateLT n $ \i => contains (V i) vs + +export +toSet : {n : Nat} -> FreeVars n -> SortedSet (Var n) +toSet (FV vs) = + foldl_ (\s, i => maybe s (\i => insert i s) i) empty $ + zipWith (\i, b => guard b $> i) (tabulateLT n V) vs + + +public export +interface HasFreeVars (0 term : Nat -> Type) where + constructor HFV + fv : {n : Nat} -> term n -> FreeVars n + +public export +interface HasFreeDVars (0 term : TermLike) where + constructor HFDV + fdv : {d, n : Nat} -> term d n -> FreeVars d + +export +Fdv : (0 term : TermLike) -> {n : Nat} -> + HasFreeDVars term => HasFreeVars (\d => term d n) +Fdv term @{HFDV fdv} = HFV fdv + + +export +fvEach : {n1, n2 : Nat} -> HasFreeVars env => + Subst env n1 n2 -> Context' (Lazy (FreeVars n2)) n1 +fvEach (Shift by) = map (delay . shift by) self +fvEach (t ::: th) = fvEach th :< fv t + +export +fdvEach : {d, n1, n2 : Nat} -> HasFreeDVars env => + Subst (env d) n1 n2 -> Context' (Lazy (FreeVars d)) n1 +fdvEach (Shift by) = replicate n1 none +fdvEach (t ::: th) = fdvEach th :< fdv t + + +export +HasFreeVars Dim where + fv (K _ _) = none + fv (B i _) = only i + + +export +{s : Nat} -> HasFreeVars term => HasFreeVars (Scoped s term) where + fv (S _ (Y body)) = FV $ drop s (fv body).vars + fv (S _ (N body)) = fv body + +export +implementation [DScope] + {s : Nat} -> HasFreeDVars term => + HasFreeDVars (\d, n => Scoped s (\d' => term d' n) d) +where + fdv (S _ (Y body)) = FV $ drop s (fdv body).vars + fdv (S _ (N body)) = fdv body + +export +fvD : {0 term : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (term d)) => + Scoped s (\d => term d n) d -> FreeVars n +fvD (S _ (Y body)) = fv body +fvD (S _ (N body)) = fv body + +export +fdvT : HasFreeDVars term => {s, d, n : Nat} -> Scoped s (term d) n -> FreeVars d +fdvT (S _ (Y body)) = fdv body +fdvT (S _ (N body)) = fdv body + + +private +guardM : Monoid a => Bool -> Lazy a -> a +guardM b x = if b then x else neutral + +export +implementation + (HasFreeVars term, HasFreeVars env) => + HasFreeVars (WithSubst term env) +where + fv (Sub term subst) = + let Val from = getFrom subst in + foldMap (uncurry guardM) $ zipWith (,) (fv term).vars (fvEach subst) + +export +implementation [WithSubst] + ((forall d. HasFreeVars (term d)), HasFreeDVars term, HasFreeDVars env) => + HasFreeDVars (\d => WithSubst (term d) (env d)) +where + fdv (Sub term subst) = + let Val from = getFrom subst in + fdv term <+> + foldMap (uncurry guardM) (zipWith (,) (fv term).vars (fdvEach subst)) + + +export HasFreeVars (Term d) +export HasFreeVars (Elim d) + +export +HasFreeVars (Term d) where + fv (TYPE {}) = none + fv (Pi {arg, res, _}) = fv arg <+> fv res + fv (Lam {body, _}) = fv body + fv (Sig {fst, snd, _}) = fv fst <+> fv snd + fv (Pair {fst, snd, _}) = fv fst <+> fv snd + fv (Enum {}) = none + fv (Tag {}) = none + fv (Eq {ty, l, r, _}) = fvD ty <+> fv l <+> fv r + fv (DLam {body, _}) = fvD body + fv (Nat {}) = none + fv (Zero {}) = none + fv (Succ {p, _}) = fv p + fv (BOX {ty, _}) = fv ty + fv (Box {val, _}) = fv val + fv (E e) = fv e + fv (CloT s) = fv s + fv (DCloT s) = fv s.term + +export +HasFreeVars (Elim d) where + fv (F {}) = none + fv (B i _) = only i + fv (App {fun, arg, _}) = fv fun <+> fv arg + fv (CasePair {pair, ret, body, _}) = fv pair <+> fv ret <+> fv body + fv (CaseEnum {tag, ret, arms, _}) = + fv tag <+> fv ret <+> foldMap fv (values arms) + fv (CaseNat {nat, ret, zero, succ, _}) = + fv nat <+> fv ret <+> fv zero <+> fv succ + fv (CaseBox {box, ret, body, _}) = + fv box <+> fv ret <+> fv body + fv (DApp {fun, _}) = fv fun + fv (Ann {tm, ty, _}) = fv tm <+> fv ty + fv (Coe {ty, val, _}) = fvD ty <+> fv val + fv (Comp {ty, val, zero, one, _}) = + fv ty <+> fv val <+> fvD zero <+> fvD one + fv (TypeCase {ty, ret, arms, def, _}) = + fv ty <+> fv ret <+> fv def <+> foldMap (\x => fv x.snd) (toList arms) + fv (CloE s) = fv s + fv (DCloE s) = fv s.term + + + +private +expandDShift : {d1 : Nat} -> Shift d1 d2 -> Context' (Dim d2) d1 +expandDShift by = tabulateLT d1 (\i => BV i noLoc // by) + +private +expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Context' (Dim d2) d1 +expandDSubst (Shift by) = expandDShift by +expandDSubst (t ::: th) = expandDSubst th :< t + + +private +fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars term => + term d1 n -> DSubst d1 d2 -> FreeVars d2 +fdvSubst' t th = + fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th) +where + maybeOnly : {d : Nat} -> Bool -> Dim d -> FreeVars d + maybeOnly True (B i _) = only i + maybeOnly _ _ = none + +private +fdvSubst : {d, n : Nat} -> HasFreeDVars term => + WithSubst (\d => term d n) Dim d -> FreeVars d +fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th + + +export HasFreeDVars Term +export HasFreeDVars Elim + +export +HasFreeDVars Term where + fdv (TYPE {}) = none + fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res + fdv (Lam {body, _}) = fdvT body + fdv (Sig {fst, snd, _}) = fdv fst <+> fdvT snd + fdv (Pair {fst, snd, _}) = fdv fst <+> fdv snd + fdv (Enum {}) = none + fdv (Tag {}) = none + fdv (Eq {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r + fdv (DLam {body, _}) = fdv @{DScope} body + fdv (Nat {}) = none + fdv (Zero {}) = none + fdv (Succ {p, _}) = fdv p + fdv (BOX {ty, _}) = fdv ty + fdv (Box {val, _}) = fdv val + fdv (E e) = fdv e + fdv (CloT s) = fdv s @{WithSubst} + fdv (DCloT s) = fdvSubst s + +export +HasFreeDVars Elim where + fdv (F {}) = none + fdv (B {}) = none + fdv (App {fun, arg, _}) = fdv fun <+> fdv arg + fdv (CasePair {pair, ret, body, _}) = fdv pair <+> fdvT ret <+> fdvT body + fdv (CaseEnum {tag, ret, arms, _}) = + fdv tag <+> fdvT ret <+> foldMap fdv (values arms) + fdv (CaseNat {nat, ret, zero, succ, _}) = + fdv nat <+> fdvT ret <+> fdv zero <+> fdvT succ + fdv (CaseBox {box, ret, body, _}) = + fdv box <+> fdvT ret <+> fdvT body + fdv (DApp {fun, arg, _}) = + fdv fun <+> fv arg + fdv (Ann {tm, ty, _}) = + fdv tm <+> fdv ty + fdv (Coe {ty, p, q, val, _}) = + fdv @{DScope} ty <+> fv p <+> fv q <+> fdv val + fdv (Comp {ty, p, q, val, r, zero, one, _}) = + fdv ty <+> fv p <+> fv q <+> fdv val <+> + fv r <+> fdv @{DScope} zero <+> fdv @{DScope} one + fdv (TypeCase {ty, ret, arms, def, _}) = + fdv ty <+> fdv ret <+> fdv def <+> foldMap (\x => fdvT x.snd) (toList arms) + fdv (CloE s) = fdv s @{WithSubst} + fdv (DCloE s) = fdvSubst s diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr index c8079d8..0ef0ddd 100644 --- a/lib/Quox/Syntax/DimEq.idr +++ b/lib/Quox/Syntax/DimEq.idr @@ -6,6 +6,7 @@ import public Quox.Syntax.Subst import public Quox.Context import Quox.Pretty import Quox.Name +import Quox.FreeVars import Data.Maybe import Data.Nat @@ -185,20 +186,28 @@ split1 e loc eqs = case setConst VZ e loc eqs of C (eqs :< _) => Just (eqs, K e loc ::: id) export %inline -split : Loc -> DimEq' (S d) -> List (Split d) -split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs) +split1' : DimConst -> Loc -> DimEq' (S d) -> List (Split d) +split1' e loc eqs = toList $ split1 e loc eqs + +export %inline +split : Loc -> DimEq' (S d) -> Bool -> List (Split d) +split loc eqs False = split1' Zero loc eqs +split loc eqs True = split1' Zero loc eqs <+> split1' One loc eqs export -splits' : Loc -> DimEq' d -> List (DSubst d 0) -splits' _ [<] = [id] -splits' loc eqs@(_ :< _) = - [th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs'] +splits' : Loc -> DimEq' d -> FreeVars d -> List (DSubst d 0) +splits' _ [<] _ = [id] +splits' loc eqs@(_ :< _) us = do + let (us, u) = uncons us + (eqs', th) <- split loc eqs u + ph <- splits' loc eqs' us + pure $ th . ph ||| the Loc is put into each of the DimConsts export %inline -splits : Loc -> DimEq d -> List (DSubst d 0) -splits _ ZeroIsOne = [] -splits loc (C eqs) = splits' loc eqs +splits : Loc -> DimEq d -> FreeVars d -> List (DSubst d 0) +splits _ ZeroIsOne _ = [] +splits loc (C eqs) fvs = splits' loc eqs fvs private diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr index ecfe476..9e005b7 100644 --- a/lib/Quox/Syntax/Shift.idr +++ b/lib/Quox/Syntax/Shift.idr @@ -4,6 +4,8 @@ import public Quox.Syntax.Var import Data.Nat import Data.So +import Data.Singleton +import Syntax.PreorderReasoning %default total @@ -146,6 +148,25 @@ weakViaNat s by = %transform "Shift.weak" Shift.weak = weakViaNat +export +getFrom : {to : Nat} -> Shift from to -> Singleton from +getFrom SZ = Val to +getFrom (SS by) = getFrom by + +private +0 getFromViaNatProof : (by : Shift from to) -> from = to `minus` by.nat +getFromViaNatProof by = Calc $ + |~ from + ~~ minus (by.nat + from) by.nat ..<(minusPlus {}) + ~~ minus to by.nat ..<(cong (flip minus by.nat) (shiftDiff by)) + +private +getFromViaNat : {to : Nat} -> Shift from to -> Singleton from +getFromViaNat by = rewrite getFromViaNatProof by in Val _ + +%transform "Shift.getFrom" Shift.getFrom = getFromViaNat + + public export shift : Shift from to -> Var from -> Var to shift SZ i = i @@ -178,11 +199,12 @@ by . SS bz = SS $ by . bz private 0 compNatProof : (by : Shift from mid) -> (bz : Shift mid to) -> to = by.nat + bz.nat + from -compNatProof by bz = - trans (shiftDiff bz) $ - trans (cong (bz.nat +) (shiftDiff by)) $ - trans (plusAssociative bz.nat by.nat from) $ - cong (+ from) (plusCommutative bz.nat by.nat) +compNatProof by bz = Calc $ + |~ to + ~~ bz.nat + mid ...(shiftDiff {}) + ~~ bz.nat + (by.nat + from) ...(cong (bz.nat +) (shiftDiff {})) + ~~ bz.nat + by.nat + from ...(plusAssociative {}) + ~~ by.nat + bz.nat + from ...(cong (+ from) (plusCommutative {})) private %inline compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) -> diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr index 976f7bb..e584d4b 100644 --- a/lib/Quox/Syntax/Subst.idr +++ b/lib/Quox/Syntax/Subst.idr @@ -7,6 +7,7 @@ import Quox.Name import Data.Nat import Data.List import Data.SnocVect +import Data.Singleton import Derive.Prelude %default total @@ -124,6 +125,12 @@ one : f n -> Subst f (S n) n one x = fromSnocVect [< x] +export +getFrom : {to : Nat} -> Subst _ from to -> Singleton from +getFrom (Shift by) = getFrom by +getFrom (t ::: th) = [|S $ getFrom th|] + + ||| whether two substitutions with the same codomain have the same shape ||| (the same number of terms and the same shift at the end). if so, they ||| also have the same domain diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr index c1db5fe..15e5b1e 100644 --- a/lib/Quox/Typing/Context.idr +++ b/lib/Quox/Typing/Context.idr @@ -33,7 +33,7 @@ record TyContext d n where dctx : DimEq d dnames : BContext d tctx : TContext d n - tnames : BContext n + tnames : BContext n -- only used for printing qtys : QContext n -- only used for printing %name TyContext ctx @@ -46,7 +46,7 @@ record EqContext n where dassign : DimAssign dimLen -- only used for printing dnames : BContext dimLen -- only used for printing tctx : TContext 0 n - tnames : BContext n + tnames : BContext n -- only used for printing qtys : QContext n -- only used for printing %name EqContext ctx @@ -78,6 +78,10 @@ public export CtxExtension : Nat -> Nat -> Nat -> Type CtxExtension d = Telescope ((Qty, BindName,) . Term d) +public export +CtxExtension0 : Nat -> Nat -> Nat -> Type +CtxExtension0 d = Telescope ((BindName,) . Term d) + namespace TyContext public export %inline empty : TyContext 0 0 @@ -100,10 +104,18 @@ namespace TyContext qtys = qtys . qs } + export %inline + extendTyN0 : CtxExtension0 d n1 n2 -> TyContext d n1 -> TyContext d n2 + extendTyN0 xss = extendTyN (map (Zero,) xss) + export %inline extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n) 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 extendDim : BindName -> TyContext d n -> TyContext (S d) n extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) = @@ -158,7 +170,7 @@ makeEqContext' ctx th = MkEqContext { export makeEqContext : TyContext d n -> DSubst d 0 -> EqContext n makeEqContext ctx@(MkTyContext {dnames, _}) th = - let (d' ** Refl) = lengthPrf0 dnames in makeEqContext' ctx th + let Val d = lengthPrf0 dnames in makeEqContext' ctx th namespace EqContext public export %inline @@ -183,10 +195,18 @@ namespace EqContext dassign, dnames } + export %inline + extendTyN0 : CtxExtension0 0 n1 n2 -> EqContext n1 -> EqContext n2 + extendTyN0 xss = extendTyN (map (Zero,) xss) + export %inline extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n) 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 extendDim : BindName -> DimConst -> EqContext n -> EqContext n extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) = diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 6fd3882..41cc4cd 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -32,6 +32,7 @@ modules = Quox.Syntax.Term.Pretty, Quox.Syntax.Term.Subst, Quox.Syntax.Var, + Quox.FreeVars, Quox.Displace, Quox.Definition, Quox.Whnf.Interface,