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

Compare commits

base: rhi:a9ef12cb31ca0c9e4eaa0d7d8d7a3bffc0da7324
Branches Tags
rhi:🐉
rhi:qpoly
rhi:🎋
rhi:𝕎
rhi:🥚🛁
rhi:ope
..
compare: rhi:bb8d2464af1f709ab36e72c118e63f8a8276b122
Branches Tags
rhi:🐉
rhi:qpoly
rhi:🎋
rhi:𝕎
rhi:🥚🛁
rhi:ope

2 Commits
a9ef12cb31 ... bb8d2464af

Author SHA1 Message Date
rhiannon morris bb8d2464af add fst and snd 2023-09-18 21:53:38 +02:00
rhiannon morris e6c06a5c81 pass the subject quantity through equality etc 
in preparation for non-linear η laws
 2023-09-18 21:53:38 +02:00
18 changed files with 320 additions and 125 deletions
Show Stats Expand all files Collapse all files

2
exe/Main.idr
View File

@ -23,7 +23,7 @@ die : Doc Opts -> IO a
die err = do putDoc err; exitFailure
private
prettySig : {opts : _} -> Name -> Definition -> Eff Pretty (Doc opts)
prettySig : Name -> Definition -> Eff Pretty (Doc Opts)
prettySig name def = do
qty <- prettyQty def.qty.qty
name <- prettyFree name

2
lib/Quox/Displace.idr
View File

@ -49,6 +49,8 @@ parameters (k : Universe)
doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
doDisplace (CasePair qty pair ret body loc) =
CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
doDisplace (Fst pair loc) = Fst (doDisplace pair) loc
doDisplace (Snd pair loc) = Snd (doDisplace pair) loc
doDisplace (CaseEnum qty tag ret arms loc) =
CaseEnum qty (doDisplace tag) (doDisplaceS ret)
(assert_total $ map doDisplace arms) loc

21
lib/Quox/Equal.idr
View File

@ -544,6 +544,27 @@ namespace Elim
compare0Inner' defs ctx sg e'@(CasePair {}) f' ne nf =
clashE defs ctx sg e' f'
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
-- ------------------------------
-- Ψ | Γ ⊢ fst e = fst f ⇒ A
compare0Inner' defs ctx sg (Fst e eloc) (Fst f floc) ne nf =
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
fst <$> expectSig defs ctx sg eloc ety
compare0Inner' defs ctx sg e@(Fst {}) f _ _ =
clashE defs ctx sg e f
-- Ψ | Γ ⊢ e = f ⇒ (x : A) × B
-- ------------------------------------
-- Ψ | Γ ⊢ snd e = snd f ⇒ B[fst e/x]
compare0Inner' defs ctx sg (Snd e eloc) (Snd f floc) ne nf =
local_ Equal $ do
ety <- compare0Inner defs ctx sg e f
(_, tsnd) <- expectSig defs ctx sg eloc ety
pure $ sub1 tsnd (Fst e eloc)
compare0Inner' defs ctx sg e@(Snd {}) f _ _ =
clashE defs ctx sg e f
-- Ψ | Γ ⊢ e = f ⇒ {𝐚s}
-- Ψ | Γ, x : {𝐚s} ⊢ Q = R
-- Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]

4
lib/Quox/FreeVars.idr
View File

@ -196,6 +196,8 @@ HasFreeVars (Elim d) where
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 (Fst pair _) = fv pair
fv (Snd pair _) = fv pair
fv (CaseEnum {tag, ret, arms, _}) =
fv tag <+> fv ret <+> foldMap fv (values arms)
fv (CaseNat {nat, ret, zero, succ, _}) =
@ -269,6 +271,8 @@ HasFreeDVars Elim where
fdv (B {}) = none
fdv (App {fun, arg, _}) = fdv fun <+> fdv arg
fdv (CasePair {pair, ret, body, _}) = fdv pair <+> fdvT ret <+> fdvT body
fdv (Fst pair _) = fdv pair
fdv (Snd pair _) = fdv pair
fdv (CaseEnum {tag, ret, arms, _}) =
fdv tag <+> fdvT ret <+> foldMap fdv (values arms)
fdv (CaseNat {nat, ret, zero, succ, _}) =

6
lib/Quox/Parser/FromParser.idr
View File

@ -141,6 +141,12 @@ mutual
<*> fromPTermTScope ds ns [< x, y] body
<*> pure loc
Fst pair loc =>
map E $ Fst <$> fromPTermElim ds ns pair <*> pure loc
Snd pair loc =>
map E $ Snd <$> fromPTermElim ds ns pair <*> pure loc
Case pi tag (r, ret) (CaseEnum arms _) loc =>
map E $ CaseEnum (fromPQty pi)
<$> fromPTermElim ds ns tag

1
lib/Quox/Parser/Lexer.idr
View File

@ -203,6 +203,7 @@ reserved =
Word "caseω" `Or` Word "case#",
Word1 "return",
Word1 "of",
Word1 "fst", Word1 "snd",
Word1 "_",
Word1 "Eq",
Word "λ" `Or` Word "fun",

19
lib/Quox/Parser/Parser.idr
View File

@ -372,10 +372,23 @@ eqTerm : FileName -> Grammar True PTerm
eqTerm fname = withLoc fname $
resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|]
export
resAppTerm : FileName -> (word : String) -> (0 _ : IsReserved word) =>
(PTerm -> Loc -> PTerm) -> Grammar True PTerm
resAppTerm fname word f = withLoc fname $
resC word *> mustWork [|f (termArg fname)|]
export
succTerm : FileName -> Grammar True PTerm
succTerm fname = withLoc fname $
resC "succ" *> mustWork [|Succ (termArg fname)|]
succTerm fname = resAppTerm fname "succ" Succ
export
fstTerm : FileName -> Grammar True PTerm
fstTerm fname = resAppTerm fname "fst" Fst
export
sndTerm : FileName -> Grammar True PTerm
sndTerm fname = resAppTerm fname "snd" Snd
||| a dimension argument with an `@` prefix, or
||| a term argument with no prefix
@ -403,6 +416,8 @@ appTerm fname =
<|> splitUniverseTerm fname
<|> eqTerm fname
<|> succTerm fname
<|> fstTerm fname
<|> sndTerm fname
<|> normalAppTerm fname
export

3
lib/Quox/Parser/Syntax.idr
View File

@ -73,6 +73,7 @@ namespace PTerm
| Sig PatVar PTerm PTerm Loc
| Pair PTerm PTerm Loc
| Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
| Fst PTerm Loc | Snd PTerm Loc
| Enum (List TagVal) Loc
| Tag TagVal Loc
@ -113,6 +114,8 @@ Located PTerm where
(App _ _ loc).loc = loc
(Sig _ _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(Case _ _ _ _ loc).loc = loc
(Enum _ loc).loc = loc
(Tag _ loc).loc = loc

4
lib/Quox/Pretty.idr
View File

@ -234,7 +234,7 @@ prettyDBind = hl DVar . prettyBind'
export %inline
typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
{opts : LayoutOpts} -> Eff Pretty (Doc opts)
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
arrowD = hl Delim . text =<< ifUnicode "→" "->"
@ -261,6 +261,8 @@ compD = hl Syntax $ text "comp"
undD = hl Syntax $ text "_"
cstD = hl Syntax $ text "="
pipeD = hl Syntax $ text "|"
fstD = hl Syntax $ text "fst"
sndD = hl Syntax $ text "snd"
export

10
lib/Quox/Syntax/Term/Base.idr
View File

@ -155,6 +155,12 @@ mutual
(loc : Loc) ->
Elim d n
||| first element of a pair. only works in non-linear contexts.
Fst : (pair : Elim d n) -> (loc : Loc) -> Elim d n
||| second element of a pair. only works in non-linear contexts.
Snd : (pair : Elim d n) -> (loc : Loc) -> Elim d n
||| enum matching
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
(ret : ScopeTerm d n) ->
@ -369,6 +375,8 @@ Located (Elim d n) where
(B _ loc).loc = loc
(App _ _ loc).loc = loc
(CasePair _ _ _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(CaseEnum _ _ _ _ loc).loc = loc
(CaseNat _ _ _ _ _ _ loc).loc = loc
(CaseBox _ _ _ _ loc).loc = loc
@ -417,6 +425,8 @@ Relocatable (Elim d n) where
setLoc loc (App fun arg _) = App fun arg loc
setLoc loc (CasePair qty pair ret body _) =
CasePair qty pair ret body loc
setLoc loc (Fst pair _) = Fst pair loc
setLoc loc (Snd pair _) = Fst pair loc
setLoc loc (CaseEnum qty tag ret arms _) =
CaseEnum qty tag ret arms loc
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =

10
lib/Quox/Syntax/Term/Pretty.idr
View File

@ -493,6 +493,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do
prettyCase dnames tnames qty pair ret
[MkCaseArm pat [<] [< x, y] body.term]
prettyElim dnames tnames (Fst pair _) =
parensIfM App =<< do
pair <- prettyTArg dnames tnames (E pair)
prettyAppD !fstD [pair]
prettyElim dnames tnames (Snd pair _) =
parensIfM App =<< do
pair <- prettyTArg dnames tnames (E pair)
prettyAppD !sndD [pair]
prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
arms <- for (SortedMap.toList arms) $ \(tag, body) =>
pure $ MkCaseArm !(prettyTag tag) [<] [<] body

4
lib/Quox/Syntax/Term/Subst.idr
View File

@ -299,6 +299,10 @@ mutual
nclo $ App (f // th // ph) (s // th // ph) loc
pushSubstsWith th ph (CasePair pi p r b loc) =
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
pushSubstsWith th ph (Fst pair loc) =
nclo $ Fst (pair // th // ph) loc
pushSubstsWith th ph (Snd pair loc) =
nclo $ Snd (pair // th // ph) loc
pushSubstsWith th ph (CaseEnum pi t r arms loc) =
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
(map (\b => b // th // ph) arms) loc

8
lib/Quox/Syntax/Term/Tighten.idr
View File

@ -87,6 +87,10 @@ mutual
<*> tightenS p ret
<*> tightenS p body
<*> pure loc
tightenE' p (Fst pair loc) =
Fst <$> tightenE p pair <*> pure loc
tightenE' p (Snd pair loc) =
Snd <$> tightenE p pair <*> pure loc
tightenE' p (CaseEnum qty tag ret arms loc) =
CaseEnum qty <$> tightenE p tag
<*> tightenS p ret
@ -202,6 +206,10 @@ mutual
<*> dtightenS p ret
<*> dtightenS p body
<*> pure loc
dtightenE' p (Fst pair loc) =
Fst <$> dtightenE p pair <*> pure loc
dtightenE' p (Snd pair loc) =
Snd <$> dtightenE p pair <*> pure loc
dtightenE' p (CaseEnum qty tag ret arms loc) =
CaseEnum qty <$> dtightenE p tag
<*> dtightenS p ret

20
lib/Quox/Typechecker.idr
View File

@ -379,6 +379,26 @@ mutual
qout = pi * pairres.qout + bodyout
}
infer' ctx sg (Fst pair loc) = do
-- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
pairres <- inferC ctx sg pair
(tfst, _) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
-- then Ψ | Γ ⊢ σ · fst e ⇒ A ⊳ ωΣ
pure $ InfRes {
type = tfst,
qout = Any * pairres.qout
}
infer' ctx sg (Snd pair loc) = do
-- if Ψ | Γ ⊢ σ · e ⇒ (x : A) × B ⊳ Σ
pairres <- inferC ctx sg pair
(_, tsnd) <- expectSig !(askAt DEFS) ctx SZero pair.loc pairres.type
-- then Ψ | Γ ⊢ σ · snd e ⇒ B[fst e/x] ⊳ ωΣ
pure $ InfRes {
type = sub1 tsnd (Fst pair loc),
qout = Any * pairres.qout
}
infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
-- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
tres <- inferC ctx sg t

82
lib/Quox/Whnf/Coercion.idr
View File

@ -23,12 +23,12 @@ where
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (pi : SQty)
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
||| reduce a function application `App (Coe ty p q val) s loc`
export covering
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
(val, s : Term d n) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
piCoe sty@(S [< i] ty) p q val s loc = do
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
-- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@ -42,17 +42,17 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
(s // shift 1) s.loc
whnf defs ctx pi $ CoeT i (sub1 res s1) p q body loc
whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc
||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc`
export covering
sigCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
-- ⇝
-- ⇝
-- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
-- of { (a, b) ⇒
-- e[(coe [i ⇒ A] @p @q a)/a,
@ -68,17 +68,57 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
(weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
whnf defs ctx pi $ CasePair qty (Ann val (ty // one p) val.loc) ret
whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
||| reduce a pair projection `Fst (Coe ty p q val) loc`
export covering
fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
fstCoe sty@(S [< i] ty) p q val loc = do
-- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s)
-- ⇝
-- coe (𝑖 ⇒ A) @p @q (fst (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(tfst, _) <- tycaseSig defs ctx1 ty
whnf defs ctx sg $
Coe (ST [< i] tfst) p q
(E (Fst (Ann val (ty // one p) val.loc) val.loc)) loc
||| reduce a pair projection `Snd (Coe ty p q val) loc`
export covering
sndCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
sndCoe sty@(S [< i] ty) p q val loc = do
-- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s)
-- ⇝
-- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @q
-- (snd (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(tfst, tsnd) <- tycaseSig defs ctx1 ty
whnf defs ctx sg $
Coe (ST [< i] $ sub1 tsnd $
Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
(weakD 1 p) (BV 0 loc)
(E (Fst (Ann (dweakT 1 val) ty val.loc) val.loc)) loc)
p q
(E (Snd (Ann val (ty // one p) val.loc) val.loc))
loc
||| reduce a dimension application `DApp (Coe ty p q val) r loc`
export covering
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(r : Dim d) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
eqCoe sty@(S [< j] ty) p q val r loc = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
-- ⇝
-- ⇝
-- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
-- @r { 0 j ⇒ L; 1 j ⇒ R }
let ctx1 = extendDim j ctx
@ -86,23 +126,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
let a' = dsub1 a (weakD 1 r)
val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
whnf defs ctx pi $ CompH j a' p q val' r j s j t loc
whnf defs ctx sg $ CompH j a' p q val' r j s j t loc
||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
export covering
boxCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs pi))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg))
boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
-- ⇝
-- ⇝
-- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
ta <- tycaseBOX defs ctx1 ty
let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
whnf defs ctx pi $ CaseBox qty (Ann val (ty // one p) val.loc) ret
whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: shift 1)) loc
@ -110,13 +150,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
export covering
pushCoe : BindName ->
(ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
(0 pc : So (canPushCoe pi ty s)) =>
Eff Whnf (NonRedex Elim d n defs pi)
(0 pc : So (canPushCoe sg ty s)) =>
Eff Whnf (NonRedex Elim d n defs sg)
pushCoe i ty p q s loc =
case ty of
-- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
TYPE l tyLoc =>
whnf defs ctx pi $ Ann s (TYPE l tyLoc) loc
whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc
-- η expand it so that whnf for App can deal with it
--
@ -125,7 +165,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (λ 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 pi $
whnf defs ctx sg $
Ann (LamY !(mnb "y" loc)
(E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
(ty // one q) loc
@ -147,12 +187,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(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 pi $
whnf defs ctx sg $
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
Enum cases tyLoc =>
whnf defs ctx pi $ Ann s (Enum cases tyLoc) loc
whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
-- η expand, same as for Π
--
@ -161,14 +201,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (δ 𝑘 ⇒ (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 pi $
whnf defs ctx sg $
Ann (DLamY !(mnb "k" loc)
(E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
(ty // one q) loc
-- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
Nat tyLoc =>
whnf defs ctx pi $ Ann s (Nat tyLoc) loc
whnf defs ctx sg $ Ann s (Nat tyLoc) loc
-- η expand
--
@ -185,4 +225,4 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
loc
}
in
whnf defs ctx pi $ Ann (Box (E inner) loc) (ty // one q) loc
whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc

12
lib/Quox/Whnf/ComputeElimType.idr
View File

@ -41,11 +41,21 @@ computeElimType defs ctx pi e {ne} =
App f s loc =>
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
t => throw $ ExpectedPi loc ctx.names t
ty => throw $ ExpectedPi loc ctx.names ty
CasePair {pair, ret, _} =>
pure $ sub1 ret pair
Fst pair loc =>
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
Sig {fst, _} => pure fst
ty => throw $ ExpectedSig loc ctx.names ty
Snd pair loc =>
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
ty => throw $ ExpectedSig loc ctx.names ty
CaseEnum {tag, ret, _} =>
pure $ sub1 ret tag

94
lib/Quox/Whnf/Interface.idr
View File

@ -155,24 +155,24 @@ isK _ = False
||| - `val` is a constructor form
public export %inline
canPushCoe : SQty -> (ty, val : Term {}) -> Bool
canPushCoe pi (TYPE {}) _ = True
canPushCoe pi (Pi {}) _ = True
canPushCoe pi (Lam {}) _ = False
canPushCoe pi (Sig {}) (Pair {}) = True
canPushCoe pi (Sig {}) _ = False
canPushCoe pi (Pair {}) _ = False
canPushCoe pi (Enum {}) _ = True
canPushCoe pi (Tag {}) _ = False
canPushCoe pi (Eq {}) _ = True
canPushCoe pi (DLam {}) _ = False
canPushCoe pi (Nat {}) _ = True
canPushCoe pi (Zero {}) _ = False
canPushCoe pi (Succ {}) _ = False
canPushCoe pi (BOX {}) _ = True
canPushCoe pi (Box {}) _ = False
canPushCoe pi (E {}) _ = False
canPushCoe pi (CloT {}) _ = False
canPushCoe pi (DCloT {}) _ = False
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (Nat {}) _ = True
canPushCoe sg (Zero {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
mutual
@ -184,40 +184,44 @@ mutual
||| an application whose head is an annotated lambda,
||| a case expression whose head is an annotated constructor form, etc
||| 4. a redundant annotation, or one whose term or type is reducible
||| 5. a coercion `coe (𝑖 ⇒ A) @p @pi s` where:
||| 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 = pi`
||| 6. a composition `comp A @p @pi s @r {⋯}`
||| where `p = pi`, `r = 0`, or `r = 1`
||| 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 pi (F {x, u, _}) {d, n} =
isRedexE defs sg (F {x, u, _}) {d, n} =
isJust $ lookupElim x u defs {d, n}
isRedexE _ pi (B {}) = False
isRedexE defs pi (App {fun, _}) =
isRedexE defs pi fun || isLamHead fun
isRedexE defs pi (CasePair {pair, _}) =
isRedexE defs pi pair || isPairHead pair
isRedexE defs pi (CaseEnum {tag, _}) =
isRedexE defs pi tag || isTagHead tag
isRedexE defs pi (CaseNat {nat, _}) =
isRedexE defs pi nat || isNatHead nat
isRedexE defs pi (CaseBox {box, _}) =
isRedexE defs pi box || isBoxHead box
isRedexE defs pi (DApp {fun, arg, _}) =
isRedexE defs pi fun || isDLamHead fun || isK arg
isRedexE defs pi (Ann {tm, ty, _}) =
isE tm || isRedexT defs pi tm || isRedexT defs SZero ty
isRedexE defs pi (Coe {ty = S _ (N _), _}) = True
isRedexE defs pi (Coe {ty = S _ (Y ty), p, q, val, _}) =
isRedexT defs SZero ty || canPushCoe pi ty val || isYes (p `decEqv` q)
isRedexE defs pi (Comp {ty, p, q, r, _}) =
isRedexE _ sg (B {}) = False
isRedexE defs sg (App {fun, _}) =
isRedexE defs sg fun || isLamHead fun
isRedexE defs sg (CasePair {pair, _}) =
isRedexE defs sg pair || isPairHead pair || isYes (sg `decEq` SZero)
isRedexE defs sg (Fst pair _) =
isRedexE defs sg pair || isPairHead pair
isRedexE defs sg (Snd pair _) =
isRedexE defs sg pair || isPairHead pair
isRedexE defs sg (CaseEnum {tag, _}) =
isRedexE defs sg tag || isTagHead tag
isRedexE defs sg (CaseNat {nat, _}) =
isRedexE defs sg nat || isNatHead nat
isRedexE defs sg (CaseBox {box, _}) =
isRedexE defs sg box || isBoxHead box
isRedexE defs sg (DApp {fun, arg, _}) =
isRedexE defs sg fun || isDLamHead fun || isK arg
isRedexE defs sg (Ann {tm, ty, _}) =
isE tm || isRedexT defs sg tm || isRedexT defs SZero ty
isRedexE defs sg (Coe {ty = S _ (N _), _}) = True
isRedexE defs sg (Coe {ty = S _ (Y ty), p, q, val, _}) =
isRedexT defs SZero ty || canPushCoe sg ty val || isYes (p `decEqv` q)
isRedexE defs sg (Comp {ty, p, q, r, _}) =
isYes (p `decEqv` q) || isK r
isRedexE defs pi (TypeCase {ty, ret, _}) =
isRedexE defs pi ty || isRedexT defs pi ret || isAnnTyCon ty
isRedexE defs sg (TypeCase {ty, ret, _}) =
isRedexE defs sg ty || isRedexT defs sg ret || isAnnTyCon ty
isRedexE _ _ (CloE {}) = True
isRedexE _ _ (DCloE {}) = True
@ -231,5 +235,5 @@ mutual
isRedexT : RedexTest Term
isRedexT _ _ (CloT {}) = True
isRedexT _ _ (DCloT {}) = True
isRedexT defs pi (E {e, _}) = isAnn e || isRedexE defs pi e
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
isRedexT _ _ _ = False

143
lib/Quox/Whnf/Main.idr
View File

@ -16,53 +16,88 @@ export covering CanWhnf Elim Interface.isRedexE
covering
CanWhnf Elim Interface.isRedexE where
whnf defs ctx rh (F x u loc) with (lookupElim x u defs) proof eq
_ | Just y = whnf defs ctx rh $ setLoc loc y
whnf defs ctx sg (F x u loc) with (lookupElim x u defs) proof eq
_ | Just y = whnf defs ctx sg $ setLoc loc y
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
whnf _ _ _ (B i loc) = pure $ nred $ B i loc
-- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
whnf defs ctx rh (App f s appLoc) = do
Element f fnf <- whnf defs ctx rh f
whnf defs ctx sg (App f s appLoc) = do
Element f fnf <- whnf defs ctx sg f
case nchoose $ isLamHead f of
Left _ => case f of
Ann (Lam {body, _}) (Pi {arg, res, _}) floc =>
let s = Ann s arg s.loc in
whnf defs ctx rh $ Ann (sub1 body s) (sub1 res s) appLoc
Coe ty p q val _ => piCoe defs ctx rh ty p q val s appLoc
whnf defs ctx sg $ Ann (sub1 body s) (sub1 res s) appLoc
Coe ty p q val _ => piCoe defs ctx sg ty p q val s appLoc
Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
-- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
-- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
whnf defs ctx rh (CasePair pi pair ret body caseLoc) = do
Element pair pairnf <- whnf defs ctx rh pair
--
-- 0 · case e return p ⇒ C of { (a, b) ⇒ u } ⇝
-- u[fst e/a, snd e/b] ∷ C[e/p]
whnf defs ctx sg (CasePair pi pair ret body caseLoc) = do
Element pair pairnf <- whnf defs ctx sg pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
let fst = Ann fst tfst fst.loc
snd = Ann snd (sub1 tsnd fst) snd.loc
in
whnf defs ctx rh $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
whnf defs ctx sg $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
Coe ty p q val _ => do
sigCoe defs ctx rh pi ty p q val ret body caseLoc
sigCoe defs ctx sg pi ty p q val ret body caseLoc
Right np =>
pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
case sg `decEq` SZero of
Yes Refl =>
whnf defs ctx SZero $
Ann (subN body [< Fst pair caseLoc, Snd pair caseLoc])
(sub1 ret pair)
caseLoc
No n0 =>
pure $ Element (CasePair pi pair ret body caseLoc)
(pairnf `orNo` np `orNo` notYesNo n0)
-- fst ((s, t) ∷ (x : A) × B) ⇝ s ∷ A
whnf defs ctx sg (Fst pair fstLoc) = do
Element pair pairnf <- whnf defs ctx sg pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
whnf defs ctx sg $ Ann fst tfst pairLoc
Coe ty p q val _ => do
fstCoe defs ctx sg ty p q val fstLoc
Right np =>
pure $ Element (Fst pair fstLoc) (pairnf `orNo` np)
-- snd ((s, t) ∷ (x : A) × B) ⇝ t ∷ B[(s ∷ A)/x]
whnf defs ctx sg (Snd pair sndLoc) = do
Element pair pairnf <- whnf defs ctx sg pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
whnf defs ctx sg $ Ann snd (sub1 tsnd (Ann fst tfst fst.loc)) sndLoc
Coe ty p q val _ => do
sndCoe defs ctx sg ty p q val sndLoc
Right np =>
pure $ Element (Snd pair sndLoc) (pairnf `orNo` np)
-- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
-- u ∷ C['a∷{a,…}/p]
whnf defs ctx rh (CaseEnum pi tag ret arms caseLoc) = do
Element tag tagnf <- whnf defs ctx rh tag
whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
Element tag tagnf <- whnf defs ctx sg tag
case nchoose $ isTagHead tag of
Left _ => case tag of
Ann (Tag t _) (Enum ts _) _ =>
let ty = sub1 ret tag in
case lookup t arms of
Just arm => whnf defs ctx rh $ Ann arm ty arm.loc
Just arm => whnf defs ctx sg $ Ann arm ty arm.loc
Nothing => throw $ MissingEnumArm caseLoc t (keys arms)
Coe ty p q val _ =>
-- there is nowhere an equality can be hiding inside an enum type
whnf defs ctx rh $
whnf defs ctx sg $
CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc
Right nt =>
pure $ Element (CaseEnum pi tag ret arms caseLoc) $ tagnf `orNo` nt
@ -72,37 +107,37 @@ CanWhnf Elim Interface.isRedexE where
--
-- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
-- u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
whnf defs ctx rh (CaseNat pi piIH nat ret zer suc caseLoc) = do
Element nat natnf <- whnf defs ctx rh nat
whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
Element nat natnf <- whnf defs ctx sg nat
case nchoose $ isNatHead nat of
Left _ =>
let ty = sub1 ret nat in
case nat of
Ann (Zero _) (Nat _) _ =>
whnf defs ctx rh $ Ann zer ty zer.loc
whnf defs ctx sg $ Ann zer ty zer.loc
Ann (Succ n succLoc) (Nat natLoc) _ =>
let nn = Ann n (Nat natLoc) succLoc
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
in
whnf defs ctx rh $ Ann tm ty caseLoc
whnf defs ctx sg $ Ann tm ty caseLoc
Coe ty p q val _ =>
-- same deal as Enum
whnf defs ctx rh $
whnf defs ctx sg $
CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc
Right nn => pure $
Element (CaseNat pi piIH nat ret zer suc caseLoc) (natnf `orNo` nn)
-- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
-- u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
whnf defs ctx rh (CaseBox pi box ret body caseLoc) = do
Element box boxnf <- whnf defs ctx rh box
whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
Element box boxnf <- whnf defs ctx sg box
case nchoose $ isBoxHead box of
Left _ => case box of
Ann (Box val boxLoc) (BOX q bty tyLoc) _ =>
let ty = sub1 ret box in
whnf defs ctx rh $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
whnf defs ctx sg $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
Coe ty p q val _ =>
boxCoe defs ctx rh pi ty p q val ret body caseLoc
boxCoe defs ctx sg pi ty p q val ret body caseLoc
Right nb =>
pure $ Element (CaseBox pi box ret body caseLoc) (boxnf `orNo` nb)
@ -110,35 +145,35 @@ CanWhnf Elim Interface.isRedexE where
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
--
-- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
whnf defs ctx rh (DApp f p appLoc) = do
Element f fnf <- whnf defs ctx rh f
whnf defs ctx sg (DApp f p appLoc) = do
Element f fnf <- whnf defs ctx sg f
case nchoose $ isDLamHead f of
Left _ => case f of
Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ =>
whnf defs ctx rh $
whnf defs ctx sg $
Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
(dsub1 ty p) appLoc
Coe ty p' q' val _ =>
eqCoe defs ctx rh ty p' q' val p appLoc
eqCoe defs ctx sg ty p' q' val p appLoc
Right ndlh => case p of
K e _ => do
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx rh f
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
| ty => throw $ ExpectedEq ty.loc ctx.names ty
whnf defs ctx rh $
whnf defs ctx sg $
ends (Ann (setLoc appLoc l) ty.zero appLoc)
(Ann (setLoc appLoc r) ty.one appLoc) e
B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
-- e ∷ A ⇝ e
whnf defs ctx rh (Ann s a annLoc) = do
Element s snf <- whnf defs ctx rh s
whnf defs ctx sg (Ann s a annLoc) = do
Element s snf <- whnf defs ctx sg s
case nchoose $ isE s of
Left _ => let E e = s in pure $ Element e $ noOr2 snf
Right ne => do
Element a anf <- whnf defs ctx SZero a
pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
whnf defs ctx rh (Coe sty p q val coeLoc) =
whnf defs ctx sg (Coe sty p q val coeLoc) =
-- 𝑖 ∉ fv(A)
-- -------------------------------
-- coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
@ -148,30 +183,30 @@ CanWhnf Elim Interface.isRedexE where
([< i], Left ty) =>
case p `decEqv` q of
-- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
Yes _ => whnf defs ctx rh $ Ann val (dsub1 sty p) coeLoc
Yes _ => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
No npq => do
Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
case nchoose $ canPushCoe rh ty val of
Left pc => pushCoe defs ctx rh i ty p q val coeLoc
case nchoose $ canPushCoe sg ty val of
Left pc => pushCoe defs ctx sg i ty p q val coeLoc
Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
(tynf `orNo` npc `orNo` notYesNo npq)
(_, Right ty) =>
whnf defs ctx rh $ Ann val ty coeLoc
whnf defs ctx sg $ Ann val ty coeLoc
whnf defs ctx rh (Comp ty p q val r zero one compLoc) =
whnf defs ctx sg (Comp ty p q val r zero one compLoc) =
case p `decEqv` q of
-- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
Yes y => whnf defs ctx rh $ Ann val ty compLoc
Yes y => whnf defs ctx sg $ 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 rh $ Ann (dsub1 zero q) ty compLoc
K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc
-- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
K One _ => whnf defs ctx rh $ Ann (dsub1 one q) ty compLoc
K One _ => whnf defs ctx sg $ Ann (dsub1 one q) ty compLoc
B {} => pure $ Element (Comp ty p q val r zero one compLoc)
(notYesNo npq `orNo` Ah)
whnf defs ctx rh (TypeCase ty ret arms def tcLoc) =
case rh `decEq` SZero of
whnf defs ctx sg (TypeCase ty ret arms def tcLoc) =
case sg `decEq` SZero of
Yes Refl => do
Element ty tynf <- whnf defs ctx SZero ty
Element ret retnf <- whnf defs ctx SZero ret
@ -181,12 +216,12 @@ CanWhnf Elim Interface.isRedexE where
Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
(tynf `orNo` retnf `orNo` nt)
No _ =>
throw $ ClashQ tcLoc rh.qty Zero
throw $ ClashQ tcLoc sg.qty Zero
whnf defs ctx rh (CloE (Sub el th)) =
whnf defs ctx rh $ pushSubstsWith' id th el
whnf defs ctx rh (DCloE (Sub el th)) =
whnf defs ctx rh $ pushSubstsWith' th id el
whnf defs ctx sg (CloE (Sub el th)) =
whnf defs ctx sg $ pushSubstsWith' id th el
whnf defs ctx sg (DCloE (Sub el th)) =
whnf defs ctx sg $ pushSubstsWith' th id el
covering
CanWhnf Term Interface.isRedexT where
@ -206,13 +241,13 @@ CanWhnf Term Interface.isRedexT where
whnf _ _ _ t@(Box {}) = pure $ nred t
-- s ∷ A ⇝ s (in term context)
whnf defs ctx rh (E e) = do
Element e enf <- whnf defs ctx rh e
whnf defs ctx sg (E e) = do
Element e enf <- whnf defs ctx sg e
case nchoose $ isAnn e of
Left _ => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
Right na => pure $ Element (E e) $ na `orNo` enf
whnf defs ctx rh (CloT (Sub tm th)) =
whnf defs ctx rh $ pushSubstsWith' id th tm
whnf defs ctx rh (DCloT (Sub tm th)) =
whnf defs ctx rh $ pushSubstsWith' th id tm
whnf defs ctx sg (CloT (Sub tm th)) =
whnf defs ctx sg $ pushSubstsWith' id th tm
whnf defs ctx sg (DCloT (Sub tm th)) =
whnf defs ctx sg $ pushSubstsWith' th id tm