improved printing

src/Lib/Check.idr

@@ -24,6 +24,7 @@ forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
   (Solved k t) => vappSpine t sp
 forceMeta x = pure x
 
+
 parameters (ctx: Context)
   -- return renaming, the position is the new VVar
   invert : Nat -> SnocList Val -> M (List Nat)
@@ -63,7 +64,8 @@ parameters (ctx: Context)
 
   lams : Nat -> Tm -> Tm
   lams 0 tm = tm
-  lams (S k) tm = Lam "arg:\{show k}" (lams k tm)
+  -- REVIEW can I get better names in here?
+  lams (S k) tm = Lam "arg_\{show k}" (lams k tm)
 
 
   solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
@@ -142,7 +144,7 @@ check ctx tm ty with (force ty)
                 pure $ Lam nm' sc
               else
                 error [(DS "Icity issue checking \{show t} at \{show ty}")]
-          other => error [(DS "Expected pi type, got \{show !(quote 0 ty)}")]
+          other => error [(DS "Expected pi type, got \{!(prval ty)}")]
   check ctx tm _ | (VPi nm' Implicit a b) = do
     putStrLn "XXX edge \{show tm} against VPi"
     let var = VVar (length ctx.env) [<]
@@ -159,7 +161,7 @@ check ctx tm ty with (force ty)
     (tm', ty') <- case !(infer ctx tm) of
       (tm'@(Lam{}),ty') => pure (tm', ty')
       (tm', ty') => insert ctx tm' ty'
-    putStrLn "infer \{show tm} to \{show tm'} : \{show ty'} expect \{show ty}"
+    putStrLn "infer \{show tm} to \{pprint [] tm'} : \{show ty'} expect \{show ty}"
     when( ctx.lvl /= length ctx.env) $ error [DS "level mismatch \{show ctx.lvl} \{show ctx.env}"]
     unify ctx ctx.lvl ty' ty
     pure tm'
@@ -219,7 +221,7 @@ infer ctx (RLam nm icit tm) = do
   a <- freshMeta ctx >>= eval ctx.env CBN
   let ctx' = extend ctx nm a
   (tm', b) <- infer ctx' tm
-  putStrLn "make lam for \{show nm} scope \{show tm'} : \{show b}"
+  putStrLn "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}"
   pure $ (Lam nm tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
   -- error {ctx} [DS "can't infer lambda"]
 

src/Lib/TT.idr

@@ -67,23 +67,6 @@ lookupMeta ix = do
     go (meta@(Unsolved _ k ys) :: xs) = if k == ix then pure meta else go xs
     go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs
 
-export
-solveMeta : TopContext -> Nat -> Val -> M ()
-solveMeta ctx ix tm = do
-  mc <- readIORef ctx.metas
-  metas <- go mc.metas [<]
-  writeIORef ctx.metas $ {metas := metas} mc
-  where
-    go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
-    go [] _ = error' "Meta \{show ix} not found"
-    go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix
-      then do
-        putStrLn "INFO at \{show pos}: solve \{show k} as \{show tm}"
-        pure $ lhs <>> (Solved k tm :: xs)
-      else go xs (lhs :< meta)
-    go (meta@(Solved k _) :: xs) lhs = if k == ix
-      then error' "Meta \{show ix} already solved!"
-      else go xs (lhs :< meta)
 
 export partial
 Show Context where
@@ -187,4 +170,24 @@ export
 nf : Env -> Tm -> M Tm
 nf env t = quote (length env) !(eval env CBN t)
 
+export
+prval : Val -> M String
+prval v = pure $ pprint [] !(quote 0 v)
 
+export
+solveMeta : TopContext -> Nat -> Val -> M ()
+solveMeta ctx ix tm = do
+  mc <- readIORef ctx.metas
+  metas <- go mc.metas [<]
+  writeIORef ctx.metas $ {metas := metas} mc
+  where
+    go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
+    go [] _ = error' "Meta \{show ix} not found"
+    go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix
+      then do
+        putStrLn "INFO at \{show pos}: solve \{show k} as \{!(prval tm)}"
+        pure $ lhs <>> (Solved k tm :: xs)
+      else go xs (lhs :< meta)
+    go (meta@(Solved k _) :: xs) lhs = if k == ix
+      then error' "Meta \{show ix} already solved!"
+      else go xs (lhs :< meta)

src/Lib/Types.idr

@@ -52,7 +52,7 @@ data Tm : Type where
 
 %name Tm t, u, v
 
-public export
+-- public export
 Show Tm where
   show (Bnd k) = "(Bnd \{show k})"
   show (Ref str _) = "(Ref \{show str})"
@@ -84,6 +84,23 @@ Eq (Tm) where
   (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
   _ == _ = False
 
+
+export
+pprint : List String -> Tm -> String
+pprint names tm = render 80 $ go names tm
+  where
+    go : List String -> Tm -> Doc
+    go names (Bnd k) = case getAt k names of
+      Nothing => text "BND \{show k}"
+      Just nm => text "\{nm}:\{show k}"
+    go names (Ref str mt) = text str
+    go names (Meta k) = text "?m:\{show k}"
+    go names (Lam nm t) = text "(\\ \{nm} =>" <+> go (nm :: names) t <+> ")"
+    go names (App t u) = text "(" <+> go names t <+> go names u <+> ")"
+    go names U = "U"
+    go names (Pi nm icit t u) =
+      text "(" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")"
+
 public export
 Pretty Tm where
   pretty (Bnd k) = ?rhs_0
@@ -92,7 +109,7 @@ Pretty Tm where
   pretty (Lam str t) = text "(\\ \{str} => " <+> pretty t <+> ")"
   pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
   pretty U = "U"
-  pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> "=>" <+> pretty u <+> ")"
+  pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")"
 
 -- public export
 -- data Closure : Nat -> Type
@@ -250,6 +267,10 @@ record Context where
   metas : IORef MetaContext
 
 
+export
+names : Context -> List String
+names ctx = toList $ map fst ctx.types
+
 public export
 M : Type -> Type
 M = (StateT TopContext (EitherT Impl.Error IO))

src/Main.idr

@@ -52,7 +52,7 @@ processDecl (TypeSig nm tm) = do
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas) tm VU
   ty' <- nf [] ty
-  putStrLn "got \{show ty'}"
+  putStrLn "got \{pprint [] ty'}"
   modify $ claim nm ty'
 
 -- FIXME - this should be in another file
@@ -68,11 +68,11 @@ processDecl (Def nm raw) = do
     | Nothing => throwError $ E pos "skip def \{nm} without Decl"
   let (MkEntry name ty Axiom) := entry
     | _ => throwError $ E pos "\{nm} already defined"
-  putStrLn "check \{nm} = \{show raw} at \{show $ ty}"
+  putStrLn "check \{nm} = \{show raw} at \{pprint [] ty}"
   vty <- eval empty CBN ty
   putStrLn "vty is \{show vty}"
   tm <- check (mkCtx ctx.metas) raw vty
-  putStrLn "Ok \{show tm}"
+  putStrLn "Ok \{pprint [] tm}"
 
   mc <- readIORef ctx.metas
   for_ mc.metas $ \case
@@ -88,12 +88,12 @@ processDecl (DCheck tm ty) = do
   top <- get
   putStrLn "check \{show tm} at \{show ty}"
   ty' <- check (mkCtx top.metas) tm VU
-  putStrLn "got type \{show ty'}"
+  putStrLn "got type \{pprint [] ty'}"
   vty <- eval [] CBN ty'
   res <- check (mkCtx top.metas) ty vty
-  putStrLn "got \{show res}"
+  putStrLn "got \{pprint [] res}"
   norm <- nf [] res
-  putStrLn "norm \{show norm}"
+  putStrLn "norm \{pprint [] norm}"
   -- top <- get
   -- ctx <- mkCtx top.metas
   -- I need a type to check against