go all in on unicode: rename ctx and heap to \Gamma and \Sigma

6 files changed, 72 insertions, 72 deletions

diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 1ab83ba..09a6dc8 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -5,67 +5,67 @@
 ;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption
 
 ;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [ctx #hash()])
-  (interpret- (strip (desugar expr)) ctx))
-(define (interpret- expr ctx heap)
+(define (interpret expr [Γ #hash()])
+  (interpret- (strip (desugar expr)) Γ))
+(define (interpret- expr Γ Σ)
   (match expr
     ['sole 'sole]
     [s #:when (string? s) s]
     [n #:when (natural? n) n]
     [b #:when (boolean? b) b]
-    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
 
     [`(inc ,e)
-      (match (interpret- e ctx heap)
+      (match (interpret- e Γ Σ)
         [n #:when (natural? n) (+ n 1)]
         [e (format "incrementing an unknown value ~a" e)])]
     [`(if ,c ,e1 ,e2)
-      (match (interpret- c ctx heap)
-        ['#t (interpret- e1 ctx heap)]
-        ['#f (interpret- e2 ctx heap)]
+      (match (interpret- c Γ Σ)
+        ['#t (interpret- e1 Γ Σ)]
+        ['#f (interpret- e2 Γ Σ)]
         [e (err (format "calling if on unknown expression ~a" e))])]
 
     [`(pair ,e1 ,e2)
-      `(pair ,(interpret- e1 ctx) ,(interpret- e2 ctx))]
+      `(pair ,(interpret- e1 Γ) ,(interpret- e2 Γ))]
     [`(car ,e)
-      (match (interpret- e ctx)
+      (match (interpret- e Γ)
         [`(pair ,e1 ,e2) e1]
         [e (err (format "calling car on unknown expression ~a" e))])]
     [`(cdr ,e)
-      (match (interpret- e ctx)
+      (match (interpret- e Γ)
         [`(pair ,e1 ,e2) e2]
         [e (err (format "calling cdr on unknown expression ~a" e))])]
 
-    [`(inl ,e) `(inl ,(interpret- e ctx))]
-    [`(inr ,e) `(inr ,(interpret- e ctx))]
+    [`(inl ,e) `(inl ,(interpret- e Γ))]
+    [`(inr ,e) `(inr ,(interpret- e Γ))]
     [`(case ,e ,f1 ,f2)
-      (match (interpret- e ctx)
-        [`(inl ,e) (interpret- `(,f1 ,e) ctx)]
-        [`(inr ,e) (interpret- `(,f2 ,e) ctx)]
+      (match (interpret- e Γ)
+        [`(inl ,e) (interpret- `(,f1 ,e) Γ)]
+        [`(inr ,e) (interpret- `(,f2 ,e) Γ)]
         [e (err (format "calling case on unknown expression ~a" e))])]
 
     ['nil 'nil]
     [`(nil? ,e)
-      (match (interpret- e ctx)
+      (match (interpret- e Γ)
         ['nil '#t]
         [`(cons ,e1 ,e2) '#f]
         [e (err (format "calling isnil on unknown expression ~a" e))])]
     [`(cons ,e1 ,e2)
-     `(cons ,(interpret- e1 ctx) ,(interpret- e2 ctx))]
+     `(cons ,(interpret- e1 Γ) ,(interpret- e2 Γ))]
     [`(head ,e)
-      (match (interpret- e ctx)
-        [`(cons ,e1 ,e2) (interpret- e1 ctx)]
+      (match (interpret- e Γ)
+        [`(cons ,e1 ,e2) (interpret- e1 Γ)]
         [e (err (format "calling head on unknown expression ~a" e))])]
     [`(tail ,e)
-      (match (interpret- e ctx)
-        [`(cons ,e1 ,e2) (interpret- e2 ctx)]
+      (match (interpret- e Γ)
+        [`(cons ,e1 ,e2) (interpret- e2 Γ)]
         [e (err (format "calling tail on unknown expression ~a" e))])]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret- e1 ctx)
+      (match (interpret- e1 Γ)
         [`(λ ,x ,e ,env)
-          (interpret- e (dict-set env x (interpret- e2 ctx)))]
+          (interpret- e (dict-set env x (interpret- e2 Γ)))]
         [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
 
     [e (err (format "interpreting an unknown expression ~a" e))]))
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index f5ad384..bcb28cb 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -4,27 +4,27 @@
 ;; The Simply-Typed Lambda Calculus, with general recursion
 
 ;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [ctx #hash()])
-  (interpret- (strip (desugar expr)) ctx))
-(define (interpret- expr ctx)
+(define (interpret expr [Γ #hash()])
+  (interpret- (strip (desugar expr)) Γ))
+(define (interpret- expr Γ)
   (match expr
     ['sole 'sole]
     [n #:when (natural? n) n]
-    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
 
     [`(fix ,e)
-      (match (interpret- e ctx)
+      (match (interpret- e Γ)
         [`(λ ,x ,e ,env)
-          ; FIXME: unsure what should be ctx and what should be env
-          (interpret- e (dict-set ctx x `(fix (λ ,x ,e ,ctx))))]
+          ; FIXME: unsure what should be Γ and what should be env
+          (interpret- e (dict-set Γ x `(fix (λ ,x ,e ,Γ))))]
         [e (err (format "applying fix to unknown expression ~a" e))])]
 
-    [`(λ ,id ,body) `(λ ,id ,body ,ctx)]
+    [`(λ ,id ,body) `(λ ,id ,body ,Γ)]
     [`(λ ,id ,body ,env) `(λ ,id ,body ,env)]
     [`(,body ,arg)
-      (match (interpret- body ctx)
+      (match (interpret- body Γ)
         [`(λ ,id ,body ,env)
-          (interpret- body (dict-set env id (interpret- arg ctx)))]
+          (interpret- body (dict-set env id (interpret- arg Γ)))]
         [e (err (format "applying arg ~a to unknown expression ~a" arg e))])]
 
     [e (err (format "interpreting an unknown expression ~a" e))]))
diff --git a/stlc-let.rkt b/stlc-let.rkt
index 3d6afc6..04dbd84 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -4,18 +4,18 @@
 ;; The Simply-Typed Lambda Calculus, with let sugar and some base types
 
 ;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [ctx #hash()])
-  (interpret- (strip (desugar expr)) ctx))
-(define (interpret- expr ctx)
+(define (interpret expr [Γ #hash()])
+  (interpret- (strip (desugar expr)) Γ))
+(define (interpret- expr Γ)
   (match expr
     ['sole 'sole]
     [n #:when (natural? n) n]
-    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
-    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret- e1 ctx)
-        [`(λ ,x ,e1 ,env) (interpret- e1 (dict-set env x (interpret- e2 ctx)))]
-        [e1 `(,e1 ,(interpret- e2 ctx))])]
+      (match (interpret- e1 Γ)
+        [`(λ ,x ,e1 ,env) (interpret- e1 (dict-set env x (interpret- e2 Γ)))]
+        [e1 `(,e1 ,(interpret- e2 Γ))])]
     [e e]))
 
 ;;      (check Expr Type Table[Sym, Type]): Bool
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index 24bbb8f..97ee9a3 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -12,22 +12,22 @@
 ; Γ ⊢ unfold [μx.t] e: [x ↦ μx.t] t
 
 ;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [ctx #hash()])
-  (interpret- (strip (desugar expr)) ctx))
-(define (interpret- expr ctx)
+(define (interpret expr [Γ #hash()])
+  (interpret- (strip (desugar expr)) Γ))
+(define (interpret- expr Γ)
   (match expr
     ['sole 'sole]
     [n #:when (natural? n) n]
-    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
 
     [`(fold ,t ,e) `(fold ,t ,(interpret- e))]
     [`(unfold ,t ,e) `(unfold ,t ,(interpret- e))]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret- e1 ctx)
+      (match (interpret- e1 Γ)
         [`(λ ,x ,e ,env)
-          (interpret- e (dict-set env x (interpret- e2 ctx)))]
+          (interpret- e (dict-set env x (interpret- e2 Γ)))]
         [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
 
     [e (err (format "interpreting an unknown expression ~a" e))]))
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index 73365f2..43af60f 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -4,36 +4,36 @@
 ;; The Simply-Typed Lambda Calculus with references
 
 ;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value
-(define (interpret expr [ctx #hash()] [heap (make-hash)])
-  (interpret- (strip (desugar expr)) ctx heap))
-(define (interpret- expr ctx heap)
+(define (interpret expr [Γ #hash()] [Σ (make-hash)])
+  (interpret- (strip (desugar expr)) Γ Σ))
+(define (interpret- expr Γ Σ)
   ; (print (format "interpret: ~a" (fmt expr)))
   (match expr
     ['sole 'sole]
     [n #:when (natural? n) n]
-    [r #:when (dict-has-key? heap r) r]
-    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+    [r #:when (dict-has-key? Σ r) r]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
 
     [`(new ,e)
       (let ([r (gensym)])
-      (dict-set! heap r e) r)]
+      (dict-set! Σ r e) r)]
     [`(! ,e)
-      (let ([r (interpret- e ctx heap)])
-      (if (dict-has-key? heap r)
-        (interpret- (dict-ref heap r) ctx heap)
+      (let ([r (interpret- e Γ Σ)])
+      (if (dict-has-key? Σ r)
+        (interpret- (dict-ref Σ r) Γ Σ)
         (err (format "attempting to deref unknown reference ~a" r))))]
     [`(set ,e1 ,e2)
-      (let ([r (interpret- e1 ctx heap)])
-      (if (dict-has-key? heap r) (dict-set! heap r (interpret- e2 ctx heap))
+      (let ([r (interpret- e1 Γ Σ)])
+      (if (dict-has-key? Σ r) (dict-set! Σ r (interpret- e2 Γ Σ))
         (err (format "attempting to update unknown reference ~a" r))))
       'sole]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(λ ,x ,e ,env) `(λ ,x ,e ,env)] ; ???
     [`(,e1 ,e2)
-      (match (interpret- e1 ctx heap)
+      (match (interpret- e1 Γ Σ)
         [`(λ ,x ,e1 ,env)
-          (interpret- e1 (dict-set env x (interpret- e2 ctx heap)) heap)]
+          (interpret- e1 (dict-set env x (interpret- e2 Γ Σ)) Σ)]
         [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]
 
     [e (err (format "attempting to interpret unknown expression ~a" e))]))
diff --git a/stlc.rkt b/stlc.rkt
index f9167ed..bde09b0 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -4,16 +4,16 @@
 ;; The Simply-Typed Lambda Calculus
 
 ;;      (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [ctx #hash()])
-  (interpret- (strip expr) ctx))
-(define (interpret- expr ctx)
+(define (interpret expr [Γ #hash()])
+  (interpret- (strip expr) Γ))
+(define (interpret- expr Γ)
   (match expr
-    [x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
-    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret- e1 ctx)
-        [`(λ ,x ,e ,env) (interpret- e (dict-set env x (interpret- e2 ctx)))]
-        [e `(,e ,(interpret- e2 ctx))])]
+      (match (interpret- e1 Γ)
+        [`(λ ,x ,e ,env) (interpret- e (dict-set env x (interpret- e2 Γ)))]
+        [e `(,e ,(interpret- e2 Γ))])]
     [e e]))
 
 ;;      (check Expr Type Table[Sym, Type]): Bool