add + to poly-stlc

This commit is contained in:
Robby Findler 2014-03-19 11:13:36 -05:00
parent cc2d547389
commit 3d175cba40
20 changed files with 168 additions and 183 deletions

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "app rule the range of the function is matched to the argument")
73c73
74c74
< [(typeof Γ M (σσ_2))
---
> [(typeof Γ M (σ_2 → σ_2))
262c262
261c261
< M]
---
> M]

View File

@ -2,9 +2,9 @@
< (define the-error "no error")
---
> (define the-error "the (([cons @ τ] v) v) value has been omitted")
47d46
48d47
< (([cons @ τ] v) v)
262,263c261
261,262c260
< M]
< [#f #f]))
---

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "the order of the types in the function position of application has been swapped")
73c73
74c74
< [(typeof Γ M (σσ_2))
---
> [(typeof Γ M (σ_2 → σ))
262c262
261c261
< M]
---
> M]

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "the type of cons is incorrect")
120c120
124c124
< (∀ a (a → ((list a) → (list a))))]
---
> (∀ a (a → ((list a) → a)))]
262c262
261c261
< M]
---
> M]

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "the tail reduction returns the wrong value")
166c166
172c172
< (in-hole E v_2)
---
> (in-hole E v_1)
262c262
261c261
< M]
---
> M]

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "hd reduction acts on partially applied cons")
162c162
168c168
< (--> (in-hole E ((hd @ τ) (((cons @ τ) v_1) v_2)))
---
> (--> (in-hole E ((hd @ τ) ((cons @ τ) v_1)))
262c262
261c261
< M]
---
> M]

View File

@ -2,12 +2,12 @@
< (define the-error "no error")
---
> (define the-error "evaluation isn't allowed on the rhs of applications")
50,51c50
51,52c51
< (E M)
< (v E)))
---
> (E M)))
262c261
261c260
< M]
---
> M]

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "lookup always returns int")
109c109
113c113
< σ]
---
> int]
262c262
261c261
< M]
---
> M]

View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "variables aren't required to match in lookup")
108c108
112c112
< [(lookup (x σ Γ) x)
---
> [(lookup (x σ Γ) x_2)
262c262
261c261
< M]
---
> M]

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
([[map @ τ_1] @ τ_2] v))
(E hole
@ -92,7 +93,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -122,7 +126,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -175,7 +181,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -213,16 +222,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -92,7 +93,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -122,7 +126,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -175,7 +181,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -213,16 +222,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -16,7 +16,7 @@
(λ (x σ) M)
(M N)
C
number
integer
x)
(C ::=
[C @ σ]
@ -38,11 +38,12 @@
γ)
(x y ::= variable-not-otherwise-mentioned)
(α β ::= variable-not-otherwise-mentioned)
(c d ::= map nil cons hd tl)
(c d ::= map nil cons hd tl +)
(v (λ (x τ) M)
C
number
integer
(+ v)
([cons @ τ] v)
(([cons @ τ] v) v)
([[map @ τ_1] @ τ_2] v))
@ -93,7 +94,10 @@
; (where σ (t-subst2 γ α τ_1 β τ_2))
; ------------------------------
; (typeof-C [[c @ τ_1] @ τ_2] σ)]
)
[(where γ (const-type c))
------------------------------
(typeof-C c γ)])
(define-extended-judgment-form poly-stlc typeof
#:mode (typ-ind I I O)
@ -123,7 +127,9 @@
[(const-type tl)
( a ((list a) (list a)))]
[(const-type map)
( α ( β ((α β) ((list α) (list β)))))])
( α ( β ((α β) ((list α) (list β)))))]
[(const-type +)
(int (int int))])
(define-metafunction poly-stlc
t-subst : γ α τ -> γ
@ -176,7 +182,10 @@
"hd-err")
(--> (in-hole E ((tl @ τ) (nil @ τ)))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match poly-stlc M))
(define/contract (Eval M)
@ -214,16 +223,6 @@
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define (generate-M-term)
(generate-term poly-stlc M 5))

View File

@ -92,10 +92,6 @@
(term 3))
#|
;; tests for arithmetic; not yet added to the model.
(test-equal (judgment-holds (typeof ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
(list (term int)))
(test-->> red
@ -107,6 +103,5 @@
(test-->> red
(term ((λ (f (int int)) (f 3)) (+ 1)))
(term 4))
|#
(test-results)