File locations are now ranges.
This commit is contained in:
@@ -110,20 +110,20 @@ export function activate(context: vscode.ExtensionContext) {
|
|||||||
console.log("top data", topData);
|
console.log("top data", topData);
|
||||||
}
|
}
|
||||||
const match = line.match(
|
const match = line.match(
|
||||||
/(INFO|WARN|ERROR) at (.*):\((\d+), (\d+)\):\s*(.*)/
|
/(INFO|WARN|ERROR) at (.*):\((\d+):(\d+)-(\d+):(\d+)\):\s*(.*)/
|
||||||
);
|
);
|
||||||
if (match) {
|
if (match) {
|
||||||
let [_full, kind, file, line, column, message] = match;
|
let [_full, kind, file, line, column, eline, ecol, message] = match;
|
||||||
let lnum = Number(line) - 1;
|
let lnum = +line - 1;
|
||||||
let cnum = Number(column) - 1;
|
let cnum = +column - 1;
|
||||||
if (file !== fileName) lnum = cnum = 0;
|
let elnum = +eline - 1;
|
||||||
|
let ecnum = +ecol - 1;
|
||||||
let start = new vscode.Position(lnum, cnum);
|
let start = new vscode.Position(lnum, cnum);
|
||||||
// we don't have the full range, so grab the surrounding word
|
let end = new vscode.Position(elnum, ecnum);
|
||||||
let end = new vscode.Position(lnum, cnum + 1);
|
let range = new vscode.Range(start, end);
|
||||||
let range =
|
if (file !== fileName) {
|
||||||
document.getWordRangeAtPosition(start) ??
|
range = new vscode.Range(new vscode.Position(0,0), new vscode.Position(0,0));
|
||||||
new vscode.Range(start, end);
|
}
|
||||||
// anything indented after the ERROR/INFO line are part of
|
// anything indented after the ERROR/INFO line are part of
|
||||||
// the message
|
// the message
|
||||||
while (lines[i + 1]?.match(/^( )/)) message += "\n" + lines[++i];
|
while (lines[i + 1]?.match(/^( )/)) message += "\n" + lines[++i];
|
||||||
|
|||||||
@@ -440,18 +440,20 @@ const processOutput = (
|
|||||||
for (let i = 0; i < lines.length; i++) {
|
for (let i = 0; i < lines.length; i++) {
|
||||||
const line = lines[i];
|
const line = lines[i];
|
||||||
const match = line.match(
|
const match = line.match(
|
||||||
/(INFO|ERROR) at ([^:]+):\((\d+), (\d+)\):\s*(.*)/
|
/(INFO|ERROR) at ([^:]+):\((\d+):(\d+)-(\d+):(\d+)\):\s*(.*)/
|
||||||
);
|
);
|
||||||
if (match) {
|
if (match) {
|
||||||
let [_full, kind, file, line, col, message] = match;
|
let [_full, kind, file, line, col, eline, ecol, message] = match;
|
||||||
let lineNumber = +line;
|
let startLineNumber = +line;
|
||||||
let column = +col;
|
let startColumn = +col;
|
||||||
|
let endLineNumber = +eline;
|
||||||
|
let endColumn = +ecol
|
||||||
// FIXME - pass the real path in
|
// FIXME - pass the real path in
|
||||||
if (fn && fn !== file) {
|
if (fn && fn !== file) {
|
||||||
lineNumber = column = 0;
|
startLineNumber = startColumn = 0;
|
||||||
}
|
}
|
||||||
// we don't have the full range, so grab the surrounding word
|
// we don't have the full range, so grab the surrounding word
|
||||||
let endColumn = column + 1;
|
// let endColumn = startColumn + 1;
|
||||||
|
|
||||||
// heuristics to grab the entire message:
|
// heuristics to grab the entire message:
|
||||||
// anything indented
|
// anything indented
|
||||||
@@ -460,13 +462,13 @@ const processOutput = (
|
|||||||
while (lines[i + 1]?.match(/^( )/)) {
|
while (lines[i + 1]?.match(/^( )/)) {
|
||||||
message += "\n" + lines[++i];
|
message += "\n" + lines[++i];
|
||||||
}
|
}
|
||||||
if (kind === "ERROR" || lineNumber)
|
if (kind === "ERROR" || startLineNumber)
|
||||||
markers.push({
|
markers.push({
|
||||||
severity: kind === "ERROR" ? "error" : "info",
|
severity: kind === "ERROR" ? "error" : "info",
|
||||||
message,
|
message,
|
||||||
startLineNumber: lineNumber,
|
startLineNumber,
|
||||||
endLineNumber: lineNumber,
|
endLineNumber,
|
||||||
startColumn: column,
|
startColumn,
|
||||||
endColumn,
|
endColumn,
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -18,7 +18,7 @@ for fn in tests/*.newt ; do
|
|||||||
if [ -f ${fn}.fail ]; then
|
if [ -f ${fn}.fail ]; then
|
||||||
if ! diff -q tmp/${bn}.compile ${fn}.fail; then
|
if ! diff -q tmp/${bn}.compile ${fn}.fail; then
|
||||||
echo "Compile failure mismatch for $fn"
|
echo "Compile failure mismatch for $fn"
|
||||||
diff tmp/${bn}.comp ${fn}.fail
|
diff ${fn}.fail tmp/${bn}.compile
|
||||||
failed=$((failed + 1))
|
failed=$((failed + 1))
|
||||||
continue
|
continue
|
||||||
fi
|
fi
|
||||||
@@ -38,7 +38,7 @@ for fn in tests/*.newt ; do
|
|||||||
fi
|
fi
|
||||||
if ! diff -q tmp/${bn}.out ${fn}.golden; then
|
if ! diff -q tmp/${bn}.out ${fn}.golden; then
|
||||||
echo "Output mismatch for $fn"
|
echo "Output mismatch for $fn"
|
||||||
diff -q tmp/${bn}.out ${fn}.golden
|
diff ${fn}.golden tmp/${bn}.out
|
||||||
failed=$((failed + 1))
|
failed=$((failed + 1))
|
||||||
fi
|
fi
|
||||||
fi
|
fi
|
||||||
|
|||||||
@@ -5,6 +5,32 @@ import Data.String
|
|||||||
import Data.Int
|
import Data.Int
|
||||||
import Data.SortedMap
|
import Data.SortedMap
|
||||||
|
|
||||||
|
record Bounds where
|
||||||
|
constructor MkBounds
|
||||||
|
startLine : Int
|
||||||
|
startCol : Int
|
||||||
|
endLine : Int
|
||||||
|
endCol : Int
|
||||||
|
|
||||||
|
-- FIXME we should handle overlap and out of order..
|
||||||
|
instance Add Bounds where
|
||||||
|
a + b = MkBounds a.startLine a.startCol b.endLine b.endCol
|
||||||
|
|
||||||
|
instance Eq Bounds where
|
||||||
|
(MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
|
||||||
|
sl == sl'
|
||||||
|
&& sc == sc'
|
||||||
|
&& el == el'
|
||||||
|
&& ec == ec'
|
||||||
|
|
||||||
|
record WithBounds ty where
|
||||||
|
constructor MkBounded
|
||||||
|
val : ty
|
||||||
|
bounds : Bounds
|
||||||
|
|
||||||
|
emptyBounds : Bounds
|
||||||
|
emptyBounds = MkBounds 0 0 0 0
|
||||||
|
|
||||||
-- l is environment size, this works for both lvl2ix and ix2lvl
|
-- l is environment size, this works for both lvl2ix and ix2lvl
|
||||||
|
|
||||||
range : Int → Int → List Int
|
range : Int → Int → List Int
|
||||||
@@ -74,19 +100,19 @@ instance ToJSON Int where
|
|||||||
record FC where
|
record FC where
|
||||||
constructor MkFC
|
constructor MkFC
|
||||||
file : String
|
file : String
|
||||||
start : (Int × Int)
|
bnds : Bounds
|
||||||
|
|
||||||
|
|
||||||
instance ToJSON FC where
|
instance ToJSON FC where
|
||||||
toJson (MkFC file (line,col)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: Nil)
|
toJson (MkFC file (MkBounds line col endline endcol)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: ("endline", toJson endline) :: ("endcol", toJson endcol):: Nil)
|
||||||
|
|
||||||
|
|
||||||
fcLine : FC -> Int
|
fcLine : FC -> Int
|
||||||
fcLine (MkFC file (l, c)) = l
|
fcLine fc = fc.bnds.startLine
|
||||||
|
|
||||||
|
|
||||||
fcCol : FC -> Int
|
fcCol : FC -> Int
|
||||||
fcCol (MkFC file (l, c)) = c
|
fcCol fc = fc.bnds.startCol
|
||||||
|
|
||||||
|
|
||||||
class HasFC a where
|
class HasFC a where
|
||||||
@@ -96,7 +122,10 @@ primNS : List String
|
|||||||
primNS = ("Prim" :: Nil)
|
primNS = ("Prim" :: Nil)
|
||||||
|
|
||||||
emptyFC : FC
|
emptyFC : FC
|
||||||
emptyFC = MkFC "" (0,0)
|
emptyFC = MkFC "" (MkBounds 0 0 0 0)
|
||||||
|
|
||||||
|
emptyFC' : String → FC
|
||||||
|
emptyFC' fn = MkFC fn (MkBounds 0 0 0 0)
|
||||||
|
|
||||||
-- Error of a parse
|
-- Error of a parse
|
||||||
|
|
||||||
@@ -119,7 +148,8 @@ data Error
|
|||||||
| Postpone FC QName String
|
| Postpone FC QName String
|
||||||
|
|
||||||
instance Show FC where
|
instance Show FC where
|
||||||
show (MkFC file (l,c)) = "\{file}:(\{show $ l + 1}, \{show $ c + 1})"
|
-- We add one to the end column so it points after the end, which seems to be what Idris does
|
||||||
|
show (MkFC file (MkBounds l c el ec)) = "\{file}:(\{show $ l + 1}:\{show $ c + 1}-\{show $ el + 1}:\{show $ ec + 2})"
|
||||||
|
|
||||||
|
|
||||||
showError : String -> Error -> String
|
showError : String -> Error -> String
|
||||||
|
|||||||
@@ -9,6 +9,8 @@ import Lib.Syntax
|
|||||||
import Lib.Token
|
import Lib.Token
|
||||||
import Lib.Types
|
import Lib.Types
|
||||||
|
|
||||||
|
-- TODO - anywhere this says getPos, we probably have to fix bounds? It is token sized though.
|
||||||
|
|
||||||
lazy : ∀ a. (Unit → Parser a) → Parser a
|
lazy : ∀ a. (Unit → Parser a) → Parser a
|
||||||
lazy pa = pa MkUnit
|
lazy pa = pa MkUnit
|
||||||
|
|
||||||
@@ -61,10 +63,8 @@ interp = do
|
|||||||
token EndInterp
|
token EndInterp
|
||||||
pure tm
|
pure tm
|
||||||
|
|
||||||
|
|
||||||
interpString : Parser Raw
|
interpString : Parser Raw
|
||||||
interpString = do
|
interpString = do
|
||||||
-- fc <- getPos
|
|
||||||
ignore $ token StartQuote
|
ignore $ token StartQuote
|
||||||
part <- term
|
part <- term
|
||||||
parts <- many (stringLit <|> interp)
|
parts <- many (stringLit <|> interp)
|
||||||
|
|||||||
@@ -15,13 +15,13 @@ TokenList = List BTok
|
|||||||
-- Result of a parse
|
-- Result of a parse
|
||||||
|
|
||||||
data Result : U -> U where
|
data Result : U -> U where
|
||||||
OK : ∀ a. a -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
|
OK : ∀ a. a -> Bounds -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
|
||||||
Fail : ∀ a. Bool -> Error -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
|
Fail : ∀ a. Bool -> Error -> Bounds -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
|
||||||
|
|
||||||
|
|
||||||
instance Functor Result where
|
instance Functor Result where
|
||||||
map f (OK a toks com ops) = OK (f a) toks com ops
|
map f (OK a last toks com ops) = OK (f a) last toks com ops
|
||||||
map _ (Fail fatal err toks com ops) = Fail fatal err toks com ops
|
map _ (Fail fatal err last toks com ops) = Fail fatal err last toks com ops
|
||||||
|
|
||||||
-- So sixty just has a newtype function here now (probably for perf).
|
-- So sixty just has a newtype function here now (probably for perf).
|
||||||
-- A record might be more ergonomic, but would require a record impl before
|
-- A record might be more ergonomic, but would require a record impl before
|
||||||
@@ -34,108 +34,97 @@ instance Functor Result where
|
|||||||
-- Since I've already built out the pratt stuff, I guess I'll
|
-- Since I've already built out the pratt stuff, I guess I'll
|
||||||
-- leave it in the parser for now
|
-- leave it in the parser for now
|
||||||
|
|
||||||
-- This is a Reader in FC, a State in Operators, Commit flag, TokenList
|
-- This is a Reader in FC (indent), a State in Operators, Commit flag, TokenList
|
||||||
|
-- Using FC to pass around the fileName, but the indent only uses line and column
|
||||||
|
data Parser a = P (Bounds -> TokenList -> Bool -> Operators -> (lc : FC) -> Result a)
|
||||||
|
|
||||||
|
|
||||||
data Parser a = P (TokenList -> Bool -> Operators -> (lc : FC) -> Result a)
|
runP : ∀ a. Parser a -> Bounds -> TokenList -> Bool -> Operators -> FC -> Result a
|
||||||
|
|
||||||
|
|
||||||
runP : ∀ a. Parser a -> TokenList -> Bool -> Operators -> FC -> Result a
|
|
||||||
runP (P f) = f
|
runP (P f) = f
|
||||||
|
|
||||||
-- FIXME no filename, also half the time it is pointing at the token after the error
|
-- FIXME half the time it is pointing at the token after the error
|
||||||
perror : String -> TokenList -> String -> Error
|
perror : String -> TokenList -> String -> Error
|
||||||
perror fn Nil msg = E (MkFC fn (0,0)) msg
|
perror fn Nil msg = E (emptyFC' fn) msg
|
||||||
perror fn ((MkBounded val (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg
|
perror fn ((MkBounded val bnds) :: _) msg = E (MkFC fn bnds) msg
|
||||||
|
|
||||||
|
|
||||||
parse : ∀ a. String -> Parser a -> TokenList -> Either Error a
|
parse : ∀ a. String -> Parser a -> TokenList -> Either Error a
|
||||||
parse fn pa toks = case runP pa toks False emptyMap (MkFC fn (-1,-1)) of
|
parse fn pa toks = case runP pa emptyBounds toks False emptyMap (MkFC fn (MkBounds -1 -1 -1 -1)) of
|
||||||
Fail fatal err toks com ops => Left err
|
Fail fatal err last toks com ops => Left err
|
||||||
OK a Nil _ _ => Right a
|
OK a _ Nil _ _ => Right a
|
||||||
OK a ts _ _ => Left (perror fn ts "Extra toks")
|
OK a _ ts _ _ => Left (perror fn ts "Extra toks")
|
||||||
|
|
||||||
-- Intended for parsing a top level declaration
|
-- Intended for parsing a top level declaration
|
||||||
|
|
||||||
partialParse : ∀ a. String -> Parser a -> Operators -> TokenList -> Either (Error × TokenList) (a × Operators × TokenList)
|
partialParse : ∀ a. 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
|
partialParse fn pa ops toks = case runP pa emptyBounds toks False ops (emptyFC' fn) of
|
||||||
Fail fatal err toks com ops => Left (err, toks)
|
Fail fatal err last toks com ops => Left (err, toks)
|
||||||
OK a ts _ ops => Right (a,ops,ts)
|
OK a last toks _ ops => Right (a,ops,toks)
|
||||||
|
|
||||||
-- I think I want to drop the typeclasses for v1
|
|
||||||
|
|
||||||
|
|
||||||
try : ∀ a. Parser a -> Parser a
|
try : ∀ a. Parser a -> Parser a
|
||||||
try (P pa) = P $ \toks com ops col => case pa toks com ops col of
|
try (P pa) = P $ \last toks com ops col => case pa last toks com ops col of
|
||||||
(Fail x err toks com ops) => Fail x err toks False ops
|
(Fail x err last toks com ops) => Fail x err last toks False ops
|
||||||
res => res
|
res => res
|
||||||
|
|
||||||
|
|
||||||
fail : ∀ a. String -> Parser a
|
fail : ∀ a. String -> Parser a
|
||||||
fail msg = P $ \toks com ops col => Fail False (perror col.file toks msg) toks com ops
|
fail msg = P $ \last toks com ops col => Fail False (perror col.file toks msg) last toks com ops
|
||||||
|
|
||||||
|
|
||||||
fatal : ∀ a. String -> Parser a
|
fatal : ∀ a. String -> Parser a
|
||||||
fatal msg = P $ \toks com ops col => Fail True (perror col.file toks msg) toks com ops
|
fatal msg = P $ \last toks com ops col => Fail True (perror col.file toks msg) last toks com ops
|
||||||
|
|
||||||
|
|
||||||
getOps : Parser (Operators)
|
getOps : Parser (Operators)
|
||||||
getOps = P $ \ toks com ops col => OK ops toks com ops
|
getOps = P $ \last toks com ops col => OK ops last toks com ops
|
||||||
|
|
||||||
|
|
||||||
addOp : String -> Int -> Fixity -> Parser Unit
|
addOp : String -> Int -> Fixity -> Parser Unit
|
||||||
addOp nm prec fix = P $ \ toks com ops col =>
|
addOp nm prec fix = P $ \ last toks com ops col =>
|
||||||
let parts = split nm "_" in
|
let parts = split nm "_" in
|
||||||
case parts of
|
case parts of
|
||||||
"" :: key :: rule => OK MkUnit toks com (updateMap key (MkOp nm prec fix False rule) ops)
|
"" :: key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix False rule) ops)
|
||||||
key :: rule => OK MkUnit toks com (updateMap key (MkOp nm prec fix True rule) ops)
|
key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix True rule) ops)
|
||||||
Nil => Fail True (perror col.file toks "Internal error parsing mixfix") toks com ops
|
Nil => Fail True (perror col.file toks "Internal error parsing mixfix") last toks com ops
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
instance Functor Parser where
|
instance Functor Parser where
|
||||||
map f (P pa) = P $ \ toks com ops col => map f (pa toks com ops col)
|
map f (P pa) = P $ \ last toks com ops col => map f (pa last toks com ops col)
|
||||||
|
|
||||||
|
|
||||||
instance Applicative Parser where
|
instance Applicative Parser where
|
||||||
return pa = P (\ toks com ops col => OK pa toks com ops)
|
return pa = P (\ last toks com ops col => OK pa last toks com ops)
|
||||||
P pab <*> P pa = P $ \toks com ops col =>
|
P pab <*> P pa = P $ \last toks com ops col =>
|
||||||
case pab toks com ops col of
|
case pab last toks com ops col of
|
||||||
Fail fatal err toks com ops => Fail fatal err toks com ops
|
Fail fatal err last toks com ops => Fail fatal err last toks com ops
|
||||||
OK f toks com ops =>
|
OK f last toks com ops =>
|
||||||
case pa toks com ops col of
|
case pa last toks com ops col of
|
||||||
(OK x toks com ops) => OK (f x) toks com ops
|
(OK x last toks com ops) => OK (f x) last toks com ops
|
||||||
(Fail fatal err toks com ops) => Fail fatal err toks com ops
|
(Fail fatal err last toks com ops) => Fail fatal err last toks com ops
|
||||||
|
|
||||||
-- Second argument lazy so we don't have circular refs when defining parsers.
|
-- Second argument lazy so we don't have circular refs when defining parsers.
|
||||||
|
|
||||||
instance Alternative Parser where
|
instance Alternative Parser where
|
||||||
(P pa) <|> (P pb) = P $ \toks com ops col =>
|
(P pa) <|> (P pb) = P $ \last toks com ops col =>
|
||||||
case pa toks False ops col of
|
case pa last toks False ops col of
|
||||||
OK a toks' _ ops => OK a toks' com ops
|
OK a last' toks' _ ops => OK a last' toks' com ops
|
||||||
Fail True err toks' com ops => Fail True err toks' com ops
|
Fail True err last' toks' com ops => Fail True err last' toks' com ops
|
||||||
Fail fatal err toks' True ops => Fail fatal err toks' True ops
|
Fail fatal err last' toks' True ops => Fail fatal err last' toks' True ops
|
||||||
Fail fatal err toks' False ops => pb toks com ops col
|
Fail fatal err last' toks' False ops => pb last toks com ops col
|
||||||
|
|
||||||
|
|
||||||
instance Monad Parser where
|
instance Monad Parser where
|
||||||
pure = return
|
pure = return
|
||||||
bind (P pa) pab = P $ \toks com ops col =>
|
bind (P pa) pab = P $ \last toks com ops col =>
|
||||||
case pa toks com ops col of
|
case pa last toks com ops col of
|
||||||
(OK a toks com ops) => runP (pab a) toks com ops col
|
(OK a last toks com ops) => runP (pab a) last toks com ops col
|
||||||
(Fail fatal err xs x ops) => Fail fatal err xs x ops
|
(Fail fatal err last toks x ops) => Fail fatal err last toks x ops
|
||||||
|
|
||||||
|
|
||||||
satisfy : (BTok -> Bool) -> String -> Parser String
|
satisfy : (BTok -> Bool) -> String -> Parser String
|
||||||
satisfy f msg = P $ \toks com ops col =>
|
satisfy f msg = P $ \last toks com ops col =>
|
||||||
case toks of
|
case toks of
|
||||||
(t :: ts) => if f t then OK (value t) ts True ops else Fail False (perror col.file toks "\{msg} at \{show t.val.kind}:\{value t}") toks com ops
|
(t :: ts) => if f t then OK (value t) t.bounds ts True ops else Fail False (perror col.file toks "\{msg} at \{show t.val.kind}:\{value t}") last toks com ops
|
||||||
Nil => Fail False (perror col.file toks "\{msg} at EOF") toks com ops
|
Nil => Fail False (perror col.file toks "\{msg} at EOF") last toks com ops
|
||||||
|
|
||||||
|
|
||||||
commit : Parser Unit
|
|
||||||
commit = P $ \toks com ops col => OK MkUnit toks True ops
|
|
||||||
|
|
||||||
|
|
||||||
some : ∀ a. Parser a -> Parser (List a)
|
some : ∀ a. Parser a -> Parser (List a)
|
||||||
@@ -154,34 +143,50 @@ sepBy s a = _::_ <$> a <*> many (s *> a)
|
|||||||
|
|
||||||
|
|
||||||
getPos : Parser FC
|
getPos : Parser FC
|
||||||
getPos = P $ \toks com ops indent => case toks of
|
getPos = P $ \last toks com ops indent => case toks of
|
||||||
Nil => OK emptyFC toks com ops
|
Nil => OK (MkFC indent.file last) last toks com ops
|
||||||
(t :: ts) => OK (MkFC indent.file (getStart t)) toks com ops
|
(t :: ts) => OK (MkFC indent.file t.bounds) last toks com ops
|
||||||
|
|
||||||
|
tokStart : TokenList → Bounds
|
||||||
|
tokStart Nil = emptyBounds
|
||||||
|
tokStart (t :: ts) = t.bounds
|
||||||
|
|
||||||
|
bounded : ∀ a. Parser a → Parser (WithBounds a)
|
||||||
|
bounded pa = P $ \last toks com ops indent =>
|
||||||
|
case runP pa last toks com ops indent of
|
||||||
|
(OK a last toks' com ops) => (OK (MkBounded a (tokStart toks + last)) last toks' com ops)
|
||||||
|
(Fail fatal err last toks x ops) => Fail fatal err last toks x ops
|
||||||
|
|
||||||
|
withFC : ∀ a. Parser a → Parser (FC × a)
|
||||||
|
withFC pa = P $ \last toks com ops indent =>
|
||||||
|
case runP pa last toks com ops indent of
|
||||||
|
(OK a last toks' com ops) => OK ((MkFC indent.file $ tokStart toks + last), a) last toks' com ops
|
||||||
|
(Fail fatal err last toks x ops) => Fail fatal err last toks x ops
|
||||||
|
|
||||||
|
|
||||||
-- Start an indented block and run parser in it
|
-- Start an indented block and run parser in it
|
||||||
|
|
||||||
startBlock : ∀ a. Parser a -> Parser a
|
startBlock : ∀ a. Parser a -> Parser a
|
||||||
startBlock (P p) = P $ \toks com ops indent => case toks of
|
startBlock (P p) = P $ \last toks com ops indent => case toks of
|
||||||
Nil => p toks com ops indent
|
Nil => p last toks com ops indent
|
||||||
(t :: _) =>
|
(t :: _) =>
|
||||||
-- If next token is at or before the current level, we've got an empty block
|
-- If next token is at or before the current level, we've got an empty block
|
||||||
let (tl,tc) = getStart t in
|
let (tl,tc) = getStart t in
|
||||||
let (MkFC file (line,col)) = indent in
|
let (MkFC file (MkBounds line col _ _)) = indent in
|
||||||
p toks com ops (MkFC file (tl, ite (tc <= col) (col + 1) tc))
|
p last toks com ops (MkFC file ((ite (tc <= col) (MkBounds tl (col + 1) 0 0) t.bounds)))
|
||||||
|
|
||||||
-- Assert that parser starts at our current column by
|
-- Assert that parser starts at our current column by
|
||||||
-- checking column and then updating line to match the current
|
-- checking column and then updating line to match the current
|
||||||
|
|
||||||
sameLevel : ∀ a. Parser a -> Parser a
|
sameLevel : ∀ a. Parser a -> Parser a
|
||||||
sameLevel (P p) = P $ \toks com ops indent => case toks of
|
sameLevel (P p) = P $ \last toks com ops indent => case toks of
|
||||||
Nil => p toks com ops indent
|
Nil => p last toks com ops indent
|
||||||
(t :: _) =>
|
(t :: _) =>
|
||||||
let (tl,tc) = getStart t in
|
let (tl,tc) = getStart t in
|
||||||
let (MkFC file (line,col)) = indent in
|
let (MkFC file (MkBounds line col _ _)) = indent in
|
||||||
if tc == col then p toks com ops (MkFC file (tl, col))
|
if tc == col then p last toks com ops (MkFC file t.bounds)
|
||||||
else if col < tc then Fail False (perror file toks "unexpected indent") toks com ops
|
else if col < tc then Fail False (perror file toks "unexpected indent") last toks com ops
|
||||||
else Fail False (perror file toks "unexpected indent") toks com ops
|
else Fail False (perror file toks "unexpected indent") last toks com ops
|
||||||
|
|
||||||
|
|
||||||
someSame : ∀ a. Parser a -> Parser (List a)
|
someSame : ∀ a. Parser a -> Parser (List a)
|
||||||
someSame pa = some $ sameLevel pa
|
someSame pa = some $ sameLevel pa
|
||||||
@@ -193,12 +198,12 @@ manySame pa = many $ sameLevel pa
|
|||||||
-- check indent on next token and run parser
|
-- check indent on next token and run parser
|
||||||
|
|
||||||
indented : ∀ a. Parser a -> Parser a
|
indented : ∀ a. Parser a -> Parser a
|
||||||
indented (P p) = P $ \toks com ops indent => case toks of
|
indented (P p) = P $ \last toks com ops indent => case toks of
|
||||||
Nil => p toks com ops indent
|
Nil => p last toks com ops indent
|
||||||
(t :: _) =>
|
(t :: _) =>
|
||||||
let (tl,tc) = getStart t
|
let (tl,tc) = getStart t
|
||||||
in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent
|
in if tc > fcCol indent || tl == fcLine indent then p last toks com ops indent
|
||||||
else Fail False (perror indent.file toks "unexpected outdent") toks com ops
|
else Fail False (perror indent.file toks "unexpected outdent") last toks com ops
|
||||||
|
|
||||||
-- expect token of given kind
|
-- expect token of given kind
|
||||||
|
|
||||||
|
|||||||
@@ -31,8 +31,6 @@ instance HasFC Pattern where
|
|||||||
getFC (PatWild fc _) = fc
|
getFC (PatWild fc _) = fc
|
||||||
getFC (PatLit fc lit) = fc
|
getFC (PatLit fc lit) = fc
|
||||||
|
|
||||||
-- %runElab deriveShow `{Pattern}
|
|
||||||
|
|
||||||
Constraint : U
|
Constraint : U
|
||||||
Constraint = (String × Pattern)
|
Constraint = (String × Pattern)
|
||||||
|
|
||||||
|
|||||||
@@ -1,28 +1,7 @@
|
|||||||
module Lib.Token
|
module Lib.Token
|
||||||
|
|
||||||
import Prelude
|
import Prelude
|
||||||
|
import Lib.Common
|
||||||
record Bounds where
|
|
||||||
constructor MkBounds
|
|
||||||
startLine : Int
|
|
||||||
startCol : Int
|
|
||||||
endLine : Int
|
|
||||||
endCol : Int
|
|
||||||
|
|
||||||
|
|
||||||
instance Eq Bounds where
|
|
||||||
(MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
|
|
||||||
sl == sl'
|
|
||||||
&& sc == sc'
|
|
||||||
&& el == el'
|
|
||||||
&& ec == ec'
|
|
||||||
|
|
||||||
|
|
||||||
record WithBounds ty where
|
|
||||||
constructor MkBounded
|
|
||||||
val : ty
|
|
||||||
bounds : Bounds
|
|
||||||
|
|
||||||
|
|
||||||
data Kind
|
data Kind
|
||||||
= Ident
|
= Ident
|
||||||
@@ -98,3 +77,6 @@ value (MkBounded (Tok _ s) _) = s
|
|||||||
|
|
||||||
getStart : BTok -> (Int × Int)
|
getStart : BTok -> (Int × Int)
|
||||||
getStart (MkBounded _ (MkBounds l c _ _)) = (l,c)
|
getStart (MkBounded _ (MkBounds l c _ _)) = (l,c)
|
||||||
|
|
||||||
|
getEnd : BTok -> (Int × Int)
|
||||||
|
getEnd (MkBounded _ (MkBounds _ _ el ec)) = (el,ec)
|
||||||
|
|||||||
@@ -52,13 +52,13 @@ quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of
|
|||||||
'}' :: cs =>
|
'}' :: cs =>
|
||||||
let tok = MkBounded (Tok EndInterp "}") (MkBounds el ec el (ec + 1))
|
let tok = MkBounded (Tok EndInterp "}") (MkBounds el ec el (ec + 1))
|
||||||
in quoteTokenise (TS el (ec + 1) (toks :< tok) cs) el (ec + 1) Lin
|
in quoteTokenise (TS el (ec + 1) (toks :< tok) cs) el (ec + 1) Lin
|
||||||
cs => Left $ E (MkFC "" (el, ec)) "Expected '{'"
|
cs => Left $ E (MkFC "" (MkBounds el ec el ec)) "Expected '{'"
|
||||||
-- TODO newline in string should be an error
|
-- TODO newline in string should be an error
|
||||||
'\n' :: cs => Left $ E (MkFC "" (el, ec)) "Newline in string"
|
'\n' :: cs => Left $ E (MkFC "" (MkBounds el ec el ec)) "Newline in string"
|
||||||
'\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< '\n')
|
'\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< '\n')
|
||||||
'\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< c)
|
'\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< c)
|
||||||
c :: cs => quoteTokenise (TS el (ec + 1) toks cs) startl startc (acc :< c)
|
c :: cs => quoteTokenise (TS el (ec + 1) toks cs) startl startc (acc :< c)
|
||||||
Nil => Left $ E (MkFC "" (el, ec)) "Expected '\"' at EOF"
|
Nil => Left $ E (MkFC "" (MkBounds el ec el ec)) "Expected '\"' at EOF"
|
||||||
|
|
||||||
where
|
where
|
||||||
stok : BTok
|
stok : BTok
|
||||||
@@ -78,7 +78,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
|
|||||||
Right (TS sl sc toks chars) => case chars of
|
Right (TS sl sc toks chars) => case chars of
|
||||||
'"' :: cs => let tok = mktok False sl (sc + 1) EndQuote "\"" in
|
'"' :: cs => let tok = mktok False sl (sc + 1) EndQuote "\"" in
|
||||||
rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
|
rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
|
||||||
cs => Left $ E (MkFC "" (sl, sc)) "Expected '\"'"
|
cs => Left $ E (MkFC "" (MkBounds sl sc sl sc)) "Expected '\"'"
|
||||||
|
|
||||||
'{' :: '{' :: cs =>
|
'{' :: '{' :: cs =>
|
||||||
let tok = mktok False sl (sc + 2) Keyword "{{" in
|
let tok = mktok False sl (sc + 2) Keyword "{{" in
|
||||||
@@ -87,7 +87,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
|
|||||||
Right (TS sl sc toks chars) => case chars of
|
Right (TS sl sc toks chars) => case chars of
|
||||||
'}' :: '}' :: cs => let tok = mktok False sl (sc + 2) Keyword "}}" in
|
'}' :: '}' :: cs => let tok = mktok False sl (sc + 2) Keyword "}}" in
|
||||||
rawTokenise (TS sl (sc + 2) (toks :< tok) cs)
|
rawTokenise (TS sl (sc + 2) (toks :< tok) cs)
|
||||||
cs => Left $ E (MkFC "" (sl, sc)) "Expected '}}'"
|
cs => Left $ E (MkFC "" (MkBounds sl sc sl sc)) "Expected '}}'"
|
||||||
|
|
||||||
'}' :: cs => Right ts
|
'}' :: cs => Right ts
|
||||||
'{' :: cs =>
|
'{' :: cs =>
|
||||||
@@ -97,7 +97,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
|
|||||||
Right (TS sl sc toks chars) => case chars of
|
Right (TS sl sc toks chars) => case chars of
|
||||||
'}' :: cs => let tok = mktok False sl (sc + 1) Symbol "}" in
|
'}' :: cs => let tok = mktok False sl (sc + 1) Symbol "}" in
|
||||||
rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
|
rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
|
||||||
cs => Left $ E (MkFC "" (sl, sc)) "Expected '}'"
|
cs => Left $ E (MkFC "" (MkBounds sl sc sl sc)) "Expected '}'"
|
||||||
|
|
||||||
',' :: cs => rawTokenise (TS sl (sc + 1) (toks :< mktok False sl (sc + 1) Ident ",") cs)
|
',' :: cs => rawTokenise (TS sl (sc + 1) (toks :< mktok False sl (sc + 1) Ident ",") cs)
|
||||||
'_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs)
|
'_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs)
|
||||||
@@ -125,7 +125,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
|
|||||||
isUIdent c = isIdent c || c == '.'
|
isUIdent c = isIdent c || c == '.'
|
||||||
|
|
||||||
doBacktick : TState -> SnocList Char -> Either Error TState
|
doBacktick : TState -> SnocList Char -> Either Error TState
|
||||||
doBacktick (TS l c toks Nil) acc = Left $ E (MkFC "" (l,c)) "EOF in backtick string"
|
doBacktick (TS l c toks Nil) acc = Left $ E (MkFC "" (MkBounds l c l c)) "EOF in backtick string"
|
||||||
doBacktick (TS el ec toks ('`' :: cs)) acc =
|
doBacktick (TS el ec toks ('`' :: cs)) acc =
|
||||||
let tok = MkBounded (Tok JSLit (pack $ acc <>> Nil)) (MkBounds sl sc el ec) in
|
let tok = MkBounded (Tok JSLit (pack $ acc <>> Nil)) (MkBounds sl sc el ec) in
|
||||||
rawTokenise (TS el (ec + 1) (toks :< tok) cs)
|
rawTokenise (TS el (ec + 1) (toks :< tok) cs)
|
||||||
@@ -144,7 +144,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
|
|||||||
lineComment (TS line col toks (c :: cs)) = lineComment (TS line (col + 1) toks cs)
|
lineComment (TS line col toks (c :: cs)) = lineComment (TS line (col + 1) toks cs)
|
||||||
|
|
||||||
blockComment : TState -> Either Error TState
|
blockComment : TState -> Either Error TState
|
||||||
blockComment (TS line col toks Nil) = Left $ E (MkFC "" (line, col)) "EOF in block comment"
|
blockComment (TS line col toks Nil) = Left $ E (MkFC "" (MkBounds line col line col)) "EOF in block comment"
|
||||||
blockComment (TS line col toks ('-' :: '/' :: cs)) = rawTokenise (TS line (col + 2) toks cs)
|
blockComment (TS line col toks ('-' :: '/' :: cs)) = rawTokenise (TS line (col + 2) toks cs)
|
||||||
blockComment (TS line col toks ('\n' :: cs)) = blockComment (TS (line + 1) 0 toks cs)
|
blockComment (TS line col toks ('\n' :: cs)) = blockComment (TS (line + 1) 0 toks cs)
|
||||||
blockComment (TS line col toks (c :: cs)) = blockComment (TS line (col + 1) toks cs)
|
blockComment (TS line col toks (c :: cs)) = blockComment (TS line (col + 1) toks cs)
|
||||||
@@ -167,7 +167,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
|
|||||||
tokenise : String -> String -> Either Error (List BTok)
|
tokenise : String -> String -> Either Error (List BTok)
|
||||||
tokenise fn text = case rawTokenise (TS 0 0 Lin (unpack text)) of
|
tokenise fn text = case rawTokenise (TS 0 0 Lin (unpack text)) of
|
||||||
Right (TS trow tcol acc Nil) => Right $ acc <>> Nil
|
Right (TS trow tcol acc Nil) => Right $ acc <>> Nil
|
||||||
Right (TS trow tcol acc chars) => Left $ E (MkFC fn (trow, tcol)) "Extra toks"
|
Right (TS trow tcol acc chars) => Left $ E (MkFC fn (MkBounds trow tcol trow tcol)) "Extra toks"
|
||||||
Left (E (MkFC file start) str) => Left $ E (MkFC fn start) str
|
Left (E (MkFC file start) str) => Left $ E (MkFC fn start) str
|
||||||
Left err => Left err
|
Left err => Left err
|
||||||
|
|
||||||
|
|||||||
@@ -34,8 +34,8 @@ splitTele = go Nil
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
getBaseDir : String → String → M (String × QName)
|
getBaseDir : String → FC → String → M (String × QName)
|
||||||
getBaseDir fn modName = do
|
getBaseDir fn fc modName = do
|
||||||
let (path, modName') = unsnoc $ split1 modName "."
|
let (path, modName') = unsnoc $ split1 modName "."
|
||||||
let parts = split1 fn "/"
|
let parts = split1 fn "/"
|
||||||
let (dirs,file) = unsnoc parts
|
let (dirs,file) = unsnoc parts
|
||||||
@@ -44,9 +44,9 @@ getBaseDir fn modName = do
|
|||||||
let parts = split1 fn "/"
|
let parts = split1 fn "/"
|
||||||
let (dirs,file) = unsnoc parts
|
let (dirs,file) = unsnoc parts
|
||||||
let (path, modName') = unsnoc $ split1 modName "."
|
let (path, modName') = unsnoc $ split1 modName "."
|
||||||
unless (modName' == name) $ \ _ => error (MkFC fn (0,0)) "module name \{modName'} doesn't match \{name}"
|
unless (modName' == name) $ \ _ => error fc "module name \{modName'} doesn't match \{name}"
|
||||||
let (Right base) = baseDir (Lin <>< dirs) (Lin <>< path)
|
let (Right base) = baseDir (Lin <>< dirs) (Lin <>< path)
|
||||||
| Left err => error (MkFC fn (0,0)) err
|
| Left err => error fc err
|
||||||
let base = if base == "" then "." else base
|
let base = if base == "" then "." else base
|
||||||
pure (base, QN path modName')
|
pure (base, QN path modName')
|
||||||
where
|
where
|
||||||
|
|||||||
@@ -217,13 +217,13 @@ processFile fn = do
|
|||||||
log 1 $ \ _ => "\{show dir} \{show name} \{show ext}"
|
log 1 $ \ _ => "\{show dir} \{show name} \{show ext}"
|
||||||
|
|
||||||
(Right src) <- liftIO {M} $ readFile fn
|
(Right src) <- liftIO {M} $ readFile fn
|
||||||
| Left err => error (MkFC fn (0,0)) "error reading \{fn}: \{show err}"
|
| Left err => error (emptyFC' fn) "error reading \{fn}: \{show err}"
|
||||||
let (Right toks) = tokenise fn src
|
let (Right toks) = tokenise fn src
|
||||||
| Left err => throwError err
|
| Left err => throwError err
|
||||||
let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
|
let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
|
||||||
| Left (err,toks) => throwError err
|
| Left (err,toks) => throwError err
|
||||||
|
|
||||||
(base,qn) <- getBaseDir fn modName
|
(base,qn) <- getBaseDir fn nameFC modName
|
||||||
|
|
||||||
-- declare internal primitives
|
-- declare internal primitives
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user