Add filenames to FC, relocate errors from other files in playground/vscode

src/Lib/Common.idr

@@ -3,10 +3,20 @@ module Lib.Common
 import Data.String
 import public Data.SortedMap
 
--- I was going to use a record, but we're peeling this off of bounds at the moment.
+
 public export
-FC : Type
-FC = (Int,Int)
+record FC where
+  constructor MkFC
+  file : String
+  start : (Int,Int)
+
+export
+(.line) : FC -> Int
+fc.line = fst fc.start
+
+export
+(.col) : FC -> Int
+fc.col = snd fc.start
 
 public export
 interface HasFC a where
@@ -16,7 +26,7 @@ interface HasFC a where
 
 export
 emptyFC : FC
-emptyFC = (0,0)
+emptyFC = MkFC "" (0,0)
 
 -- Error of a parse
 public export
@@ -25,25 +35,29 @@ data Error
   | Postpone FC Nat String
 %name Error err
 
+export
+Show FC where
+  show fc = "\{fc.file}:\{show fc.start}"
+
 public export
 showError : String -> Error -> String
-showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ go 0 (lines src)
+showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src)
   where
     go : Int -> List String -> String
     go l [] = ""
     go l (x :: xs) =
-      if l == line then
-        "  \{x}\n  \{replicate (cast col) ' '}^\n"
-      else if line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      if l == fc.line then
+        "  \{x}\n  \{replicate (cast fc.col) ' '}^\n"
+      else if fc.line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
       else go (l + 1) xs
-showError src (Postpone (line, col) ix msg) = "ERROR at \{show (line,col)}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
+showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
   where
     go : Int -> List String -> String
     go l [] = ""
     go l (x :: xs) =
-      if l == line then
-        "  \{x}\n  \{replicate (cast col) ' '}^\n"
-      else if line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
+      if l == fc.line then
+        "  \{x}\n  \{replicate (cast fc.col) ' '}^\n"
+      else if fc.line - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
       else go (l + 1) xs
 
 public export

src/Lib/Parser/Impl.idr

@@ -41,21 +41,22 @@ export
 runP : Parser a -> TokenList -> Bool -> Operators -> FC -> Result a
 runP (P f) = f
 
-error : TokenList -> String -> Error
-error [] msg = E emptyFC msg
-error ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (line, col) msg
+-- FIXME no filename, also half the time it is pointing at the token after the error
+error : String -> TokenList -> String -> Error
+error fn [] msg = E (MkFC fn (0,0)) msg
+error fn ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg
 
 export
-parse : Parser a -> TokenList -> Either Error a
-parse pa toks = case runP pa toks False empty (-1,-1) of
+parse : String -> Parser a -> TokenList -> Either Error a
+parse fn pa toks = case runP pa toks False empty (MkFC fn (-1,-1)) of
   Fail fatal err toks com ops => Left err
   OK a [] _ _ => Right a
-  OK a ts _ _ => Left (error ts "Extra toks")
+  OK a ts _ _ => Left (error fn ts "Extra toks")
 
 ||| Intended for parsing a top level declaration
 export
-partialParse : Parser a -> Operators -> TokenList -> Either Error (a, Operators, TokenList)
-partialParse pa ops toks = case runP pa toks False ops (0,0) of
+partialParse : String -> Parser a -> Operators -> TokenList -> Either Error (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
   OK a ts _ ops => Right (a,ops,ts)
 
@@ -69,11 +70,11 @@ try (P pa) = P $ \toks,com,ops,col => case pa toks com ops col of
 
 export
 fail : String -> Parser a
-fail msg = P $ \toks,com,ops,col => Fail False (error toks msg) toks com ops
+fail msg = P $ \toks,com,ops,col => Fail False (error col.file toks msg) toks com ops
 
 export
 fatal : String -> Parser a
-fatal msg = P $ \toks,com,ops,col => Fail True (error toks msg) toks com ops
+fatal msg = P $ \toks,com,ops,col => Fail True (error col.file toks msg) toks com ops
 
 export
 getOps : Parser (Operators)
@@ -125,8 +126,8 @@ Monad Parser where
 pred : (BTok -> Bool) -> String -> Parser String
 pred f msg = P $ \toks,com,ops,col =>
   case toks of
-    (t :: ts) => if f t then OK (value t) ts True ops else Fail False (error toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops
-    [] => Fail False (error toks "\{msg} at EOF") toks com ops
+    (t :: ts) => if f t then OK (value t) ts True ops else Fail False (error col.file toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops
+    [] => Fail False (error col.file toks "\{msg} at EOF") toks com ops
 
 export
 commit : Parser ()
@@ -141,31 +142,33 @@ mutual
 
 export
 getPos : Parser FC
-getPos = P $ \toks,com, ops, (l,c) => case toks of
+getPos = P $ \toks, com, ops, indent => case toks of
   [] => OK emptyFC toks com ops
-  (t :: ts) => OK (start t) toks com ops
+  (t :: ts) => OK (MkFC indent.file (start t)) toks com ops
 
 ||| Start an indented block and run parser in it
 export
 startBlock : Parser a -> Parser a
-startBlock (P p) = P $ \toks,com,ops,(l,c) => case toks of
-  [] => p toks com ops (l,c)
+startBlock (P p) = P $ \toks,com,ops,indent => case toks of
+  [] => p toks com ops indent
   (t :: _) =>
     -- If next token is at or before the current level, we've got an empty block
     let (tl,tc) = start t
-    in p toks com ops (tl,ifThenElse (tc <= c) (c + 1) tc)
+        (MkFC file (line,col)) = indent
+    in p toks com ops (MkFC file (tl, ifThenElse (tc <= col) (col + 1) tc))
 
 ||| Assert that parser starts at our current column by
 ||| checking column and then updating line to match the current
 export
 sameLevel : Parser a -> Parser a
-sameLevel (P p) = P $ \toks,com,ops,(l,c) => case toks of
-  [] => p toks com ops (l,c)
+sameLevel (P p) = P $ \toks,com,ops,indent => case toks of
+  [] => p toks com ops indent
   (t :: _) =>
     let (tl,tc) = start t
-    in if tc == c then p toks com ops (tl, c)
-    else if c < tc then Fail False (error toks "unexpected indent") toks com ops
-    else Fail False (error toks "unexpected indent") toks com ops
+        (MkFC file (line,col)) = indent
+    in if tc == col then p toks com ops ({start := (tl, col)} indent)
+    else if col < tc then Fail False (error file toks "unexpected indent") toks com ops
+    else Fail False (error file toks "unexpected indent") toks com ops
 
 export
 someSame : Parser a -> Parser (List a)
@@ -178,12 +181,12 @@ manySame pa = many $ sameLevel pa
 ||| check indent on next token and run parser
 export
 indented : Parser a -> Parser a
-indented (P p) = P $ \toks,com,ops,(l,c) => case toks of
-  [] => p toks com ops (l,c)
+indented (P p) = P $ \toks,com,ops,indent => case toks of
+  [] => p toks com ops indent
   (t::_) =>
     let (tl,tc) = start t
-    in if tc > c || tl == l then p toks com ops (l,c)
-    else Fail False (error toks "unexpected outdent") toks com ops
+    in if tc > indent.col || tl == indent.line then p toks com ops indent
+    else Fail False (error indent.file toks "unexpected outdent") toks com ops
 
 ||| expect token of given kind
 export

src/Lib/ProcessDecl.idr

@@ -143,7 +143,7 @@ logMetas mstart = do
       env <- dumpEnv ctx
       let msg = "\{env}  -----------\n  \{pprint names ty'}"
       info fc "User Hole\n\{msg}"
-    (Unsolved (l,c) k ctx ty kind cons) => do
+    (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
       -- TODO - log constraints?
@@ -151,7 +151,7 @@ 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 (l,c) $ unlines ([msg] ++ msgs)
+      addError $ E fc $ unlines ([msg] ++ msgs)
 
 
 export
@@ -409,7 +409,7 @@ processDecl (Data fc nm ty cons) = do
           for_ names $ \ nm' => do
             setDef nm' fc dty (DCon (getArity dty) nm)
           pure names
-      _ => throwError $ E (0,0) "expected constructor declaration"
+      decl => throwError $ E (getFC decl) "expected constructor declaration"
   putStrLn "setDef \{nm}  TCon \{show $ join cnames}"
   updateDef nm fc tyty (TCon (join cnames))
   -- logMetas mstart

src/Lib/Tokenizer.idr

@@ -90,8 +90,8 @@ notSpace (MkBounded (Tok Space _) _ _) = False
 notSpace _ = True
 
 export
-tokenise : String -> Either Error (List BTok)
-tokenise s = case lex rawTokens s of
+tokenise : String -> String -> Either Error (List BTok)
+tokenise fn s = case lex rawTokens s of
   (toks, EndInput, l, c, what) => Right (filter notSpace toks)
-  (toks, reason, l, c, what) => Left (E (l,c) "\{show reason}")
+  (toks, reason, l, c, what) => Left (E (MkFC fn (l,c)) "\{show reason}")
 

src/Lib/Types.idr

@@ -512,7 +512,7 @@ error fc msg = throwError $ E fc msg
 
 export
 error' : String -> M a
-error' msg = throwError $ E (0,0) msg
+error' msg = throwError $ E emptyFC msg
 
 export
 freshMeta : Context -> FC -> Val -> MetaKind -> M Tm