From b87999a64d94379cdf7b85ce671b37d335c79b61 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 3 Jan 2025 21:57:15 -0800 Subject: [PATCH] More porting. Parser is working now. Some improvements have been made to auto resolution --- TODO.md | 3 +- done/Data/String.newt | 2 ++ done/Lib/Parser/Impl.newt | 6 +++- done/Lib/Syntax.newt | 7 ++-- done/Lib/Types.newt | 32 ++++++++++-------- src/Lib/Elab.idr | 69 ++++++++++++++++++++++++++++++++------- src/Lib/Eval.idr | 6 ++-- src/Lib/ProcessDecl.idr | 5 +-- src/Main.idr | 2 +- 9 files changed, 96 insertions(+), 36 deletions(-) diff --git a/TODO.md b/TODO.md index 2c57467..250ed82 100644 --- a/TODO.md +++ b/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. diff --git a/done/Data/String.newt b/done/Data/String.newt index 25a622c..ccc39f7 100644 --- a/done/Data/String.newt +++ b/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 diff --git a/done/Lib/Parser/Impl.newt b/done/Lib/Parser/Impl.newt index 433c1a0..90f4132 100644 --- a/done/Lib/Parser/Impl.newt +++ b/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` diff --git a/done/Lib/Syntax.newt b/done/Lib/Syntax.newt index 62d0a37..7691be1 100644 --- a/done/Lib/Syntax.newt +++ b/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) - | Record FC Name Telescope (Maybe Name) (Maybe (List Decl)) + | Instance FC Raw (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 (Just decls)) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele) + pretty (Record _ nm tele cname 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)) diff --git a/done/Lib/Types.newt b/done/Lib/Types.newt index 7ffe588..316612a 100644 --- a/done/Lib/Types.newt +++ b/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 - Left err => pure $ Left err - Right (tc', a) => pure $ Right (tc', f a) + map f (MkM run) = MkM $ \tc => do + (Right (tc', a)) <- (run tc) + | 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 - Left err => pure $ Left err - Right (tc', f') => bind {IO} (x tc') $ \case - Left err => pure $ Left err - Right (tc'', x') => pure $ Right (tc'', f' x') + (MkM f) <*> (MkM x) = MkM $ \tc => do + Right (tc', f') <- f tc + | Left err => pure $ Left err + Right (tc'', x') <- x tc' + | 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 - Left err => pure $ Left err - Right (tc', a) => runM (f a) tc' + bind (MkM x) f = MkM $ \tc => do + (Right (tc', a)) <- x 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 - Left err => runM (handler err) tc - Right (tc', a) => pure $ Right (tc', a) +catchError (MkM ma) handler = MkM $ \tc => do + (Right (tc', a)) <- ma tc + | 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) diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 514ccef..fd24b7b 100644 --- a/src/Lib/Elab.idr +++ b/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 mstart [] = pure () -solveAutos mstart (entry :: es) = do - case !(trySolveAuto entry) of - False => solveAutos mstart es - True => do - top <- get - mc <- readIORef top.metaCtx - let mlen = length mc.metas `minus` mstart - solveAutos mstart (take mlen mc.metas) +solveAutos : Nat -> M () +solveAutos mstart = do + top <- get + mc <- readIORef top.metaCtx + let mlen = length mc.metas `minus` mstart + res <- run $ filter isAuto (take mlen mc.metas) + if res then solveAutos mstart else pure () + where + isAuto : MetaEntry -> Bool + 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 diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr index 3ee99cd..2b73789 100644 --- a/src/Lib/Eval.idr +++ b/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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index eb7270c..4701c2d 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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 diff --git a/src/Main.idr b/src/Main.idr index c0ff9e8..bd6842a 100644 --- a/src/Main.idr +++ b/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