From 3dc516e5b46119eafd172ac51e0a7d9465ac76f7 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 22 Oct 2023 19:17:29 +0200 Subject: [PATCH] wip --- examples/bool.quox | 9 +++- exe/Main.idr | 6 +-- lib/Quox/Definition.idr | 2 +- lib/Quox/Parser/FromParser.idr | 8 ++-- lib/Quox/Pretty.idr | 8 ++++ lib/Quox/Syntax/Term/Pretty.idr | 27 ++++++------ lib/Quox/Untyped/Erase.idr | 41 +++++++++++------- lib/Quox/Untyped/Syntax.idr | 76 ++++++++++++++++++++++----------- 8 files changed, 114 insertions(+), 63 deletions(-) diff --git a/examples/bool.quox b/examples/bool.quox index 055e28f..a6f8140 100644 --- a/examples/bool.quox +++ b/examples/bool.quox @@ -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; diff --git a/exe/Main.idr b/exe/Main.idr index dbb7897..be03398 100644 --- a/exe/Main.idr +++ b/exe/Main.idr @@ -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 diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index 8bd2fa9..4842c29 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -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 diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index f34a3d7..84eaed9 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -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) diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index 4753d76..73357ee 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -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 diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 691cfd6..a8db924 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -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 : _} -> @@ -307,10 +304,16 @@ prettyCase_ : {opts : _} -> Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) -> Eff Pretty (Doc 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] + head <- assert_total prettyElim dnames tnames head + ret <- prettyCaseRet dnames tnames ret + 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 : _} -> diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr index 8118920..a79e297 100644 --- a/lib/Quox/Untyped/Erase.idr +++ b/lib/Quox/Untyped/Erase.idr @@ -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 + body <- eraseTerm (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 {}) = 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] diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr index e4f67e4..36bbedd 100644 --- a/lib/Quox/Untyped/Syntax.idr +++ b/lib/Quox/Untyped/Syntax.idr @@ -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,31 +43,38 @@ 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 Located (Term n) where - (F x loc).loc = loc - (B i loc).loc = loc - (Lam x body loc).loc = loc - (App fun arg loc).loc = loc - (Pair fst snd loc).loc = loc - (Fst pair loc).loc = loc - (Snd pair loc).loc = loc - (Tag tag loc).loc = loc - (CaseEnum tag cases loc).loc = loc - (Absurd loc).loc = loc - (Zero loc).loc = loc - (Succ nat loc).loc = loc - (CaseNat nat zer x ih suc loc).loc = loc - (Erased loc).loc = loc + (F x loc).loc = loc + (B i loc).loc = loc + (Lam x body loc).loc = loc + (App fun arg loc).loc = loc + (Pair fst snd loc).loc = loc + (Fst pair loc).loc = loc + (Snd pair loc).loc = loc + (Tag tag loc).loc = loc + (CaseEnum tag cases loc).loc = loc + (Absurd loc).loc = loc + (Zero loc).loc = loc + (Succ nat loc).loc = loc + (CaseNat nat zer suc loc).loc = loc + (Erased loc).loc = loc public export @@ -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