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

Compare commits

base: rhi:cdf1ec6debdaa837aadd4013b9929108ad999715
Branches Tags
rhi:🐉
rhi:qpoly
rhi:🎋
rhi:𝕎
rhi:🥚🛁
rhi:ope
...
compare: rhi:a14c4ca1cb66b2a30115b81b9d33f8b368018725
Branches Tags
rhi:🐉
rhi:qpoly
rhi:🎋
rhi:𝕎
rhi:🥚🛁
rhi:ope

8 Commits
cdf1ec6deb ... a14c4ca1cb

Author SHA1 Message Date
rhiannon morris a14c4ca1cb never inline let bindings from the original source 2023-12-21 18:04:12 +01:00
rhiannon morris b7074720ad pretty printing fixes 2023-12-21 18:03:57 +01:00
rhiannon morris 48a050491c fix several quantity issues 
- contents of box intro
- definition of let
- non-recursive ℕ case
- also make a few var names more consistent
 2023-12-21 18:01:17 +01:00
rhiannon morris aa4ead592a allow "let x : A = e in s" with type annotation 2023-12-21 17:54:31 +01:00
rhiannon morris 54db7e27ef make #[fail] run in the current namespace 2023-12-21 17:53:46 +01:00
rhiannon morris 7afcbfe258 recognise nats other than 0 in eq checker 2023-12-21 17:48:12 +01:00
rhiannon morris 0fdd4741be print quantity on let 2023-12-07 01:43:39 +01:00
rhiannon morris 03c197bd04 add local bindings to context 
- without this, inside the body of `let x = e in …`, the typechecker
  would forget that `x = e`
- now bound variables can reduce, if they have a definition, so RedexTest
  needs to take the context too
 2023-12-07 01:43:39 +01:00
21 changed files with 433 additions and 307 deletions
Show Stats Expand all files Collapse all files

7
exe/Main.idr
View File

@ -164,7 +164,7 @@ private
liftFromParser : Eff FromParserIO a -> Eff CompileStop a
liftFromParser act =
runEff act $ with Union.(::)
[handleExcept (\err => throw $ FromParserError err),
[handleExcept $ \err => throw $ FromParserError err,
handleStateIORef !(asksAt STATE defs),
handleStateIORef !(asksAt STATE ns),
handleStateIORef !(asksAt STATE suf),
@ -174,8 +174,7 @@ private
liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
liftErase defs act =
runEff act
[\case Err e => throw $ EraseError e,
\case Ask => pure defs,
[handleExcept $ \err => throw $ EraseError err,
handleStateIORef !(asksAt STATE suf)]
private
@ -207,7 +206,7 @@ processFile file = withEarlyStop $ do
traverse (uncurry Q.prettyDef) defList
let defs = SortedMap.fromList defList
erased <- liftErase defs $
traverse (\(x, d) => (x,) <$> eraseDef x d) defList
traverse (\(x, d) => (x,) <$> eraseDef defs x d) defList
outputDocStopIf Erase $
traverse (uncurry U.prettyDef) erased
(scheme, mains) <- liftScheme $ map catMaybes $

42
lib/Quox/Equal.idr
View File

@ -170,12 +170,19 @@ compareType : Definitions -> EqContext n -> (s, t : Term 0 n) ->
Eff EqualInner ()
private
0 NotRedexEq : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> EqContext n -> SQty -> Pred (tm 0 n)
NotRedexEq defs ctx sg t = NotRedex defs (toWhnfContext ctx) sg t
namespace Term
private covering
compare0' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
compare0' : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) ->
(ty, s, t : Term 0 n) ->
(0 _ : NotRedex defs SZero ty) => (0 _ : So (isTyConE ty)) =>
(0 _ : NotRedex defs sg s) => (0 _ : NotRedex defs sg t) =>
(0 _ : NotRedexEq defs ctx SZero ty) =>
(0 _ : So (isTyConE ty)) =>
(0 _ : NotRedexEq defs ctx sg s) =>
(0 _ : NotRedexEq defs ctx sg t) =>
Eff EqualInner ()
compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t
@ -298,10 +305,10 @@ namespace Term
(E _, Nat 0 {}) => clashT s.loc ctx nat s t
(E _, Succ {}) => clashT s.loc ctx nat s t
(Nat 0 {}, t) => wrongType t.loc ctx nat t
(Succ {}, t) => wrongType t.loc ctx nat t
(E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s
(Nat {}, t) => wrongType t.loc ctx nat t
(Succ {}, t) => wrongType t.loc ctx nat t
(E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s
compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
case (s, t) of
@ -350,9 +357,10 @@ namespace Term
private covering
compareType' : (defs : Definitions) -> EqContext n -> (s, t : Term 0 n) ->
(0 _ : NotRedex defs SZero s) => (0 _ : So (isTyConE s)) =>
(0 _ : NotRedex defs SZero t) => (0 _ : So (isTyConE t)) =>
compareType' : (defs : Definitions) -> (ctx : EqContext n) ->
(s, t : Term 0 n) ->
(0 _ : NotRedexEq defs ctx SZero s) => (0 _ : So (isTyConE s)) =>
(0 _ : NotRedexEq defs ctx SZero t) => (0 _ : So (isTyConE t)) =>
(0 _ : So (sameTyCon s t)) =>
Eff EqualInner ()
-- equality is the same as subtyping, except with the
@ -477,8 +485,9 @@ namespace Elim
EqualElim = InnerErrEff :: EqualInner
private covering
computeElimTypeE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
(e : Elim 0 n) -> (0 ne : NotRedex defs sg e) =>
computeElimTypeE : (defs : Definitions) -> (ctx : EqContext n) ->
(sg : SQty) ->
(e : Elim 0 n) -> (0 ne : NotRedexEq defs ctx sg e) =>
Eff EqualElim (Term 0 n)
computeElimTypeE defs ectx sg e = lift $
computeElimType defs (toWhnfContext ectx) sg e
@ -492,8 +501,8 @@ namespace Elim
try act = lift $ catch putError $ lift act {fs' = EqualElim}
private covering %inline
clashE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
(e, f : Elim 0 n) -> (0 nf : NotRedex defs sg f) =>
clashE : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) ->
(e, f : Elim 0 n) -> (0 nf : NotRedexEq defs ctx sg f) =>
Eff EqualElim (Term 0 n)
clashE defs ctx sg e f = do
putError $ ClashE e.loc ctx !mode e f
@ -522,9 +531,10 @@ namespace Elim
(e, f : Elim 0 n) -> Eff EqualElim (Term 0 n)
private covering
compare0Inner' : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
compare0Inner' : (defs : Definitions) -> (ctx : EqContext n) -> (sg : SQty) ->
(e, f : Elim 0 n) ->
(0 ne : NotRedex defs sg e) -> (0 nf : NotRedex defs sg f) ->
(0 ne : NotRedexEq defs ctx sg e) ->
(0 nf : NotRedexEq defs ctx sg f) ->
Eff EqualElim (Term 0 n)
compare0Inner' defs ctx sg e@(F {}) f _ _ = do

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

@ -45,7 +45,8 @@ FromParserIO = FromParserPure ++ [LoadFile]
export
fromParserPure : NameSuf -> Definitions ->
fromParserPure : {default [<] ns : Mods} ->
NameSuf -> Definitions ->
Eff FromParserPure a ->
Either Error (a, NameSuf, Definitions)
fromParserPure suf defs act = runSTErr $ do
@ -54,7 +55,7 @@ fromParserPure suf defs act = runSTErr $ do
res <- runEff act $ with Union.(::)
[handleExcept (\e => stLeft e),
handleStateSTRef defs,
handleStateSTRef !(liftST $ newSTRef [<]),
handleStateSTRef !(liftST $ newSTRef ns),
handleStateSTRef suf]
pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
@ -375,7 +376,7 @@ data HasFail = NoFail | AnyFail | FailWith String
export covering
expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error
expectFail loc act =
case fromParserPure !(getAt GEN) !(getAt DEFS) act of
case fromParserPure !(getAt GEN) !(getAt DEFS) {ns = !(getAt NS)} act of
Left err => pure err
Right _ => throw $ ExpectedFail loc

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

@ -593,15 +593,21 @@ letIntro fname =
<|> withLoc fname (Just . PQ Any <$ res "letω")
<|> Nothing <$ resC "let"
export
private
letBinder : FileName -> Maybe PQty -> Grammar True (PQty, PatVar, PTerm)
letBinder fname mq = do
qty <- the (Grammar False PQty) $ case mq of
Just q => pure q
Nothing => qty fname <* mustWork (resC ".") <|> defLoc fname (PQ One)
x <- patVar fname; mustWork (resC "=")
rhs <- term fname
pure $ (qty, x, rhs)
qty <- letQty fname mq
x <- patVar fname
type <- optional $ resC ":" *> term fname
rhs <- resC "=" *> term fname
pure (qty, x, makeLetRhs rhs type)
where
letQty : FileName -> Maybe PQty -> Grammar False PQty
letQty fname Nothing = qty fname <* mustWork (resC ".") <|> defLoc fname (PQ One)
letQty fname (Just q) = pure q
makeLetRhs : PTerm -> Maybe PTerm -> PTerm
makeLetRhs tm ty = maybe tm (\t => Ann tm t (extendL tm.loc t.loc)) ty
export
letTerm : FileName -> Grammar True PTerm

6
lib/Quox/Pretty.idr
View File

@ -308,9 +308,9 @@ export
prettyApp : {opts : LayoutOpts} -> Nat -> Doc opts ->
List (Doc opts) -> Doc opts
prettyApp ind f args =
hsep (f :: args)
<|> hsep [f, vsep args]
<|> vsep (f :: map (indent ind) args)
ifMultiline
(hsep (f :: args))
(f <++> vsep args <|> vsep (f :: map (indent ind) args))
export
prettyAppD : {opts : LayoutOpts} -> Doc opts -> List (Doc opts) ->

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

@ -342,17 +342,39 @@ private covering
prettyLets : {opts : LayoutOpts} ->
BContext d -> BContext a -> Telescope (LetBinder d) a b ->
Eff Pretty (SnocList (Doc opts))
prettyLets dnames xs lets = sequence $ snd $ go lets where
prettyLets dnames xs lets = snd <$> go lets where
peelAnn : forall d, n. Elim d n -> Maybe (Term d n, Term d n)
peelAnn (Ann tm ty _) = Just (tm, ty)
peelAnn e = Nothing
letHeader : Qty -> BindName -> Eff Pretty (Doc opts)
letHeader qty x = do
lett <- [|letD <+> prettyQty qty|]
x <- prettyTBind x
pure $ lett <++> x
letBody : forall n. BContext n ->
Doc opts -> Elim d n -> Eff Pretty (Doc opts)
letBody tnames hdr e = case peelAnn e of
Just (tm, ty) => do
ty <- withPrec Outer $ assert_total prettyTerm dnames tnames ty
tm <- withPrec Outer $ assert_total prettyTerm dnames tnames tm
colon <- colonD; eq <- cstD; d <- askAt INDENT
pure $ hangSingle d (hangSingle d hdr (colon <++> ty)) (eq <++> tm)
Nothing => do
e <- withPrec Outer $ assert_total prettyElim dnames tnames e
eq <- cstD; d <- askAt INDENT
pure $ ifMultiline
(hsep [hdr, eq, e])
(vsep [hdr, indent d $ hsep [eq, e]])
go : forall b. Telescope (LetBinder d) a b ->
(BContext b, SnocList (Eff Pretty (Doc opts)))
go [<] = (xs, [<])
go (lets :< (qty, x, rhs)) =
let (ys, docs) = go lets
doc = do
x <- prettyTBind x
rhs <- withPrec Outer $ assert_total prettyElim dnames ys rhs
hangDSingle (hsep [!letD, x, !cstD]) (hsep [rhs, !inD]) in
(ys :< x, docs :< doc)
Eff Pretty (BContext b, SnocList (Doc opts))
go [<] = pure (xs, [<])
go (lets :< (qty, x, rhs)) = do
(ys, docs) <- go lets
doc <- letBody ys !(letHeader qty x) rhs
pure (ys :< x, docs :< doc)
private
@ -503,7 +525,10 @@ prettyTerm dnames tnames (Let qty rhs body _) = do
let lines = toList $ heads :< body
pure $ ifMultiline (hsep lines) (vsep lines)
prettyTerm dnames tnames (E e) = prettyElim dnames tnames e
prettyTerm dnames tnames (E e) =
case the (Elim d n) (pushSubsts' e) of
Ann tm _ _ => assert_total prettyTerm dnames tnames tm
_ => assert_total prettyElim dnames tnames e
prettyTerm dnames tnames t0@(CloT (Sub t ph)) =
prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' id ph t
@ -566,9 +591,12 @@ prettyElim dnames tnames e@(DApp {}) =
prettyDTApps dnames tnames f xs
prettyElim dnames tnames (Ann tm ty _) =
parensIfM Outer =<<
hangDSingle !(withPrec AnnL [|prettyTerm dnames tnames tm <++> annD|])
!(withPrec Outer (prettyTerm dnames tnames ty))
case the (Term d n) (pushSubsts' tm) of
E e => assert_total prettyElim dnames tnames e
_ => do
tm <- withPrec AnnL $ assert_total prettyTerm dnames tnames tm
ty <- withPrec Outer $ assert_total prettyTerm dnames tnames ty
parensIfM Outer =<< hangDSingle (tm <++> !annD) ty
prettyElim dnames tnames (Coe ty p q val _) =
parensIfM App =<< do

37
lib/Quox/Typechecker.idr
View File

@ -208,16 +208,17 @@ mutual
check' ctx sg (Box val loc) ty = do
(q, ty) <- expectBOX !(askAt DEFS) ctx SZero ty.loc ty
-- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
valout <- checkC ctx sg val ty
-- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ
valout <- checkC ctx (subjMult sg q) val ty
-- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
pure $ q * valout
check' ctx sg (Let qty rhs body loc) ty = do
eres <- inferC ctx (subjMult sg qty) rhs
qout <- checkC (extendTy (qty * sg.qty) body.name eres.type ctx) sg
body.term (weakT 1 ty)
>>= popQ loc qty
let sqty = sg.qty * qty
qout <- checkC (extendTyLet sqty body.name eres.type (E rhs) ctx)
sg body.term (weakT 1 ty)
>>= popQ loc sqty
pure $ qty * eres.qout + qout
check' ctx sg (E e) ty = do
@ -338,8 +339,8 @@ mutual
pure $ lookupBound sg.qty i ctx.tctx
where
lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
lookupBound pi VZ (ctx :< type) =
InfRes {type = weakT 1 type, qout = zeroFor ctx :< pi}
lookupBound pi VZ (ctx :< var) =
InfRes {type = weakT 1 var.type, qout = zeroFor ctx :< pi}
lookupBound pi (VS i) (ctx :< _) =
let InfRes {type, qout} = lookupBound pi i ctx in
InfRes {type = weakT 1 type, qout = qout :< Zero}
@ -432,8 +433,8 @@ mutual
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
zerout <- checkC ctx sg zer $ sub1 ret $ Ann (Zero zer.loc) nat zer.loc
-- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
-- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
-- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ.p, ς.ih
-- with ς ≤ π'σ, (ρ + ς) ≤ πσ
let [< p, ih] = suc.names
pisg = pi * sg.qty
sucCtx = extendTyN [< (pisg, p, NAT p.loc), (pi', ih, ret.term)] ctx
@ -442,24 +443,28 @@ mutual
expectCompatQ loc qih (pi' * sg.qty)
-- [fixme] better error here
expectCompatQ loc (qp + qih) pisg
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
-- if ς = 0, then Σb = lubs(Σz, Σs), otherwise Σb = Σz + ωςΣs
let bodyout = case qih of
Zero => lubs ctx [zerout, sucout]
_ => zerout + Any * sucout
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σb
pure $ InfRes {
type = sub1 ret n,
qout = pi * nres.qout + zerout + Any * sucout
qout = pi * nres.qout + bodyout
}
infer' ctx sg (CaseBox pi box ret body loc) = do
-- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
boxres <- inferC ctx sg box
(q, ty) <- expectBOX !(askAt DEFS) ctx SZero box.loc boxres.type
(rh, ty) <- expectBOX !(askAt DEFS) ctx SZero box.loc boxres.type
-- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
-- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
-- with ς ≤ ρπσ
let qpisg = q * pi * sg.qty
bodyCtx = extendTy qpisg body.name ty ctx
let rhpisg = rh * pi * sg.qty
bodyCtx = extendTy rhpisg body.name ty ctx
bodyType = substCaseBoxRet body.name ty ret
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc qpisg
bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ loc rhpisg
-- then Ψ | Γ ⊢ caseπ ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
pure $ InfRes {
type = sub1 ret box,

4
lib/Quox/Typing.idr
View File

@ -70,7 +70,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc)
export covering
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm d n -> Eff fs (NonRedex tm d n defs sg)
tm d n -> Eff fs (NonRedex tm d n defs ? sg)
whnf tm = do
let Val n = ctx.termLen; Val d = ctx.dimLen
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
@ -120,7 +120,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
export covering
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm 0 n -> Eff fs (NonRedex tm 0 n defs sg)
tm 0 n -> Eff fs (NonRedex tm 0 n defs ? sg)
whnf tm = do
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
rethrow res

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

@ -14,9 +14,27 @@ public export
QContext : Nat -> Type
QContext = Context' Qty
public export
record LocalVar d n where
constructor MkLocal
type : Term d n
term : Maybe (Term d n) -- if from a `let`
%runElab deriveIndexed "LocalVar" [Show]
export
CanShift (LocalVar d) where
l // by = {type $= (// by), term $= map (// by)} l
namespace LocalVar
subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
subD th = {type $= (// th), term $= map (// th)}
weakD : LocalVar d n -> LocalVar (S d) n
weakD = subD $ shift 1
public export
TContext : TermLike
TContext d = Context (Term d)
TContext d = Context (\n => LocalVar d n)
public export
QOutput : Nat -> Type
@ -67,10 +85,6 @@ record WhnfContext d n where
%runElab deriveIndexed "WhnfContext" [Show]
namespace TContext
export %inline
pushD : TContext d n -> TContext (S d) n
pushD tel = map (// shift 1) tel
export %inline
zeroFor : Context tm n -> QOutput n
zeroFor ctx = Zero <$ ctx
@ -89,6 +103,14 @@ public export
CtxExtension0 : Nat -> Nat -> Nat -> Type
CtxExtension0 d = Telescope ((BindName,) . Term d)
public export
CtxExtensionLet : Nat -> Nat -> Nat -> Type
CtxExtensionLet d = Telescope ((Qty, BindName,) . LocalVar d)
public export
CtxExtensionLet0 : Nat -> Nat -> Nat -> Type
CtxExtensionLet0 d = Telescope ((BindName,) . LocalVar d)
namespace TyContext
public export %inline
empty : TyContext 0 0
@ -100,21 +122,34 @@ namespace TyContext
null ctx = null ctx.dnames && null ctx.tnames
export %inline
extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
let (qs, xs, ss) = unzip3 xss in
extendTyLetN : CtxExtensionLet d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyLetN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
let (qs, xs, ls) = unzip3 xss in
MkTyContext {
dctx, dnames,
termLen = extendLen xss termLen,
tctx = tctx . ss,
tctx = tctx . ls,
tnames = tnames . xs,
qtys = qtys . qs
}
export %inline
extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
export %inline
extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyLetN0 xss = extendTyLetN (map (Zero,) xss)
export %inline
extendTyN0 : CtxExtension0 d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN0 xss = extendTyN (map (Zero,) xss)
export %inline
extendTyLet : Qty -> BindName -> Term d n -> Term d n ->
TyContext d n -> TyContext d (S n)
extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
export %inline
extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
extendTy q x s = extendTyN [< (q, x, s)]
@ -130,7 +165,7 @@ namespace TyContext
dctx = dctx :<? Nothing,
dnames = dnames :< x,
dimLen = [|S dimLen|],
tctx = pushD tctx,
tctx = map weakD tctx,
tnames, qtys
}
@ -169,7 +204,7 @@ makeEqContext' ctx th = MkEqContext {
termLen = ctx.termLen,
dassign = makeDAssign th,
dnames = ctx.dnames,
tctx = map (// th) ctx.tctx,
tctx = map (subD th) ctx.tctx,
tnames = ctx.tnames,
qtys = ctx.qtys
}
@ -191,21 +226,34 @@ namespace EqContext
null ctx = null ctx.dnames && null ctx.tnames
export %inline
extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
let (qs, xs, ss) = unzip3 xss in
extendTyLetN : CtxExtensionLet 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyLetN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
let (qs, xs, ls) = unzip3 xss in
MkEqContext {
termLen = extendLen xss termLen,
tctx = tctx . ss,
tctx = tctx . ls,
tnames = tnames . xs,
qtys = qtys . qs,
dassign, dnames
}
export %inline
extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
export %inline
extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyLetN0 xss = extendTyLetN (map (Zero,) xss)
export %inline
extendTyN0 : CtxExtension0 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN0 xss = extendTyN (map (Zero,) xss)
export %inline
extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n ->
EqContext n -> EqContext (S n)
extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
export %inline
extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
extendTy q x s = extendTyN [< (q, x, s)]
@ -225,7 +273,7 @@ namespace EqContext
toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
MkTyContext {
dctx = fromGround dassign,
tctx = map (// shift0 dimLen) tctx,
tctx = map (subD $ shift0 dimLen) tctx,
dnames, tnames, qtys
}
@ -252,7 +300,7 @@ namespace WhnfContext
MkWhnfContext {
dimLen = [|Val s + dimLen|],
dnames = dnames ++ toSnocVect' ns,
tctx = dweakT s <$> tctx,
tctx = map (subD $ shift s) tctx,
tnames
}
@ -264,10 +312,20 @@ namespace WhnfContext
private
prettyTContextElt : {opts : _} ->
BContext d -> BContext n ->
Qty -> BindName -> Term d n -> Eff Pretty (Doc opts)
prettyTContextElt dnames tnames q x s =
pure $ hsep [hcat [!(prettyQty q), !dotD, !(prettyTBind x)], !colonD,
!(withPrec Outer $ prettyTerm dnames tnames s)]
Qty -> BindName -> LocalVar d n -> Eff Pretty (Doc opts)
prettyTContextElt dnames tnames q x s = do
q <- prettyQty q; dot <- dotD
x <- prettyTBind x; colon <- colonD
ty <- withPrec Outer $ prettyTerm dnames tnames s.type; eq <- cstD
tm <- traverse (withPrec Outer . prettyTerm dnames tnames) s.term
d <- askAt INDENT
let qx = hcat [q, dot, x]
pure $ case tm of
Nothing =>
ifMultiline (hsep [qx, colon, ty]) (vsep [qx, indent d $ colon <++> ty])
Just tm =>
ifMultiline (hsep [qx, colon, ty, eq, tm])
(vsep [qx, indent d $ colon <++> ty, indent d $ eq <++> tm])
private
prettyTContext' : {opts : _} ->
@ -282,8 +340,10 @@ export
prettyTContext : {opts : _} ->
BContext d -> QContext n -> BContext n ->
TContext d n -> Eff Pretty (Doc opts)
prettyTContext dnames qtys tnames tys =
separateTight !commaD <$> prettyTContext' dnames qtys tnames tys
prettyTContext dnames qtys tnames tys = do
comma <- commaD
sepSingle . exceptLast (<+> comma) . toList <$>
prettyTContext' dnames qtys tnames tys
export
prettyTyContext : {opts : _} -> TyContext d n -> Eff Pretty (Doc opts)
@ -291,8 +351,8 @@ prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
case dctx of
C [<] => prettyTContext dnames qtys tnames tctx
_ => pure $
sep [!(prettyDimEq dnames dctx) <++> !pipeD,
!(prettyTContext dnames qtys tnames tctx)]
sepSingle [!(prettyDimEq dnames dctx) <++> !pipeD,
!(prettyTContext dnames qtys tnames tctx)]
export
prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)

7
lib/Quox/Typing/Error.idr
View File

@ -256,7 +256,7 @@ parameters {opts : LayoutOpts} (showContext : Bool)
Doc opts -> Eff Pretty (Doc opts)
inContext' null ctx f doc =
if showContext && not null then
pure $ vappend doc (sep ["in context", !(f ctx)])
vappend doc <$> hangDSingle "in context" !(f ctx)
else pure doc
export %inline
@ -416,5 +416,6 @@ parameters {opts : LayoutOpts} (showContext : Bool)
export
prettyError : Error -> Eff Pretty (Doc opts)
prettyError err = sep <$> sequence
[prettyLoc err.loc, indentD =<< prettyErrorNoLoc err]
prettyError err = hangDSingle
!(prettyLoc err.loc)
!(indentD =<< prettyErrorNoLoc err)

227
lib/Quox/Untyped/Erase.idr
View File

@ -88,16 +88,16 @@ parameters {opts : LayoutOpts} (showContext : Bool)
public export
Erase : List (Type -> Type)
Erase = [Except Error, DefsReader, NameGen]
Erase = [Except Error, NameGen]
export
liftWhnf : Eff Whnf a -> Eff Erase a
liftWhnf act = lift $ wrapErr WrapTypeError act
export covering
computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n)
computeElimType ctx sg e = do
defs <- askAt DEFS
computeElimType : Q.Definitions -> ErasureContext d n -> SQty ->
Elim d n -> Eff Erase (Term d n)
computeElimType defs ctx sg e = do
let ctx = toWhnfContext ctx
liftWhnf $ do
Element e _ <- whnf defs ctx sg e
@ -106,10 +106,11 @@ computeElimType ctx sg e = do
private %macro
wrapExpect : TTImp ->
Elab (TyContext d n -> Loc -> Term d n -> Eff Erase a)
Elab (Q.Definitions -> TyContext d n -> Loc ->
Term d n -> Eff Erase a)
wrapExpect f_ = do
f <- check `(\x => ~(f_) x)
pure $ \ctx, loc, s => liftWhnf $ f !(askAt DEFS) ctx SZero loc s
pure $ \defs, ctx, loc, s => liftWhnf $ f defs ctx SZero loc s
public export
@ -119,27 +120,36 @@ record EraseElimResult d n where
term : U.Term n
export covering
eraseTerm' : (defs : Q.Definitions) -> (ctx : ErasureContext d n) ->
(ty, tm : Q.Term d n) ->
(0 _ : NotRedex defs (toWhnfContext ctx) SZero ty) =>
Eff Erase (U.Term n)
-- "Ψ | Γ | Σ ⊢ s ⤋ s' ⇐ A" for `s' <- eraseTerm (Ψ,Γ,Σ) A s`
--
-- in the below comments, Ψ, Γ, Σ are implicit and
-- only their extensions are written
export covering
eraseTerm : ErasureContext d n ->
eraseTerm : Q.Definitions -> ErasureContext d n ->
(ty, tm : Q.Term d n) -> Eff Erase (U.Term n)
eraseTerm defs ctx ty tm = do
Element ty _ <- liftWhnf $ Interface.whnf defs (toWhnfContext ctx) SZero ty
eraseTerm' defs ctx ty tm
-- "Ψ | Γ | Σ ⊢ e ⤋ e' ⇒ A" for `EraRes A e' <- eraseElim (Ψ,Γ,Σ) e`
export covering
eraseElim : ErasureContext d n -> (tm : Q.Elim d n) ->
eraseElim : Q.Definitions -> ErasureContext d n -> (tm : Q.Elim d n) ->
Eff Erase (EraseElimResult d n)
eraseTerm ctx _ s@(TYPE {}) =
eraseTerm' defs ctx _ s@(TYPE {}) =
throw $ CompileTimeOnly ctx s
eraseTerm ctx _ s@(IOState {}) =
eraseTerm' defs ctx _ s@(IOState {}) =
throw $ CompileTimeOnly ctx s
eraseTerm ctx _ s@(Pi {}) =
eraseTerm' defs ctx _ s@(Pi {}) =
throw $ CompileTimeOnly ctx s
-- x : A | 0.x ⊢ s ⤋ s' ⇐ B
@ -149,66 +159,66 @@ eraseTerm ctx _ s@(Pi {}) =
-- x : A | π.x ⊢ s ⤋ s' ⇐ B π ≠ 0
-- ----------------------------------------
-- (λ x ⇒ s) ⤋ (λ x ⇒ s') ⇐ π.(x : A) → B
eraseTerm ctx ty (Lam body loc) = do
eraseTerm' defs ctx ty (Lam body loc) = do
let x = body.name
(qty, arg, res) <- wrapExpect `(expectPi) ctx loc ty
body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
(qty, arg, res) <- wrapExpect `(expectPi) defs ctx loc ty
body <- eraseTerm defs (extendTy qty x arg ctx) res.term body.term
pure $ case isErased qty of
Kept => U.Lam x body loc
Erased => sub1 (Erased loc) body
eraseTerm ctx _ s@(Sig {}) =
eraseTerm' defs ctx _ s@(Sig {}) =
throw $ CompileTimeOnly ctx s
-- s ⤋ s' ⇐ A t ⤋ t' ⇐ B[s/x]
-- ---------------------------------
-- (s, t) ⤋ (s', t') ⇐ (x : A) × B
eraseTerm ctx ty (Pair fst snd loc) = do
(a, b) <- wrapExpect `(expectSig) ctx loc ty
eraseTerm' defs ctx ty (Pair fst snd loc) = do
(a, b) <- wrapExpect `(expectSig) defs ctx loc ty
let b = sub1 b (Ann fst a a.loc)
fst <- eraseTerm ctx a fst
snd <- eraseTerm ctx b snd
fst <- eraseTerm defs ctx a fst
snd <- eraseTerm defs ctx b snd
pure $ Pair fst snd loc
eraseTerm ctx _ s@(Enum {}) =
eraseTerm' defs ctx _ s@(Enum {}) =
throw $ CompileTimeOnly ctx s
-- '𝐚 ⤋ '𝐚 ⇐ {⋯}
eraseTerm ctx _ (Tag tag loc) =
eraseTerm' defs ctx _ (Tag tag loc) =
pure $ Tag tag loc
eraseTerm ctx ty s@(Eq {}) =
eraseTerm' defs ctx ty s@(Eq {}) =
throw $ CompileTimeOnly ctx s
-- 𝑖 ⊢ s ⤋ s' ⇐ A
-- ---------------------------------
-- (δ 𝑖 ⇒ s) ⤋ s' ⇐ Eq (𝑖 ⇒ A) l r
eraseTerm ctx ty (DLam body loc) = do
a <- fst <$> wrapExpect `(expectEq) ctx loc ty
eraseTerm (extendDim body.name ctx) a.term body.term
eraseTerm' defs ctx ty (DLam body loc) = do
a <- fst <$> wrapExpect `(expectEq) defs ctx loc ty
eraseTerm defs (extendDim body.name ctx) a.term body.term
eraseTerm ctx _ s@(NAT {}) =
eraseTerm' defs ctx _ s@(NAT {}) =
throw $ CompileTimeOnly ctx s
-- n ⤋ n ⇐ ℕ
eraseTerm _ _ (Nat n loc) =
eraseTerm' _ _ _ (Nat n loc) =
pure $ Nat n loc
-- s ⤋ s' ⇐ ℕ
-- -----------------------
-- succ s ⤋ succ s' ⇐ ℕ
eraseTerm ctx ty (Succ p loc) = do
p <- eraseTerm ctx ty p
eraseTerm' defs ctx ty (Succ p loc) = do
p <- eraseTerm defs ctx ty p
pure $ Succ p loc
eraseTerm ctx ty s@(STRING {}) =
eraseTerm' defs ctx ty s@(STRING {}) =
throw $ CompileTimeOnly ctx s
-- s ⤋ s ⇐ String
eraseTerm _ _ (Str s loc) =
eraseTerm' _ _ _ (Str s loc) =
pure $ Str s loc
eraseTerm ctx ty s@(BOX {}) =
eraseTerm' defs ctx ty s@(BOX {}) =
throw $ CompileTimeOnly ctx s
-- [s] ⤋ ⌷ ⇐ [0.A]
@ -216,48 +226,49 @@ eraseTerm ctx ty s@(BOX {}) =
-- π ≠ 0 s ⤋ s' ⇐ A
-- --------------------
-- [s] ⤋ s' ⇐ [π.A]
eraseTerm ctx ty (Box val loc) = do
(qty, a) <- wrapExpect `(expectBOX) ctx loc ty
eraseTerm' defs ctx ty (Box val loc) = do
(qty, a) <- wrapExpect `(expectBOX) defs ctx loc ty
case isErased qty of
Erased => pure $ Erased loc
Kept => eraseTerm ctx a val
Kept => eraseTerm defs ctx a val
-- s ⤋ s' ⇐ A
-- ---------------------------------
-- let0 x = e in s ⤋ s'[⌷/x] ⇐ A
--
-- e ⤋ e' s ⤋ s' ⇐ A π ≠ 0
-- e ⤋ e' ⇒ E π ≠ 0
-- x : E ≔ e ⊢ s ⤋ s' ⇐ A
-- -------------------------------------
-- letπ x = e in s ⤋ let x = e' in s'
eraseTerm ctx ty (Let pi e s loc) = do
eraseTerm' defs ctx ty (Let pi e s loc) = do
let x = s.name
case isErased pi of
Erased => do
ety <- computeElimType ctx SZero e
s' <- eraseTerm (extendTy pi x ety ctx) (weakT 1 ty) s.term
ety <- computeElimType defs ctx SZero e
s' <- eraseTerm defs (extendTyLet pi x ety (E e) ctx) (weakT 1 ty) s.term
pure $ sub1 (Erased e.loc) s'
Kept => do
EraRes ety e' <- eraseElim ctx e
s' <- eraseTerm (extendTy pi x ety ctx) (weakT 1 ty) s.term
pure $ Let x e' s' loc
EraRes ety e' <- eraseElim defs ctx e
s' <- eraseTerm defs (extendTyLet pi x ety (E e) ctx) (weakT 1 ty) s.term
pure $ Let True x e' s' loc
-- e ⤋ e' ⇒ B
-- ------------
-- e ⤋ e' ⇐ A
eraseTerm ctx ty (E e) =
term <$> eraseElim ctx e
eraseTerm' defs ctx ty (E e) =
term <$> eraseElim defs ctx e
eraseTerm ctx ty (CloT (Sub term th)) =
eraseTerm ctx ty $ pushSubstsWith' id th term
eraseTerm' defs ctx ty (CloT (Sub term th)) =
eraseTerm defs ctx ty $ pushSubstsWith' id th term
eraseTerm ctx ty (DCloT (Sub term th)) =
eraseTerm ctx ty $ pushSubstsWith' th id term
eraseTerm' defs ctx ty (DCloT (Sub term th)) =
eraseTerm defs ctx ty $ pushSubstsWith' th id term
-- defω x : A = s
-- ----------------
-- x ⤋ x ⇒ A
eraseElim ctx e@(F x u loc) = do
Just def <- asksAt DEFS $ lookup x
eraseElim defs ctx e@(F x u loc) = do
let Just def = lookup x defs
| Nothing => throw $ notInScope loc x
case isErased def.qty.qty of
Erased => throw $ CompileTimeOnly ctx $ E e
@ -266,10 +277,10 @@ eraseElim ctx e@(F x u loc) = do
-- π.x ∈ Σ π ≠ 0
-- -----------------
-- x ⤋ x ⇒ A
eraseElim ctx e@(B i loc) = do
eraseElim defs ctx e@(B i loc) = do
case isErased $ ctx.qtys !!! i of
Erased => throw $ CompileTimeOnly ctx $ E e
Kept => pure $ EraRes (ctx.tctx !! i) $ B i loc
Kept => pure $ EraRes (ctx.tctx !! i).type $ B i loc
-- f ⤋ f' ⇒ π.(x : A) → B s ⤋ s' ⇒ A π ≠ 0
-- ---------------------------------------------
@ -278,13 +289,13 @@ eraseElim ctx e@(B i loc) = do
-- f ⤋ f' ⇒ 0.(x : A) → B
-- -------------------------
-- f s ⤋ f' ⇒ B[s/x]
eraseElim ctx (App fun arg loc) = do
efun <- eraseElim ctx fun
(qty, targ, tres) <- wrapExpect `(expectPi) ctx loc efun.type
eraseElim defs ctx (App fun arg loc) = do
efun <- eraseElim defs ctx fun
(qty, targ, tres) <- wrapExpect `(expectPi) defs ctx loc efun.type
let ty = sub1 tres (Ann arg targ arg.loc)
case isErased qty of
Erased => pure $ EraRes ty efun.term
Kept => do arg <- eraseTerm ctx targ arg
Kept => do arg <- eraseTerm defs ctx targ arg
pure $ EraRes ty $ App efun.term arg loc
-- e ⇒ (x : A) × B
@ -298,46 +309,46 @@ eraseElim ctx (App fun arg loc) = do
-- (caseρ e return z ⇒ R of {(x, y) ⇒ s}) ⤋
-- ⤋
-- let xy = e' in let x = fst xy in let y = snd xy in s' ⇒ R[e/z]
eraseElim ctx (CasePair qty pair ret body loc) = do
eraseElim defs ctx (CasePair qty pair ret body loc) = do
let [< x, y] = body.names
case isErased qty of
Kept => do
EraRes ety eterm <- eraseElim ctx pair
EraRes ety eterm <- eraseElim defs ctx pair
let ty = sub1 (ret // shift 2) $
Ann (Pair (BVT 0 loc) (BVT 1 loc) loc) (weakT 2 ety) loc
(tfst, tsnd) <- wrapExpect `(expectSig) ctx loc ety
(tfst, tsnd) <- wrapExpect `(expectSig) defs ctx loc ety
let ctx' = extendTyN [< (qty, x, tfst), (qty, y, tsnd.term)] ctx
body' <- eraseTerm ctx' ty body.term
body' <- eraseTerm defs ctx' ty body.term
p <- mnb "p" loc
pure $ EraRes (sub1 ret pair) $
Let p eterm
(Let x (Fst (B VZ loc) loc)
(Let y (Snd (B (VS VZ) loc) loc)
Let False p eterm
(Let False x (Fst (B VZ loc) loc)
(Let False y (Snd (B (VS VZ) loc) loc)
(body' // (B VZ loc ::: B (VS VZ) loc ::: shift 3))
loc) loc) loc
Erased => do
ety <- computeElimType ctx SOne pair
ety <- computeElimType defs ctx SOne pair
let ty = sub1 (ret // shift 2) $
Ann (Pair (BVT 0 loc) (BVT 1 loc) loc) (weakT 2 ety) loc
(tfst, tsnd) <- wrapExpect `(expectSig) ctx loc ety
(tfst, tsnd) <- wrapExpect `(expectSig) defs ctx loc ety
let ctx' = extendTyN0 [< (x, tfst), (y, tsnd.term)] ctx
body' <- eraseTerm ctx' ty body.term
body' <- eraseTerm defs ctx' ty body.term
pure $ EraRes (sub1 ret pair) $ subN [< Erased loc, Erased loc] body'
-- e ⤋ e' ⇒ (x : A) × B
-- ----------------------
-- fst e ⤋ fst e' ⇒ A
eraseElim ctx (Fst pair loc) = do
epair <- eraseElim ctx pair
a <- fst <$> wrapExpect `(expectSig) ctx loc epair.type
eraseElim defs ctx (Fst pair loc) = do
epair <- eraseElim defs ctx pair
a <- fst <$> wrapExpect `(expectSig) defs ctx loc epair.type
pure $ EraRes a $ Fst epair.term loc
-- e ⤋ e' ⇒ (x : A) × B
-- -----------------------------
-- snd e ⤋ snd e' ⇒ B[fst e/x]
eraseElim ctx (Snd pair loc) = do
epair <- eraseElim ctx pair
b <- snd <$> wrapExpect `(expectSig) ctx loc epair.type
eraseElim defs ctx (Snd pair loc) = do
epair <- eraseElim defs ctx pair
b <- snd <$> wrapExpect `(expectSig) defs ctx loc epair.type
pure $ EraRes (sub1 b (Fst pair loc)) $ Snd epair.term loc
-- caseρ e return z ⇒ R of {} ⤋ absurd ⇒ R[e/z]
@ -349,23 +360,23 @@ eraseElim ctx (Snd pair loc) = do
-- e ⤋ e' ⇒ A sᵢ ⤋ s'ᵢ ⇐ R[𝐚ᵢ/z] ρ ≠ 0 i ≠ 0
-- -------------------------------------------------------------------
-- caseρ e return z ⇒ R of {𝐚ᵢ ⇒ sᵢ} ⤋ case e of {𝐚ᵢ ⇒ s'ᵢ} ⇒ R[e/z]
eraseElim ctx e@(CaseEnum qty tag ret arms loc) = do
eraseElim defs ctx e@(CaseEnum qty tag ret arms loc) = do
let ty = sub1 ret tag
case isErased qty of
Erased => case SortedMap.toList arms of
[] => pure $ EraRes ty $ Absurd loc
[(t, rhs)] => do
let ty' = sub1 ret (Ann (Tag t loc) (enum [t] loc) loc)
rhs' <- eraseTerm ctx ty' rhs
rhs' <- eraseTerm defs ctx ty' rhs
pure $ EraRes ty rhs'
_ => throw $ CompileTimeOnly ctx $ E e
Kept => case List1.fromList $ SortedMap.toList arms of
Nothing => pure $ EraRes ty $ Absurd loc
Just arms => do
etag <- eraseElim ctx tag
etag <- eraseElim defs ctx tag
arms <- for arms $ \(t, rhs) => do
let ty' = sub1 ret (Ann (Tag t loc) etag.type loc)
rhs' <- eraseTerm ctx ty' rhs
rhs' <- eraseTerm defs ctx ty' rhs
pure (t, rhs')
pure $ EraRes ty $ CaseEnum etag.term arms loc
@ -382,12 +393,12 @@ eraseElim ctx e@(CaseEnum qty tag ret arms loc) = do
-- caseρ n return z ⇒ R of {0 ⇒ z; succ m, 0.ih ⇒ s}
-- ⤋
-- case n' of {0 ⇒ z'; succ m ⇒ s'[⌷/ih]} ⇒ R[n/z]
eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
eraseElim defs ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
let ty = sub1 ret nat
enat <- eraseElim ctx nat
zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (NAT loc) loc)) zero
enat <- eraseElim defs ctx nat
zero <- eraseTerm defs ctx (sub1 ret (Ann (Zero loc) (NAT loc) loc)) zero
let [< p, ih] = succ.names
succ' <- eraseTerm
succ' <- eraseTerm defs
(extendTyN [< (qty, p, NAT loc),
(qtyIH, ih, sub1 (ret // shift 1) (BV 0 loc))] ctx)
(sub1 (ret // shift 2) (Ann (Succ (BVT 1 loc) loc) (NAT loc) loc))
@ -404,56 +415,56 @@ eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
-- b ⇒ [π.A] x : A | 0.x ⊢ s ⤋ s' ⇐ R[[x]∷[0.A]/z] πρ = 0
-- -------------------------------------------------------------
-- caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ s'[⌷/x] ⇒ R[b/z]
eraseElim ctx (CaseBox qty box ret body loc) = do
tbox <- computeElimType ctx SOne box -- [fixme] is there any way to avoid this?
(pi, tinner) <- wrapExpect `(expectBOX) ctx loc tbox
eraseElim defs ctx (CaseBox qty box ret body loc) = do
tbox <- computeElimType defs ctx SOne box
(pi, tinner) <- wrapExpect `(expectBOX) defs ctx loc tbox
let ctx' = extendTy (pi * qty) body.name tinner ctx
bty = sub1 (ret // shift 1) $
Ann (Box (BVT 0 loc) loc) (weakT 1 tbox) loc
case isErased $ qty * pi of
Kept => do
ebox <- eraseElim ctx box
ebody <- eraseTerm ctx' bty body.term
pure $ EraRes (sub1 ret box) $ Let body.name ebox.term ebody loc
ebox <- eraseElim defs ctx box
ebody <- eraseTerm defs ctx' bty body.term
pure $ EraRes (sub1 ret box) $ Let False body.name ebox.term ebody loc
Erased => do
body' <- eraseTerm ctx' bty body.term
body' <- eraseTerm defs ctx' bty body.term
pure $ EraRes (sub1 ret box) $ body' // one (Erased loc)
-- f ⤋ f' ⇒ Eq (𝑖 ⇒ A) l r
-- ------------------------------
-- f @r ⤋ f' ⇒ A‹r/𝑖›
eraseElim ctx (DApp fun arg loc) = do
efun <- eraseElim ctx fun
a <- fst <$> wrapExpect `(expectEq) ctx loc efun.type
eraseElim defs ctx (DApp fun arg loc) = do
efun <- eraseElim defs ctx fun
a <- fst <$> wrapExpect `(expectEq) defs ctx loc efun.type
pure $ EraRes (dsub1 a arg) efun.term
-- s ⤋ s' ⇐ A
-- ----------------
-- s ∷ A ⤋ s' ⇒ A
eraseElim ctx (Ann tm ty loc) =
EraRes ty <$> eraseTerm ctx ty tm
eraseElim defs ctx (Ann tm ty loc) =
EraRes ty <$> eraseTerm defs ctx ty tm
-- s ⤋ s' ⇐ A‹p/𝑖›
-- -----------------------------------
-- coe (𝑖 ⇒ A) @p @q s ⤋ s' ⇒ A‹q/𝑖›
eraseElim ctx (Coe ty p q val loc) = do
val <- eraseTerm ctx (dsub1 ty p) val
eraseElim defs ctx (Coe ty p q val loc) = do
val <- eraseTerm defs ctx (dsub1 ty p) val
pure $ EraRes (dsub1 ty q) val
-- s ⤋ s' ⇐ A
-- --------------------------------
-- comp A @p @q s @r {⋯} ⤋ s' ⇒ A
eraseElim ctx (Comp ty p q val r zero one loc) =
EraRes ty <$> eraseTerm ctx ty val
eraseElim defs ctx (Comp ty p q val r zero one loc) =
EraRes ty <$> eraseTerm defs ctx ty val
eraseElim ctx t@(TypeCase ty ret arms def loc) =
eraseElim defs ctx t@(TypeCase ty ret arms def loc) =
throw $ CompileTimeOnly ctx $ E t
eraseElim ctx (CloE (Sub term th)) =
eraseElim ctx $ pushSubstsWith' id th term
eraseElim defs ctx (CloE (Sub term th)) =
eraseElim defs ctx $ pushSubstsWith' id th term
eraseElim ctx (DCloE (Sub term th)) =
eraseElim ctx $ pushSubstsWith' th id term
eraseElim defs ctx (DCloE (Sub term th)) =
eraseElim defs ctx $ pushSubstsWith' th id term
export
@ -476,7 +487,7 @@ uses i (CaseNat nat zer suc _) = uses i nat + max (uses i zer) (uses' suc)
uses' (NSRec _ _ s) = uses (VS (VS i)) s
uses' (NSNonrec _ s) = uses (VS i) s
uses i (Str {}) = 0
uses i (Let x rhs body _) = uses i rhs + uses (VS i) body
uses i (Let _ x rhs body _) = uses i rhs + uses (VS i) body
uses i (Erased {}) = 0
export
@ -528,19 +539,21 @@ trimLets (CaseNat nat zer suc loc) =
trimLets' (NSRec x ih s) = NSRec x ih $ trimLets s
trimLets' (NSNonrec x s) = NSNonrec x $ trimLets s
trimLets (Str s loc) = Str s loc
trimLets (Let x rhs body loc) =
trimLets (Let True x rhs body loc) =
Let True x (trimLets rhs) (trimLets body) loc
trimLets (Let False x rhs body loc) =
let rhs' = trimLets rhs
body' = trimLets body
uses = uses VZ body in
if inlineable rhs' || uses == 1 || (droppable rhs' && uses == 0)
then sub1 rhs' body'
else Let x rhs' body' loc
else Let False x rhs' body' loc
trimLets (Erased loc) = Erased loc
export covering
eraseDef : Name -> Q.Definition -> Eff Erase U.Definition
eraseDef name def@(MkDef qty type body scheme isMain loc) =
eraseDef : Q.Definitions -> Name -> Q.Definition -> Eff Erase U.Definition
eraseDef defs name def@(MkDef qty type body scheme isMain loc) =
wrapErr (WhileErasing name def) $
case isErased qty.qty of
Erased => do
@ -552,4 +565,4 @@ eraseDef name def@(MkDef qty type body scheme isMain loc) =
Nothing => case body of
Postulate => throw $ Postulate loc name
Concrete body => KeptDef isMain . trimLets <$>
eraseTerm empty type body
eraseTerm defs empty type body

2
lib/Quox/Untyped/Scheme.idr
View File

@ -225,7 +225,7 @@ toScheme xs (CaseNat nat zer (NSNonrec p suc) _) =
Lambda [p] !(toScheme (xs :< p) suc),
!(toScheme xs nat)]
toScheme xs (Let x rhs body _) =
toScheme xs (Let _ x rhs body _) =
freshInB x $ \x =>
pure $ Let x !(toScheme xs rhs) !(toScheme (xs :< x) body)

64
lib/Quox/Untyped/Syntax.idr
View File

@ -41,16 +41,14 @@ data Term where
Nat : (val : Nat) -> Loc -> Term n
Succ : (nat : Term n) -> Loc -> Term n
CaseNat : (nat : Term n) ->
(zer : Term n) ->
(suc : CaseNatSuc n) ->
Loc ->
Term n
CaseNat : (nat : Term n) -> (zer : Term n) -> (suc : CaseNatSuc n) ->
Loc -> Term n
Str : (str : String) -> Loc -> Term n
Let : (x : BindName) -> (rhs : Term n) -> (body : Term (S n)) -> Loc ->
Term n
||| bool is true if the let comes from the original source code
Let : (real : Bool) -> (x : BindName) -> (rhs : Term n) ->
(body : Term (S n)) -> Loc -> Term n
Erased : Loc -> Term n
%name Term s, t, u
@ -80,7 +78,7 @@ Located (Term n) where
(Succ _ loc).loc = loc
(CaseNat _ _ _ loc).loc = loc
(Str _ loc).loc = loc
(Let _ _ _ loc).loc = loc
(Let _ _ _ _ loc).loc = loc
(Erased loc).loc = loc
@ -105,25 +103,17 @@ prettyArg : {opts : LayoutOpts} -> BContext n -> Term n -> Eff Pretty (Doc opts)
prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
export covering
prettyAppHead : {opts : LayoutOpts} -> BContext n ->
Term n -> Eff Pretty (Doc opts)
prettyAppHead xs fun = withPrec App $ prettyTerm xs fun
prettyApp_ : {opts : LayoutOpts} -> BContext n ->
Doc opts -> SnocList (Term n) -> Eff Pretty (Doc opts)
prettyApp_ xs fun args =
parensIfM App =<<
prettyAppD fun (toList !(traverse (prettyArg xs) args))
export
prettyApp' : {opts : LayoutOpts} ->
Doc opts -> SnocList (Doc opts) -> Eff Pretty (Doc opts)
prettyApp' fun args = do
d <- askAt INDENT
let args = toList args
parensIfM App $
hsep (fun :: args)
<|> hsep [fun, vsep args]
<|> vsep (fun :: map (indent d) args)
export covering
export covering %inline
prettyApp : {opts : LayoutOpts} -> BContext n ->
Doc opts -> SnocList (Term n) -> Eff Pretty (Doc opts)
prettyApp xs fun args = prettyApp' fun =<< traverse (prettyArg xs) args
Term n -> SnocList (Term n) -> Eff Pretty (Doc opts)
prettyApp xs fun args =
prettyApp_ xs !(prettyArg xs fun) args
public export
record PrettyCaseArm a n where
@ -173,8 +163,8 @@ splitLam ys t = Evidence _ (ys, t)
export
splitLet : Telescope (\i => (BindName, Term i)) a b -> Term b ->
Exists $ \c => (Telescope (\i => (BindName, Term i)) a c, Term c)
splitLet ys (Let x rhs body _) = splitLet (ys :< (x, rhs)) body
splitLet ys t = Evidence _ (ys, t)
splitLet ys (Let _ x rhs body _) = splitLet (ys :< (x, rhs)) body
splitLet ys t = Evidence _ (ys, t)
private covering
prettyLets : {opts : LayoutOpts} ->
@ -208,26 +198,26 @@ prettyTerm xs (Lam x body _) =
vars <- hsep . toList' <$> traverse prettyTBind ys
body <- withPrec Outer $ prettyTerm (xs . ys) body
hangDSingle (hsep [!lamD, vars, !darrowD]) body
prettyTerm xs (App fun arg _) =
let (fun, args) = splitApp fun in
prettyApp xs !(prettyAppHead xs fun) (args :< arg)
prettyTerm xs (App fun arg _) = do
let (fun, args) = splitApp fun
prettyApp xs fun (args :< arg)
prettyTerm xs (Pair fst snd _) =
parens . separateTight !commaD =<<
traverse (withPrec Outer . prettyTerm xs) (fst :: splitPair snd)
prettyTerm xs (Fst pair _) = prettyApp xs !fstD [< pair]
prettyTerm xs (Snd pair _) = prettyApp xs !sndD [< pair]
prettyTerm xs (Fst pair _) = prettyApp_ xs !fstD [< pair]
prettyTerm xs (Snd pair _) = prettyApp_ xs !sndD [< pair]
prettyTerm xs (Tag tag _) = prettyTag tag
prettyTerm xs (CaseEnum tag cases _) =
prettyCase xs prettyTag tag $
map (\(t, rhs) => MkPrettyCaseArm t [] rhs) $ toList cases
prettyTerm xs (Absurd _) = hl Syntax "absurd"
prettyTerm xs (Nat n _) = hl Constant $ pshow n
prettyTerm xs (Succ nat _) = prettyApp xs !succD [< nat]
prettyTerm xs (Succ nat _) = prettyApp_ xs !succD [< nat]
prettyTerm xs (CaseNat nat zer suc _) =
prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
prettyTerm xs (Str s _) =
prettyStrLit s
prettyTerm xs (Let x rhs body _) =
prettyTerm xs (Let _ x rhs body _) =
parensIfM Outer =<< do
let Evidence n' (lets, body) = splitLet [< (x, rhs)] body
heads <- prettyLets xs lets
@ -235,7 +225,7 @@ prettyTerm xs (Let x rhs body _) =
let lines = toList $ heads :< body
pure $ ifMultiline (hsep lines) (vsep lines)
prettyTerm _ (Erased _) =
hl Syntax =<< ifUnicode "⌷" "[]"
hl Syntax =<< ifUnicode "□" "[]"
export covering
prettyDef : {opts : LayoutOpts} -> Name ->
@ -296,8 +286,8 @@ CanSubstSelf Term where
(assert_total substSuc suc th) loc
Str s loc =>
Str s loc
Let x rhs body loc =>
Let x (rhs // th) (assert_total $ body // push th) loc
Let u x rhs body loc =>
Let u x (rhs // th) (assert_total $ body // push th) loc
Erased loc =>
Erased loc
where

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

@ -28,7 +28,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
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 sg))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx 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›)
@ -49,7 +49,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
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 sg))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx 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 }
-- ⇝
@ -74,7 +74,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| 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))
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
fstCoe sty@(S [< i] ty) p q val loc = do
-- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s)
-- ⇝
@ -91,7 +91,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| 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))
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
sndCoe sty@(S [< i] ty) p q val loc = do
-- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s)
-- ⇝
@ -115,7 +115,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
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 sg))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
eqCoe sty@(S [< j] ty) p q val r loc = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
-- ⇝
@ -133,7 +133,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
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 sg))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx 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 }
-- ⇝
@ -151,7 +151,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
pushCoe : BindName ->
(ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
(0 pc : So (canPushCoe sg ty s)) =>
Eff Whnf (NonRedex Elim d n defs sg)
Eff Whnf (NonRedex Elim d n defs ctx sg)
pushCoe i ty p q s loc =
case ty of
-- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)

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

@ -14,8 +14,8 @@ export covering
computeElimType :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
(defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term d n)
@ -24,8 +24,8 @@ export covering
computeWhnfElimType0 :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
(defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term d n)
computeElimType defs ctx sg e =
@ -36,7 +36,7 @@ computeElimType defs ctx sg e =
pure $ def.typeWithAt ctx.dimLen ctx.termLen u
B i _ =>
pure $ ctx.tctx !! i
pure (ctx.tctx !! i).type
App f s loc =>
case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of

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

@ -18,13 +18,14 @@ Whnf = [Except Error, NameGen]
public export
0 RedexTest : TermLike -> Type
RedexTest tm = {0 d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
RedexTest tm =
{0 d, n : Nat} -> Definitions -> WhnfContext d n -> SQty -> tm d n -> Bool
public export
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs q))
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
-- having isRedex be part of the class header, and needing to be explicitly
-- quantified on every use since idris can't infer its type, is a little ugly.
-- but none of the alternatives i've thought of so far work. e.g. in some
@ -37,19 +38,20 @@ whnf0 defs ctx q t = fst <$> whnf defs ctx q t
public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> SQty -> Pred (tm d n)
IsRedex defs q = So . isRedex defs q
NotRedex defs q = No . isRedex defs q
Definitions -> WhnfContext d n -> SQty -> Pred (tm d n)
IsRedex defs ctx q = So . isRedex defs ctx q
NotRedex defs ctx q = No . isRedex defs ctx q
public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
CanWhnf tm isRedex => (d, n : Nat) ->
(defs : Definitions) -> SQty -> Type
NonRedex tm d n defs q = Subset (tm d n) (NotRedex defs q)
Definitions -> WhnfContext d n -> SQty -> Type
NonRedex tm d n defs ctx q = Subset (tm d n) (NotRedex defs ctx q)
public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs q t) => NonRedex tm d n defs q
(t : tm d n) -> (0 nr : NotRedex defs ctx q t) =>
NonRedex tm d n defs ctx q
nred t = Element t nr
@ -193,50 +195,52 @@ mutual
||| a reducible elimination
|||
||| 1. a free variable, if its definition is known
||| 2. an elimination whose head is reducible
||| 3. an "active" elimination:
||| 2. a bound variable pointing to a `let`
||| 3. an elimination whose head is reducible
||| 4. an "active" elimination:
||| 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 @q s` where:
||| 5. a redundant annotation, or one whose term or type is reducible
||| 6. 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 {⋯}`
||| 7. a composition `comp A @p @q s @r {⋯}`
||| where `p = q`, `r = 0`, or `r = 1`
||| 7. a closure
||| 8. a closure
public export
isRedexE : RedexTest Elim
isRedexE defs sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
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, _}) =
isRedexE defs ctx sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
isRedexE _ ctx sg (B {i, _}) = isJust (ctx.tctx !! i).term
isRedexE defs ctx sg (App {fun, _}) =
isRedexE defs ctx sg fun || isLamHead fun
isRedexE defs ctx sg (CasePair {pair, _}) =
isRedexE defs ctx sg pair || isPairHead pair || isYes (sg `decEq` SZero)
isRedexE defs ctx sg (Fst pair _) =
isRedexE defs ctx sg pair || isPairHead pair
isRedexE defs ctx sg (Snd pair _) =
isRedexE defs ctx sg pair || isPairHead pair
isRedexE defs ctx sg (CaseEnum {tag, _}) =
isRedexE defs ctx sg tag || isTagHead tag
isRedexE defs ctx sg (CaseNat {nat, _}) =
isRedexE defs ctx sg nat || isNatHead nat
isRedexE defs ctx sg (CaseBox {box, _}) =
isRedexE defs ctx sg box || isBoxHead box
isRedexE defs ctx sg (DApp {fun, arg, _}) =
isRedexE defs ctx sg fun || isDLamHead fun || isK arg
isRedexE defs ctx sg (Ann {tm, ty, _}) =
isE tm || isRedexT defs ctx sg tm || isRedexT defs ctx SZero ty
isRedexE defs ctx sg (Coe {ty = S _ (N _), _}) = True
isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, q, val, _}) =
isRedexT defs (extendDim i ctx) SZero ty ||
canPushCoe sg ty val || isYes (p `decEqv` q)
isRedexE defs ctx sg (Comp {ty, p, q, r, _}) =
isYes (p `decEqv` q) || isK r
isRedexE defs sg (TypeCase {ty, ret, _}) =
isRedexE defs sg ty || isRedexT defs sg ret || isAnnTyCon ty
isRedexE _ _ (CloE {}) = True
isRedexE _ _ (DCloE {}) = True
isRedexE defs ctx sg (TypeCase {ty, ret, _}) =
isRedexE defs ctx sg ty || isRedexT defs ctx sg ret || isAnnTyCon ty
isRedexE _ _ _ (CloE {}) = True
isRedexE _ _ _ (DCloE {}) = True
||| a reducible term
|||
@ -248,9 +252,9 @@ mutual
||| 5. a `let` expression
public export
isRedexT : RedexTest Term
isRedexT _ _ (CloT {}) = True
isRedexT _ _ (DCloT {}) = True
isRedexT _ _ (Let {}) = True
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
isRedexT _ _ (Succ p {}) = isNatConst p
isRedexT _ _ _ = False
isRedexT _ _ _ (CloT {}) = True
isRedexT _ _ _ (DCloT {}) = True
isRedexT _ _ _ (Let {}) = True
isRedexT defs ctx sg (E {e, _}) = isAnn e || isRedexE defs ctx sg e
isRedexT _ _ _ (Succ p {}) = isNatConst p
isRedexT _ _ _ _ = False

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

@ -20,7 +20,10 @@ CanWhnf Elim Interface.isRedexE where
_ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
whnf _ _ _ (B i loc) = pure $ nred $ B i loc
whnf defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
_ | l with (l.term) proof eq2
_ | Just y = whnf defs ctx sg $ Ann y l.type loc
_ | Nothing = pure $ Element (B i loc) $ rewrite eq1 in rewrite eq2 in Ah
-- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
whnf defs ctx sg (App f s appLoc) = do

10
lib/Quox/Whnf/TypeCase.idr
View File

@ -35,7 +35,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
export covering
tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n, ScopeTerm d n)
tycasePi (Pi {arg, res, _}) = pure (arg, res)
tycasePi (E e) {tnf} = do
@ -53,7 +53,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
export covering
tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n, ScopeTerm d n)
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
tycaseSig (E e) {tnf} = do
@ -71,7 +71,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns a type-case that will reduce to that;
||| for other intro forms error
export covering
tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n)
tycaseBOX (BOX {ty, _}) = pure ty
tycaseBOX (E e) {tnf} = do
@ -83,7 +83,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns five type-cases that will reduce to that;
||| for other intro forms error
export covering
tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs SZero t)) =>
tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
tycaseEq (E e) {tnf} = do
@ -107,7 +107,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
reduceTypeCase : (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
(arms : TypeCaseArms d n) -> (def : Term d n) ->
(0 _ : So (isTyCon ty)) => Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs SZero))
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx SZero))
reduceTypeCase ty u ret arms def loc = case ty of
-- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
TYPE {} =>

8
tests/AstExtra.idr
View File

@ -24,13 +24,17 @@ anys : {n : Nat} -> QContext n
anys {n = 0} = [<]
anys {n = S n} = anys :< Any
public export
locals : Context (Term d) n -> Context (LocalVar d) n
locals = map $ \t => MkLocal t Nothing
public export
ctx, ctx01 : {n : Nat} -> Context (\n => (BindName, Term 0 n)) n ->
TyContext 0 n
ctx tel = let (ns, ts) = unzip tel in
MkTyContext new [<] ts ns anys
MkTyContext new [<] (locals ts) ns anys
ctx01 tel = let (ns, ts) = unzip tel in
MkTyContext ZeroIsOne [<] ts ns anys
MkTyContext ZeroIsOne [<] (locals ts) ns anys
export
mkDef : GQty -> Term 0 0 -> Term 0 0 -> Definition

2
tests/Tests/Parser.idr
View File

@ -422,6 +422,8 @@ tests = "parser" :- [
`(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "letω x = y in z"
`(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "letω x : X = y in z"
`(Let (PQ Any _, PV "x" {}, Ann (V "y" {}) (V "X" {}) _) (V "z" {}) _),
parseMatch term "let ω.x = y in z"
`(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
parseMatch term "let x = y1 y2 in z1 z2"

2
tests/Tests/Reduce.idr
View File

@ -33,7 +33,7 @@ parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
private
ctx : {n : Nat} -> Context (\n => (BindName, Term 0 n)) n -> WhnfContext 0 n
ctx xs = let (ns, ts) = unzip xs in MkWhnfContext [<] ns ts
ctx xs = let (ns, ts) = unzip xs in MkWhnfContext [<] ns (locals ts)
export