From fe323618e7c5d7378f78057e5b928a8c28167605 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 22 Oct 2024 22:08:34 -0700 Subject: [PATCH] Visible infix info from imports --- TODO.md | 6 ++--- aoc2023/Day1.newt | 17 ------------ aoc2023/Lib.newt | 5 ++++ src/Lib/Parser.idr | 19 ++++++++++--- src/Lib/Parser/Impl.idr | 26 +++++++++++++----- src/Lib/TopContext.idr | 4 +-- src/Lib/Types.idr | 2 +- src/Main.idr | 60 ++++++++++++++++++++++------------------- 8 files changed, 79 insertions(+), 60 deletions(-) diff --git a/TODO.md b/TODO.md index 56e7b4f..b90cb4c 100644 --- a/TODO.md +++ b/TODO.md @@ -1,10 +1,8 @@ ## TODO -- [ ] Remember operators from imports - - This one is tricky because we need to parse to get imports, but can't parse expressions until we've loaded imports. - - It could be handled by parsing and processing one declaration at a time. We would want this with memoization to do Lean-style incremental builds, but we're not at the LSP stage yet. -- [ ] Default cases (currently gets expanded to all constructors) +- [x] Remember operators from imports +- [ ] Default cases for non-primitives (currently gets expanded to all constructors) - [x] Case for primitives - [ ] aoc2023 translation - [x] day1 diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt index 5c6c666..d678bf0 100644 --- a/aoc2023/Day1.newt +++ b/aoc2023/Day1.newt @@ -1,23 +1,6 @@ module Day1 import Lib -ptype Int - --- TODO fix import of fixity declarations -infixr 4 _::_ -infixl 3 _<_ -infixl 4 _-_ -infixl 4 _+_ -infixl 5 _*_ -infixl 5 _/_ -infixr 0 _$_ --- Code - - -infixl 7 _._ -_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C -(f . g) x = f ( g x) - digits1 : List Char -> List Int digits1 Nil = Nil diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt index 1259e34..071f788 100644 --- a/aoc2023/Lib.newt +++ b/aoc2023/Lib.newt @@ -131,3 +131,8 @@ foldl f acc (x :: xs) = foldl f (f acc x) xs map : {A B : U} -> (A -> B) -> List A -> List B map f Nil = Nil map f (x :: xs) = f x :: map f xs + + +infixl 7 _._ +_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C +(f . g) x = f ( g x) diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 17903e3..739c81e 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -90,6 +90,10 @@ parseApp = do rest <- many pArg pure $ foldl (\a, (icit,fc,b) => RApp fc a b icit) hd rest +lookup : String -> List OpDef -> Maybe OpDef +lookup _ [] = Nothing +lookup name (op :: ops) = if op.name == name then Just op else lookup name ops + parseOp : Parser Raw parseOp = parseApp >>= go 0 where @@ -100,7 +104,7 @@ parseOp = parseApp >>= go 0 op <- token Oper ops <- getOps let op' = "_" ++ op ++ "_" - let Just (p,fix) = lookup op' ops + let Just (MkOp _ p fix) = lookup op' ops -- this is eaten, but we need `->` and `:=` to not be an operator to have fatal here | Nothing => case op of -- Location is poor on these because we pull off of the remaining token list... @@ -320,12 +324,21 @@ export parseDecl : Parser Decl parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseNorm <|> parseData <|> (try $ parseSig) <|> parseDef + +export +parseModHeader : Parser String +parseModHeader = sameLevel (keyword "module") >> uident + +export +parseImports : Parser (List Import) +parseImports = manySame $ parseImport + export parseMod : Parser Module parseMod = do - keyword "module" - name <- uident startBlock $ do + keyword "module" + name <- uident imports <- manySame $ parseImport decls <- manySame $ parseDecl pure $ MkModule name imports decls diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 1f2ae6c..7f119eb 100644 --- a/src/Lib/Parser/Impl.idr +++ b/src/Lib/Parser/Impl.idr @@ -49,11 +49,18 @@ showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ g else if line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs else go (l + 1) xs +public export +record OpDef where + constructor MkOp + name : String + prec : Int + fix : Fixity + -- Result of a parse public export data Result : Type -> Type where - OK : a -> (toks : TokenList) -> (com : Bool) -> List (String, Int, Fixity) -> Result a - Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> List (String, Int, Fixity) -> Result a + OK : a -> (toks : TokenList) -> (com : Bool) -> List OpDef -> Result a + Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> List OpDef -> Result a export Functor Result where @@ -74,10 +81,10 @@ Functor Result where -- This is a Reader in FC, a State in Operators, Commit flag, TokenList export -data Parser a = P (TokenList -> Bool -> List (String, Int, Fixity) -> (lc : FC) -> Result a) +data Parser a = P (TokenList -> Bool -> List OpDef -> (lc : FC) -> Result a) export -runP : Parser a -> TokenList -> Bool -> List (String, Int, Fixity) -> FC -> Result a +runP : Parser a -> TokenList -> Bool -> List OpDef -> FC -> Result a runP (P f) = f error : TokenList -> String -> Error @@ -91,6 +98,13 @@ parse pa toks = case runP pa toks False [] (-1,-1) of OK a [] _ _ => Right a OK a ts _ _ => Left (error ts "Extra toks") +||| Intended for parsing a top level declaration +export +partialParse : Parser a -> List OpDef -> TokenList -> Either Error (a, List OpDef, TokenList) +partialParse pa ops toks = case runP pa toks False ops (0,0) of + Fail fatal err toks com ops => Left err + OK a ts _ ops => Right (a,ops,ts) + -- I think I want to drop the typeclasses for v1 export @@ -108,13 +122,13 @@ fatal : String -> Parser a fatal msg = P $ \toks,com,ops,col => Fail True (error toks msg) toks com ops export -getOps : Parser (List (String, Int, Fixity)) +getOps : Parser (List OpDef) getOps = P $ \ toks, com, ops, col => OK ops toks com ops export addOp : String -> Int -> Fixity -> Parser () addOp nm prec fix = P $ \ toks, com, ops, col => - OK () toks com ((nm, prec, fix) :: ops) + OK () toks com ((MkOp nm prec fix) :: ops) export Functor Parser where diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index 548152f..a6d4827 100644 --- a/src/Lib/TopContext.idr +++ b/src/Lib/TopContext.idr @@ -19,11 +19,11 @@ lookup nm top = go top.defs export covering Show TopContext where - show (MkTop defs metas _ _ _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" + show (MkTop defs metas _ _ _ _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" public export empty : HasIO m => m TopContext -empty = pure $ MkTop [] !(newIORef (MC [] 0)) False !(newIORef []) [] +empty = pure $ MkTop [] !(newIORef (MC [] 0)) False !(newIORef []) [] [] ||| set or replace def. probably need to check types and Axiom on replace public export diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index b35ec86..084b2a4 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -366,7 +366,7 @@ record TopContext where errors : IORef (List Error) ||| loaded modules loaded : List String - + ops : List OpDef -- we'll use this for typechecking, but need to keep a TopContext around too. public export diff --git a/src/Main.idr b/src/Main.idr index 3707912..c7aefd2 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -38,7 +38,6 @@ dumpContext top = do go [] = pure () go (x :: xs) = putStrLn " \{show x}" >> go xs - writeSource : String -> M () writeSource fn = do docs <- compile @@ -50,50 +49,57 @@ writeSource fn = do Right _ <- chmodRaw fn 493 | Left err => fail (show err) pure () -parseFile : String -> M (String,Module) -parseFile fn = do +||| New style loader, one def at a time +processModule : String -> List String -> String -> M String +processModule base stk name = do + top <- get + let False := elem name top.loaded | _ => pure "" + modify { loaded $= (name::) } + let fn = base ++ "/" ++ name ++ ".newt" Right src <- readFile $ fn | Left err => fail (show err) let toks = tokenise src - let Right res = parse parseMod toks - | Left y => fail (showError src y) - pure (src, res) -loadModule : String -> List String -> String -> M () -loadModule base stk name = do - top <- get - -- already loaded? - let False := elem name top.loaded | _ => pure () - modify { loaded $= (name::) } - let fn = base ++ "/" ++ name ++ ".newt" - (src, res) <- parseFile fn - putStrLn "module \{res.name}" - let True = name == res.name - | _ => fail "ERROR at (0, 0): module name \{show res.name} doesn't match file name \{show fn}" - -- TODO separate imports and detect loops / redundant - for_ res.imports $ \ (MkImport fc name') => do + let Right (modName, ops, toks) := partialParse parseModHeader top.ops toks + | Left err => fail (showError src err) + + + putStrLn "module \{modName}" + let True = name == modName + | _ => fail "ERROR at (0, 0): module name \{show modName} doesn't match file name \{show fn}" + + let Right (imports, ops, toks) := partialParse parseImports ops toks + | Left err => fail (showError src err) + + for_ imports $ \ (MkImport fc name') => do -- we could use `fc` if it had a filename in it - when (name' `elem` stk) $ error emptyFC "import loop \{show name} -> \{show name'}" - loadModule base (name :: stk) name' - -- TODO Lift the error exit, so import errors can get a FC in current file + when (name' `elem` stk) $ error emptyFC "import loop \{show name} -> \{show name'}" + processModule base (name :: stk) name' + + top <- get + let Right (decls, ops, toks) := partialParse (manySame parseDecl) top.ops toks + | Left err => fail (showError src err) + let [] := toks | (x :: xs) => fail "extra toks" -- FIXME FC from xs + + modify { ops := ops } + putStrLn "process Decls" - Right _ <- tryError $ traverse_ processDecl (collectDecl res.decls) + Right _ <- tryError $ traverse_ processDecl (collectDecl decls) | Left y => fail (showError src y) - pure () + pure src processFile : String -> M () processFile fn = do putStrLn "*** Process \{fn}" - (src, res) <- parseFile fn - putStrLn "module \{res.name}" let parts = splitPath fn let file = fromMaybe "" $ last' parts let dir = fromMaybe "./" $ parent fn let (name,ext) = splitFileName (fromMaybe "" $ last' parts) putStrLn "\{show dir} \{show name} \{show ext}" - loadModule dir [] name + + src <- processModule dir [] name top <- get -- dumpContext top