make coercion computation type-directed like it should be
This commit is contained in:
parent
0bcb8c24db
commit
22db2724ce
4 changed files with 145 additions and 114 deletions
|
|
@ -52,3 +52,8 @@ export %inline
|
|||
nchoose : (b : Bool) -> Either (So b) (No b)
|
||||
nchoose True = Left Oh
|
||||
nchoose False = Right Ah
|
||||
|
||||
export
|
||||
0 notYesNo : {f : Dec p} -> Not p -> No (isYes f)
|
||||
notYesNo {f = Yes y} g = absurd $ g y
|
||||
notYesNo {f = No n} g = Ah
|
||||
|
|
|
|||
|
|
@ -107,92 +107,84 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
|
|||
(ST body.names $ body.term // (a' ::: shift 1)) loc
|
||||
|
||||
|
||||
|
||||
||| pushes a coercion inside a whnf-ed term
|
||||
export covering
|
||||
pushCoe : BindName ->
|
||||
(ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
|
||||
Dim d -> Dim d ->
|
||||
(s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc ->
|
||||
(ty : Term (S d) n) ->
|
||||
(p, q : Dim d) -> (0 npq : Not (p `Eqv` q)) =>
|
||||
(s : Term d n) -> (0 pc : So (canPushCoe ty s)) => Loc ->
|
||||
Eff Whnf (NonRedex Elim d n defs)
|
||||
pushCoe i ty p q s loc {snf} =
|
||||
if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
|
||||
case s of
|
||||
-- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
|
||||
TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
Pi {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
Sig {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
Eq {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
Nat {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
BOX {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
|
||||
pushCoe i ty p q s loc =
|
||||
case ty of
|
||||
-- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
|
||||
TYPE l tyLoc =>
|
||||
whnf defs ctx $ Ann s (TYPE l tyLoc) loc
|
||||
|
||||
-- just η expand it. then whnf for App will handle it later
|
||||
-- this is how @xtt does it
|
||||
-- η expand it so that whnf for App can deal with it
|
||||
--
|
||||
-- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝
|
||||
-- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯
|
||||
lam@(Lam {body, _}) => do
|
||||
let lam' = CoeT i ty p q lam loc
|
||||
term' = LamY !(fresh body.name)
|
||||
(E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc
|
||||
type' = ty // one q
|
||||
whnf defs ctx $ Ann term' type' loc
|
||||
-- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
|
||||
-- ⇝
|
||||
-- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
|
||||
Pi {} =>
|
||||
let inner = Coe (SY [< i] ty) p q s loc in
|
||||
whnf defs ctx $
|
||||
Ann (LamY !(mnb "y" loc)
|
||||
(E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
|
||||
(ty // one q) loc
|
||||
|
||||
-- (coe [i ⇒ (x : A) × B] @p @q (s, t)) ⇝
|
||||
-- (coe [i ⇒ A] @p @q s,
|
||||
-- coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t)
|
||||
-- ∷ (x : A‹q/i›) × B‹q/i›
|
||||
-- no η!!!
|
||||
-- push into a pair constructor, otherwise still stuck
|
||||
--
|
||||
-- can't use η here because... it doesn't exist
|
||||
Pair {fst, snd, loc = pairLoc} => do
|
||||
let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty
|
||||
| _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty
|
||||
let fst' = E $ CoeT i tfst p q fst fst.loc
|
||||
tfst' = tfst // (B VZ noLoc ::: shift 2)
|
||||
tsnd' = sub1 tsnd $
|
||||
CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc)
|
||||
(dweakT 1 fst) fst.loc
|
||||
snd' = E $ CoeT i tsnd' p q snd snd.loc
|
||||
pure $
|
||||
Element (Ann (Pair fst' snd' pairLoc)
|
||||
(Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah
|
||||
-- s̃‹𝑘› ≔ coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑘 s
|
||||
-- -----------------------------------------------
|
||||
-- (coe (𝑖 ⇒ (x : A) × B) @p @q (s, t))
|
||||
-- ⇝
|
||||
-- (s̃‹q›, coe (𝑖 ⇒ B[s̃‹𝑖›/x]) @p @q t)
|
||||
-- ∷ ((x : A) × B)‹q/𝑖›
|
||||
Sig tfst tsnd tyLoc => do
|
||||
let Pair fst snd sLoc = s
|
||||
fst' = CoeT i tfst p q fst fst.loc
|
||||
fstInSnd =
|
||||
CoeT !(fresh i)
|
||||
(tfst // (BV 0 loc ::: shift 2))
|
||||
(weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
|
||||
snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
|
||||
whnf defs ctx $
|
||||
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
|
||||
|
||||
-- η expand, like for Lam
|
||||
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
|
||||
Enum cases tyLoc =>
|
||||
whnf defs ctx $ Ann s (Enum cases tyLoc) loc
|
||||
|
||||
-- η expand, same as for Π
|
||||
--
|
||||
-- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝
|
||||
-- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯
|
||||
dlam@(DLam {body, _}) => do
|
||||
let dlam' = CoeT i ty p q dlam loc
|
||||
term' = DLamY !(mnb "j")
|
||||
(E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc
|
||||
type' = ty // one q
|
||||
whnf defs ctx $ Ann term' type' loc
|
||||
-- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
|
||||
-- ⇝
|
||||
-- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
|
||||
Eq {} =>
|
||||
let inner = Coe (SY [< i] ty) p q s loc in
|
||||
whnf defs ctx $
|
||||
Ann (DLamY !(mnb "k" loc)
|
||||
(E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
|
||||
(ty // one q) loc
|
||||
|
||||
-- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
|
||||
Tag {tag, loc = tagLoc} => do
|
||||
let Enum {cases, loc = enumLoc} = ty
|
||||
| _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty
|
||||
pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah
|
||||
-- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
|
||||
Nat tyLoc =>
|
||||
whnf defs ctx $ Ann s (Nat tyLoc) loc
|
||||
|
||||
-- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ)
|
||||
Zero {loc = zeroLoc} => do
|
||||
pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah
|
||||
Succ {p = pred, loc = succLoc} => do
|
||||
pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah
|
||||
|
||||
-- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
|
||||
-- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›]
|
||||
Box {val, loc = boxLoc} => do
|
||||
let BOX {qty, ty = a, loc = tyLoc} = ty
|
||||
| _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty
|
||||
pure $ Element
|
||||
(Ann (Box (E $ CoeT i a p q val val.loc) boxLoc)
|
||||
(BOX qty (a // one q) tyLoc) loc)
|
||||
Ah
|
||||
|
||||
E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah)
|
||||
where
|
||||
unwrapTYPE : Term (S d) n -> Eff Whnf Universe
|
||||
unwrapTYPE (TYPE {l, _}) = pure l
|
||||
unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty
|
||||
-- η expand
|
||||
--
|
||||
-- (coe (𝑖 ⇒ [π. A]) @p @q s)
|
||||
-- ⇝
|
||||
-- [case1 coe (𝑖 ⇒ [π. A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
|
||||
-- ∷ [π. A]‹q/𝑖›
|
||||
BOX qty inner tyLoc =>
|
||||
let inner = CaseBox {
|
||||
qty = One,
|
||||
box = Coe (SY [< i] ty) p q s loc,
|
||||
ret = SN $ ty // one q,
|
||||
body = SY [< !(mnb "x" loc)] $ BVT 0 loc,
|
||||
loc
|
||||
}
|
||||
in
|
||||
whnf defs ctx $ Ann (Box (E inner) loc) (ty // one q) loc
|
||||
|
|
|
|||
|
|
@ -147,25 +147,50 @@ isK (K {}) = True
|
|||
isK _ = False
|
||||
|
||||
|
||||
||| if `ty` is a type constructor, and `val` is a value of that type where a
|
||||
||| coercion can be reduced. which is the case if any of:
|
||||
||| - `ty` is an atomic type
|
||||
||| - `ty` has η
|
||||
||| - `val` is a constructor form
|
||||
public export %inline
|
||||
canPushCoe : (ty, val : Term {}) -> Bool
|
||||
canPushCoe (TYPE {}) _ = True
|
||||
canPushCoe (Pi {}) _ = True
|
||||
canPushCoe (Lam {}) _ = False
|
||||
canPushCoe (Sig {}) (Pair {}) = True
|
||||
canPushCoe (Sig {}) _ = False
|
||||
canPushCoe (Pair {}) _ = False
|
||||
canPushCoe (Enum {}) _ = True
|
||||
canPushCoe (Tag {}) _ = False
|
||||
canPushCoe (Eq {}) _ = True
|
||||
canPushCoe (DLam {}) _ = False
|
||||
canPushCoe (Nat {}) _ = True
|
||||
canPushCoe (Zero {}) _ = False
|
||||
canPushCoe (Succ {}) _ = False
|
||||
canPushCoe (BOX {}) _ = True
|
||||
canPushCoe (Box {}) _ = False
|
||||
canPushCoe (E {}) _ = False
|
||||
canPushCoe (CloT {}) _ = False
|
||||
canPushCoe (DCloT {}) _ = False
|
||||
|
||||
|
||||
mutual
|
||||
||| a reducible elimination
|
||||
|||
|
||||
||| - a free variable, if its definition is known
|
||||
||| - an application whose head is an annotated lambda,
|
||||
||| 1. a free variable, if its definition is known
|
||||
||| 2. an elimination whose head is reducible
|
||||
||| 3. an "active" elimination:
|
||||
||| an application whose head is an annotated lambda,
|
||||
||| a case expression whose head is an annotated constructor form, etc
|
||||
||| - a redundant annotation, or one whose term or type is reducible
|
||||
||| - coercions `coe (𝑖 ⇒ A) @p @q s` where:
|
||||
||| - `A` is in whnf, or
|
||||
||| - `𝑖` is not mentioned in `A`, or
|
||||
||| - `p = q`
|
||||
||| - [fixme] this is not true right now but that's because i wrote it
|
||||
||| wrong
|
||||
||| - compositions `comp A @p @q s @r {⋯}` where:
|
||||
||| - `A` is in whnf, or
|
||||
||| - `p = q`, or
|
||||
||| - `r = 0` or `r = 1`
|
||||
||| - [fixme] the p=q condition is also missing here
|
||||
||| - closures
|
||||
||| 4. a redundant annotation, or one whose term or type is reducible
|
||||
||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
|
||||
||| a. `A` is reducible or a type constructor, or
|
||||
||| b. `𝑖` is not mentioned in `A`
|
||||
||| ([fixme] should be A‹0/𝑖› = A‹1/𝑖›), or
|
||||
||| c. `p = q`
|
||||
||| 6. a composition `comp A @p @q s @r {⋯}`
|
||||
||| where `p = q`, `r = 0`, or `r = 1`
|
||||
||| 7. a closure
|
||||
public export
|
||||
isRedexE : RedexTest Elim
|
||||
isRedexE defs (F {x, _}) {d, n} =
|
||||
|
|
@ -185,10 +210,11 @@ mutual
|
|||
isRedexE defs fun || isDLamHead fun || isK arg
|
||||
isRedexE defs (Ann {tm, ty, _}) =
|
||||
isE tm || isRedexT defs tm || isRedexT defs ty
|
||||
isRedexE defs (Coe {val, _}) =
|
||||
isRedexT defs val || not (isE val)
|
||||
isRedexE defs (Comp {ty, r, _}) =
|
||||
isRedexT defs ty || isK r
|
||||
isRedexE defs (Coe {ty = S _ (N _), _}) = True
|
||||
isRedexE defs (Coe {ty = S _ (Y ty), p, q, val, _}) =
|
||||
isRedexT defs ty || canPushCoe ty val || isYes (p `decEqv` q)
|
||||
isRedexE defs (Comp {ty, r, p, q, _}) =
|
||||
isYes (p `decEqv` q) || isK r
|
||||
isRedexE defs (TypeCase {ty, ret, _}) =
|
||||
isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
|
||||
isRedexE _ (CloE {}) = True
|
||||
|
|
@ -196,10 +222,10 @@ mutual
|
|||
|
||||
||| a reducible term
|
||||
|||
|
||||
||| - a reducible elimination, as `isRedexE`
|
||||
||| - an annotated elimination
|
||||
||| 1. a reducible elimination, as `isRedexE`
|
||||
||| 2. an annotated elimination
|
||||
||| (the annotation is redundant in a checkable context)
|
||||
||| - a closure
|
||||
||| 3. a closure
|
||||
public export
|
||||
isRedexT : RedexTest Term
|
||||
isRedexT _ (CloT {}) = True
|
||||
|
|
|
|||
|
|
@ -140,23 +140,31 @@ CanWhnf Elim Interface.isRedexE where
|
|||
|
||||
whnf defs ctx (Coe (S _ (N ty)) _ _ val coeLoc) =
|
||||
whnf defs ctx $ Ann val ty coeLoc
|
||||
whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do
|
||||
whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) =
|
||||
case p `decEqv` q of
|
||||
Yes y => whnf defs ctx $ Ann val (ty // one q) coeLoc
|
||||
No npq => do
|
||||
Element ty tynf <- whnf defs (extendDim i ctx) ty
|
||||
Element val valnf <- whnf defs ctx val
|
||||
case nchoose $ canPushCoe ty val of
|
||||
Left y =>
|
||||
pushCoe defs ctx i ty p q val coeLoc
|
||||
Right npc =>
|
||||
-- [fixme] what about ty.zero = ty.one????
|
||||
pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
|
||||
(tynf `orNo` npc `orNo` notYesNo npq)
|
||||
|
||||
whnf defs ctx (Comp ty p q val r zero one compLoc) =
|
||||
-- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
|
||||
if p == q then whnf defs ctx $ Ann val ty compLoc else
|
||||
case nchoose (isK r) of
|
||||
-- comp [A] @p @q s @0 { 0 j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
|
||||
-- comp [A] @p @q s @1 { 1 j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
|
||||
Left y => case r of
|
||||
case p `decEqv` q of
|
||||
-- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
|
||||
Yes y => whnf defs ctx $ Ann val ty compLoc
|
||||
No npq => case r of
|
||||
-- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
|
||||
K Zero _ => whnf defs ctx $ Ann (dsub1 zero q) ty compLoc
|
||||
-- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
|
||||
K One _ => whnf defs ctx $ Ann (dsub1 one q) ty compLoc
|
||||
Right nk => do
|
||||
Element ty tynf <- whnf defs ctx ty
|
||||
pure $ Element (Comp ty p q val r zero one compLoc) $ tynf `orNo` nk
|
||||
B {} =>
|
||||
pure $ Element (Comp ty p q val r zero one compLoc)
|
||||
(notYesNo npq `orNo` Ah)
|
||||
|
||||
whnf defs ctx (TypeCase ty ret arms def tcLoc) = do
|
||||
Element ty tynf <- whnf defs ctx ty
|
||||
|
|
|
|||
Loading…
Reference in a new issue