wip
This commit is contained in:
parent
0987b91596
commit
3dc516e5b4
|
@ -18,8 +18,13 @@ def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B =
|
|||
|
||||
def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False;
|
||||
|
||||
def boolω : Bool → [ω.Bool] =
|
||||
λ b ⇒ if [ω.Bool] b ['true] ['false];
|
||||
def dup! : (b : Bool) → [ω. Sing Bool b] =
|
||||
λ b ⇒ if-dep (λ b ⇒ [ω. Sing Bool b]) b
|
||||
[('true, [δ _ ⇒ 'true])]
|
||||
[('false, [δ _ ⇒ 'false])];
|
||||
|
||||
def dup : Bool → [ω. Bool] =
|
||||
λ b ⇒ appω (Sing Bool b) Bool (sing.val Bool b) (dup! b);
|
||||
|
||||
def true-not-false : Not ('true ≡ 'false : Bool) =
|
||||
λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true;
|
||||
|
|
|
@ -146,11 +146,11 @@ private
|
|||
liftFromParser : Eff FromParserIO a -> Eff CompileStop a
|
||||
liftFromParser act =
|
||||
runEff act $ with Union.(::)
|
||||
[\g => send g,
|
||||
handleExcept (\err => throw $ FromParserError err),
|
||||
[handleExcept (\err => throw $ FromParserError err),
|
||||
handleStateIORef !(asksAt STATE defs),
|
||||
handleStateIORef !(asksAt STATE ns),
|
||||
handleStateIORef !(asksAt STATE suf)]
|
||||
handleStateIORef !(asksAt STATE suf),
|
||||
\g => send g]
|
||||
|
||||
private
|
||||
liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
|
||||
|
|
|
@ -114,4 +114,4 @@ prettyDef name (MkDef qty type _ _) = withPrec Outer $ do
|
|||
name <- prettyFree name
|
||||
colon <- colonD
|
||||
type <- prettyTerm [<] [<] type
|
||||
pure $ sep [hsep [hcat [qty, dot, name], colon], type]
|
||||
hangDSingle (hsep [hcat [qty, dot, name], colon]) type
|
||||
|
|
|
@ -41,7 +41,7 @@ FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen]
|
|||
|
||||
public export
|
||||
FromParserIO : List (Type -> Type)
|
||||
FromParserIO = LoadFile :: FromParserPure
|
||||
FromParserIO = FromParserPure ++ [LoadFile]
|
||||
|
||||
|
||||
export
|
||||
|
@ -66,11 +66,11 @@ fromParserIO : (MonadRec io, HasIO io) =>
|
|||
Eff FromParserIO a -> io (Either Error a)
|
||||
fromParserIO inc seen suf defs act =
|
||||
liftIO $ fromIOErr $ runEff act $ with Union.(::)
|
||||
[handleLoadFileIOE LoadError WrapParseError seen inc,
|
||||
handleExcept (\e => ioLeft e),
|
||||
[handleExcept (\e => ioLeft e),
|
||||
handleStateIORef defs,
|
||||
handleStateIORef !(newIORef [<]),
|
||||
handleStateIORef suf]
|
||||
handleStateIORef suf,
|
||||
handleLoadFileIOE LoadError WrapParseError seen inc]
|
||||
|
||||
|
||||
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
|
||||
|
|
|
@ -191,6 +191,14 @@ parameters {opts : LayoutOpts} {auto _ : Foldable t}
|
|||
separateTight : Doc opts -> t (Doc opts) -> Doc opts
|
||||
separateTight d = sep . exceptLast (<+> d) . toList
|
||||
|
||||
export
|
||||
hseparateTight : Doc opts -> t (Doc opts) -> Doc opts
|
||||
hseparateTight d = hsep . exceptLast (<+> d) . toList
|
||||
|
||||
export
|
||||
vseparateTight : Doc opts -> t (Doc opts) -> Doc opts
|
||||
vseparateTight d = vsep . exceptLast (<+> d) . toList
|
||||
|
||||
export
|
||||
fillSeparateTight : Doc opts -> t (Doc opts) -> Doc opts
|
||||
fillSeparateTight d = fillSep . exceptLast (<+> d) . toList
|
||||
|
|
|
@ -251,12 +251,11 @@ parameters {opts : LayoutOpts} (dnames : BContext d) (tnames : BContext n)
|
|||
body <- withPrec Outer $ assert_total
|
||||
prettyTerm (dnames . dbinds) (tnames . tbinds) body
|
||||
header <- (pat <++>) <$> darrowD
|
||||
pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
|
||||
pure $ ifMultiline (header <++> body) (vsep [header, !(indentD body)])
|
||||
|
||||
private
|
||||
prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (Doc opts)
|
||||
prettyCaseBody xs =
|
||||
braces . separateTight !semiD =<< traverse prettyCaseArm xs
|
||||
prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (List (Doc opts))
|
||||
prettyCaseBody xs = traverse prettyCaseArm xs
|
||||
|
||||
private
|
||||
prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts)
|
||||
|
@ -278,9 +277,7 @@ layoutComp typq val r arms = do
|
|||
pure $ ifMultiline
|
||||
(hsep $ concat {t = List} [[comp], typq, [val, r, lb], arms, [rb]]) $
|
||||
(comp <++>
|
||||
vsep [sep typq, val, r <++> lb, indent ind $ vsep arms, rb]) <|>
|
||||
(vsep $ (comp ::) $ map (indent ind) $ concat {t = List}
|
||||
[typq, [val, r <++> lb], map (indent ind) arms, [rb]])
|
||||
vsep [sep typq, val, r <++> lb, indent ind $ vsep arms, rb])
|
||||
|
||||
|
||||
export
|
||||
|
@ -299,7 +296,7 @@ prettyCaseRet dnames tnames body = withPrec Outer $ case body of
|
|||
S [< x] (Y tm) => do
|
||||
header <- [|prettyTBind x <++> darrowD|]
|
||||
body <- assert_total prettyTerm dnames (tnames :< x) tm
|
||||
pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
|
||||
hangDSingle header body
|
||||
|
||||
private
|
||||
prettyCase_ : {opts : _} ->
|
||||
|
@ -309,8 +306,14 @@ prettyCase_ : {opts : _} ->
|
|||
prettyCase_ dnames tnames intro head ret body = do
|
||||
head <- assert_total prettyElim dnames tnames head
|
||||
ret <- prettyCaseRet dnames tnames ret
|
||||
body <- prettyCaseBody dnames tnames body
|
||||
parensIfM Outer $ sep [intro <++> head, !returnD <++> ret, !ofD <++> body]
|
||||
bodys <- prettyCaseBody dnames tnames body
|
||||
return <- returnD; of_ <- ofD
|
||||
lb <- hl Delim "{"; rb <- hl Delim "}"; semi <- semiD
|
||||
ind <- askAt INDENT
|
||||
parensIfM Outer $ ifMultiline
|
||||
(hsep [intro, head, return, ret, of_, lb, hseparateTight semi bodys, rb])
|
||||
(vsep [intro <++> head, return <++> ret, of_ <++> lb,
|
||||
indent ind $ vseparateTight semi bodys, rb])
|
||||
|
||||
private
|
||||
prettyCase : {opts : _} ->
|
||||
|
|
|
@ -144,18 +144,20 @@ eraseTerm ctx _ s@(TYPE {}) =
|
|||
eraseTerm ctx _ s@(Pi {}) =
|
||||
throw $ CompileTimeOnly ctx s
|
||||
|
||||
-- x : A | π.x ⊢ s ⤋ s' ⇐ B
|
||||
-- x : A | 0.x ⊢ s ⤋ s' ⇐ B
|
||||
-- -------------------------------------
|
||||
-- (λ x ⇒ s) ⤋ s'[⌷/x] ⇐ 0.(x : A) → B
|
||||
--
|
||||
-- x : A | π.x ⊢ s ⤋ s' ⇐ B π ≠ 0
|
||||
-- ----------------------------------------
|
||||
-- (λ x ⇒ s) ⤋ (λ x ⇒ s') ⇐ π.(x : A) → B
|
||||
--
|
||||
-- becomes a lambda even when π = 0,
|
||||
-- to preserve expected evaluation order
|
||||
eraseTerm ctx ty (Lam body loc) = do
|
||||
let x = body.name
|
||||
(qty, arg, res) <- wrapExpect `(expectPi) ctx loc ty
|
||||
let x = case isErased qty of Kept => body.name
|
||||
Erased => BN Unused body.name.loc
|
||||
body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
|
||||
pure $ U.Lam x body loc
|
||||
pure $ case isErased qty of
|
||||
Kept => U.Lam x body loc
|
||||
Erased => sub1 (Erased loc) body
|
||||
|
||||
eraseTerm ctx _ s@(Sig {}) =
|
||||
throw $ CompileTimeOnly ctx s
|
||||
|
@ -251,13 +253,13 @@ eraseElim ctx e@(B i loc) = do
|
|||
--
|
||||
-- f ⤋ f' ⇒ 0.(x : A) → B
|
||||
-- -------------------------
|
||||
-- f s ⤋ f' ⌷ ⇒ B[s/x]
|
||||
-- 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
|
||||
let ty = sub1 tres (Ann arg targ arg.loc)
|
||||
case isErased qty of
|
||||
Erased => pure $ EraRes ty $ App efun.term (Erased arg.loc) loc
|
||||
Erased => pure $ EraRes ty efun.term
|
||||
Kept => do arg <- eraseTerm ctx targ arg
|
||||
pure $ EraRes ty $ App efun.term arg loc
|
||||
|
||||
|
@ -322,24 +324,33 @@ eraseElim ctx e@(CaseEnum qty tag ret arms loc) =
|
|||
pure (t, rhs')
|
||||
pure $ EraRes ty $ CaseEnum etag.term arms loc
|
||||
|
||||
-- n ⤋ n' ⇒ ℕ z ⤋ z' ⇐ R[zero∷ℕ/z]
|
||||
-- n ⤋ n' ⇒ ℕ z ⤋ z' ⇐ R[zero∷ℕ/z] ς ≠ 0
|
||||
-- m : ℕ, ih : R[m/z] | ρ.m, ς.ih ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
|
||||
-- -----------------------------------------------------------
|
||||
-- caseρ n return z ⇒ R of {0 ⇒ z; succ m, ς.ih ⇒ s}
|
||||
-- ⤋
|
||||
-- case n' of {0 ⇒ z'; succ m, ih ⇒ s'}
|
||||
-- ⇒ R[n/z]
|
||||
-- case n' of {0 ⇒ z'; succ m, ih ⇒ s'} ⇒ R[n/z]
|
||||
--
|
||||
-- n ⤋ n' ⇒ ℕ z ⤋ z' ⇐ R[zero∷ℕ/z]
|
||||
-- m : ℕ, ih : R[m/z] | ρ.m, 0.ih ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
|
||||
-- -----------------------------------------------------------
|
||||
-- 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
|
||||
let ty = sub1 ret nat
|
||||
enat <- eraseElim ctx nat
|
||||
zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (Nat loc) loc)) zero
|
||||
let [< p, ih] = succ.names
|
||||
succ <- eraseTerm
|
||||
succ' <- eraseTerm
|
||||
(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))
|
||||
succ.term
|
||||
pure $ EraRes ty $ CaseNat enat.term zero p ih succ loc
|
||||
let succ = case isErased qtyIH of
|
||||
Kept => NSRec p ih succ'
|
||||
Erased => NSNonrec p (sub1 (Erased loc) succ')
|
||||
pure $ EraRes ty $ CaseNat enat.term zero succ loc
|
||||
|
||||
-- b ⤋ b' ⇒ [π.A] π ≠ 0
|
||||
-- x : A | πρ.x ⊢ s ⤋ s' ⇐ R[[x]∷[π.A]/z]
|
||||
|
|
|
@ -18,7 +18,12 @@ import Derive.Prelude
|
|||
|
||||
|
||||
public export
|
||||
data Term : Nat -> Type where
|
||||
data Term : Nat -> Type
|
||||
|
||||
public export
|
||||
data CaseNatSuc : Nat -> Type
|
||||
|
||||
data Term where
|
||||
F : (x : Name) -> Loc -> Term n
|
||||
B : (i : Var n) -> Loc -> Term n
|
||||
|
||||
|
@ -38,13 +43,20 @@ data Term : Nat -> Type where
|
|||
Succ : (nat : Term n) -> Loc -> Term n
|
||||
CaseNat : (nat : Term n) ->
|
||||
(zer : Term n) ->
|
||||
(x, ih : BindName) -> (suc : Term (2 + n)) ->
|
||||
(suc : CaseNatSuc n) ->
|
||||
Loc ->
|
||||
Term n
|
||||
|
||||
Erased : Loc -> Term n
|
||||
%name Term s, t, u
|
||||
%runElab deriveIndexed "Term" [Eq, Ord, Show]
|
||||
|
||||
data CaseNatSuc where
|
||||
NSRec : (x, ih : BindName) -> Term (2 + n) -> CaseNatSuc n
|
||||
NSNonrec : (x : BindName) -> Term (S n) -> CaseNatSuc n
|
||||
%name CaseNatSuc suc
|
||||
|
||||
%runElab deriveParam $
|
||||
map (\ty => PI ty allIndices [Eq, Ord, Show]) ["Term", "CaseNatSuc"]
|
||||
|
||||
|
||||
export
|
||||
|
@ -61,7 +73,7 @@ Located (Term n) where
|
|||
(Absurd loc).loc = loc
|
||||
(Zero loc).loc = loc
|
||||
(Succ nat loc).loc = loc
|
||||
(CaseNat nat zer x ih suc loc).loc = loc
|
||||
(CaseNat nat zer suc loc).loc = loc
|
||||
(Erased loc).loc = loc
|
||||
|
||||
|
||||
|
@ -120,6 +132,18 @@ prettyCase xs f head arms =
|
|||
(hsep [header, lb, separateTight sc cases, rb])
|
||||
(vsep [hsep [header, lb], indent d $ vsep (map (<+> sc) cases), rb])
|
||||
|
||||
private
|
||||
sucPat : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts)
|
||||
sucPat x = pure $ !succD <++> !(prettyTBind x)
|
||||
|
||||
private
|
||||
sucCaseArm : {opts : LayoutOpts} ->
|
||||
CaseNatSuc n -> Eff Pretty (PrettyCaseArm (Doc opts) n)
|
||||
sucCaseArm (NSRec x ih s) = pure $
|
||||
MkPrettyCaseArm (!(sucPat x) <+> !commaD <++> !(prettyTBind ih)) [x, ih] s
|
||||
sucCaseArm (NSNonrec x s) = pure $
|
||||
MkPrettyCaseArm !(sucPat x) [x] s
|
||||
|
||||
prettyTerm _ (F x _) = prettyFree x
|
||||
prettyTerm xs (B i _) = prettyTBind $ xs !!! i
|
||||
prettyTerm xs (Lam x body _) =
|
||||
|
@ -141,14 +165,9 @@ prettyTerm xs (CaseEnum tag cases _) =
|
|||
prettyTerm xs (Absurd _) = hl Syntax "absurd"
|
||||
prettyTerm xs (Zero _) = zeroD
|
||||
prettyTerm xs (Succ nat _) = prettyApp' xs !succD nat
|
||||
prettyTerm xs (CaseNat nat zer x ih suc _) =
|
||||
prettyTerm xs (CaseNat nat zer suc _) =
|
||||
assert_total
|
||||
prettyCase xs pure nat
|
||||
[MkPrettyCaseArm !zeroD [] zer,
|
||||
MkPrettyCaseArm !sucPat [x, ih] suc]
|
||||
where
|
||||
sucPat = pure $
|
||||
hsep [!succD, !(prettyTBind x) <+> !commaD, !(prettyTBind ih)]
|
||||
prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
|
||||
prettyTerm _ (Erased _) =
|
||||
hl Syntax =<< ifUnicode "⌷" "[]"
|
||||
|
||||
|
@ -198,11 +217,16 @@ CanSubstSelf Term where
|
|||
Zero loc
|
||||
Succ nat loc =>
|
||||
Succ (nat // th) loc
|
||||
CaseNat nat zer x ih suc loc =>
|
||||
CaseNat nat zer suc loc =>
|
||||
CaseNat (nat // th) (zer // th)
|
||||
x ih (assert_total $ suc // pushN 2 th) loc
|
||||
(assert_total substSuc suc th) loc
|
||||
Erased loc =>
|
||||
Erased loc
|
||||
where
|
||||
substSuc : forall from, to.
|
||||
CaseNatSuc from -> USubst from to -> CaseNatSuc to
|
||||
substSuc (NSRec x ih t) th = NSRec x ih $ t // pushN 2 th
|
||||
substSuc (NSNonrec x t) th = NSNonrec x $ t // push th
|
||||
|
||||
public export
|
||||
subN : SnocVect s (Term n) -> Term (s + n) -> Term n
|
||||
|
|
Loading…
Reference in New Issue