From 91bb79a998fe8de07bdb0ff3b9a158181d52bd63 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 9 Nov 2024 22:11:58 -0800
Subject: [PATCH] Mixfix operators

---
 aoc2023/Day1.newt                 |   4 +-
 aoc2023/Lib.newt                  |   4 +-
 playground/samples/Day1.newt      |   4 +-
 playground/samples/Lib.newt       |   6 +-
 playground/samples/Reasoning.newt | 157 ++++++++++++++++++++++++++++++
 playground/src/main.ts            |   1 +
 scripts/test                      |   2 +-
 src/Lib/Common.idr                |  10 ++
 src/Lib/Parser.idr                |  71 ++++++++++----
 src/Lib/Parser/Impl.idr           |  22 +++--
 src/Lib/Tokenizer.idr             |   9 +-
 src/Lib/TopContext.idr            |   2 +-
 src/Lib/Types.idr                 |   2 +-
 13 files changed, 250 insertions(+), 44 deletions(-)
 create mode 100644 playground/samples/Reasoning.newt

diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt
index a291ddf..63d2957 100644
--- a/aoc2023/Day1.newt
+++ b/aoc2023/Day1.newt
@@ -59,9 +59,9 @@ runFile fn =
   let text = readFile fn in
   log fn >>
   log "part1" >>
-  log (part1 text (digits1 . unpack)) >>
+  log (part1 text (digits1 ∘  unpack)) >>
   log "part2" >>
-  log (part1 text (digits2 . unpack)) >>
+  log (part1 text (digits2 ∘ unpack)) >>
   log ""
 
 
diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt
index 09b4465..d59ccbf 100644
--- a/aoc2023/Lib.newt
+++ b/aoc2023/Lib.newt
@@ -157,6 +157,6 @@ map f Nil = Nil
 map f (x :: xs) = f x :: map f xs
 
 
-infixl 9 _._
-_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+infixl 9 _∘_
+_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
 (f . g) x = f ( g x)
diff --git a/playground/samples/Day1.newt b/playground/samples/Day1.newt
index a291ddf..3338b6c 100644
--- a/playground/samples/Day1.newt
+++ b/playground/samples/Day1.newt
@@ -59,9 +59,9 @@ runFile fn =
   let text = readFile fn in
   log fn >>
   log "part1" >>
-  log (part1 text (digits1 . unpack)) >>
+  log (part1 text (digits1 ∘ unpack)) >>
   log "part2" >>
-  log (part1 text (digits2 . unpack)) >>
+  log (part1 text (digits2 ∘ unpack)) >>
   log ""
 
 
diff --git a/playground/samples/Lib.newt b/playground/samples/Lib.newt
index 09b4465..f90c397 100644
--- a/playground/samples/Lib.newt
+++ b/playground/samples/Lib.newt
@@ -157,6 +157,6 @@ map f Nil = Nil
 map f (x :: xs) = f x :: map f xs
 
 
-infixl 9 _._
-_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
-(f . g) x = f ( g x)
+infixl 9 _∘_
+_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+(f ∘ g) x = f (g x)
diff --git a/playground/samples/Reasoning.newt b/playground/samples/Reasoning.newt
new file mode 100644
index 0000000..b5eedf0
--- /dev/null
+++ b/playground/samples/Reasoning.newt
@@ -0,0 +1,157 @@
+module Reasoning
+
+infix 4 _≡_
+data _≡_ : {A : U} → A → A → U where
+  Refl : {A} {x : A} → x ≡ x
+
+sym : {A} {x y : A} → x ≡ y → y ≡ x
+sym Refl = Refl
+
+trans : {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans Refl eq = eq
+
+cong : {A B} (f : A → B) {x y : A}
+  → x ≡ y
+  → f x ≡ f y
+cong f Refl = Refl
+
+cong-app : {A B} {f g : A → B}
+  → f ≡ g
+  → (x : A) →  f x ≡ g x
+cong-app Refl = λ y => Refl
+
+infixl 1 begin_
+infixr 2 _≡⟨⟩_ _≡⟨_⟩_
+infixl 3 _∎
+
+begin_ : {A} {x y : A} → x ≡ y → x ≡ y
+begin_ x≡y = x≡y
+
+_≡⟨⟩_  : {A} (x : A) {y : A} → x ≡ y → x ≡ y
+x ≡⟨⟩ x≡y = x≡y
+
+_≡⟨_⟩_ : {A} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
+x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
+
+_∎ : {A} → (x : A) → x ≡ x
+x ∎ = Refl
+
+
+-- From the "Lists" chapter of Programming Language Foundations in Agda
+-- https://plfa.github.io/Lists/
+
+-- We define a few types and functions on lists and prove a couple of properties
+-- about them
+
+-- Natural numbers are zero (Z) or the successor (S) of a natural number
+-- We'll use these to represent the length of lists
+data Nat : U where
+    Z : Nat
+    S : Nat -> Nat
+
+-- declare a plus operator and define the corresponding function
+infixl 7 _+_
+_+_ : Nat -> Nat -> Nat
+Z + m = m
+S n + m = S (n + m)
+
+-- A list is empty (Nil) or a value followed by a list (separated by the :: operator)
+infixr 7  _::_
+data List : U -> U where
+    Nil : ∀ A. List A
+    _::_ : ∀ A. A -> List A -> List A
+
+-- length of a list is defined inductively
+length : ∀ A . List A -> Nat
+length Nil = Z
+length (x :: xs) = S (length xs)
+
+-- List concatenation
+infixl 5 _++_
+_++_ : ∀ A. List A -> List A -> List A
+Nil ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+-- This lets us replace a with b inside an expression if a ≡ b
+replace : ∀ A a b. (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+-- if concatenate two lists, the length is the sum of the lengths
+-- of the original lists
+length-++ : ∀ A. (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
+length-++ Nil ys = Refl
+length-++ (x :: xs) ys = cong S (length-++ xs ys)
+
+-- a function to reverse a list
+reverse : ∀ A. List A -> List A
+reverse Nil = Nil
+reverse (x :: xs) = reverse xs ++ (x :: Nil)
+
+-- if we add an empty list to a list, we get the original back
+++-identity : ∀ A. (xs : List A) -> xs ++ Nil ≡ xs
+++-identity Nil = Refl
+++-identity (x :: xs) = cong (_::_ x) (++-identity xs)
+
+-- concatenation is associative
+++-associative : ∀ A. (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
+
+-- reverse distributes over ++, but switches order
+reverse-++-distrib : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+reverse-++-distrib Nil ys = -- sym (++-identity (reverse ys))
+  begin
+    reverse ( Nil ++ ys )
+  ≡⟨⟩
+    reverse ys
+  ≡⟨ sym (++-identity (reverse ys)) ⟩
+    reverse ys ++ Nil
+  ∎
+
+reverse-++-distrib (x :: xs) ys =
+  begin
+    reverse ((x :: xs ) ++ ys)
+  ≡⟨⟩
+    reverse (xs ++ ys) ++ (x :: Nil)
+  ≡⟨ cong (\ z => z  ++ (x :: Nil)) (reverse-++-distrib xs ys) ⟩
+    (reverse ys ++ reverse xs) ++ (x :: Nil)
+  ≡⟨ sym (++-associative (reverse ys) (reverse xs) (x :: Nil)) ⟩
+    reverse ys ++ reverse (x :: xs)
+  ∎
+
+-- reverse of reverse gives you the original list
+reverse-involutive : ∀ A. (xs : List A) -> reverse (reverse xs) ≡ xs
+reverse-involutive Nil = Refl
+reverse-involutive (x :: xs) =
+  begin
+    reverse (reverse (x :: xs))
+  ≡⟨ reverse-++-distrib (reverse xs) (x :: Nil) ⟩
+    (x :: Nil) ++ reverse (reverse xs)
+  ≡⟨ cong (_::_ x) (reverse-involutive xs) ⟩
+    x :: xs
+  ∎
+
+-- helper for a different version of reverse
+shunt : ∀ A. List A -> List A -> List A
+shunt Nil ys = ys
+shunt (x :: xs) ys = shunt xs (x :: ys)
+
+-- lemma
+shunt-reverse : ∀ A. (xs ys : List A) -> shunt xs ys ≡ reverse xs ++ ys
+shunt-reverse Nil ys = Refl
+shunt-reverse (x :: xs) ys =
+  begin
+    shunt xs (x :: ys)
+  ≡⟨ shunt-reverse xs (x :: ys) ⟩
+    reverse xs ++ (x :: ys)
+  ≡⟨⟩
+    reverse xs ++ ((x :: Nil) ++ ys)
+  ≡⟨ (++-associative (reverse xs) (x :: Nil) ys) ⟩
+    reverse (x :: xs) ++ ys
+  ∎
+
+-- an alternative definition of reverse
+reverse' : ∀ A. List A -> List A
+reverse' xs = shunt xs Nil
+
+-- proof that the reverse and reverse' give the same results
+reverses : ∀ A. (xs : List A) → reverse' xs ≡ reverse xs
+reverses xs = trans (shunt-reverse xs Nil) (++-identity _)
diff --git a/playground/src/main.ts b/playground/src/main.ts
index c94170b..7fb9099 100644
--- a/playground/src/main.ts
+++ b/playground/src/main.ts
@@ -146,6 +146,7 @@ const SAMPLES = [
   "Tour.newt",
   "Tree.newt",
   // "Prelude.newt",
+  "Reasoning.newt",
   "Lists.newt",
   "Day1.newt",
   "Day2.newt",
diff --git a/scripts/test b/scripts/test
index e3e226d..b2ac60b 100755
--- a/scripts/test
+++ b/scripts/test
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-for i in tests/black/*.newt; do
+for i in tests/black/*.newt playground/samples/*.newt; do
   ./build/exec/newt $i
   if [ $? != "0" ]; then
     echo FAIL $i
diff --git a/src/Lib/Common.idr b/src/Lib/Common.idr
index 0590511..02b8082 100644
--- a/src/Lib/Common.idr
+++ b/src/Lib/Common.idr
@@ -1,6 +1,7 @@
 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
@@ -54,10 +55,19 @@ Show Fixity where
   show InfixR = "infixr"
   show Infix = "infix"
 
+
 public export
 record OpDef where
   constructor MkOp
   name : String
   prec : Int
   fix : Fixity
+  isPrefix : Bool
+  ||| rule is everything after the first part of the operator, splitting on `_`
+  ||| a normal infix operator will have a trailing `""` which will match to
+  ||| prec / prec - 1
+  rule : List String
 
+public export
+Operators : Type
+Operators = SortedMap String OpDef
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 5fd87a6..3db1b68 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -74,10 +74,6 @@ export term : (Parser Raw)
 withPos : Parser a -> Parser (FC, a)
 withPos pa = (,) <$> getPos <*> pa
 
-lookup : String -> List OpDef -> Maybe OpDef
-lookup _ [] = Nothing
-lookup name (op :: ops) = if op.name == name then Just op else lookup name ops
-
 -- the inside of Raw
 atom : Parser Raw
 atom = RU <$> getPos <* keyword "U"
@@ -98,22 +94,55 @@ pArg = do
 
 AppSpine = List (Icit,FC,Raw)
 
-pratt : List OpDef -> Int -> Raw -> AppSpine -> Parser (Raw, AppSpine)
-pratt ops prec left [] = pure (left, [])
-pratt ops prec left rest@((Explicit, fc, tm@(RVar x nm)) :: xs) =
-  let op' = ("_" ++ nm ++ "_") in
-  case lookup op' ops of
-    Nothing => pratt ops prec (RApp fc left tm Explicit) xs
-    Just (MkOp name p fix) => if p < prec
-      then pure (left, rest)
-      else
-        let pr = case fix of InfixR => p; _ => p + 1 in
-        case xs of
-          ((_, _, right) :: rest) => do
-            (right, rest) <- pratt ops pr right rest
-            pratt ops prec (RApp fc(RApp fc (RVar fc op') left Explicit) right Explicit) rest
-          _ => fail "trailing operator"
-pratt ops prec left ((icit, fc, tm) :: xs) = pratt ops prec (RApp fc left tm icit) xs
+-- helper for debugging
+traceM : Monad m => String -> m ()
+traceM msg = trace msg $ pure ()
+
+pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
+pratt ops prec stop left spine = do
+  (left, spine) <- runPrefix stop left spine
+  case spine of
+    [] => pure (left, [])
+    ((Explicit, fc, tm@(RVar x nm)) :: rest) =>
+        if nm == stop then pure (left,spine) else
+        case lookup nm ops of
+          Just (MkOp name p fix False rule) => if p < prec
+            then pure (left, spine)
+            else
+              runRule p fix stop rule (RApp fc (RVar fc name) left Explicit) rest
+          Just _ => fail "expected operator"
+          Nothing => pratt ops prec stop (RApp fc left tm Explicit) rest
+    ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp fc left tm icit) rest
+  where
+    runRule : Int -> Fixity -> String -> List String -> Raw -> AppSpine -> Parser (Raw,AppSpine)
+    runRule p fix stop [] left spine = pure (left,spine)
+    runRule p fix stop [""] left spine = do
+      let pr = case fix of InfixR => p; _ => p + 1
+      case spine of
+                ((_, fc, right) :: rest) => do
+                  (right, rest) <- pratt ops pr stop right rest
+                  pratt ops prec stop (RApp fc left right Explicit) rest
+                _ => fail "trailing operator"
+
+    runRule p fix stop (nm :: rule) left spine = do
+      let ((_,_,right)::rest) = spine | _ => fail "short"
+      (right,rest) <- pratt ops 0 nm right rest -- stop!!
+      let ((_,fc',RVar fc name) :: rest) = rest
+        | _ => fail "expected \{nm}"
+
+      if name == nm
+          then runRule p fix stop rule (RApp fc left right Explicit) rest
+          else fail "expected \{nm}"
+
+
+    runPrefix : String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
+    runPrefix stop (RVar fc nm) spine =
+      case lookup nm ops of
+           -- TODO False should be an error here
+         Just (MkOp name p fix True rule) => do
+            runRule p fix stop rule (RVar fc name) spine
+         _ => pure (left, spine)
+    runPrefix stop left spine = pure (left, spine)
 
 parseOp : Parser Raw
 parseOp = do
@@ -121,7 +150,7 @@ parseOp = do
   ops <- getOps
   hd <- atom
   rest <- many pArg
-  (res, []) <- pratt ops 0 hd rest
+  (res, []) <- pratt ops 0 "" hd rest
     | _ => fail "extra stuff"
   pure res
 
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index cdaaa22..63dc0bd 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -4,6 +4,7 @@ import Lib.Token
 import Lib.Common
 import Data.String
 import Data.Nat
+import Data.List1
 
 public export
 TokenList : Type
@@ -12,8 +13,8 @@ TokenList = List BTok
 -- Result of a parse
 public export
 data Result : Type -> Type where
-  OK : a -> (toks : TokenList) -> (com : Bool) -> List OpDef -> Result a
-  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> List OpDef -> Result a
+  OK : a -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
+  Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a
 
 export
 Functor Result where
@@ -34,10 +35,10 @@ Functor Result where
 -- This is a Reader in FC, a State in Operators, Commit flag, TokenList
 
 export
-data Parser a = P (TokenList -> Bool -> List OpDef -> (lc : FC) -> Result a)
+data Parser a = P (TokenList -> Bool -> Operators -> (lc : FC) -> Result a)
 
 export
-runP : Parser a -> TokenList -> Bool -> List OpDef -> FC -> Result a
+runP : Parser a -> TokenList -> Bool -> Operators -> FC -> Result a
 runP (P f) = f
 
 error : TokenList -> String -> Error
@@ -46,14 +47,14 @@ error ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (line,
 
 export
 parse : Parser a -> TokenList -> Either Error a
-parse pa toks = case runP pa toks False [] (-1,-1) of
+parse pa toks = case runP pa toks False empty (-1,-1) of
   Fail fatal err toks com ops => Left err
   OK a [] _ _ => Right a
   OK a ts _ _ => Left (error ts "Extra toks")
 
 ||| Intended for parsing a top level declaration
 export
-partialParse : Parser a -> List OpDef -> TokenList -> Either Error (a, List OpDef, TokenList)
+partialParse : Parser a -> Operators -> TokenList -> Either Error (a, Operators, TokenList)
 partialParse pa ops toks = case runP pa toks False ops (0,0) of
   Fail fatal err toks com ops => Left err
   OK a ts _ ops => Right (a,ops,ts)
@@ -75,13 +76,18 @@ fatal : String -> Parser a
 fatal msg = P $ \toks,com,ops,col => Fail True (error toks msg) toks com ops
 
 export
-getOps : Parser (List OpDef)
+getOps : Parser (Operators)
 getOps = P $ \ toks, com, ops, col => OK ops toks com ops
 
 export
 addOp : String -> Int -> Fixity -> Parser ()
 addOp nm prec fix = P $ \ toks, com, ops, col =>
-  OK () toks com ((MkOp nm prec fix) :: ops)
+  let parts = split (=='_') nm in
+  case parts of
+    "" ::: key :: rule => OK () toks com (insert key (MkOp nm prec fix False rule) ops)
+    key ::: rule => OK () toks com (insert key (MkOp nm prec fix True rule) ops)
+
+
 
 export
 Functor Parser where
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index 19f3ed6..f0135e0 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -8,11 +8,14 @@ import Lib.Common
 keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "ptype", "pfunc", "module", "infixl", "infixr", "infix",
-            "∀", "forall", ".",
+            "∀", "forall",
              "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"]
 
 checkKW : String -> Token Kind
-checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
+checkKW s =
+  if s /= "_" && elem '_' (unpack s) then Tok MixFix s else
+  if elem s keywords then Tok Keyword s
+  else Tok Ident s
 
 checkUKW : String -> Token Kind
 checkUKW s = if elem s keywords then Tok Keyword s else Tok UIdent s
@@ -54,7 +57,7 @@ rawTokens
   -- for now, our lambda slash is singleton
   <|> match (singleton) (Tok Symbol)
   -- TODO Drop MixFix token type when we support if_then_else_
-  <|> match (exact "_" <+> (some opMiddle) <+> exact "_") (Tok MixFix)
+  <|> match (exact "_,_" <|> exact "_._") (Tok MixFix)
   -- REVIEW - expect non-alpha after?
   <|> match (some digit) (Tok Number)
   -- for module names and maybe type constructors
diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr
index a6d4827..f25df4c 100644
--- a/src/Lib/TopContext.idr
+++ b/src/Lib/TopContext.idr
@@ -23,7 +23,7 @@ Show TopContext where
 
 public export
 empty : HasIO m => m TopContext
-empty = pure $ MkTop [] !(newIORef (MC [] 0)) False !(newIORef []) [] []
+empty = pure $ MkTop [] !(newIORef (MC [] 0)) False !(newIORef []) [] empty
 
 ||| set or replace def. probably need to check types and Axiom on replace
 public export
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 0f13e51..858e432 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -398,7 +398,7 @@ record TopContext where
   errors : IORef (List Error)
   ||| loaded modules
   loaded : List String
-  ops : List OpDef
+  ops : Operators
 
 -- we'll use this for typechecking, but need to keep a TopContext around too.
 public export