From b6264f388d8f55609bdc9c2f0ec7cc52cf60e1f0 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 17 Jul 2023 03:50:16 +0200 Subject: [PATCH] fix #11 the easy way tightening just pushes substitutions all the way through. bleh --- lib/Quox/Reduce.idr | 12 +- lib/Quox/Syntax/Term/Subst.idr | 49 ------ lib/Quox/Syntax/Term/Tighten.idr | 272 +++++++++++++++++-------------- 3 files changed, 157 insertions(+), 176 deletions(-) diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr index 4879e9f..8bc1d9a 100644 --- a/lib/Quox/Reduce.idr +++ b/lib/Quox/Reduce.idr @@ -219,7 +219,7 @@ private coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc -> ScopeTermN s d n -> ScopeTermN s d n coeScoped ty p q loc (S names (Y body)) = - S names $ Y $ E $ Coe (weakDS s ty) p q body loc + ST names $ E $ Coe (weakDS s ty) p q body loc coeScoped ty p q loc (S names (N body)) = S names $ N $ E $ Coe ty p q body loc @@ -273,7 +273,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret] (BVT 0 loc) loc - res = SY [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc + res = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc pure (arg, res) tycasePi t = throw $ ExpectedPi t.loc ctx.names t @@ -291,7 +291,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd] (BVT 0 loc) loc - snd = SY [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc + snd = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc pure (fst, snd) tycaseSig t = throw $ ExpectedSig t.loc ctx.names t @@ -322,7 +322,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n) a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc a1 = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc a' = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc - a = SY [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc + a = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc l = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc r = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc pure (a0, a1, a, l, r) @@ -692,8 +692,8 @@ CanWhnf Elim Reduce.isRedexE where whnf defs ctx (Coe (S _ (N ty)) _ _ val coeLoc) = whnf defs ctx $ Ann val ty coeLoc - whnf defs ctx (Coe (S [< i] ty) p q val coeLoc) = do - Element ty tynf <- whnf defs (extendDim i ctx) ty.term + whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do + Element ty tynf <- whnf defs (extendDim i ctx) ty Element val valnf <- whnf defs ctx val pushCoe defs ctx i ty p q val coeLoc diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr index c0b62f6..6a9c899 100644 --- a/lib/Quox/Syntax/Term/Subst.idr +++ b/lib/Quox/Syntax/Term/Subst.idr @@ -2,7 +2,6 @@ module Quox.Syntax.Term.Subst import Quox.No import Quox.Syntax.Term.Base -import Quox.Syntax.Term.Tighten import Data.SnocVect %default total @@ -325,51 +324,3 @@ mutual pushSubstsWith th (comp th ps ph) e pushSubstsWith th ph (DCloE (Sub e ps)) = pushSubstsWith (ps . th) ph e - - -private %inline -CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> - (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n -CompHY {ty, p, q, val, r, zero, one, loc} = - let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in - Comp { - ty = dsub1 ty q, p, q, - val = E $ Coe ty p q val val.loc, r, - -- [fixme] better locations for these vars? - zero = SY zero.names $ E $ - Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc, - one = SY one.names $ E $ - Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc, - loc - } - -public export %inline -CompH' : (ty : DScopeTerm d n) -> - (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) -> - (zero : DScopeTerm d n) -> - (one : DScopeTerm d n) -> - (loc : Loc) -> - Elim d n -CompH' {ty, p, q, val, r, zero, one, loc} = - case dsqueeze ty of - S _ (N ty) => Comp {ty, p, q, val, r, zero, one, loc} - S _ (Y _) => CompHY {ty, p, q, val, r, zero, one, loc} - -||| heterogeneous composition, using Comp and Coe (and subst) -||| -||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ } -||| ≔ -||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r { -||| 0 j ⇒ coe [i ⇒ A] @j @q t₀; -||| 1 j ⇒ coe [i ⇒ A] @j @q t₁ -||| } -public export %inline -CompH : (i : BindName) -> (ty : Term (S d) n) -> - (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) -> - (j0 : BindName) -> (zero : Term (S d) n) -> - (j1 : BindName) -> (one : Term (S d) n) -> - (loc : Loc) -> - Elim d n -CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} = - CompH' {ty = SY [< i] ty, p, q, val, r, - zero = SY [< j0] zero, one = SY [< j0] one, loc} diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr index 931ac65..8d67c2b 100644 --- a/lib/Quox/Syntax/Term/Tighten.idr +++ b/lib/Quox/Syntax/Term/Tighten.idr @@ -1,8 +1,9 @@ module Quox.Syntax.Term.Tighten import Quox.Syntax.Term.Base -import Quox.Syntax.Subst +import Quox.Syntax.Term.Subst import public Quox.OPE +import Quox.No %default total @@ -24,17 +25,6 @@ Tighten Dim where tighten p (B i loc) = B <$> tighten p i <*> pure loc -export -tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) -> - OPE t1 t2 -> Subst env f t2 -> Maybe (Subst env f t1) -tightenSub f p (Shift by) = [|Shift $ tighten p by|] -tightenSub f p (t ::: th) = [|f p t !::: tightenSub f p th|] - -export -Tighten env => Tighten (Subst env f) where - tighten p th = tightenSub tighten p th - - export tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) -> {s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m) @@ -52,82 +42,90 @@ tightenDScope f p (S names (N body)) = S names . N <$> f p body mutual private tightenT : OPE n1 n2 -> Term d n2 -> Maybe (Term d n1) - tightenT p (TYPE l loc) = pure $ TYPE l loc - tightenT p (Pi qty arg res loc) = - Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc - tightenT p (Lam body loc) = - Lam <$> tightenS p body <*> pure loc - tightenT p (Sig fst snd loc) = - Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc - tightenT p (Pair fst snd loc) = - Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc - tightenT p (Enum cases loc) = - pure $ Enum cases loc - tightenT p (Tag tag loc) = - pure $ Tag tag loc - tightenT p (Eq ty l r loc) = - Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc - tightenT p (DLam body loc) = - DLam <$> tightenDS p body <*> pure loc - tightenT p (Nat loc) = - pure $ Nat loc - tightenT p (Zero loc) = - pure $ Zero loc - tightenT p (Succ s loc) = - Succ <$> tightenT p s <*> pure loc - tightenT p (BOX qty ty loc) = - BOX qty <$> tightenT p ty <*> pure loc - tightenT p (Box val loc) = - Box <$> tightenT p val <*> pure loc - tightenT p (E e) = - assert_total $ E <$> tightenE p e - tightenT p (CloT (Sub tm th)) = do - th <- assert_total $ tightenSub tightenE p th - pure $ CloT $ Sub tm th - tightenT p (DCloT (Sub tm th)) = do - tm <- tightenT p tm - pure $ DCloT $ Sub tm th + tightenT p s = + let Element s' _ = pushSubsts s in + tightenT' p $ assert_smaller s s' private tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1) - tightenE p (F x u loc) = + tightenE p e = + let Element e' _ = pushSubsts e in + tightenE' p $ assert_smaller e e' + + private + tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) => + Maybe (Term d n1) + tightenT' p (TYPE l loc) = pure $ TYPE l loc + tightenT' p (Pi qty arg res loc) = + Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc + tightenT' p (Lam body loc) = + Lam <$> tightenS p body <*> pure loc + tightenT' p (Sig fst snd loc) = + Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc + tightenT' p (Pair fst snd loc) = + Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc + tightenT' p (Enum cases loc) = + pure $ Enum cases loc + tightenT' p (Tag tag loc) = + pure $ Tag tag loc + tightenT' p (Eq ty l r loc) = + Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc + tightenT' p (DLam body loc) = + DLam <$> tightenDS p body <*> pure loc + tightenT' p (Nat loc) = + pure $ Nat loc + tightenT' p (Zero loc) = + pure $ Zero loc + tightenT' p (Succ s loc) = + Succ <$> tightenT p s <*> pure loc + tightenT' p (BOX qty ty loc) = + BOX qty <$> tightenT p ty <*> pure loc + tightenT' p (Box val loc) = + Box <$> tightenT p val <*> pure loc + tightenT' p (E e) = + assert_total $ E <$> tightenE p e + + private + tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) => + Maybe (Elim d n1) + tightenE' p (F x u loc) = pure $ F x u loc - tightenE p (B i loc) = + tightenE' p (B i loc) = B <$> tighten p i <*> pure loc - tightenE p (App fun arg loc) = + tightenE' p (App fun arg loc) = App <$> tightenE p fun <*> tightenT p arg <*> pure loc - tightenE p (CasePair qty pair ret body loc) = + tightenE' p (CasePair qty pair ret body loc) = CasePair qty <$> tightenE p pair <*> tightenS p ret <*> tightenS p body <*> pure loc - tightenE p (CaseEnum qty tag ret arms loc) = + tightenE' p (CaseEnum qty tag ret arms loc) = CaseEnum qty <$> tightenE p tag <*> tightenS p ret <*> traverse (tightenT p) arms <*> pure loc - tightenE p (CaseNat qty qtyIH nat ret zero succ loc) = + tightenE' p (CaseNat qty qtyIH nat ret zero succ loc) = CaseNat qty qtyIH <$> tightenE p nat <*> tightenS p ret <*> tightenT p zero <*> tightenS p succ <*> pure loc - tightenE p (CaseBox qty box ret body loc) = + tightenE' p (CaseBox qty box ret body loc) = CaseBox qty <$> tightenE p box <*> tightenS p ret <*> tightenS p body <*> pure loc - tightenE p (DApp fun arg loc) = + tightenE' p (DApp fun arg loc) = DApp <$> tightenE p fun <*> pure arg <*> pure loc - tightenE p (Ann tm ty loc) = + tightenE' p (Ann tm ty loc) = Ann <$> tightenT p tm <*> tightenT p ty <*> pure loc - tightenE p (Coe ty q0 q1 val loc) = + tightenE' p (Coe ty q0 q1 val loc) = Coe <$> tightenDS p ty <*> pure q0 <*> pure q1 <*> tightenT p val <*> pure loc - tightenE p (Comp ty q0 q1 val r zero one loc) = + tightenE' p (Comp ty q0 q1 val r zero one loc) = Comp <$> tightenT p ty <*> pure q0 <*> pure q1 <*> tightenT p val @@ -135,18 +133,12 @@ mutual <*> tightenDS p zero <*> tightenDS p one <*> pure loc - tightenE p (TypeCase ty ret arms def loc) = + tightenE' p (TypeCase ty ret arms def loc) = TypeCase <$> tightenE p ty <*> tightenT p ret <*> traverse (tightenS p) arms <*> tightenT p def <*> pure loc - tightenE p (CloE (Sub el th)) = do - th <- assert_total $ tightenSub tightenE p th - pure $ CloE $ Sub el th - tightenE p (DCloE (Sub el th)) = do - el <- tightenE p el - pure $ DCloE $ Sub el th export tightenS : {s : Nat} -> OPE m n -> @@ -164,95 +156,95 @@ export Tighten (Term d) where tighten p t = tightenT p t mutual export dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n) - dtightenT p (TYPE l loc) = - pure $ TYPE l loc - dtightenT p (Pi qty arg res loc) = - Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc - dtightenT p (Lam body loc) = - Lam <$> dtightenS p body <*> pure loc - dtightenT p (Sig fst snd loc) = - Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc - dtightenT p (Pair fst snd loc) = - Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc - dtightenT p (Enum cases loc) = - pure $ Enum cases loc - dtightenT p (Tag tag loc) = - pure $ Tag tag loc - dtightenT p (Eq ty l r loc) = - Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc - dtightenT p (DLam body loc) = - DLam <$> dtightenDS p body <*> pure loc - dtightenT p (Nat loc) = - pure $ Nat loc - dtightenT p (Zero loc) = - pure $ Zero loc - dtightenT p (Succ s loc) = - Succ <$> dtightenT p s <*> pure loc - dtightenT p (BOX qty ty loc) = - BOX qty <$> dtightenT p ty <*> pure loc - dtightenT p (Box val loc) = - Box <$> dtightenT p val <*> pure loc - dtightenT p (E e) = - assert_total $ E <$> dtightenE p e - dtightenT p (CloT (Sub tm th)) = do - tm <- dtightenT p tm - th <- assert_total $ traverse (dtightenE p) th - pure $ CloT $ Sub tm th - dtightenT p (DCloT (Sub tm th)) = do - th <- tighten p th - pure $ DCloT $ Sub tm th + dtightenT p s = + let Element s' _ = pushSubsts s in + dtightenT' p $ assert_smaller s s' export dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n) - dtightenE p (F x u loc) = + dtightenE p e = + let Element e' _ = pushSubsts e in + dtightenE' p $ assert_smaller e e' + + private + dtightenT' : OPE d1 d2 -> (t : Term d2 n) -> (0 nt : NotClo t) => + Maybe (Term d1 n) + dtightenT' p (TYPE l loc) = + pure $ TYPE l loc + dtightenT' p (Pi qty arg res loc) = + Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc + dtightenT' p (Lam body loc) = + Lam <$> dtightenS p body <*> pure loc + dtightenT' p (Sig fst snd loc) = + Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc + dtightenT' p (Pair fst snd loc) = + Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc + dtightenT' p (Enum cases loc) = + pure $ Enum cases loc + dtightenT' p (Tag tag loc) = + pure $ Tag tag loc + dtightenT' p (Eq ty l r loc) = + Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc + dtightenT' p (DLam body loc) = + DLam <$> dtightenDS p body <*> pure loc + dtightenT' p (Nat loc) = + pure $ Nat loc + dtightenT' p (Zero loc) = + pure $ Zero loc + dtightenT' p (Succ s loc) = + Succ <$> dtightenT p s <*> pure loc + dtightenT' p (BOX qty ty loc) = + BOX qty <$> dtightenT p ty <*> pure loc + dtightenT' p (Box val loc) = + Box <$> dtightenT p val <*> pure loc + dtightenT' p (E e) = + assert_total $ E <$> dtightenE p e + + export + dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) => + Maybe (Elim d1 n) + dtightenE' p (F x u loc) = pure $ F x u loc - dtightenE p (B i loc) = + dtightenE' p (B i loc) = pure $ B i loc - dtightenE p (App fun arg loc) = + dtightenE' p (App fun arg loc) = App <$> dtightenE p fun <*> dtightenT p arg <*> pure loc - dtightenE p (CasePair qty pair ret body loc) = + dtightenE' p (CasePair qty pair ret body loc) = CasePair qty <$> dtightenE p pair <*> dtightenS p ret <*> dtightenS p body <*> pure loc - dtightenE p (CaseEnum qty tag ret arms loc) = + dtightenE' p (CaseEnum qty tag ret arms loc) = CaseEnum qty <$> dtightenE p tag <*> dtightenS p ret <*> traverse (dtightenT p) arms <*> pure loc - dtightenE p (CaseNat qty qtyIH nat ret zero succ loc) = + dtightenE' p (CaseNat qty qtyIH nat ret zero succ loc) = CaseNat qty qtyIH <$> dtightenE p nat <*> dtightenS p ret <*> dtightenT p zero <*> dtightenS p succ <*> pure loc - dtightenE p (CaseBox qty box ret body loc) = + dtightenE' p (CaseBox qty box ret body loc) = CaseBox qty <$> dtightenE p box <*> dtightenS p ret <*> dtightenS p body <*> pure loc - dtightenE p (DApp fun arg loc) = + dtightenE' p (DApp fun arg loc) = DApp <$> dtightenE p fun <*> tighten p arg <*> pure loc - dtightenE p (Ann tm ty loc) = + dtightenE' p (Ann tm ty loc) = Ann <$> dtightenT p tm <*> dtightenT p ty <*> pure loc - dtightenE p (Coe ty q0 q1 val loc) = + dtightenE' p (Coe ty q0 q1 val loc) = [|Coe (dtightenDS p ty) (tighten p q0) (tighten p q1) (dtightenT p val) (pure loc)|] - dtightenE p (Comp ty q0 q1 val r zero one loc) = + dtightenE' p (Comp ty q0 q1 val r zero one loc) = [|Comp (dtightenT p ty) (tighten p q0) (tighten p q1) (dtightenT p val) (tighten p r) (dtightenDS p zero) (dtightenDS p one) (pure loc)|] - dtightenE p (TypeCase ty ret arms def loc) = + dtightenE' p (TypeCase ty ret arms def loc) = [|TypeCase (dtightenE p ty) (dtightenT p ret) (traverse (dtightenS p) arms) (dtightenT p def) (pure loc)|] - dtightenE p (CloE (Sub el th)) = do - el <- dtightenE p el - th <- assert_total $ traverse (dtightenE p) th - pure $ CloE $ Sub el th - dtightenE p (DCloE (Sub el th)) = do - th <- tighten p th - pure $ DCloE $ Sub el th export dtightenS : OPE d1 d2 -> ScopeTermN s d2 n -> Maybe (ScopeTermN s d1 n) @@ -332,3 +324,41 @@ dsqueeze : {s : Nat} -> DScopeTermN s d n -> DScopeTermN s d n dsqueeze (S names (Y body)) = S names $ maybe (Y body) N $ tightenN s body @{TermD} dsqueeze (S names (N body)) = S names $ N body + + + +public export %inline +CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> + (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n +CompH' {ty, p, q, val, r, zero, one, loc} = + -- [fixme] maintain location of existing B VZ + let ty' = DST ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in + Comp { + ty = dsub1 ty q, p, q, + val = E $ Coe ty p q val val.loc, r, + -- [fixme] better locations for these vars? + zero = DST zero.names $ E $ + Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc, + one = DST one.names $ E $ + Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc, + loc + } + +||| heterogeneous composition, using Comp and Coe (and subst) +||| +||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ } +||| ≔ +||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r { +||| 0 j ⇒ coe [i ⇒ A] @j @q t₀; +||| 1 j ⇒ coe [i ⇒ A] @j @q t₁ +||| } +public export %inline +CompH : (i : BindName) -> (ty : Term (S d) n) -> + (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) -> + (j0 : BindName) -> (zero : Term (S d) n) -> + (j1 : BindName) -> (one : Term (S d) n) -> + (loc : Loc) -> + Elim d n +CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} = + CompH' {ty = DST [< i] ty, p, q, val, r, + zero = DST [< j0] zero, one = DST [< j1] one, loc}