More porting. Parser is working now. Some improvements have been made to auto resolution

TODO.md

@@ -23,9 +23,10 @@ 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.
+  - ~~`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.
+  - I've gotten it to the point where things are solved for good code, but it still does poorly when there is an error. (Auto fails to solve and it doesn't get far enough to report error.)
 - [ ] add error for non-linear pattern
 - [ ] typeclass dependencies
   - need to flag internal functions to not search (or flag functions for search). I need to decide on syntax for this.

done/Data/String.newt

@@ -9,3 +9,5 @@ class Interpolation a where
 unwords : List String → String
 unwords stuff = joinBy " " stuff
 
+instance Cast String Int where
+  cast = stringToInt

done/Lib/Parser/Impl.newt

@@ -139,7 +139,11 @@ commit = P $ \toks com ops col => OK MkUnit toks True ops
 
 some : ∀ a. Parser a -> Parser (List a)
 many : ∀ a. Parser a -> Parser (List a)
-some p = _::_ <$> p <*> many p
+
+some p = do
+  x <- p
+  xs <- many p
+  pure (x :: xs)
 many p = some p <|> pure Nil
 
 -- one or more `a` seperated by `s`

done/Lib/Syntax.newt

@@ -115,8 +115,8 @@ data Decl
   | PFunc FC Name (List String) Raw String
   | PMixFix FC (List Name) Int Fixity
   | Class FC Name Telescope (List Decl)
-  | Instance FC Raw (List Decl)
+  | Instance FC Raw (Maybe (List Decl))
-  | Record FC Name Telescope (Maybe Name) (Maybe (List Decl))
+  | Record FC Name Telescope (Maybe Name) (List Decl)
 
 
 instance HasFC Decl where
@@ -277,8 +277,7 @@ instance Pretty Decl where
   pretty (PFunc _ nm Nil ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))
   pretty (PFunc _ nm used ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text used) <+> 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 Nothing) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
+  pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
-  pretty (Record _ nm tele cname (Just 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 <+> text ":" <+> spread (map prettyBind tele)
     <+> (nest 2 $ text "where" </> stack (map pretty decls))

done/Lib/Types.newt

@@ -403,23 +403,26 @@ record M a where
   runM : TopContext -> IO (Either Error (TopContext × a))
 
 instance Functor M where
-  map f (MkM run) = MkM $ \tc => bind {IO} (run tc) $ \case
+  map f (MkM run) = MkM $ \tc => do
-      Left err => pure $ Left err
+    (Right (tc', a))  <- (run tc)
-      Right (tc', a) => pure $ Right (tc', f a)
+      | Left err => pure $ Left err
+    pure $ Right (tc', f a)
 
 instance Applicative M where
   return x = MkM $ \tc => pure $ Right (tc, x)
-  (MkM f) <*> (MkM x) = MkM $ \tc => bind {IO} (f tc) $ \case
+  (MkM f) <*> (MkM x) = MkM $ \tc => do
-      Left err => pure $ Left err
+    Right (tc', f') <- f tc
-      Right (tc', f') => bind {IO} (x tc') $ \case
+      | Left err => pure $ Left err
-          Left err => pure $ Left err
+    Right (tc'', x') <- x tc'
-          Right (tc'', x') => pure $ Right (tc'', f' x')
+      | Left err => pure $ Left err
+    pure $ Right (tc'', f' x')
 
 instance Monad M where
   pure = return
-  bind (MkM x) f = MkM $ \tc => bind {IO} (x tc) $ \case
+  bind (MkM x) f = MkM $ \tc => do
-      Left err => pure $ Left err
+    (Right (tc', a)) <- x tc
-      Right (tc', a) => runM (f a) tc'
+      | Left err => pure $ Left err
+    .runM (f a) tc'
 
 instance HasIO M where
   liftIO io = MkM $ \tc => do
@@ -430,9 +433,10 @@ throwError : ∀ a. Error -> M a
 throwError err = MkM $ \_ => pure $ Left err
 
 catchError : ∀ a. M a -> (Error -> M a) -> M a
-catchError (MkM ma) handler = MkM $ \tc => bind {IO} (ma tc) $ \case
+catchError (MkM ma) handler = MkM $ \tc => do
-    Left err => runM (handler err) tc
+  (Right (tc', a)) <- ma tc
-    Right (tc', a) => pure $ Right (tc', a)
+    | Left err => .runM (handler err) tc
+  pure $ Right (tc', a)
 
 tryError : ∀ a. M a -> M (Either Error a)
 tryError ma = catchError (map Right ma) (pure ∘ Left)

src/Lib/Elab.idr

@@ -218,17 +218,42 @@ trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do
       pure True
 trySolveAuto _ = pure False
 
+-- export
+-- solveAutos : Nat -> List MetaEntry -> M ()
+-- solveAutos mstart [] = pure ()
+-- solveAutos mstart (entry :: es) = do
+--       res <- trySolveAuto entry
+--       -- idris is inlining this and blowing stack?
+--       if res
+--         then do
+--           top <- get
+--           mc <- readIORef top.metaCtx
+--           let mlen = length mc.metas `minus` mstart
+--           solveAutos mstart (take mlen mc.metas)
+--         else
+--           solveAutos mstart es
+
+
+-- Called from ProcessDecl, this was popping the stack, the tail call optimization doesn't
+-- handle the traversal of the entire meta list.  I've turned the restart into a trampoline
+-- and filtered it down to unsolved autos.
 export
-solveAutos : Nat -> List MetaEntry -> M ()
+solveAutos : Nat -> M ()
-solveAutos mstart [] = pure ()
+solveAutos mstart = do
-solveAutos mstart (entry :: es) = do
+  top <- get
-      case !(trySolveAuto entry) of
+  mc <- readIORef top.metaCtx
-        False => solveAutos mstart es
+  let mlen = length mc.metas `minus` mstart
-        True => do
+  res <- run $ filter isAuto (take mlen mc.metas)
-          top <- get
+  if res then solveAutos mstart else pure ()
-          mc <- readIORef top.metaCtx
+  where
-          let mlen = length mc.metas `minus` mstart
+    isAuto : MetaEntry -> Bool
-          solveAutos mstart (take mlen mc.metas)
+    isAuto (Unsolved fc k ctx x AutoSolve xs) = True
+    isAuto _ = False
+
+    run : List MetaEntry -> M Bool
+    run Nil = pure False
+    run (e :: es) =
+      if !(trySolveAuto e) then pure True else run es
 
 -- We need to switch to SortedMap here
 export
@@ -379,7 +404,13 @@ solve env m sp t = do
       MkMc fc env sp rhs => do
         val <- vappSpine soln sp
         debug "discharge l=\{show $ length env} \{(show val)} =?= \{(show rhs)}"
-        unify env Normal val rhs)
+        unify env Normal val rhs
+    mc <- readIORef top.metaCtx
+    -- stack ...
+    -- checkAutos ix mc.metas
+    pure MkUnit
+    )
+
     (\case
       Postpone fc ix msg => do
         -- let someone else solve this and then check again.
@@ -1116,6 +1147,22 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
 
   -- REVIEW We probably need to know this is a VRef before we decide to split on this slot..
   scty' <- unlet ctx.env scty >>= forceType ctx.env
+  -- TODO attempting to pick up Autos that could have been solved immediately
+  -- If we try on creation, we're looping at the moment, because of the possibility
+  -- of Ord a -> Ord b -> Ord (a \x b). Need to cut earlier when solving or switch to
+  -- Idris method...
+  scty' <- case scty' of
+    (VMeta fc1 ix sp) => do
+      case !(lookupMeta ix) of
+        (Solved _ k t) => forceType ctx.env scty'
+        (Unsolved _ k xs _ _ _) => do
+          top <- get
+          mc <- readIORef top.metaCtx
+          ignore $ solveAutos 0
+          forceType ctx.env scty'
+
+    _ => pure scty'
+
   case pat of
     PatCon fc _ _ _ as => do
       -- expand vars that may be solved, eval top level functions

src/Lib/Eval.idr

@@ -17,12 +17,14 @@ eval : Env -> Mode -> Tm -> M Val
 -- It would be nice if the environment were lazy.
 -- e.g. case is getting evaluated when passed to a function because
 -- of dependencies in pi-types, even if the dependency isn't used
+
+public export
+infixl 8 $$
+
 public export
 ($$) : {auto mode : Mode} -> Closure -> Val -> M Val
 ($$) {mode} (MkClosure env tm) u = eval (u :: env) mode tm
 
-public export
-infixl 8 $$
 
 export
 vapp : Val -> Val -> M Val

src/Lib/ProcessDecl.idr

@@ -74,7 +74,8 @@ logMetas mstart = do
           -- pure $ "  \{show $ length matches} Solutions:" :: map (("  " ++) . interpolate . pprint (names ctx) . fst) matches
 
         _ => pure []
-      addError $ E fc $ unlines ([msg] ++ msgs ++ sols)
+      info fc $ unlines ([msg] ++ msgs ++ sols)
+      -- addError $ E fc $ unlines ([msg] ++ msgs ++ sols)
 
 
 -- Used for Class and Record
@@ -155,7 +156,7 @@ processDecl ns (Def fc nm clauses) = do
 
   mc <- readIORef top.metaCtx
   let mlen = length mc.metas `minus` mstart
-  solveAutos mstart (take mlen mc.metas)
+  solveAutos mstart
   -- TODO - make nf that expands all metas and drop zonk
   -- Day1.newt is a test case
   -- tm' <- nf [] tm

src/Main.idr

@@ -139,7 +139,7 @@ processModule importFC base stk qn@(QN ns nm) = do
   -- we don't want implict errors from half-processed functions
   -- but suppress them all on error for simplicity.
   errors <- readIORef top.errors
-  if stk == [] && length errors == 0 then logMetas mstart else pure ()
+  if stk == [] then logMetas mstart else pure ()
   pure src
   where