From f4e96d06ece2e7d3f76af3932a3bc89e03e95795 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 30 Dec 2024 22:34:03 -0800 Subject: [PATCH] changes to support translation --- TODO.md | 6 +++ newt/Prelude.newt | 12 ++++++ scripts/translate.sh | 6 +++ src/Lib/Common.idr | 22 +++++----- src/Lib/Compile.idr | 48 +++++++++++----------- src/Lib/Elab.idr | 12 +++--- src/Lib/Parser/Impl.idr | 4 +- src/Lib/Prettier.idr | 8 +--- src/Lib/Syntax.idr | 24 +++++------ src/Lib/Types.idr | 91 ++++++++++++++++++++--------------------- 10 files changed, 126 insertions(+), 107 deletions(-) diff --git a/TODO.md b/TODO.md index 3c80422..f339c19 100644 --- a/TODO.md +++ b/TODO.md @@ -4,8 +4,13 @@ More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff. - [x] tokenizer that can be ported to newt +- [ ] Add default path for library, so we don't need symlinks everywhere and can write tests for the library - [ ] string interpolation? + - The tricky part here is the `}` - I need to run the normal tokenizer in a way that treats `}` specially. + - Idris handles `putStrLn "done \{ show $ add {x=1} 2}"` - it recurses for `{` `}` pairs. Do we want that complexity? + - The mini version would be recurse on `{`, pop on `}` (and expect caller to handle), fail if we get to the top with a tokens remaining. - [ ] mutual recursion in where? + - need to scan sigs and then defs, will have to make sure Compile.idr puts them all in scope before processing each. - [x] Move on to next decl in case of error - [x] for parse error, seek to col 0 token and process next decl - [ ] record update sugar, syntax TBD @@ -17,6 +22,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] fix "insufficient patterns", wire in M or Either String - [x] Matching _,_ when Maybe is expected should be an error - [ ] There are issues with matching inside do blocks, I think we need to guess scrutinee? I could imagine constraining metas too (e.g. if Just ... at ?m123 then ?m123 =?= Maybe ?m456) + - `newt/Fixme.newt` - I can drop `do` _and_ put `bind {IO}` to push it along. It may need to try to solve autos earlier and better. - Also, the root cause is tough to track down if there is a type error (this happens with `do` in Idris, too). - Part of it is the auto solutions are getting discarded because of an unrelated unification failure. Either auto shouldn't go as deep or should run earlier. Forgetting that lookupMap returns a (k,v) pair is a good example. - [ ] add error for non-linear pattern diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 97a4d9a..e76d748 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -771,3 +771,15 @@ snoc xs x = xs ++ (x :: Nil) instance ∀ a b. {{Show a}} {{Show b}} → Show (a × b) where show (a,b) = "(" ++ show a ++ "," ++ show b ++ ")" + +-- For now, I'm not having the compiler do this automatically + +Lazy : U → U +Lazy a = Unit → a + +force : ∀ a. Lazy a → a +force f = f MkUnit + +-- unlike Idris, user will have to write \ _ => ... +when : ∀ f. {{Applicative f}} → Bool → Lazy (f Unit) → f Unit +when b fa = if b then force fa else return MkUnit diff --git a/scripts/translate.sh b/scripts/translate.sh index 26f86d9..ba441fc 100755 --- a/scripts/translate.sh +++ b/scripts/translate.sh @@ -17,6 +17,12 @@ find src -type f -name '*.idr' | while read -r file; do s/import public/import/g; s/^\s*covering//g; s/^export//g; + s/pure \(\)/pure MkUnit/; + s/M \(\)/M Unit/; + s/Parser \(\)/Parser Unit/; + s/OK \(\)/OK MkUnit/; + s/\bNat\b/Int/g; + s/(\s+when [^\$]+\$)(.*)/\1 \\ _ =>\2/; s/^public export//g; s/\(([A-Z]\w+), ?([^)]+)\)/(\1 × \2)/g; s/\|\|\|/--/; diff --git a/src/Lib/Common.idr b/src/Lib/Common.idr index a7dbbf5..1cac9be 100644 --- a/src/Lib/Common.idr +++ b/src/Lib/Common.idr @@ -70,15 +70,15 @@ record FC where export ToJSON FC where - toJson (MkFC file (line,col)) = JsonObj [ ("file", toJson file), ("line", toJson line), ("col", toJson col)] + toJson (MkFC file (line,col)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: Nil) export -(.line) : FC -> Int -fc.line = fst fc.start +fcLine : FC -> Int +fcLine (MkFC file (l, c)) = l export -(.col) : FC -> Int -fc.col = snd fc.start +fcCol : FC -> Int +fcCol (MkFC file (l, c)) = c public export interface HasFC a where @@ -108,18 +108,18 @@ showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src) go : Int -> List String -> String go l [] = "" go l (x :: xs) = - if l == fc.line then - " \{x}\n \{replicate (cast fc.col) ' '}^\n" - else if fc.line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs + if l == fcLine fc then + " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" + else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs else go (l + 1) xs showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src) where go : Int -> List String -> String go l [] = "" go l (x :: xs) = - if l == fc.line then - " \{x}\n \{replicate (cast fc.col) ' '}^\n" - else if fc.line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs + if l == fcLine fc then + " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" + else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs else go (l + 1) xs public export diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 7087a49..9d0d093 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -218,45 +218,45 @@ stmtToDoc : JSStmt e -> Doc expToDoc : JSExp -> Doc expToDoc (LitArray xs) = ?expToDoc_rhs_0 -expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ ", " <+/> e) (map entry xs) <+> text "}" +expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ text ", " <+/> e) (map entry xs) <+> text "}" where entry : (String, JSExp) -> Doc -- TODO quote if needed - entry (nm, exp) = jsIdent nm ++ ":" <+> expToDoc exp + entry (nm, exp) = jsIdent nm ++ text ":" <+> expToDoc exp expToDoc (LitString str) = text $ quoteString str expToDoc (LitInt i) = text $ show i -- TODO add precedence -expToDoc (Apply x@(JLam{}) xs) = text "(" ++ expToDoc x ++ ")" ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")" -expToDoc (Apply x xs) = expToDoc x ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")" +expToDoc (Apply x@(JLam{}) xs) = text "(" ++ expToDoc x ++ text ")" ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")" +expToDoc (Apply x xs) = expToDoc x ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")" expToDoc (Var nm) = jsIdent nm -expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")" -expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}" +expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> text "(" ++ expToDoc exp ++ text ")" +expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> bracket "{" (stmtToDoc body) "}" expToDoc JUndefined = text "undefined" -expToDoc (Index obj ix) = expToDoc obj ++ "[" ++ expToDoc ix ++ "]" -expToDoc (Dot obj nm) = expToDoc obj ++ "." ++ jsIdent nm +expToDoc (Index obj ix) = expToDoc obj ++ text "[" ++ expToDoc ix ++ text "]" +expToDoc (Dot obj nm) = expToDoc obj ++ text "." ++ jsIdent nm caseBody : JSStmt e -> Doc caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt) -- caseBody {e = Return} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt) caseBody {e} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt text "break;") -caseBody stmt = line ++ "{" ++ nest 2 (line ++ stmtToDoc stmt text "break;") "}" +caseBody stmt = line ++ text "{" ++ nest 2 (line ++ stmtToDoc stmt text "break;") text "}" altToDoc : JAlt -> Doc -altToDoc (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ ":" ++ caseBody stmt -altToDoc (JDefAlt stmt) = text "default" ++ ":" ++ caseBody stmt -altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ ":" ++ caseBody stmt +altToDoc (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ text ":" ++ caseBody stmt +altToDoc (JDefAlt stmt) = text "default" ++ text ":" ++ caseBody stmt +altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ text ":" ++ caseBody stmt stmtToDoc (JSnoc x y) = stmtToDoc x stmtToDoc y -stmtToDoc (JPlain x) = expToDoc x ++ ";" +stmtToDoc (JPlain x) = expToDoc x ++ text ";" -- I might not need these split yet. -stmtToDoc (JLet nm body) = "let" <+> jsIdent nm ++ ";" stmtToDoc body -stmtToDoc (JAssign nm expr) = jsIdent nm <+> "=" <+> expToDoc expr ++ ";" -stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 ("=" <+/> expToDoc x ++ ";") -stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ ";" -stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ ");" +stmtToDoc (JLet nm body) = text "let" <+> jsIdent nm ++ text ";" stmtToDoc body +stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";" +stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";") +stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";" +stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ text ");" stmtToDoc (JCase sc alts) = - text "switch (" ++ expToDoc sc ++ ")" <+> bracket "{" (stack $ map altToDoc alts) "}" + text "switch (" ++ expToDoc sc ++ text ")" <+> bracket "{" (stack $ map altToDoc alts) "}" mkArgs : Nat -> List String -> List String mkArgs Z acc = acc @@ -279,12 +279,12 @@ entryToDoc (MkEntry _ name ty (Fn tm)) = do debug "compileFun \{pprint [] tm}" ct <- compileFun tm let exp = maybeWrap $ termToJS empty ct JReturn - pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ ";" -entryToDoc (MkEntry _ name type Axiom) = pure "" + pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";" +entryToDoc (MkEntry _ name type Axiom) = pure $ text "" entryToDoc (MkEntry _ name type (TCon strs)) = pure $ dcon name (piArity type) entryToDoc (MkEntry _ name type (DCon arity str)) = pure $ dcon name arity entryToDoc (MkEntry _ name type PrimTCon) = pure $ dcon name (piArity type) -entryToDoc (MkEntry _ name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent (show name) <+> "=" <+> text src +entryToDoc (MkEntry _ name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent (show name) <+> text "=" <+> text src ||| This version (call `reverse . snd <$> process "main" ([],[])`) will do dead ||| code elimination, but the Prelude js primitives are reaching for @@ -303,7 +303,7 @@ process (done,docs) nm = do ct <- compileFun tm -- If ct has zero arity and is a compount expression, this fails.. let exp = maybeWrap $ termToJS empty ct JReturn - let doc = text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ ";" + let doc = text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";" (done,docs) <- walkTm tm (nm :: done, docs) pure (done, doc :: docs) Just entry => pure (nm :: done, !(entryToDoc entry) :: docs) @@ -315,7 +315,7 @@ process (done,docs) nm = do let tag = QN [] nm let False = tag `elem` done | _ => pure (done,docs) (done,docs) <- process (done, docs) name - let doc = text "const" <+> jsIdent nm <+> text "=" <+> jsIdent (show name) ++ ";" + let doc = text "const" <+> jsIdent nm <+> text "=" <+> jsIdent (show name) ++ text ";" pure (tag :: done, doc :: docs) walkTm : Tm -> (List QName, List Doc) -> M (List QName, List Doc) diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 4c9fb22..8aa5586 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -139,10 +139,10 @@ invert lvl sp = go sp [] -- we have to "lift" the renaming when we go under a lambda -- I think that essentially means our domain ix are one bigger, since we're looking at lvl -- in the codomain, so maybe we can just keep that value -rename : Nat -> List Nat -> Nat -> Val -> M Tm +rename : Nat -> List Nat -> Nat -> Val -> M Tm rename meta ren lvl v = go ren lvl v where - go : List Nat -> Nat -> Val -> M Tm + go : List Nat -> Nat -> Val -> M Tm goSpine : List Nat -> Nat -> Tm -> SnocList Val -> M Tm goSpine ren lvl tm [<] = pure tm goSpine ren lvl tm (xs :< x) = do @@ -192,7 +192,7 @@ unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ toList $ zip ctx.bds (map fst ctx.types) export -solve : Env -> (k : Nat) -> SnocList Val -> Val -> M () +solve : Env -> (k : Nat) -> SnocList Val -> Val -> M () solve env m sp t = do meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m | _ => error (getFC t) "Meta \{show m} already solved! [solve]" @@ -408,10 +408,10 @@ primType fc nm = case lookup nm !(get) of _ => error fc "Primitive type \{show nm} not in scope" export -infer : Context -> Raw -> M (Tm, Val) +infer : Context -> Raw -> M (Tm, Val) export -check : Context -> Raw -> Val -> M Tm +check : Context -> Raw -> Val -> M Tm data Bind = MkBind String Icit Val @@ -1086,7 +1086,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of infer ctx (RVar fc nm) = go 0 ctx.types where - go : Nat -> Vect n (String, Val) -> M (Tm, Val) + go : Nat -> Vect n (String, Val) -> M (Tm, Val) go i [] = case lookupRaw nm !(get) of Just (MkEntry _ name ty def) => do debug "lookup \{name} as \{show def}" diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 53842af..ed23eb4 100644 --- a/src/Lib/Parser/Impl.idr +++ b/src/Lib/Parser/Impl.idr @@ -190,8 +190,8 @@ indented (P p) = P $ \toks,com,ops,indent => case toks of [] => p toks com ops indent (t::_) => let (tl,tc) = start t - in if tc > indent.col || tl == indent.line then p toks com ops indent - else Fail False (error indent.file toks "unexpected outdent") toks com ops + in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent + else Fail False (error (file indent) toks "unexpected outdent") toks com ops ||| expect token of given kind export diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr index c709fd8..3e74a6e 100644 --- a/src/Lib/Prettier.idr +++ b/src/Lib/Prettier.idr @@ -58,10 +58,10 @@ be fit acc w k ((i, (Text s)) :: xs) = if not fit || (k + length s < w) then (be fit (acc :< TEXT s) w (k + length s) xs) else Nothing -be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i+j,x)::xs) +be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x) :: xs) be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs) be fit acc w k ((i, (Alt x y)) :: xs) = - (acc <>>) <$> (be True [<] w k ((i,x)::xs) <|> be fit [<] w k ((i,y)::xs)) + (acc <>>) <$> (be True [<] w k ((i,x) :: xs) <|> be fit [<] w k ((i,y) :: xs)) best : Nat -> Nat -> Doc -> List Item best w k x = fromMaybe [] $ be False [<] w k [(0,x)] @@ -143,10 +143,6 @@ export commaSep : List Doc -> Doc commaSep = folddoc (\a, b => a ++ text "," <+/> b) -public export -FromString Doc where - fromString = text - ||| If we stick Doc into a String, try to avoid line-breaks via `flatten` public export Interpolation Doc where diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 220f41c..a663874 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -235,8 +235,8 @@ Pretty Pattern where -- FIXME - wrap Implicit with {} pretty (PatVar _ icit nm) = text nm pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args) - pretty (PatCon _ icit nm args (Just as)) = text as ++ "@(" ++ text (show nm) <+> spread (map pretty args) ++ ")" - pretty (PatWild _icit) = "_" + pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")" + pretty (PatWild _icit) = text "_" pretty (PatLit _ lit) = pretty lit wrap : Icit -> Doc -> Doc @@ -276,9 +276,9 @@ Pretty Raw where asDoc p (RImplicit _) = text "_" asDoc p (RHole _) = text "?" asDoc p (RDo _ stmts) = text "TODO - RDo" - asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> "then" <+> asDoc 0 y <+/> "else" <+> asDoc 0 z + asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> text "then" <+> asDoc 0 y <+/> text "else" <+> asDoc 0 z asDoc p (RWhere _ dd b) = text "TODO pretty where" - asDoc p (RAs _ nm x) = text nm ++ "@(" ++ asDoc 0 x ++ ")" + asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")" prettyBind : (BindInfo, Raw) -> Doc prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty) @@ -289,19 +289,19 @@ pipeSep = folddoc (\a, b => a <+/> text "|" <+> b) export Pretty Decl where pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty) - pretty (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> "=" <+> pretty b) clauses + pretty (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> text "=" <+> pretty b) clauses pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) - pretty (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y - pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty) - pretty (PFunc _ nm [] ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src)) - pretty (PFunc _ nm uses ty src) = "pfunc" <+> text nm <+> "uses" <+> spread (map text uses) <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src)) + pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y + pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty) + pretty (PFunc _ nm [] ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) + pretty (PFunc _ nm uses ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text uses) <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names) - pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> ":" <+> spread (map prettyBind tele) + pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele) <+> (nest 2 $ text "where" stack (maybe empty (\ nm' => text "constructor" <+> text nm') cname :: map pretty decls)) - pretty (Class _ nm tele decls) = text "class" <+> text nm <+> ":" <+> spread (map prettyBind tele) + pretty (Class _ nm tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele) <+> (nest 2 $ text "where" stack (map pretty decls)) pretty (Instance _ _ _) = text "TODO pretty Instance" - pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> "=" <+> pipeSep (map pretty sigs) + pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) export Pretty Module where diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index fb2c4b1..e7a584e 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -214,47 +214,46 @@ Eq (Tm) where -- maybe return Doc and have an Interpolation.. -- If we need to flatten, case is going to get in the way. +pprint' : Nat -> List String -> Tm -> Doc +pprintAlt : Nat -> List String -> CaseAlt -> Doc +pprintAlt p names (CaseDefault t) = text "_" <+> text "=>" <+> pprint' p ("_" :: names) t +pprintAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ text "=>" <+/> pprint' p (reverse args ++ names) t) +-- `;` is not in surface syntax, but sometimes we print on one line +pprintAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ text "=>" <+/> pprint' p names t ++ text ";") + +parens : Nat -> Nat -> Doc -> Doc +parens a b doc = if a < b + then text "(" ++ doc ++ text ")" + else doc + +pprint' p names (Bnd _ k) = case getAt k names of + -- Either a bug or we're printing without names + Nothing => text "BND:\{show k}" + Just nm => text "\{nm}:\{show k}" +pprint' p names (Ref _ str mt) = text (show str) +pprint' p names (Meta _ k) = text "?m:\{show k}" +pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t +pprint' p names (App _ t u) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names u +pprint' p names (UU _) = text "U" +pprint' p names (Pi _ nm Auto rig t u) = parens 0 p $ + text "{{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}}" <+> text "->" <+> pprint' 0 (nm :: names) u +pprint' p names (Pi _ nm Implicit rig t u) = parens 0 p $ + text "{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}" <+> text "->" <+> pprint' 0 (nm :: names) u +pprint' p names (Pi _ "_" Explicit Many t u) = + parens 0 p $ pprint' 1 names t <+> text "->" <+> pprint' 0 ("_" :: names) u +pprint' p names (Pi _ nm Explicit rig t u) = parens 0 p $ + text "(" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t ++ text ")" <+> text "->" <+> pprint' 0 (nm :: names) u +-- FIXME - probably way wrong on the names here. There is implicit binding going on +pprint' p names (Case _ sc alts) = parens 0 p $ text "case" <+> pprint' 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (pprintAlt 0 names) alts))) +pprint' p names (Lit _ lit) = text (show lit) +pprint' p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> text ":=" <+> pprint' 0 names t <+> text "in" (nest 2 $ pprint' 0 (nm :: names) u) +pprint' p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> text ":" <+> pprint' 0 names ty <+> text ":=" <+> pprint' 0 names t <+> text "in" (nest 2 $ pprint' 0 (nm :: names) u) +pprint' p names (Erased _) = text "ERASED" + ||| Pretty printer for Tm. export pprint : List String -> Tm -> Doc -pprint names tm = go 0 names tm - where - parens : Nat -> Nat -> Doc -> Doc - parens a b doc = if a < b - then text "(" ++ doc ++ text ")" - else doc - - go : Nat -> List String -> Tm -> Doc - goAlt : Nat -> List String -> CaseAlt -> Doc - - goAlt p names (CaseDefault t) = "_" <+> "=>" <+> go p ("_" :: names) t - goAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ "=>" <+/> go p (reverse args ++ names) t) - -- `;` is not in surface syntax, but sometimes we print on one line - goAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ "=>" <+/> go p names t ++ ";") - - go p names (Bnd _ k) = case getAt k names of - -- Either a bug or we're printing without names - Nothing => text "BND:\{show k}" - Just nm => text "\{nm}:\{show k}" - go p names (Ref _ str mt) = text (show str) - go p names (Meta _ k) = text "?m:\{show k}" - go p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> go 0 (nm :: names) t - go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u - go p names (UU _) = "U" - go p names (Pi _ nm Auto rig t u) = parens 0 p $ - text "{{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}}" <+> "->" <+> go 0 (nm :: names) u - go p names (Pi _ nm Implicit rig t u) = parens 0 p $ - text "{" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t <+> "}" <+> "->" <+> go 0 (nm :: names) u - go p names (Pi _ "_" Explicit Many t u) = - parens 0 p $ go 1 names t <+> "->" <+> go 0 ("_" :: names) u - go p names (Pi _ nm Explicit rig t u) = parens 0 p $ - text "(" ++ text (show rig) <+> text nm <+> ":" <+> go 0 names t ++ ")" <+> "->" <+> go 0 (nm :: names) u - -- FIXME - probably way wrong on the names here. There is implicit binding going on - go p names (Case _ sc alts) = parens 0 p $ text "case" <+> go 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (goAlt 0 names) alts))) - go p names (Lit _ lit) = text (show lit) - go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t <+> "in" (nest 2 $ go 0 (nm :: names) u) - go p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> ":" <+> go 0 names ty <+> ":=" <+> go 0 names t <+> "in" (nest 2 $ go 0 (nm :: names) u) - go p names (Erased _) = "ERASED" +pprint names tm = pprint' 0 names tm data Val : Type @@ -532,34 +531,34 @@ get : M TopContext get = MkM $ \ tc => pure $ Right (tc, tc) export -put : TopContext -> M () -put tc = MkM $ \_ => pure $ Right (tc, ()) +put : TopContext -> M Unit +put tc = MkM $ \_ => pure $ Right (tc, MkUnit) export -modify : (TopContext -> TopContext) -> M () +modify : (TopContext -> TopContext) -> M Unit modify f = do tc <- get put (f tc) ||| Force argument and print if verbose is true export -debug : Lazy String -> M () +debug : Lazy String -> M Unit debug x = do top <- get - when top.verbose $ putStrLn x + when top.verbose $ putStrLn $ Force x export -info : FC -> String -> M () +info : FC -> String -> M Unit info fc msg = putStrLn "INFO at \{show fc}: \{msg}" ||| Version of debug that makes monadic computation lazy export -debugM : M String -> M () +debugM : M String -> M Unit debugM x = do top <- get when top.verbose $ do putStrLn !(x) -export partial +export Show Context where show ctx = "Context \{show $ map fst $ ctx.types}"