Update Combinatory.newt, fix parse error

newt-vscode/src/abbrev.ts

@@ -1,4 +1,5 @@
-// This needs to be flexhed out a lot, I've been adding them as needed
+// This needs to be fleshed out a lot, I've been adding them as needed
+// There is a mix of agda, lean, and my own shortcuts here
 export const ABBREV: Record<string, string> = {
   "\\x": "×",
   "\\r": "→",
@@ -8,20 +9,26 @@ export const ABBREV: Record<string, string> = {
   "\\circ": "∘",
   "\\oplus": "⊕",
   "\\otimes": "⊗",
+  // lean
   "\\1": "₁",
   "\\2": "₂",
   "\\<": "⟨",
   "\\>": "⟩",
+  // agda
   "\\_0": "₀",
   "\\_1": "₁",
   "\\_2": "₂",
   "\\_3": "₃",
+  // lean has \n here, which is a royal pain
   "\\neg": "¬",
   "\\bN": "ℕ",
   "\\bZ": "ℤ",
-  "\\gi": "ι",
-  "\\gs": "σ",
-  "\\gt": "τ",
-  "\\gD": "Δ",
-  "\\gG": "Γ"
+  "\\GG": "Γ",
+  "\\Gi": "ι",
+  "\\Gl": "λ",
+  "\\Gs": "σ",
+  "\\Gt": "τ",
+  "\\GD": "Δ",
+  "\\[[": "⟦",
+  "\\]]": "⟧",
 };

newt-vscode/src/extension.ts

@@ -30,10 +30,14 @@ export function activate(context: vscode.ExtensionContext) {
     const changes = event.contentChanges;
     if (changes.length === 0) return;
 
+    // TODO - agda input mode does the replacement as soon as possible
+    // but if the sequence is a prefix, it will change for subsequent characters
+    // The latter would require keeping state, but if we don't allow sequences to prefix
+    // each other, we could activate quicker.
     const lastChange = changes[changes.length - 1];
     const text = lastChange.text;
     // Check if the last change is a potential shortcut trigger
-    if (!text || !( " ')\\".includes(text) || text.startsWith('\n'))) return;
+    if (!text || !( " ')\\_".includes(text) || text.startsWith('\n'))) return;
 
     const document = editor.document;
     const position = lastChange.range.end;

src/Lib/Parser.newt

@@ -179,7 +179,11 @@ pratt ops prec stop left spine = do
           Just (MkOp name p fix False rule) => if p < prec
             then pure (left, spine)
             else runRule p fix stop rule (RApp (getFC left + fc) (RVar fc name) left Explicit) rest
-          Just _ => fail "expected operator"
+          -- The argument is a prefix op
+          Just (MkOp name p fix True rule) => do
+            (arg, rest) <- runPrefix stop tm rest
+            pratt ops prec stop (RApp (getFC left + getFC arg) left arg Explicit) rest
+            -- fail "expected operator \{show spine} got \{show name}"
           Nothing =>
             if isPrefixOf "." nm
             then pratt ops prec stop (RApp (getFC left + getFC tm) tm left Explicit) rest
@@ -236,6 +240,8 @@ 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"
          _ =>
           pure (left, spine)
     runPrefix stop left spine = pure (left, spine)

tests/Combinatory.newt

@@ -1,6 +1,7 @@
 module Combinatory
 
 -- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
+-- prj/menagerie/papers/combinatory
 
 data Unit : U where
   MkUnit : Unit
@@ -10,8 +11,6 @@ data List : U -> U where
   Nil : {A : U} -> List A
   _::_ : {A : U} -> A -> List A -> List A
 
--- prj/menagerie/papers/combinatory
-
 infixr 6 _~>_
 data Type : U where
   ι : Type
@@ -41,23 +40,17 @@ data Env : Ctx -> U where
   ENil : Env Nil
   _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
 
--- TODO there is a problem here with coverage checking
--- I suspect something is being split before it's ready
+lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
+lookup Here (x ::: y) = x
+lookup () ENil
+lookup (There i) (x ::: env) = lookup i env
 
--- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
--- lookup Here (x ::: y) = x
--- lookup (There i) (x ::: env) = lookup i env
-
-lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
-lookup2 (x ::: y) Here = x
-lookup2 (x ::: env) (There i) = lookup2 env i
-
--- TODO MixFix - this was ⟦_⟧
-eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
+infixl 1 ⟦_⟧
+⟦_⟧ : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
 -- there was a unification error in direct application
-eval (App t u) env = (eval t env) (eval u env)
-eval (Lam t) env = \ x => eval t (x ::: env)
-eval (Var i) env = lookup2 env i
+⟦ App t u ⟧ env = (⟦ t ⟧ env) (⟦ u ⟧ env)
+⟦ Lam t ⟧ env = \ x => ⟦ t ⟧ (x ::: env)
+⟦ Var i ⟧ env = lookup i env
 
 data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
   S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
@@ -65,7 +58,7 @@ data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
   I : {Γ : Ctx} {σ : Type} → Comb Γ (σ ~> σ) (\ env => \ x => x)
   B : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => f (g x))
   C : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> τ ~> (σ ~> τ')) (\ env => \ f g x => (f x) g)
-  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup2 env i)
+  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup i env)
   CApp : {Γ : Ctx} {σ τ : Type} {f : _} {x : _} → Comb Γ (σ ~> τ) f → Comb Γ σ x → Comb Γ τ (\ env => (f env) (x env))
 
 sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
@@ -86,11 +79,12 @@ abs I = CApp K I
 abs B = CApp K B
 abs C = CApp K C
 abs (CApp t u) = sapp (abs t) (abs u)
--- lookup2 was getting stuck, needed to re-eval the types in the rewritten env.
+-- lookup was getting stuck, needed to re-eval the types in the rewritten env.
 abs (CVar Here) = I
 abs (CVar (There i)) = CApp K (CVar i)
 
-translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm)
+-- Was a bug in pratt parser when argument `⟦ tm ⟧` had a prefix operator
+translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ ⟦ tm ⟧
 translate (App t u) = CApp (translate t) (translate u)
 translate (Lam t) = abs (translate t)
 translate (Var i) = CVar i

tests/Problem.newt

@@ -1,48 +0,0 @@
-module Problem
-
--- partial finished translation of "A correct-by-construction conversion from lambda calculus to combinatory logic", by Wouter Swierstra
--- added as a test of impossible clauses (in `lookup` below)
--- prj/menagerie/papers/combinatory
-
-data Unit : U where
-  MkUnit : Unit
-
-infixr 7 _::_
-data List : U → U where
-  Nil : {A : U} → List A
-  _::_ : {A : U} → A → List A → List A
-
-infixr 6 _~>_
-data Type : U where
-  ι : Type
-  _~>_ : Type → Type → Type
-
-A : U
-A = Unit
-
-Val : Type → U
-Val ι = A
-Val (x ~> y) = Val x → Val y
-
-Ctx : U
-Ctx = List Type
-
-data Ref : Type → Ctx → U where
-  Z : {σ : Type} {Γ : Ctx} → Ref σ (σ :: Γ)
-  S : {σ τ : Type} {Γ : Ctx} → Ref σ Γ → Ref σ (τ :: Γ)
-
-data Term : Ctx → Type → U where
-  App : {Γ : Ctx} {σ τ : Type} → Term Γ (σ ~> τ) → Term Γ σ → Term Γ τ
-  Lam : {Γ : Ctx} {σ τ : Type} → Term (σ :: Γ) τ → Term Γ (σ ~> τ)
-  Var : {Γ : Ctx} {σ : Type} → Ref σ Γ → Term Γ σ
-
-infixr 7 _:::_
-data Env : Ctx → U where
-  ENil : Env Nil
-  _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
-
--- due to the order that we match constructors, we need the impossible clause here
-lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
-lookup Z (x ::: y) = x
-lookup () ENil
-lookup (S i) (x ::: env) = lookup i env