dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

additional changes for porting, fix to lexing

Browse Source
This commit is contained in:
Steve Dunham
2025-01-01 08:46:25 -08:00
parent b993425803
commit 4dec53daa1
7 changed files with 39 additions and 33 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
scripts/translate.sh
View File

@@ -21,6 +21,7 @@ find src -type f -name '*.idr' | while read -r file; do
s/M \(\)/M Unit/;
s/Parser \(\)/Parser Unit/;
s/OK \(\)/OK MkUnit/;
s/toks,\s*com,\s*ops,\s*col/toks com ops col/;
s/\bNat\b/Int/g;
s/(\s+when [^\$]+\$)(.*)/\1 \\ _ =>\2/;
s/^public export//g;
@@ -30,6 +31,8 @@ find src -type f -name '*.idr' | while read -r file; do
# patterns would be another option, but
# we would need to handle overlapping ones
s/\[\]/Nil/g;
s/ \. / ∘ /g;
s/\(([<>\/+]+)\)/_\1_/g;
s/\{-/\/-/g;
s/-\}/-\//g;
s/\[<\]/Lin/g;

4
src/Lib/Common.idr
View File

@@ -5,6 +5,10 @@ import Data.Nat
import Data.Maybe
import public Data.SortedMap
public export
lvl2ix : Nat -> Nat -> Nat
lvl2ix l k = minus (minus l k) 1
hexChars : List Char
hexChars = unpack "0123456789ABCDEF"

19
src/Lib/Elab.idr
View File

@@ -530,7 +530,7 @@ substVal k v tm = go tm
updateContext : Context -> List (Nat, Val) -> M Context
updateContext ctx [] = pure ctx
updateContext ctx ((k, val) :: cs) =
let ix = (length ctx.env `minus` k) `minus` 1 in
let ix = lvl2ix (length ctx.env) k in
case getAt ix ctx.env of
(Just (VVar _ k' [<])) =>
if k' /= k
@@ -593,16 +593,9 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
debug "case \{dcName} dotted \{show val}"
when (length vars /= length sp) $ error emptyFC "\{show $ length vars} vars /= \{show $ length sp}"
-- TODO - do we need this one?
-- Constrain the scrutinee's variable to be dcon applied to args
-- let Just x = findIndex ((==scnm) . fst) ctx'.types
-- | Nothing => error ctx.fc "\{scnm} not is scope?"
-- let lvl = ((length ctx'.env) `minus` (cast x)) `minus` 1
-- let scon : (Nat, Val) = (lvl, VRef ctx.fc dcName (DCon arity dcName) sc)
-- TODO - I think we need to define the context vars to sp via updateContext
let lvl = (length ctx'.env `minus` length vars)
let lvl = minus (length ctx'.env) (length vars)
let scons = constrainSpine lvl (sp <>> []) -- REVIEW is this the right order?
ctx' <- updateContext ctx' scons
@@ -625,7 +618,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
-- Constrain the scrutinee's variable to be dcon applied to args
let Just x = findIndex ((==scnm) . fst) ctx'.types
| Nothing => error ctx.fc "\{scnm} not is scope?"
let lvl = ((length ctx'.env) `minus` (cast x)) `minus` 1
let lvl = lvl2ix (length ctx'.env) (cast x)
let scon : (Nat, Val) = (lvl, VRef ctx.fc dcName (DCon arity dcName) sc)
debug "scty \{show scty}"
@@ -853,7 +846,7 @@ buildLitCase ctx prob fc scnm scty lit = do
-- Constrain the scrutinee's variable to be lit value
let Just ix = findIndex ((==scnm) . fst) ctx.types
| Nothing => error ctx.fc "\{scnm} not is scope?"
let lvl = ((length ctx.env) `minus` (cast ix)) `minus` 1
let lvl = lvl2ix (length ctx.env) (cast ix)
let scon : (Nat, Val) = (lvl, VLit fc lit)
ctx' <- updateContext ctx [scon]
let clauses = mapMaybe rewriteClause prob.clauses
@@ -942,13 +935,13 @@ buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) =
-- some of this is copied into check
buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
debug "buildTree \{show constraints} \{show expr}"
let Just (scnm, pat) := findSplit constraints
let Just (scnm, pat) = findSplit constraints
| _ => do
debug "checkDone \{show constraints}"
checkDone ctx constraints expr ty
debug "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}"
let Just (sctm, scty) := lookupName ctx scnm
let Just (sctm, scty) = lookupName ctx scnm
| _ => error fc "Internal Error: can't find \{scnm} in environment"
-- REVIEW We probably need to know this is a VRef before we decide to split on this slot..

4
src/Lib/Eval.idr
View File

@@ -43,7 +43,7 @@ lookupVar : Env -> Nat -> Maybe Val
lookupVar env k = let l = length env in
if k > l
then Nothing
else case getAt ((l `minus` k) `minus` 1) env of
else case getAt (lvl2ix l k) env of
Just v@(VVar fc k' sp) => if k == k' then Nothing else Just v
Just v => Just v
Nothing => Nothing
@@ -172,7 +172,7 @@ quoteSp lvl t (xs :< x) =
pure $ App emptyFC !(quoteSp lvl t xs) !(quote lvl x)
quote l (VVar fc k sp) = if k < l
then quoteSp l (Bnd fc ((l `minus` k) `minus` 1)) sp -- level to index
then quoteSp l (Bnd fc (lvl2ix l k )) sp -- level to index
else ?borken
quote l (VMeta fc i sp) =
case !(lookupMeta i) of

14
src/Lib/Parser/Impl.idr
View File

@@ -123,8 +123,8 @@ Monad Parser where
(Fail fatal err xs x ops) => Fail fatal err xs x ops
pred : (BTok -> Bool) -> String -> Parser String
pred f msg = P $ \toks,com,ops,col =>
satisfy : (BTok -> Bool) -> String -> Parser String
satisfy 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 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
@@ -158,9 +158,9 @@ 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
(MkFC file (line,col)) = indent
in p toks com ops (MkFC file (tl, ifThenElse (tc <= col) (col + 1) tc))
let (tl,tc) = start t in
let (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
@@ -196,12 +196,12 @@ indented (P p) = P $ \toks,com,ops,indent => case toks of
||| expect token of given kind
export
token' : Kind -> Parser String
token' k = pred (\t => t.val.kind == k) "Expected a \{show k} token"
token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token"
export
keyword' : String -> Parser ()
-- FIXME make this an appropriate whitelist
keyword' kw = ignore $ pred (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}"
keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}"
||| expect indented token of given kind
export

7
src/Lib/Prettier.idr
View File

@@ -124,19 +124,20 @@ export
bracket : String -> Doc -> String -> Doc
bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
export infixl 5 <+/>
export
infixl 5 <+/>
||| Either space or newline
export
(<+/>) : Doc -> Doc -> Doc
x <+/> y = x ++ (text " " `Alt` line) ++ y
x <+/> y = x ++ Alt (text " ") line ++ y
||| Reformat some docs to fill. Not sure if I want this precise behavior or not.
export
fill : List Doc -> Doc
fill [] = Empty
fill [x] = x
fill (x :: y :: xs) = (flatten x <+> fill (flatten y :: xs)) `Alt` (x </> fill (y :: xs))
fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
||| separate with comma
export

21
src/Lib/Tokenizer.idr
View File

@@ -34,7 +34,7 @@ record TState where
rawTokenise : TState -> Either Error TState
quoteTokenise : TState -> Int -> Int -> SnocList Char -> Either Error TState
quoteTokenise ts@(TS el ec toks chars) sl sc acc = case chars of
quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of
'"' :: cs => Right (TS el ec (toks :< stok) chars)
'\\' :: '{' :: cs => do
let tok = MkBounded (Tok StartInterp "\\{") (MkBounds el ec el (ec + 2))
@@ -45,14 +45,15 @@ quoteTokenise ts@(TS el ec toks chars) sl sc acc = case chars of
in quoteTokenise (TS el (ec + 1) (toks :< tok) cs) el (ec + 1) [<]
cs => Left $ E (MkFC "" (el, ec)) "Expected '{'"
-- TODO newline in string should be an error
'\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) sl sc (acc :< '\n')
'\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) sl sc (acc :< c)
c :: cs => quoteTokenise (TS el (ec + 1) toks cs) sl sc (acc :< c)
'\n' :: cs => Left $ E (MkFC "" (el, ec)) "Newline in string"
'\\' :: '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 + 1) toks cs) startl startc (acc :< c)
Nil => Left $ E (MkFC "" (el, ec)) "Expected '\"' at EOF"
where
stok : BTok
stok = MkBounded (Tok StringKind (pack $ acc <>> [])) (MkBounds sl sc el ec)
stok = MkBounded (Tok StringKind (pack $ acc <>> [])) (MkBounds startl startc el ec)
@@ -60,8 +61,6 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
Nil => Right $ ts
' ' :: cs => rawTokenise (TS sl (sc + 1) toks cs)
'\n' :: cs => rawTokenise (TS (sl + 1) 0 toks cs)
'{' :: '{' :: cs => rawTokenise (TS sl (sc + 2) (toks :< mktok False sl (sc + 2) Keyword "{{" ) cs)
'}' :: '}' :: cs => rawTokenise (TS sl (sc + 2) (toks :< mktok False sl (sc + 2) Keyword "}}" ) cs)
'"' :: cs => do
let tok = mktok False sl (sc + 1) StartQuote "\""
@@ -71,6 +70,13 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
rawTokenise (TS sl (sc + 1) (toks :< tok) cs)
cs => Left $ E (MkFC "" (sl, sc)) "Expected '\"'"
'{' :: '{' :: cs => do
let tok = mktok False sl (sc + 2) Keyword "{{"
(TS sl sc toks chars) <- rawTokenise (TS sl (sc + 2) (toks :< tok) cs)
case chars of
'}' :: '}' :: cs => let tok = mktok False sl (sc + 2) Keyword "}}" in
rawTokenise (TS sl (sc + 2) (toks :< tok) cs)
cs => Left $ E (MkFC "" (sl, sc)) "Expected '}}'"
'}' :: cs => Right ts
'{' :: cs => do
@@ -92,7 +98,6 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
'-' :: '-' :: cs => lineComment (TS sl (sc + 2) toks cs)
'/' :: '-' :: cs => blockComment (TS sl (sc + 2) toks cs)
'`' :: cs => doBacktick (TS sl (sc + 1) toks cs) [<]
'"' :: cs => doQuote (TS sl (sc + 1) toks cs) [<]
'.' :: cs => doRest (TS sl (sc + 1) toks cs) Projection isIdent (Lin :< '.')
'-' :: c :: cs => if isDigit c
then doRest (TS sl (sc + 2) toks cs) Number isDigit (Lin :< '-' :< c)