From bca61f95a07bce953ca8cc2f089c6d9728d9fc63 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 7 Feb 2026 16:55:33 -0800 Subject: [PATCH] Improve error locations --- TODO.md | 4 ++-- src/Lib/Parser.newt | 15 ++++++++------- src/Lib/ProcessDecl.newt | 34 +++++++++++++++++----------------- src/Lib/Syntax.newt | 22 +++++++++++----------- src/Main.newt | 10 ++++------ tests/BadImport.newt | 4 ++++ tests/BadImport.newt.fail | 2 ++ tests/ErrorDup.newt | 9 +++++++++ tests/ErrorDup.newt.fail | 21 +++++++++++++++++++++ 9 files changed, 78 insertions(+), 43 deletions(-) create mode 100644 tests/BadImport.newt create mode 100644 tests/BadImport.newt.fail create mode 100644 tests/ErrorDup.newt create mode 100644 tests/ErrorDup.newt.fail diff --git a/TODO.md b/TODO.md index 38915a7..db61130 100644 --- a/TODO.md +++ b/TODO.md @@ -7,8 +7,8 @@ - [ ] maybe allow "Main" module name for any file - [ ] Improve handling of names: - We need FC on names in a lot of places - - [ ] FC for duplicate data constructor name is wrong (points to `data`) - - [ ] FC on bad import should point to the name + - [x] FC for duplicate `data`, `record`, `class` name is wrong (points to `data`) + - [x] FC on bad import should point to the name - [x] Current module overrides imports - [ ] Allow Qualified names in surface syntax - Don't disambiguate on type for now diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index ab8d8c6..f9463c1 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -533,10 +533,11 @@ parseImport : Parser Import parseImport = do fc <- getPos keyword "import" - ident <- uident - rest <- many $ token Projection + -- TODO revisit when we have parser for qualified names in source + (nameFC, ident) <- withFC uident + (restFC,rest) <- withFC $ many $ token Projection let name = joinBy "" (ident :: rest) - pure $ MkImport fc name + pure $ MkImport fc (nameFC + restFC, name) -- Do we do pattern stuff now? or just name = lambda? -- TODO multiple names @@ -613,7 +614,7 @@ parseData : Parser Decl parseData = do fc <- getPos -- commit when we hit ":" - name <- try $ (keyword "data" *> (uident <|> ident <|> token MixFix) <* keyword ":") + name <- try $ (keyword "data" *> withFC (uident <|> token MixFix) <* keyword ":") ty <- typeExpr Just _ <- optional (keyword "where") | _ => pure $ Data fc name ty Nothing @@ -632,10 +633,10 @@ parseRecord : Parser Decl parseRecord = do fc <- getPos keyword "record" - name <- uident + name <- withFC uident teles <- many $ ebind <|> nakedBind keyword "where" - cname <- optional $ keyword "constructor" *> (uident <|> token MixFix) + cname <- optional $ keyword "constructor" *> withFC (uident <|> token MixFix) decls <- startBlock $ manySame $ parseSig pure $ Record fc name (join teles) cname decls @@ -645,7 +646,7 @@ parseClass : Parser Decl parseClass = do fc <- getPos keyword "class" - name <- uident + name <- withFC uident teles <- many $ ebind <|> nakedBind keyword "where" decls <- startBlock $ manySame $ parseSig diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 0e29fae..a9f91ec 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -209,8 +209,8 @@ processCheck ns fc tm ty = do putStrLn " NF \{render 90 $ pprint Nil norm}" -processClass : List String → FC → String → Telescope → List Decl → M Unit -processClass ns classFC nm tele decls = do +processClass : List String → FC → (FC × String) → Telescope → List Decl → M Unit +processClass ns classFC (nameFC, nm) tele decls = do -- REVIEW maybe we can leverage Record for this -- a couple of catches, we don't want the dotted accessors and -- the self argument should be an auto-implicit @@ -225,7 +225,7 @@ processClass ns classFC nm tele decls = do log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}" log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}" - let decl = Data classFC nm tcType (Just $ TypeSig classFC (dcName :: Nil) dcType :: Nil) + let decl = Data classFC (nameFC, nm) tcType (Just $ TypeSig classFC (dcName :: Nil) dcType :: Nil) log 1 $ \ _ => "Decl:" log 1 $ \ _ => render 90 $ pretty decl processDecl ns decl @@ -374,10 +374,10 @@ processInstance ns instfc ty decls = do -- desugars to Data and processes it processShortData : List String → FC → Raw → List Raw → M Unit processShortData ns fc lhs sigs = do - (nm,args) <- getArgs lhs Nil + (nameFC, nm,args) <- getArgs lhs Nil let ty = foldr mkPi (RU fc) args cons <- traverse (mkDecl args Nil) sigs - let dataDecl = Data fc nm ty (Just cons) + let dataDecl = Data fc (nameFC, nm) ty (Just cons) log 1 $ \ _ => "SHORTDATA" log 1 $ \ _ => "\{render 90 $ pretty dataDecl}" processDecl ns dataDecl @@ -385,8 +385,8 @@ processShortData ns fc lhs sigs = do mkPi : FC × Name → Raw → Raw mkPi (fc,n) a = RPi fc (BI fc n Explicit Zero) (RU fc) a - getArgs : Raw -> List (FC × String) -> M (String × List (FC × String)) - getArgs (RVar fc1 nm) acc = pure (nm, acc) + getArgs : Raw -> List (FC × String) -> M (FC × String × List (FC × String)) + getArgs (RVar fc1 nm) acc = pure (fc1, nm, acc) getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc) getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}" @@ -431,8 +431,8 @@ populateConInfo entries = isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ _ (Many :: Nil) hn) _) = a == b isSucc _ = False -processData : List String → FC → String → Raw → List Decl → M Unit -processData ns fc nm ty cons = do +processData : List String → FC → FC × String → Raw → List Decl → M Unit +processData ns fc (nameFC, nm) ty cons = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Data \{nm}" top <- getTop @@ -443,7 +443,7 @@ processData ns fc nm ty cons = do tyty' <- eval Nil tyty type' <- eval Nil type unifyCatch fc (mkCtx fc) tyty' type' - Just _ => error fc "\{show nm} already declared" + Just _ => error nameFC "\{show nm} already declared" Nothing => setDef (QN ns nm) fc tyty Axiom Nil -- check cons, return list of type,con allCons <- join <$> (for cons $ \x => case x of @@ -487,25 +487,25 @@ processData ns fc nm ty cons = do checkDeclType _ = error fc "data type doesn't return U" -processRecord : List String → FC → String → Telescope → Maybe Name → List Decl → M Unit -processRecord ns recordFC nm tele cname decls = do +processRecord : List String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit +processRecord ns recordFC (nameFC, nm) tele cname decls = do log 1 $ \ _ => "-----" log 1 $ \ _ => "Record" let fields = getSigs decls - let dcName = fromMaybe "Mk\{show nm}" cname + let (dcFC,dcName) = fromMaybe (nameFC,"Mk\{show nm}") cname let tcType = teleToPi tele (RU recordFC) - let tail = foldl (\ acc bi => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele + let tail = foldl (\ acc bi => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar nameFC nm) tele let dcType = teleToPi (impTele tele) $ foldr (\ x acc => case x : FC × String × Raw of (fc, nm, ty) => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}" log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}" - let decl = Data recordFC nm tcType (Just $ TypeSig recordFC (dcName :: Nil) dcType :: Nil) + let decl = Data recordFC (nameFC,nm) tcType (Just $ TypeSig recordFC (dcName :: Nil) dcType :: Nil) log 1 $ \ _ => "Decl:" log 1 $ \ _ => render 90 $ pretty decl processDecl ns decl -- pattern to peel out fields on LHS - let autoPat = foldl (\acc x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields + let autoPat = foldl (\acc x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar nameFC nm) Explicit) (RVar nameFC dcName) fields processFields autoPat tail Nil fields where processFields : Raw → Raw → List (String × Raw) → List (FC × String × Raw) → M Unit @@ -542,5 +542,5 @@ processDecl ns (Instance instfc ty decls) = processInstance ns instfc ty decls processDecl ns (ShortData fc lhs sigs) = processShortData ns fc lhs sigs processDecl ns (Data fc nm ty (Just cons)) = processData ns fc nm ty cons -- TODO distinguish from function signatures -processDecl ns (Data fc nm ty Nothing) = processTypeSig ns fc (nm :: Nil) ty +processDecl ns (Data fc (_, nm) ty Nothing) = processTypeSig ns fc (nm :: Nil) ty processDecl ns (Record recordFC nm tele cname decls) = processRecord ns recordFC nm tele cname decls diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index 47388c9..976c932 100644 --- a/src/Lib/Syntax.newt +++ b/src/Lib/Syntax.newt @@ -74,7 +74,7 @@ instance HasFC Raw where getFC (RUpdateRec fc _ _) = fc getFC (RImpossible fc) = fc -data Import = MkImport FC Name +data Import = MkImport FC (FC × Name) Telescope : U Telescope = List (BindInfo × Raw) @@ -84,14 +84,14 @@ data Decl | FunDef FC Name (List (Raw × Maybe Raw)) | DCheck FC Raw Raw -- TODO maybe add Telescope (before `:`) and auto-add to constructors... - | Data FC Name Raw (Maybe $ List Decl) + | Data FC (FC × Name) Raw (Maybe $ List Decl) | ShortData FC Raw (List Raw) | PType FC Name (Maybe Raw) | PFunc FC Name (List String) Raw String | PMixFix FC (List Name) Int Fixity - | Class FC Name Telescope (List Decl) + | Class FC (FC × Name) Telescope (List Decl) | Instance FC Raw (Maybe (List Decl)) - | Record FC Name Telescope (Maybe Name) (List Decl) + | Record FC (FC × Name) Telescope (Maybe $ FC × Name) (List Decl) instance HasFC Decl where @@ -140,7 +140,7 @@ instance Show Decl where show (ShortData _ lhs sigs) = foo ("ShortData" :: show lhs :: show sigs :: Nil) show (PFunc _ nm used ty src) = foo ("PFunc" :: nm :: show used :: show ty :: show src :: Nil) show (PMixFix _ nms prec fix) = foo ("PMixFix" :: show nms :: show prec :: show fix :: Nil) - show (Class _ nm tele decls) = foo ("Class" :: nm :: "..." :: (show $ map show decls) :: Nil) + show (Class _ (_,nm) tele decls) = foo ("Class" :: nm :: "..." :: (show $ map show decls) :: Nil) show (Instance _ nm decls) = foo ("Instance" :: show nm :: (show $ map show decls) :: Nil) show (Record _ nm tele nm1 decls) = foo ("Record" :: show nm :: show tele :: show nm1 :: show decls :: Nil) @@ -245,16 +245,16 @@ instance Pretty Decl where prettyPair : Raw × Maybe Raw → Doc prettyPair (a, Nothing) = pretty a prettyPair (a, Just b) = pretty a <+> text "=" <+> pretty b - pretty (Data _ nm x Nothing) = text "data" <+> text nm <+> text ":" <+> pretty x - pretty (Data _ nm x (Just xs)) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) + pretty (Data _ (_,nm) x Nothing) = text "data" <+> text nm <+> text ":" <+> pretty x + pretty (Data _ (_,nm) x (Just xs)) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty) 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 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) + 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 (snd 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)) pretty (Instance _ _ _) = text "TODO pretty Instance" pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) @@ -328,5 +328,5 @@ instance Pretty Module where stack (map pretty decls) where doImport : Import -> Doc - doImport (MkImport _ nm) = text "import" <+> text nm ++ line + doImport (MkImport _ (_,nm)) = text "import" <+> text nm ++ line diff --git a/src/Main.newt b/src/Main.newt index 08f3a8b..a6527fc 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -94,7 +94,7 @@ importHints (entry :: entries) = do importHints entries importToQN : Import → QName -importToQN (MkImport fc name') = uncurry QN $ unsnoc $ split1 name' "." +importToQN (MkImport fc (_,name)) = uncurry QN $ unsnoc $ split1 name "." -- New style loader, one def at a time processModule : FC -> String -> List String -> QName -> M String @@ -128,13 +128,11 @@ processModule importFC base stk qn@(QN ns nm) = do let importNames = map importToQN imports imported <- for imports $ \case - MkImport fc name' => do + MkImport fc (nameFC,name') => do let (a,b) = unsnoc $ split1 name' "." let qname = QN a b - -- we could use `fc` if it had a filename in it - when (elem name' stk) $ \ _ => error emptyFC "import loop \{show name} -> \{show name'}" - - processModule fc base (name :: stk) qname + when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} -> \{show name'}" + processModule nameFC base (name :: stk) qname pure $ split name' "." let imported = snoc imported primNS srcSum <- liftIO $ checksum src diff --git a/tests/BadImport.newt b/tests/BadImport.newt new file mode 100644 index 0000000..46cdbcf --- /dev/null +++ b/tests/BadImport.newt @@ -0,0 +1,4 @@ +module BadImport + +-- Error should point to name here +import Does.Not.Exist diff --git a/tests/BadImport.newt.fail b/tests/BadImport.newt.fail new file mode 100644 index 0000000..bf04b4b --- /dev/null +++ b/tests/BadImport.newt.fail @@ -0,0 +1,2 @@ +*** Process tests/BadImport.newt +ERROR at tests/BadImport.newt:4:8--4:22: error reading tests/Does/Not/Exist.newt: Error: ENOENT: no such file or directory, open 'tests/Does/Not/Exist.newt' diff --git a/tests/ErrorDup.newt b/tests/ErrorDup.newt new file mode 100644 index 0000000..fc5c219 --- /dev/null +++ b/tests/ErrorDup.newt @@ -0,0 +1,9 @@ +module ErrorDup + +data Nat = Z | S Nat + +data Nat = Z | S Nat + +record Nat where + +class Nat where diff --git a/tests/ErrorDup.newt.fail b/tests/ErrorDup.newt.fail new file mode 100644 index 0000000..3d02085 --- /dev/null +++ b/tests/ErrorDup.newt.fail @@ -0,0 +1,21 @@ +*** Process tests/ErrorDup.newt +module ErrorDup +ERROR at tests/ErrorDup.newt:5:6--5:9: Nat already declared + data Nat = Z | S Nat + + data Nat = Z | S Nat + ^^^ + +ERROR at tests/ErrorDup.newt:7:8--7:11: Nat already declared + data Nat = Z | S Nat + + record Nat where + ^^^ + +ERROR at tests/ErrorDup.newt:9:7--9:10: Nat already declared + record Nat where + + class Nat where + ^^^ + +Compile failed