printing improvements, improve case eval

playground/src/monarch.ts

@@ -20,6 +20,7 @@ export let newtConfig: monaco.languages.LanguageConfiguration = {
     { open: "(", close: ")" },
     { open: '"', close: '"' },
     { open: "'", close: "'" },
+    { open: "/-", close: "-/" },
   ],
   // symbols that can be used to surround a selection
   surroundingPairs: [

src/Lib/Elab.idr

@@ -58,13 +58,6 @@ forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
   (Solved _ k t) => vappSpine t sp >>= forceMeta
 forceMeta x = pure x
 
--- Force far enough to compare types
-forceType : Val -> M Val
-forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
-  (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
-  (Solved _ k t) => vappSpine t sp >>= forceType
-forceType x = fromMaybe x <$> tryEval x
-
 public export
 record UnifyResult where
   constructor MkResult
@@ -280,7 +273,7 @@ parameters (ctx: Context)
             | Just v => unify l mode t' v
           if k == k'
             then unifySpine l mode (k == k') sp sp'
-            else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
+            else error fc "vref mismatch \{show t'} \{show u'}"
 
       (VU _, VU _) => pure neutral
       -- Lennart.newt cursed type references itself

src/Lib/Eval.idr

@@ -57,6 +57,18 @@ tryEval (VRef fc k _ sp) =
       _ => pure Nothing
 tryEval _ = pure Nothing
 
+-- Force far enough to compare types
+export
+forceType : Val -> M Val
+forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
+  (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
+  (Solved _ k t) => vappSpine t sp >>= forceType
+--forceType x = fromMaybe x <$> tryEval x
+forceType x = do
+  Just x' <- tryEval x
+    | _ => pure x
+  forceType x'
+
 evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
 evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) =
   if nm == name
@@ -69,7 +81,7 @@ evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) =
     go env (arg :: args) (nm :: nms) = go (arg :: env) args nms
     go env args [] = Just <$> vappSpine !(eval env mode t) ([<] <>< args)
     go env [] rest = pure Nothing
-
+-- FIXME not good if stuck function
 evalCase env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u)
 evalCase env mode sc cc = do
   debug "CASE BAIL sc \{show sc} vs \{show cc}"
@@ -110,7 +122,7 @@ eval env mode (Lit fc lit) = pure $ VLit fc lit
 eval env mode tm@(Case fc sc alts) = do
   -- TODO we need to be able to tell eval to expand aggressively here.
   sc' <- eval env mode sc
-  let sc' = fromMaybe sc' !(tryEval sc')
+  sc' <- forceType sc'
   pure $ fromMaybe (VCase fc !(eval env mode sc) alts)
                              !(evalCase env mode sc' alts)
 

src/Lib/ProcessDecl.idr

@@ -118,6 +118,20 @@ solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
       solveAutos mlen (take mlen mc.metas)
 solveAutos mlen (_ :: es) = solveAutos mlen es
 
+dumpEnv : Context -> M String
+dumpEnv ctx =
+  unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) []
+  where
+    isVar : Nat -> Val -> Bool
+    isVar k (VVar _ k' [<]) = k == k'
+    isVar _ _ = False
+
+    go : List String -> Nat -> List (Val, String, Val) -> List String -> M (List String)
+    go _ _ [] acc = pure acc
+    go names k ((v, n, ty) :: xs) acc = if isVar k v
+      -- TODO - use Doc and add <+/> as appropriate to printing
+      then go names (S k) xs ("  \{n} : \{pprint names !(quote ctx.lvl ty)}":: acc)
+      else go names (S k) xs ("  \{n} = \{pprint names !(quote ctx.lvl v)} : \{pprint names !(quote ctx.lvl ty)}":: acc)
 
 logMetas : Nat -> M ()
 logMetas mstart = do
@@ -125,14 +139,13 @@ logMetas mstart = do
   top <- get
   mc <- readIORef top.metas
   let mlen = length mc.metas `minus` mstart
-  for_ (take mlen mc.metas) $ \case
+  for_ (reverse $ take mlen mc.metas) $ \case
     (Solved fc k soln) => info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
     (Unsolved fc k ctx ty User cons) => do
       ty' <- quote ctx.lvl ty
       let names = (toList $ map fst ctx.types)
-      -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
+      env <- dumpEnv ctx
-      env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure "  \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}"
+      let msg = "\{env}  -----------\n  \{pprint names ty'}"
-      let msg = "\{unlines (toList $ reverse env)}  -----------\n  \{pprint names ty'}"
       info fc "User Hole\n\{msg}"
     (Unsolved (l,c) k ctx ty kind cons) => do
       tm <- quote ctx.lvl !(forceMeta ty)
@@ -140,7 +153,6 @@ logMetas mstart = do
       -- TODO - log constraints?
       addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
 
-
 export
 processDecl : Decl -> M ()
 

src/Lib/Types.idr

@@ -172,33 +172,39 @@ Eq (Tm) where
 ||| Pretty printer for Tm.
 export
 pprint : List String -> Tm -> String
-pprint names tm = render 80 $ go names tm
+pprint names tm = render 80 $ go 0 names tm
   where
-    go : List String -> Tm -> Doc
+    parens : Nat -> Nat -> Doc -> Doc
-    goAlt : List String -> CaseAlt -> Doc
+    parens a b doc = if a < b
+      then text "(" ++ doc ++ text ")"
+      else doc
 
-    goAlt names (CaseDefault t) = "_" <+> "=>" <+> go ("_" :: names) t
+    go : Nat -> List String -> Tm -> Doc
-    goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go (reverse args ++ names) t
+    goAlt : Nat -> List String -> CaseAlt -> Doc
-    goAlt names (CaseLit lit t) = text (show lit) <+> "=>" <+/> go names t
 
-    go names (Bnd _ k) = case getAt k names of
+    goAlt p names (CaseDefault t) = "_" <+> "=>" <+> go p ("_" :: names) t
+    goAlt p names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go p (reverse args ++ names) t
+    goAlt p names (CaseLit lit t) = text (show lit) <+> "=>" <+/> 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 names (Ref _ str mt) = text str
+    go p names (Ref _ str mt) = text str
-    go names (Meta _ k) = text "?m:\{show k}"
+    go p names (Meta _ k) = text "?m:\{show k}"
-    go names (Lam _ nm t) = text "(\\ \{nm} =>" <+> go (nm :: names) t <+> ")"
+    go p names (Lam _ nm t) = parens 0 p $ text "\\ \{nm} =>" <+> go 0 (nm :: names) t
-    go names (App _ t u) = text "(" <+> go names t <+> go names u <+> ")"
+    go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u
-    go names (U _) = "U"
+    go p names (U _) = "U"
-    go names (Pi _ nm Auto t u) =
+    go p names (Pi _ nm Auto t u) =
-      text "({{" <+> text nm <+> ":" <+> go names t <+> "}}" <+> "->" <+> go (nm :: names) u <+> ")"
+      text "({{" <+> text nm <+> ":" <+> go p names t <+> "}}" <+> "->" <+> go p (nm :: names) u <+> ")"
-    go names (Pi _ nm Implicit t u) =
+    go p names (Pi _ nm Implicit t u) =
-      text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "->" <+> go (nm :: names) u <+> ")"
+      text "({" <+> text nm <+> ":" <+> go p names t <+> "}" <+> "->" <+> go p (nm :: names) u <+> ")"
-    go names (Pi _ nm Explicit t u) =
+    go p names (Pi _ nm Explicit t u) =
-      text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "->" <+> go (nm :: names) 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 names (Case _ sc alts) = text "case" <+> go names sc <+> text "of" </> (nest 2 (line ++ stack (map (goAlt 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 names (Lit _ lit) = text (show lit)
+    go p names (Lit _ lit) = text (show lit)
-    go names (Let _ nm t u) = text "let" <+> text nm <+> ":=" <+> go names t </> (nest 2 $ go names u)
+    go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t </> (nest 2 $ go 0 names u)
 
 -- public export
 -- data Closure : Nat -> Type
@@ -256,9 +262,11 @@ Show Closure
 
 covering export
 Show Val where
-  show (VVar _ k sp) = "(%var \{show k} \{unwords $ map show (sp <>> [])})"
+  show (VVar _ k [<]) = "%var\{show k}"
-  show (VRef _ nm _ sp) = "(%ref \{nm} \{unwords $ map show (sp <>> [])})"
+  show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> [])})"
-  show (VMeta _ ix sp) = "(%meta \{show ix} \{show $ length sp})"
+  show (VRef _ nm _ [<]) = nm
+  show (VRef _ nm _ sp) = "(\{nm} \{unwords $ map show (sp <>> [])})"
+  show (VMeta _ ix sp) = "(%meta \{show ix} ..\{show $ length sp})"
   show (VLam _ str x) = "(%lam \{str} \{show x})"
   show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
   show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"

tests/black/Zoo4eg.newt

@@ -63,13 +63,13 @@ comp : {A : U} {B : A -> U} {C : {a : A} -> B a -> U}
        -> C (g a)
 comp = \f g a => f (g a)
 
--- compExample : Bool
+-- TODO unsolved metas in dependent function composition
+-- compExample : List Bool
 -- compExample = comp (cons true) (cons false) nil
 
 Nat : U
 Nat = (N : U) -> (N -> N) -> N -> N
 
--- TODO - first underscore there, why are there two metas?
 mul : Nat -> Nat -> Nat
 mul = \a b N s z => a _ (b _ s) z