tweaks to output, fix scope issue in pprint

TODO.md

@@ -18,6 +18,8 @@
   - There is also a bit where kovacs uses the implicit on the type (a value) to decide to insert
 - [ ] consider binders in environment, to better mark let and to provide names
 - [ ] move some top-level chattiness to `debug`
+- [ ] consider optionally compiling to eliminators for a second type-checking pass. This
+      would help catch bugs.
 - [x] Allow unicode operators/names
 - Web playground
   - [x] editor

playground/samples/Combinatory.newt

@@ -39,7 +39,6 @@ data Term : Ctx -> Type -> U where
   Lam : {Γ : Ctx} {σ τ : Type} -> Term (σ :: Γ) τ -> Term Γ (σ ~> τ)
   Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ
 
--- FIXME, I wasn't getting an error when I had Nil shadowing Nil
 infixr 7 _:::_
 data Env : Ctx -> U where
   ENil : Env Nil

playground/samples/Tour.newt

@@ -54,7 +54,7 @@ plus (S n) m = S (plus n m)
 plus' : Nat -> Nat -> Nat
 plus' = \ n m => case n of
     Z => m
-    S n => S (plus n m)
+    S n => S (plus' n m)
 
 -- We can define operators, currently only infix
 -- and we allow unicode and letters in operators

src/Lib/Elab.idr

@@ -871,6 +871,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
     top <- get
     clauses <- traverse (\(MkAlt pat rawRHS) => pure $ MkClause (getFC pat) [(scnm, !(mkPat top (pat, Explicit)))] [] rawRHS ) alts
     -- buildCase expects scrutinee to be a name in the context, so we need to let it.
+    -- if it's a Bnd and not shadowed we could skip the let, but that's messy.
     let ctx' = extend ctx scnm scty
     pure $ Let fc scnm sc !(buildTree ctx' $ MkProb clauses ty)
 

src/Lib/ProcessDecl.idr

@@ -165,6 +165,8 @@ processDecl : Decl -> M ()
 processDecl (PMixFix{})  = pure ()
 
 processDecl (TypeSig fc names tm) = do
+  putStrLn "-----"
+  putStrLn "TypeSig \{unwords names} : \{show tm}"
   top <- get
   mc <- readIORef top.metas
   let mstart = length mc.metas
@@ -172,12 +174,10 @@ processDecl (TypeSig fc names tm) = do
     let Nothing := lookup nm top
       | _ => error fc "\{show nm} is already defined"
     pure ()
-  putStrLn "-----"
-  putStrLn "TypeSig \{unwords names} : \{show tm}"
   ty <- check (mkCtx top.metas fc) tm (VU fc)
   debug "got \{pprint [] ty}"
   for_ names $ \nm => setDef nm fc ty Axiom
-  -- Zoo4eg has metas in TypeSig, need to decide if I want to support that going forward.
+  -- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here
   -- logMetas mstart
 
 processDecl (PType fc nm ty) = do
@@ -194,7 +194,7 @@ processDecl (PFunc fc nm ty src) = do
 
 processDecl (Def fc nm clauses) = do
   putStrLn "-----"
-  putStrLn "def \{show nm}"
+  putStrLn "Def \{show nm}"
   top <- get
   mc <- readIORef top.metas
   let mstart = length mc.metas
@@ -203,23 +203,24 @@ processDecl (Def fc nm clauses) = do
   let (MkEntry name ty Axiom) := entry
     | _ => throwError $ E fc "\{nm} already defined"
 
-  putStrLn "check \{nm} ... at \{pprint [] ty}"
+  putStrLn "check \{nm} at \{pprint [] ty}"
   vty <- eval empty CBN ty
-  putStrLn "vty is \{show vty}"
+  debug "\{nm} vty is \{show vty}"
 
   -- I can take LHS apart syntactically or elaborate it with an infer
   clauses' <- traverse (makeClause top) clauses
   tm <- buildTree (mkCtx top.metas fc) (MkProb clauses' vty)
-  putStrLn "Ok \{pprint [] tm}"
+  -- putStrLn "Ok \{pprint [] tm}"
 
   mc <- readIORef top.metas
   let mlen = length mc.metas `minus` mstart
   solveAutos mlen (take mlen mc.metas)
 
-  -- Expand metas
-  -- tm' <- nf [] tm  -- TODO - make nf that expands all metas, Day1.newt is a test case
+  -- TODO - make nf that expands all metas and drop zonk
+  -- Day1.newt is a test case
+  -- tm' <- nf [] tm
   tm' <- zonk top 0 [] tm
-  putStrLn "NF \{pprint[] tm'}"
+  putStrLn "NF\n\{pprint[] tm'}"
   debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
   updateDef nm fc ty (Fn tm')
   logMetas mstart
@@ -241,7 +242,7 @@ processDecl (DCheck fc tm ty) = do
 
 processDecl (Data fc nm ty cons) = do
   putStrLn "-----"
-  putStrLn "process data \{nm}"
+  putStrLn "Data \{nm}"
   top <- get
   mc <- readIORef top.metas
   let mstart = length mc.metas

src/Lib/Types.idr

@@ -202,9 +202,9 @@ pprint names tm = render 80 $ go 0 names tm
     go p names (Pi _ nm Explicit t u) =
       text "((" <+> text nm <+> ":" <+> go p names t <+> ")" <+> "->" <+> go p (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 (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 </> (nest 2 $ go 0 names u)
+    go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t </> (nest 2 $ go 0 (nm :: names) u)
 
 -- public export
 -- data Closure : Nat -> Type