rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 1 Releases Wiki Activity

add FreeVars, and split only on used dvars in Equal

This commit is contained in:
rhiannon morris 2023-09-12 09:56:49 +02:00
parent 9973f8d07b
commit fa14ce1a02
8 changed files with 399 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
lib/Quox/Context.idr
View File

@ -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

25
lib/Quox/Equal.idr
View File

@ -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

280
lib/Quox/FreeVars.idr Normal file
View File

@ -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

27
lib/Quox/Syntax/DimEq.idr
View File

@ -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

32
lib/Quox/Syntax/Shift.idr
View File

@ -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) ->

7
lib/Quox/Syntax/Subst.idr
View File

@ -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

26
lib/Quox/Typing/Context.idr
View File

@ -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}) =

1
lib/quox-lib.ipkg
View File

@ -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,