From 043ac7bd62b5f6114374a33c4bff17c6fb59837b Mon Sep 17 00:00:00 2001
From: JJ
Date: Thu, 20 Jun 2024 18:00:50 -0700
Subject: broadly switch to infix operators

---
 stlc-imp.rkt | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'stlc-imp.rkt')

diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index cd392d9..e10b09c 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -45,14 +45,14 @@
         [`(Ref ,t) (check- e2 t Γ)]
         [t #f])]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
       (and
         (equal? t t1)
         (> k (max-level e (dict-set Γ x t1) t1 t2))  ; KNOB
         (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (and (equal? t2 t)
                (equal? t1 (infer- e2 Γ)))]
         [t #f])]
@@ -83,13 +83,13 @@
               e1 t e2 (infer- e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
-    [`(λ ,x (: ,t1) ,e)
+    [`(λ (,x : ,t1) ,e)
       (let ([t2 (infer- e (dict-set Γ x t1))])
         (let ([k (+ 1 (max-level e (dict-set Γ x t1) t1 t2))])  ; KNOB
-          `(→ ,k ,t1 ,t2)))]
+          `(,t1 → ,k ,t2)))]
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (if (check- e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
         [t (err (format "expected → type on application body, got ~a" t))])]
@@ -108,7 +108,7 @@
   (match t
     ['Unit 0]
     ['Nat 0]
-    [`(→ ,k ,t1 ,t2)
+    [`(,t1 → ,k ,t2)
       (if (or (< k (level-type t1)) (< k (level-type t2)))
         (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
           k t1 t2))
@@ -128,5 +128,5 @@
     [`(new ,e) (level-body e Γ)]
     [`(! ,e) (level-body e Γ)]
     [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
-    [`(λ ,x (: ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
+    [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0?
     [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]))
-- 
cgit v1.2.3-70-g09d2