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-dll.rkt | 76 ++++++++++++++++++++++++++++++------------------------------
 1 file changed, 38 insertions(+), 38 deletions(-)

(limited to 'stlc-dll.rkt')

diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 9adf978..910cdcd 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -83,7 +83,7 @@
     [('sole 'Unit) #t]
     [(n 'Nat) #:when (natural? n) #t]
     [(b 'Bool) #:when (boolean? b) #t]
-    [(e `(+ ,t1 ,t2))
+    [(e `(,t1 ⊕ ,t2))
       (or (check- e t1 Γ) (check- e t2 Γ))]
     [(x _) #:when (dict-has-key? Γ x)
       (equiv? (dict-ref Γ x) with Γ Γ)]
@@ -97,32 +97,32 @@
       (and (check- c 'Bool Γ)
         (check- e1 with Γ) (check e2 with Γ))]
 
-    [(`(pair ,e1 ,e2) `(× ,t1 ,t2))
+    [(`(pair ,e1 ,e2) `(,t1 × ,t2))
       (and (check- e1 t1 Γ) (check- e2 t2 Γ))]
     [(`(car ,e) with)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) (equiv? t1 with Γ Γ)]
+        [`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
         [t #f])]
     [(`(cdr ,e) with)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) (equiv? t2 with Γ Γ)]
+        [`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
         [t #f])]
 
     [(`(inl ,e) with)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) (equiv? t1 with Γ Γ)]
+        [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)]
         [t #f])]
     [(`(inr ,e) with)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) (equiv? t2 with Γ Γ)]
+        [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
         [t #f])]
     [(`(case ,e ,f1 ,f2) with)
       (match* ((infer- f1 Γ) (infer- f2 Γ))
-        [(`(→ ,a1 ,t1) `(→ ,a2 ,t2))
-          (and (check- e `(+ ,a1 ,a2))
-            (check- f1 `(→ ,a1 ,with) Γ) (check- f2 `(→ ,a2 ,with) Γ))]
+        [(`(,a1 → ,t1) `(,a2 → ,t2))
+          (and (check- e `(,a1 ⊕ ,a2))
+            (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))]
         [(t1 t2) #f])]
-    [(`(,e (: ,t)) with)
+    [(`(,e : ,t) with)
       (and (equiv? t with Γ Γ) (check- e t Γ))]
 
     [(`(new ,e) `(Ref ,t)) (check- e t Γ)]
@@ -138,14 +138,14 @@
       (and (check- e `(μ ,x ,t) Γ)
         (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))
+    [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
       (and
         (equiv? t t1 Γ Γ)
         (> k (max-level e t1 t2 (dict-set Γ x t1)))  ; KNOB
         (check- e t2 (dict-set Γ x t1)))]
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)
+        [`(,t1 → ,k ,t2)
           (and (equiv? t2 t Γ Γ)
                (equiv? t1 (infer- e2 Γ) Γ Γ))]
         [t #f])]
@@ -180,31 +180,31 @@
         (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))]
 
     [`(pair ,e1 ,e2)
-      `(× ,(infer- e1 Γ) ,(infer- e2 Γ))]
+      `(,(infer- e1 Γ) × ,(infer- e2 Γ))]
     [`(car ,e)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) t1]
+        [`(,t1 × ,t2) t1]
         [t (err (format "calling car on incorrect type ~a" t))])]
     [`(cdr ,e)
       (match (infer- e Γ)
-        [`(× ,t1 ,t2) t2]
+        [`(,t1 × ,t2) t2]
         [t (err (format "calling cdr on incorrect type ~a" t))])]
 
     [`(inl ,e)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) t1]
+        [`(,t1 ⊕ ,t2) t1]
         [t (err (format "calling inl on incorrect type ~a" t))])]
     [`(inr ,e)
       (match (infer- e Γ)
-        [`(+ ,t1 ,t2) t2]
+        [`(,t1 ⊕ ,t2) t2]
         [t (err (format "calling inr on incorrect type ~a" t))])]
     [`(case ,e ,f1 ,f2)
       (match* ((infer- f1 Γ) (infer- f2 Γ))
-        [(`(→ ,a1 ,t1) `(→ ,a2 ,t2))
-          (if (and (check- e `(+ ,a1 ,a2)) (equiv? t1 t2 Γ Γ)) t1
+        [(`(,a1 → ,t1) `(,a2 → ,t2))
+          (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1
             (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))]
         [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])]
-    [`(,e (: ,t))
+    [`(,e : ,t)
       (if (check- e t Γ) t
         (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
 
@@ -230,20 +230,20 @@
         (err (format ("expected ~a to be of type ~a, got ~a"
           e `(μ ,x ,t) (infer- e Γ)))))]
 
-    [`(λ ,x (: ,t1) ,e)
+    [`(λ (,x : ,t1) ,e)
       (let ([t2 (infer- e (dict-set Γ x t1))])
         (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))])  ; 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))])]
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
 
-
+;;      (expand Type Table[Id, Expr ⊕ Type]): Type
 (define (expand t Γ)
   (if (dict-has-key? Γ t) (dict-ref Γ t) t))
 
@@ -259,7 +259,7 @@
   (match (expand 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))
@@ -292,37 +292,37 @@
     [`(! ,e) (level-body e Γ)]
     [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
     [`(if ,c ,e1 ,e2) (max (level-body c Γ) (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 Γ))]))
 
 (require rackunit)
 (check-exn
   exn:fail?
   (λ () (infer '
-    (let id (: (→ 1 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 1 Nat Nat))) (new id)
-        (let f (: (→ 3 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
           (set r f
             (f 0))))))))
 
 (check-eq?
   (infer '
-    (let id (: (→ 1 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 1 Nat Nat))) (new id)
-        (let f (: (→ 3 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
           (f 0)))))
   'Nat)
 
 (check-eq?
   (check '
-    (let id (: (→ 1 Nat Nat)) (λ x x)
-      (let r (: (Ref (→ 1 Nat Nat))) (new id)
-        (let f (: (→ 3 Nat Nat)) (λ x ((! r) x))
+    (let (id : (Nat → 1 Nat)) (λ x x)
+      (let (r : (Ref (Nat → 1 Nat))) (new id)
+        (let (f : (Nat → 3 Nat)) (λ x ((! r) x))
           (f 0))))
     'Nat)
   #t)
 
 (check-eq? (interpret '(if #t 1 0)) 1)
-(check-eq? (interpret '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 2)
-(check-eq? (infer '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 'Nat)
-(check-true (check '(type Natural Nat ((λ x (: Natural) (inc x)) 1)) 'Nat))
+(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2)
+(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat)
+(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))
-- 
cgit v1.2.3-70-g09d2