diff --git a/TODO.md b/TODO.md index 3ff976e..20119f5 100644 --- a/TODO.md +++ b/TODO.md @@ -42,7 +42,7 @@ - [ ] autos / typeclass resolution - [x] very primitive version in place, not higher order, search at end - [x] monad is now working -- [ ] do blocks (needs typeclass, overloaded functions, or constrain to IO) +- [x] do blocks (needs typeclass, overloaded functions, or constrain to IO) - [x] some solution for `+` problem (classes? ambiguity?) - [x] show compiler failure in the editor (exit code != 0) - [x] write output to file diff --git a/newt/TypeClass.newt b/newt/TypeClass.newt index a0890b3..e47ef14 100644 --- a/newt/TypeClass.newt +++ b/newt/TypeClass.newt @@ -51,4 +51,4 @@ bar x = do let y = x z <- Just x -- This is not sorting out the Maybe... - pure {_} {_} z + pure z diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 9d3a4da..471d3a2 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -74,6 +74,27 @@ makeSpine (S k) (Defined :: xs) = makeSpine k xs makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<] makeSpine 0 xs = ?fixme +solveAutos : Nat -> List MetaEntry -> M () +solveAutos mlen [] = pure () +solveAutos mlen ((Unsolved fc k ctx ty AutoSolve _) :: es) = do + debug "AUTO solving \{show k} : \{show ty}" + -- we want the context here too. + top <- get + [(tm,mc)] <- findMatches ty top.defs + | res => do + debug "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}" + solveAutos mlen 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}" + let sp = makeSpine ctx.lvl ctx.bds + solve ctx ctx.lvl k sp val + mc <- readIORef top.metas + solveAutos mlen (take mlen mc.metas) +solveAutos mlen (_ :: es) = solveAutos mlen es + + export processDecl : Decl -> M () @@ -129,20 +150,7 @@ processDecl (Def fc nm clauses) = do mc <- readIORef top.metas let mlen = length mc.metas `minus` mstart - -- FIXME every time we hit solve in this loop, we need to start over with mc.metas - for_ (take mlen mc.metas) $ \case - (Unsolved fc k ctx ty AutoSolve _) => do - debug "AUTO solving \{show k} : \{show ty}" - -- we want the context here too. - [(tm,mc)] <- findMatches ty top.defs - | 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}" - let sp = makeSpine ctx.lvl ctx.bds - solve ctx ctx.lvl k sp val - pure () - _ => pure () + solveAutos mlen (take mlen mc.metas) tm' <- zonk top 0 [] tm putStrLn "NF \{pprint[] tm'}" diff --git a/tests/black/TypeClass.newt b/tests/black/TypeClass.newt index 21a261b..e28b09c 100644 --- a/tests/black/TypeClass.newt +++ b/tests/black/TypeClass.newt @@ -44,11 +44,10 @@ test : Maybe Int test = pure 10 foo : Int -> Maybe Int -foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10) +foo x = Just 42 >> Just x >>= (\ x => pure 10) bar : Int -> Maybe Int bar x = do let y = x z <- Just x - -- NOW each of these implicits is a different error, fix them - pure {_} {Maybe} z + pure z