operator sections

Sometimes a Bound variable on the LHS became Defined to itself.
This commit also resurfaces INFO messages, to aid finding the root
cause of errors.

Makefile

@@ -11,7 +11,9 @@ all: newt.js
 
 REV=$(shell git rev-parse --short HEAD)
 src/Revision.newt: .PHONY
-	echo "module Revision\nimport Prelude\ngitRevision : String\ngitRevision = \"${REV}\"" > src/Revision.newt
+	echo "module Revision\nimport Prelude\ngitRevision : String\ngitRevision = \"${REV}\"" > src/Revision.newt.new
+	cmp src/Revision.newt.new src/Revision.newt || cp src/Revision.newt.new src/Revision.newt
+	rm -f src/Revision.newt.new
 
 newt.js: ${SRCS} src/Revision.newt
 	-rm build/* >/dev/null

TODO.md

@@ -1,9 +1,11 @@
 
 ## TODO
 
+- [x] change "in prefix position" and "trailing operator" errors to do sections
 - [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly
-  - There may be ambiguity issues
+  - There may be ambiguity issues at the parsing level, but we don't have typecase, so...
 - [x] get some names on add missing cases (if not too difficult)
+- [ ] Implement "add missing cases" for playground
 - [x] add optional types to case `case xxx : Maybe Int of ...`
 - [x] "Expected keyword" at `\ a ->` should be error at the `->`
 - [x] Show Either
@@ -209,7 +211,7 @@
   - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
   - [ ] `$` no longer works inside ≡⟨ ⟩ - sort out how to support both that and `$ \ x => ...` (or don't bother)
     - We'd either need to blacklist all non-initial mixfix bits at the appropriate spots or always pass around a terminating token.
-    - I'm leaning towards _no_ here, because I may want to lift mixfix processing out of the parsing step in the future. This isn't
+    - I'm leaning towards _no_ here, because I may want to lift mixfix processing out of the parsing step in the future.
 - [x] **Translate newt to newt**
   - [x] Support @ on the LHS
   - [x] if / then / else sugar

scripts/test

@@ -30,7 +30,7 @@ for fn in tests/*.newt ; do
   fi
   # if there is a golden file, run the code and compare output
   if [ -f ${fn}.golden ]; then
-    bun run out.js > tmp/${bn}.out
+    node out.js > tmp/${bn}.out
     if [ $? != "0" ]; then
       echo Run failed for $fn
       failed=$((failed + 1))

src/Lib/Elab.newt

@@ -283,7 +283,7 @@ addConstraint env ix sp tm = do
   let (CheckAll) = mc.mcmode | _ => pure MkUnit
   updateMeta ix $ \case
     (Unsolved pos k a b c cons) => do
-      debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
+      debug $ \ _ => "Add constraint \{show ix} \{show sp} =?= \{show tm}"
       pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
     (Solved fc k tm) => error fc "Meta \{show k} already solved [addConstraint]"
     (OutOfScope) => error' "Meta \{show ix} out of scope"
@@ -391,7 +391,7 @@ solve env m sp t = do
     | _ => do
       let l = length' env
       debug $ \ _ => "meta \{show m} (\{show ix}) applied to \{show $ snoclen sp} args instead of \{show size}"
-      debug $ \ _ => "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}"
+      debug $ \ _ => "CONSTRAINT \{show ix} \{show sp} =?= \{show t}"
       addConstraint env m sp t
   let l = length' env
   debug $ \ _ => "meta \{show meta}"
@@ -435,12 +435,10 @@ solve env m sp t = do
     (\case
       Postpone fc ix msg => do
         -- let someone else solve this and then check again.
-        debug $ \ _ => "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}"
+        debug $ \ _ => "CONSTRAINT2 \{show ix} \{show sp} =?= \{show t}"
         addConstraint env m sp t
-        -- I get legit errors after stuffing in solution
-        -- report for now, tests aren't hitting this branch
-      err => throwError err
-        -- debug $ \ _ => "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}"
+      E fc msg => throwError (E fc "\{msg} for \{show ix} \{show sp} =?= \{show t}")
+        -- debug $ \ _ => "CONSTRAINT3 \{show ix} \{show sp} =?= \{show t}"
         -- debug $ \ _ => "because \{showError "" err}"
         -- addConstraint env m sp t
         )
@@ -628,7 +626,7 @@ freshMeta ctx fc ty kind = do
   debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
   -- need the ns here
   -- we were fudging this for v1
-  let qn = QN top.ns "$m\{show mc.next}"
+  let qn = QN top.ns "\{show mc.next}"
   let newmeta = Unsolved fc qn ctx ty kind Nil
   let autos = case kind of
       AutoSolve => qn :: mc.autos
@@ -671,8 +669,6 @@ primType fc nm = do
       Just (MkEntry _ name ty (PrimTCon _) _) => pure $ VRef fc name Lin
       _ => error fc "Primitive type \{show nm} not in scope"
 
-infer : Context -> Raw  -> M (Tm × Val)
-
 data Bind = MkBind String Icit Val
 
 instance Show Bind where
@@ -775,6 +771,9 @@ substVal k v tm = go tm
 updateContext : Context -> List (Int × Val) -> M Context
 updateContext ctx Nil = pure ctx
 updateContext ctx ((k, val) :: cs) =
+  -- We were turning Bound into Defined
+  if isSelf k val then updateContext ctx cs
+  else
   let ix = cast $ lvl2ix (length' ctx.env) k in
   case getAt ix ctx.env of
     (Just (VVar _ k' Lin)) =>
@@ -789,6 +788,10 @@ updateContext ctx ((k, val) :: cs) =
       updateContext ctx cs
     Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext"
   where
+    isSelf : Int → Val → Bool
+    isSelf ix (VVar _ k Lin) = ix == k
+    isSelf ix _ = False
+
     replaceV : ∀ a. Nat -> a -> List a -> List a
     replaceV k x Nil = Nil
     replaceV Z x (y :: xs) = x :: xs
@@ -1426,6 +1429,7 @@ updateRec ctx fc clauses arg ty = do
     getTele Nothing v = error (getFC v) "Expected a pi type, got \{show v}"
     getTele _ v = error (getFC v) "Expected a record type, got \{show v}"
 
+infer : Context -> Raw  -> M (Tm × Val)
 
 check ctx tm ty = do
   ty' <- forceType ctx.env ty

src/Lib/Parser.newt

@@ -219,7 +219,11 @@ pratt ops prec stop left spine = do
                 ((_, fc, right) :: rest) => do
                   (right, rest) <- pratt ops pr stop right rest
                   pratt ops prec stop (RApp (getFC left + getFC right) left right Explicit) rest
-                _ => fail "trailing operator"
+                _ =>
+                  -- Trailing operator section, like (2 +)
+                  pratt ops prec stop left Nil
+                  -- fail "trailing operator"
+
 
     runRule p fix stop (nm :: rule) left spine = do
       case spine of
@@ -240,8 +244,10 @@ pratt ops prec stop left spine = do
            -- TODO False should be an error here
          Just (MkOp name p fix True rule) => do
             runRule p fix stop rule (RVar fc name) spine
-         Just (MkOp name p fix False rule) => do
-            fail "got infix \{show name} in prefix position"
+         Just (MkOp name p fix False rule) =>
+            -- REVIEW We could also use a lambda with a fresh name
+            runRule p fix stop rule (RApp fc (RVar fc "flip") (RVar fc name) Explicit) spine
+            -- fail "got infix \{show name} in prefix position"
          _ =>
           pure (left, spine)
     runPrefix stop left spine = pure (left, spine)

src/Main.newt

@@ -179,9 +179,9 @@ processModule importFC base stk qn@(QN ns nm) = do
   let modules = updateMap modns mod top.modules
   modifyTop [modules := modules]
 
+  logMetas $ reverse $ listValues top.metaCtx.metas
   let (Nil) = top.errors
     | errors => exitFailure "Compile failed"
-  logMetas $ reverse $ listValues top.metaCtx.metas
   pure src
   where
     tryProcessDecl : String -> List String → Decl -> M Unit

src/Prelude.newt

@@ -716,6 +716,13 @@ instance Functor IO where
 uncurry : ∀ a b c. (a → b → c) → (a × b) → c
 uncurry f (a,b) = f a b
 
+curry : ∀ a b c. (a × b → c) → (a → b → c)
+curry f a b = f (a,b)
+
+-- TODO Belongs in prelude, but I need to rename a function in Lib.Compile (or let local win over imports)
+-- apply : ∀ a b. (a → b) → a → b
+-- apply f a = f a
+
 -- TODO Idris has a tail recursive version of this
 instance Applicative List where
   return a = a :: Nil

tests/Data

@@ -0,0 +1 @@
+../src/Data

tests/Data/SortedMap.newt

@@ -1 +0,0 @@
-../../src/Data/SortedMap.newt

tests/ErrMsg.newt

@@ -1,14 +0,0 @@
-module ErrMsg
-
-import Prelude
-
-infixl 5 _$$_
-
-_$$_ : Nat → (Nat → Nat) → Nat
-a $$ b = a + b a
-
--- Say something other than expected record
--- Why do we get there? shouldn't the progress made by parseDef short circuit the <|>?
-blah : Nat → Nat
-blah x = x $$ $ \ y => y
-

tests/ErrMsg.newt.fail

@@ -1,6 +0,0 @@
-*** Process tests/ErrMsg.newt
-module Prelude
-module ErrMsg
-ERROR at tests/ErrMsg.newt:13:15--13:16: trailing operator
-
-Compile failed

tests/Section.newt

@@ -0,0 +1,20 @@
+module Section
+
+import Prelude
+
+-- got infix in prefix position
+add : Int → Int → Int
+add = (+)
+
+add2 : Int → Int
+add2 = (+ 2)
+
+-- trailing operator
+add2' : Int → Int
+add2' = (2 +)
+
+main : IO Unit
+main = do
+    printLn $ (+) 2 3
+    printLn $ (+ 3) 2
+    printLn $ (2 +) 3

tests/Section.newt.golden

@@ -0,0 +1,3 @@
+5
+5
+5

tests/TrailDollar.newt

@@ -0,0 +1,13 @@
+module TrailDollar
+
+import Prelude
+
+infixl 5 _$$_
+
+_$$_ : Nat → (Nat → Nat) → Nat
+a $$ b = a + b a
+
+-- Previously this didn't parse, but it does with operator section support.
+blah : Nat → Nat
+blah x = x $$ $ \ y => y
+

tests/WellTyped.newt

@@ -0,0 +1,75 @@
+module WellTyped
+
+-- Idris2's "Well Typed Interpreter" example
+-- This is a little painful for lack of overloading.
+-- I can add idris/haskell style sections.
+-- This is revealing some issues. :/
+
+-- I had to put {0 ctxt : Vect n Ty} →  in manually, the `∀ ctxt` wasn't inferring the type.
+-- This may be because we have `n`, which becomes a parameter when do it manually.
+-- That would explain why Idris adds those...
+
+-- This also revealed an issue in case tree building where a bound name was accidentally made into a defined one.
+
+import Prelude
+import Data.Vect
+import Data.Fin
+
+data Ty = TyInt | TyBool | TyFun Ty Ty
+
+interpTy : Ty → U
+interpTy TyInt = Int
+interpTy TyBool = Bool
+interpTy (TyFun x y) = interpTy x → interpTy y
+
+data HasType : ∀ n. (i : Fin n) → Vect n Ty → Ty → U where
+  Stop : ∀ t n. {0 ctxt : Vect n Ty} → HasType FZ (t :- ctxt) t
+  Pop  : ∀ n t u. {0 ctxt : Vect n Ty} {0 k : Fin n} → HasType k ctxt t → HasType (FS k) (u :- ctxt) t
+
+data Expr : ∀ n. Vect n Ty → Ty → U where
+  Var : ∀ t n. {0 ctxt : Vect n Ty} {0 i : Fin n} → HasType i ctxt t → Expr ctxt t
+  Val : ∀ n. {0 ctxt : Vect n Ty} → (x : Int) → Expr ctxt TyInt
+  Lam : ∀ a n t. {0 ctxt : Vect n Ty} → Expr (a :- ctxt) t → Expr ctxt (TyFun a t)
+  App : ∀ n a t. {0 ctxt : Vect n Ty} → Expr ctxt (TyFun a t) → Expr ctxt a → Expr ctxt t
+  Op  : ∀ a b c n. {0 ctxt : Vect n Ty} → (interpTy a → interpTy b → interpTy c) →
+        Expr ctxt a → Expr ctxt b → Expr ctxt c
+  -- TODO Idris has Lazy on the arms, should work if we explicitly force
+  If  : ∀ n a. {0 ctxt : Vect n Ty} → Expr ctxt TyBool →
+        (Expr ctxt a) →
+        (Expr ctxt a) → Expr ctxt a
+
+infixr 4 _:::_
+data Env : ∀ n. Vect n Ty → U where
+  Empty  : Env VNil
+  _:::_ : ∀ a n. {0 ctxt : Vect n Ty} → interpTy a → Env ctxt → Env (a :- ctxt)
+
+lookup : ∀ n t. {0 ctxt : Vect n Ty} {0 i : Fin n} → HasType i ctxt t → Env ctxt → interpTy t
+lookup Stop (x ::: xs) = x
+lookup () Empty
+lookup (Pop k) (x ::: xs) = lookup k xs
+
+interp : ∀ n t. {0 ctxt : Vect n Ty} → Env ctxt → Expr ctxt t → interpTy t
+interp env (Var i)    = lookup i env
+interp env (Val x)    = x
+interp env (Lam x)    = \y => interp (y ::: env) x
+interp env (App x y)  = interp env x $ interp env y
+interp env (Op f x y) = f (interp env x) (interp env y)
+interp env (If x y z) = if interp env x then interp env y
+                                        else interp env z
+
+add : ∀ n. {0 ctxt : Vect n Ty} → Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
+add = Lam (Lam (Op _+_ (Var Stop) (Var (Pop Stop))))
+
+fact : ∀ n. {0 ctxt : Vect n Ty} → Expr ctxt (TyFun TyInt TyInt)
+-- TODO the `Bool =?= interpTy ...` is stuck on ?m14
+-- I think we may need to need to delay the constraint until m14 is solved?
+-- But I think I have code to do that already
+fact = Lam (If (Op {_} {_} {TyBool} _==_ (Var Stop) (Val 0))
+               (Val 1)
+               (Op _*_ (App fact (Op _-_ (Var Stop) (Val 1)))
+                       (Var Stop)))
+
+-- main : IO Unit
+-- main = do putStr "Enter a number: "
+--           Right x <- readLine | _ => putStrLn "EOF"
+--           printLn (interp Empty fact (stringToInt x))