From 1a05043922aa4d9967055e706bea691743071e30 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 16 Dec 2024 21:05:43 -0800 Subject: [PATCH] Generic instances for tuples, error recovery, show details when multiple solutions --- TODO.md | 6 ++++-- aoc2023/Aoc.newt | 10 ++++++---- aoc2024/Day16.newt | 13 ------------- aoc2024/Day6.newt | 12 +++--------- newt/Prelude.newt | 5 +++++ src/Lib/Parser/Impl.idr | 4 ++-- src/Lib/ProcessDecl.idr | 18 ++++++++++++++++-- src/Lib/TopContext.idr | 6 ++++-- src/Main.idr | 39 ++++++++++++++++++++++++++++++--------- vim/compiler/newt.vim | 3 ++- vim/ftplugin/newt.vim | 1 + 11 files changed, 73 insertions(+), 44 deletions(-) diff --git a/TODO.md b/TODO.md index 34c700d..88291b7 100644 --- a/TODO.md +++ b/TODO.md @@ -3,8 +3,10 @@ More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff. -- [ ] Move on to next decl in case of error - - [ ] for parse error, seek to col 0 token +- [x] Move on to next decl in case of error +- [x] for parse error, seek to col 0 token and process next decl +- [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality) +- [ ] Keep a `compare` function on `SortedMap` (like lean) - [ ] keymap for monaco - [x] SortedMap.newt issue in `where` - [x] fix "insufficient patterns", wire in M or Either String diff --git a/aoc2023/Aoc.newt b/aoc2023/Aoc.newt index 7cd501d..6b5f55e 100644 --- a/aoc2023/Aoc.newt +++ b/aoc2023/Aoc.newt @@ -40,8 +40,10 @@ instance Add Point where instance Sub Point where (a,b) - (c,d) = (a - c, b - d) -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d -instance Eq Point where - (a,b) == (c,d) = a == c && b == d + +-- instance Ord Point where +-- (a,b) < (c,d) = a < c || a == c && b < d + +-- instance Eq Point where +-- (a,b) == (c,d) = a == c && b == d diff --git a/aoc2024/Day16.newt b/aoc2024/Day16.newt index f76adac..9209a38 100644 --- a/aoc2024/Day16.newt +++ b/aoc2024/Day16.newt @@ -81,22 +81,9 @@ instance Ord Dir where instance Eq Dir where a == b = dirVal a == dirVal b -instance Eq DPoint where - (a,b) == (c,d) = a == c && b == d - -instance Ord DPoint where - (a,b) < (c,d) = a < c || a == c && b < d - - Cand : U Cand = Int × Point × Dir -instance Eq Cand where - (s,pt) == (s',pt') = s == s' && pt == pt' - -instance Ord Cand where - (s,pt) < (s',pt') = s < s' || s == s' && pt < pt' - min : Int → Int → Int min x y = if x < y then x else y diff --git a/aoc2024/Day6.newt b/aoc2024/Day6.newt index 797cabc..6be5533 100644 --- a/aoc2024/Day6.newt +++ b/aoc2024/Day6.newt @@ -24,18 +24,12 @@ instance Show Dir where show South = "S" show West = "W" +instance Eq Dir where + a == b = show a == show b + instance Ord Dir where a < b = show a < show b -instance Eq (Point × Dir) where - (a,b) == (c,d) = a == c && show b == show d - -instance Ord (Point × Dir) where - (a,b) < (c,d) = - if a < c then True - else if a /= c then False - else b < d - Done : U Done = SortedMap (Point × Dir) Unit diff --git a/newt/Prelude.newt b/newt/Prelude.newt index bc63b98..201bee8 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -746,4 +746,9 @@ instance Show Char where swap : ∀ a b. a × b → b × a swap (a,b) = (b,a) +instance ∀ a b. {{Eq a}} {{Eq b}} → Eq (a × b) where + (a,b) == (c,d) = a == c && b == d + +instance ∀ a b. {{Eq a}} {{Ord a}} {{Ord b}} → Ord (a × b) where + (a,b) < (c,d) = if a == c then b < d else a < c diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 4efac50..67eb9dc 100644 --- a/src/Lib/Parser/Impl.idr +++ b/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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index bc33de0..f7b6b46 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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 diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index 639ad50..fc2ca72 100644 --- a/src/Lib/TopContext.idr +++ b/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 ::) diff --git a/src/Main.idr b/src/Main.idr index 11b1247..a4f8578 100644 --- a/src/Main.idr +++ b/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 diff --git a/vim/compiler/newt.vim b/vim/compiler/newt.vim index 602932f..786f533 100644 --- a/vim/compiler/newt.vim +++ b/vim/compiler/newt.vim @@ -7,4 +7,5 @@ endif CompilerSet makeprg=newt " doesn't work -CompilerSet errorformat=ERROR\ at\ (%l,\ %c) +setlocal errorformat=ERROR\ at\ %f:(%l\,\ %c):\ %m,%-G%.%# + diff --git a/vim/ftplugin/newt.vim b/vim/ftplugin/newt.vim index 80e4e8e..54855c3 100644 --- a/vim/ftplugin/newt.vim +++ b/vim/ftplugin/newt.vim @@ -1,4 +1,5 @@ setlocal syntax=newt +setlocal comments=s1:/-,mb:*,ex:-/,:-- setlocal commentstring=--\ %s setlocal expandtab setlocal tabstop=2