suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Moved stlc to tests

Browse Source
This commit is contained in:
William J. Bowman 2016-01-10 18:40:38 -05:00
parent 97ddf170b2
commit f8b19801fd
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 23 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
examples/stlc.rkt → cur-test/cur/tests/stlc.rkt
View File

@ -1,18 +1,19 @@
#lang s-exp "../cur.rkt" #lang cur
(require (require
"../stdlib/nat.rkt" rackunit
"../stdlib/sugar.rkt" cur/stdlib/nat
"../oll.rkt" cur/stdlib/sugar
"../stdlib/maybe.rkt" cur/oll
"../stdlib/bool.rkt" cur/stdlib/maybe
"../stdlib/prop.rkt") cur/stdlib/bool
cur/stdlib/prop)
(define-language stlc (define-language stlc
#:vars (x) #:vars (x)
#:output-coq "stlc.v" #:output-coq "stlc.v"
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
(val (v) ::= true false unit) (val (v) ::= true false unit)
;; TODO: Allow datum as terminals ;; TODO: Allow datum, like 1, as terminals
(type (A B) ::= boolty unitty (-> A B) (* A A)) (type (A B) ::= boolty unitty (-> A B) (* A A))
(term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e) (term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e)
(let (x x) = e in e))) (let (x x) = e in e)))
@ -126,19 +127,17 @@
#'stlc-unitty #'stlc-unitty
#'e)]))) #'e)])))
(module+ test (check-equal?
(require rackunit) (begin-stlc (lambda (x : 1) x))
(check-equal? (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
(begin-stlc (lambda (x : 1) x)) (check-equal?
(stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))) (begin-stlc ((lambda (x : 1) x) ()))
(check-equal? (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
(begin-stlc ((lambda (x : 1) x) ())) (stlc-val-->-stlc-term stlc-unit)))
(stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))) (check-equal?
(stlc-val-->-stlc-term stlc-unit))) (begin-stlc '(() ()))
(check-equal? (stlc-cons (stlc-val-->-stlc-term stlc-unit)
(begin-stlc '(() ())) (stlc-val-->-stlc-term stlc-unit)))
(stlc-cons (stlc-val-->-stlc-term stlc-unit) (check-equal?
(stlc-val-->-stlc-term stlc-unit))) (begin-stlc #t)
(check-equal? (stlc-val-->-stlc-term stlc-true))
(begin-stlc #t)
(stlc-val-->-stlc-term stlc-true)))