changes to support translation

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

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

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/\|\|\|/--/;

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
+fcLine : FC -> Int
-fc.line = fst fc.start
+fcLine (MkFC file (l, c)) = l
 
 export
-(.col) : FC -> Int
+fcCol : FC -> Int
-fc.col = snd fc.start
+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
+      if l == fcLine fc then
-        "  \{x}\n  \{replicate (cast fc.col) ' '}^\n"
+        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
-      else if fc.line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      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
+      if l == fcLine fc then
-        "  \{x}\n  \{replicate (cast fc.col) ' '}^\n"
+        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
-      else if fc.line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
       else go (l + 1) xs
 
 public export

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@(JLam{}) xs) = text "(" ++ expToDoc x ++ text ")" ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")"
-expToDoc (Apply x xs) = expToDoc x ++ "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ ")"
+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 (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> text "(" ++ expToDoc exp ++ text ")"
-expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}"
+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 (Index obj ix) = expToDoc obj ++ text "[" ++ expToDoc ix ++ text "]"
-expToDoc (Dot obj nm) = expToDoc obj ++ "." ++ jsIdent nm
+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 (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ text ":" ++ caseBody stmt
-altToDoc (JDefAlt stmt) = text "default" ++ ":" ++ caseBody stmt
+altToDoc (JDefAlt stmt) = text "default" ++ text ":" ++ caseBody stmt
-altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ ":" ++ 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 (JLet nm body) = text "let" <+> jsIdent nm ++ text ";" </> stmtToDoc body
-stmtToDoc (JAssign nm expr) = jsIdent nm <+> "=" <+> expToDoc expr ++ ";"
+stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";"
-stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 ("=" <+/> expToDoc x ++ ";")
+stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";")
-stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ ";"
+stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";"
-stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ ");"
+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 ++ ";"
+  pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";"
-entryToDoc (MkEntry _ name type Axiom) = pure ""
+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)

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}"

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
+    in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent
-    else Fail False (error indent.file toks "unexpected outdent") toks com ops
+    else Fail False (error (file indent) toks "unexpected outdent") toks com ops
 
 ||| expect token of given kind
 export

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

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 (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")"
-  pretty (PatWild _icit) = "_"
+  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 (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y
-  pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
+  pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty)
-  pretty (PFunc _ nm [] ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
+  pretty (PFunc _ nm [] ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> 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 (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

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
+pprint names tm = pprint' 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"
 
 data Val : Type
 
@@ -532,34 +531,34 @@ get : M TopContext
 get = MkM $ \ tc => pure $ Right (tc, tc)
 
 export
-put : TopContext -> M ()
+put : TopContext -> M Unit
-put tc = MkM $ \_ => pure $ Right (tc, ())
+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}"