From 4dec53daa1cdf42ba2023ed664d4429a63ac772f Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 1 Jan 2025 08:46:25 -0800
Subject: [PATCH] additional changes for porting, fix to lexing

---
 scripts/translate.sh    |  3 +++
 src/Lib/Common.idr      |  4 ++++
 src/Lib/Elab.idr        | 19 ++++++-------------
 src/Lib/Eval.idr        |  4 ++--
 src/Lib/Parser/Impl.idr | 14 +++++++-------
 src/Lib/Prettier.idr    |  7 ++++---
 src/Lib/Tokenizer.idr   | 21 +++++++++++++--------
 7 files changed, 39 insertions(+), 33 deletions(-)

diff --git a/scripts/translate.sh b/scripts/translate.sh
index ba441fc..bbfc09d 100755
--- a/scripts/translate.sh
+++ b/scripts/translate.sh
@@ -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;
diff --git a/src/Lib/Common.idr b/src/Lib/Common.idr
index 1cac9be..2155dde 100644
--- a/src/Lib/Common.idr
+++ b/src/Lib/Common.idr
@@ -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"
 
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 8aa5586..05a1e89 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -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..
diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr
index cc9aa05..3ee99cd 100644
--- a/src/Lib/Eval.idr
+++ b/src/Lib/Eval.idr
@@ -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
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index ed23eb4..2c84eb2 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -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
diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr
index 3e74a6e..8dab901 100644
--- a/src/Lib/Prettier.idr
+++ b/src/Lib/Prettier.idr
@@ -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
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index 66c7d86..c021da1 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -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)