fix #11 the easy way
tightening just pushes substitutions all the way through. bleh
This commit is contained in:
parent
612fb33663
commit
b6264f388d
3 changed files with 157 additions and 176 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
Loading…
Reference in a new issue