Generic instances for tuples, error recovery, show details when multiple solutions

src/Lib/Parser/Impl.idr

@@ -55,9 +55,9 @@ parse fn pa toks = case runP pa toks False empty (MkFC fn (-1,-1)) of
 
 ||| Intended for parsing a top level declaration
 export
-partialParse : String -> Parser a -> Operators -> TokenList -> Either Error (a, Operators, TokenList)
+partialParse : String -> Parser a -> Operators -> TokenList -> Either (Error, TokenList) (a, Operators, TokenList)
 partialParse fn pa ops toks = case runP pa toks False ops (MkFC fn (0,0)) of
-  Fail fatal err toks com ops => Left err
+  Fail fatal err toks com ops => Left (err, toks)
   OK a ts _ ops => Right (a,ops,ts)
 
 -- I think I want to drop the typeclasses for v1

src/Lib/ProcessDecl.idr

@@ -108,7 +108,6 @@ solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
         | res => do
           debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
           solveAutos mstart es
-        -- | res => error fc "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}"
       writeIORef top.metas mc
       val <- eval ctx.env CBN tm
       debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
@@ -153,6 +152,7 @@ logMetas mstart = do
       env <- dumpEnv ctx
       let msg = "\{env}  -----------\n  \{pprint names ty'}"
       info fc "User Hole\n\{msg}"
+
     (Unsolved fc k ctx ty kind cons) => do
       tm <- quote ctx.lvl !(forceMeta ty)
       -- Now that we're collecting errors, maybe we simply check at the end
@@ -161,7 +161,21 @@ logMetas mstart = do
       let msg = "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
       msgs <- for cons $ \ (MkMc fc env sp val) => do
             pure "  * (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}"
-      addError $ E fc $ unlines ([msg] ++ msgs)
+      sols <- case kind of
+        AutoSolve => do
+          x <- quote ctx.lvl ty
+          ty <- eval ctx.env CBN x
+          debug "AUTO ---> \{show ty}"
+          -- we want the context here too.
+          top <- get
+          matches <- case !(contextMatches ctx ty) of
+            [] => findMatches ctx ty top.defs
+            xs => pure xs
+          -- TODO try putting mc into TopContext for to see if it gives better terms
+          pure $ "  \{show $ length matches} Solutions:" :: map (("  " ++) . interpolate . pprint (names ctx) . fst) matches
+
+        _ => pure []
+      addError $ E fc $ unlines ([msg] ++ msgs ++ sols)
 
 
 export

src/Lib/TopContext.idr

@@ -65,5 +65,7 @@ updateDef name fc ty def = do
 
 
 public export
-addError : HasIO io => {auto top : TopContext} -> Error -> io ()
-addError err = modifyIORef top.errors (err ::)
+addError : Error -> M ()
+addError err = do
+  top <- get
+  modifyIORef top.errors (err ::)

src/Main.idr

@@ -66,6 +66,21 @@ writeSource fn = do
   Right _ <- chmodRaw fn 493 | Left err => fail (show err)
   pure ()
 
+
+parseDecls : String -> Operators -> TokenList -> SnocList Decl -> M (List Decl, Operators)
+parseDecls fn ops [] acc = pure (acc <>> [], ops)
+parseDecls fn ops toks acc =
+  case partialParse fn (sameLevel parseDecl) ops toks of
+    Left (err, toks) => do
+      putStrLn $ showError "" err
+      addError err
+      parseDecls fn ops (recover toks) acc
+    Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl)
+  where
+    recover : TokenList -> TokenList
+    recover [] = []
+    recover (tok :: toks) = if tok.bounds.startCol == 0 then (tok :: toks) else recover toks
+
 ||| New style loader, one def at a time
 processModule : String -> List String -> String -> M String
 processModule base stk name = do
@@ -79,7 +94,7 @@ processModule base stk name = do
     | Left err => fail (showError src err)
 
   let Right ((nameFC, modName), ops, toks) := partialParse fn parseModHeader top.ops toks
-    | Left err => fail (showError src err)
+    | Left (err, toks) => fail (showError src err)
 
 
   putStrLn "module \{modName}"
@@ -87,7 +102,7 @@ processModule base stk name = do
     | _ => fail "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}"
 
   let Right (imports, ops, toks) := partialParse fn parseImports ops toks
-    | Left err => fail (showError src err)
+    | Left (err, toks) => fail (showError src err)
 
   for_ imports $ \ (MkImport fc name') => do
     -- we could use `fc` if it had a filename in it
@@ -100,18 +115,24 @@ processModule base stk name = do
   -- REVIEW suppressing unsolved and solved metas from previous files
   -- I may want to know about (or fail early on) unsolved
   let mstart = length mc.metas
-  let Right (decls, ops, toks) := partialParse fn (manySame parseDecl) top.ops toks
-    | Left err => fail (showError src err)
-  let [] := toks
-    | (x :: xs) =>
-        fail (showError src (E (MkFC fn (startBounds x.bounds)) "extra toks"))
+  -- let Right (decls, ops, toks) := partialParse fn (manySame parseDecl) top.ops toks
+  --   | Left (err, toks) => fail (showError src err)
+  (decls, ops) <- parseDecls fn top.ops toks [<]
   modify { ops := ops }
 
   putStrLn "process Decls"
-  Right _ <- tryError $ traverse_ processDecl (collectDecl decls)
-    | Left y => fail (showError src y)
+
+  traverse_ tryProcessDecl (collectDecl decls)
   if (stk == []) then logMetas mstart else pure ()
   pure src
+  where
+
+    -- parseDecls :
+    -- tryParseDecl :
+    tryProcessDecl : Decl -> M ()
+    tryProcessDecl decl = do
+      Left err <- tryError {e=Error} $ processDecl decl | _ => pure ()
+      addError err
 
 processFile : String -> M ()
 processFile fn = do