diff options
| -rw-r--r-- | stlc-ext.rkt | 50 | ||||
| -rw-r--r-- | stlc-fix.rkt | 20 | ||||
| -rw-r--r-- | stlc-let.rkt | 16 | ||||
| -rw-r--r-- | stlc-rec.rkt | 14 | ||||
| -rw-r--r-- | stlc-ref.rkt | 28 | ||||
| -rw-r--r-- | stlc.rkt | 16 |
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))])) @@ -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 |