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

Rewrote Olly

Browse Source 
Olly is now properly designed. This also fixes some issues with binding,
i.e. fixes #32, and extraction to Coq and Latex
Makes progress on #9.
This commit is contained in:
William J. Bowman 2016-01-12 19:07:19 -05:00
parent 3a644fae90
commit 961a5b7bb9
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
4 changed files with 537 additions and 445 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

118
cur-doc/cur/scribblings/olly.scrbl
View File

@ -14,11 +14,11 @@ the language.
maybe-vars maybe-vars
maybe-output-coq maybe-output-coq
maybe-output-latex maybe-output-latex
(nt-name (nt-metavars) maybe-bnfdef constructors ...) ...) (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
#:grammar #:grammar
[(maybe-vars [(maybe-vars
(code:line) (code:line)
(code:line #:vars (nt-metavars ...))) (code:line #:vars (nt-metavar ...)))
(maybe-output-coq (maybe-output-coq
(code:line) (code:line)
(code:line #:output-coq coq-filename)) (code:line #:output-coq coq-filename))
@ -27,26 +27,51 @@ the language.
(code:line #:output-latex latex-filename)) (code:line #:output-latex latex-filename))
(maybe-bnfdef (maybe-bnfdef
(code:line) (code:line)
(code:line ::=))]]{ (code:line ::=))
(non-terminal-def
nt-metavar
(code:line terminal)
(code:line (terminal terminal-args ...)))
(terminal-args
nt-metavar
(code:line literal)
(code:line ())
(code:line (#:bind nt-metavar . terminal-args))
(code:line (terminal-args terminal-args ...)))]]{
Defines a new language by generating inductive definitions for each Defines a new language by generating inductive definitions for each
nonterminal @racket[nt-name], whose constructors are generated by non-terminal @racket[nt-name], whose syntax is generated by
@racket[constructors]. The constructors must either with a tag that can @racket[non-terminal-def].
be used to name the constructor, or be another meta-variable. Each @racket[non-terminal-def] must either be a reference to a
The meta-variables @racket[nt-metavars] are replaced by the corresponding previously defined non-terminal using a @racket[nt-metavar], a
inductive types in @racket[constructors]. @racket[terminal] (an identifier), or a @racket[terminal] applied to
The name of each inductive datatype is generated by some @racket[terminal-args].
@racket[(format-id "~a-~a" name nt-name)]. The @racket[terminal-args] are a limited grammar of s-expressions,
which can reference previously defined @racket[nt-metavar]s to be
treated as arguments, literal symbols to be treated as syntax, binding
declarations, or a nested @racket[terminal-arg].
Later nonterminals can refer to prior nonterminals, but they cannot be The inductive definitions are generated by generating a type for each
mutually inductive due to limitations in Cur. When nonterminals appear @racket[nt-name] whose name @racket[nt-type] is generated by
in @racket[constructors], a constructor is defined that coerces one @racket[(format-id name "~a-~a" name nt-name)] and whose constructors
nonterminal to another. are generated by each @racket[non-terminal-def].
For @racket[terminal]s, the constructor is a base constructor whose
name is generated by @racket[(format-id name "~a-~a" name terminal)].
For @racket[nt-metavar]s, the constructor is a conversion constructor
whose name is generated by @racket[(format-id name "~a->~a" nt-type
nt-metavar-type)] where @racket[nt-metavar-type] is the name of the
type generated for the nonterminal to which @racket[nt-metavars] refers.
For @racket[(terminal terminal-args ...)], the constructor is a
function that expects term of of the types generated by
@racket[terminal-args ...].
If @racket[#:vars] is given, it should be a list of meta-variables that If @racket[#:vars] is given, it should be a list of meta-variables that
representing variables in the language. These meta-variables should only representing variables in the language.
appear in binding positions in @racket[constructors]. These variables These variables are represented as De Bruijn indices, and uses of
are represented as De Bruijn indexes, and Olly provides some functions variables in the syntax are treated as type @racket[Nat].
for working with De Bruijn indexes. Binding positions in the syntax, represented by @racket[#:bind
nt-metavar], are erased in converting to De Bruijn indices, although
this may change if the representation of variables used by
@racket[define-language] changes.
If @racket[#:output-coq] is given, it should be a string representing a If @racket[#:output-coq] is given, it should be a string representing a
filename. The form @racket[define-language] will output Coq versions of filename. The form @racket[define-language] will output Coq versions of
@ -66,8 +91,8 @@ Example:
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
(val (v) ::= true false unit) (val (v) ::= true false unit)
(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 (#:bind x : A) e) (cons e e)
(let (x x) = e in e))) (let (#:bind x #:bind x) = e in e)))
] ]
This example is equivalent to This example is equivalent to
@ -85,20 +110,17 @@ This example is equivalent to
(stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type)))) (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
(data stlc-term : Type (data stlc-term : Type
(stlc-var-->-stlc-term : (forall (x : Var) stlc-term)) (Var->-stlc-term : (forall (x : Nat) stlc-term))
(stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term)) (stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term))
(stlc-term-lambda : (forall (x : Var) (stlc-term-lambda : (forall (y : stlc-type)
(forall (y : stlc-type)
(forall (z : stlc-term) (forall (z : stlc-term)
stlc-term)))) stlc-term)))
(stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term))) (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
(stlc-term-let : (forall (x : Var) (stlc-term-let : (forall (e1 : stlc-term)
(forall (y : Var) (forall (e2 : stlc-term)
(forall (e1 : stlc-term) stlc-term))))]
(forall (e2 : stlc-term)
stlc-term))))))]
@margin-note{This example is taken from @racketmodname[cur/examples/stlc]} @margin-note{This example is taken from @racketmodname[cur/tests/stlc]}
} }
@defform[(define-relation (name args ...) @defform[(define-relation (name args ...)
@ -126,20 +148,20 @@ explain the syntax in detail, here is an example:
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
[(g : Gamma) [(g : Gamma)
------------------------ T-Unit ------------------------ T-Unit
(has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)] (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
[(g : Gamma) [(g : Gamma)
------------------------ T-True ------------------------ T-True
(has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)] (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
[(g : Gamma) [(g : Gamma)
------------------------ T-False ------------------------ T-False
(has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)] (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
[(g : Gamma) (x : Var) (t : stlc-type) [(g : Gamma) (x : Nat) (t : stlc-type)
(== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t)) (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
------------------------ T-Var ------------------------ T-Var
(has-type g (Var-->-stlc-term x) t)] (has-type g (Var->stlc-term x) t)]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
@ -151,16 +173,15 @@ explain the syntax in detail, here is an example:
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(t : stlc-type) (t : stlc-type)
(x : Var) (y : Var)
(has-type g e1 (stlc-* t1 t2)) (has-type g e1 (stlc-* t1 t2))
(has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t) (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
---------------------- T-Let ---------------------- T-Let
(has-type g (stlc-let x y e1 e2) t)] (has-type g (stlc-let e1 e2) t)]
[(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var) [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
(has-type (extend-gamma g x t1) e1 t2) (has-type (extend-gamma g t1) e1 t2)
---------------------- T-Fun ---------------------- T-Fun
(has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))] (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
@ -179,22 +200,11 @@ This example is equivalent to:
(T-Unit : (forall (g : Gamma) (T-Unit : (forall (g : Gamma)
(has-type (has-type
g g
(stlc-val-->-stlc-term stlc-unit) (stlc-val->stlc-term stlc-unit)
stlc-unitty))) stlc-unitty)))
....)] ....)]
} }
@deftogether[(@defthing[Var Type]
@defthing[avar (forall (x : Nat) Var)])]{
The type of a De Bruijn variable.
}
@defproc[(var-equal? [v1 Var] [v2 Var])
Bool]{
A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
represent the same variable.
}
@todo{Need a Scribble library for defining Cur/Racket things in the same @todo{Need a Scribble library for defining Cur/Racket things in the same
library in a nice way.} library in a nice way.}

668
cur-lib/cur/olly.rkt
View File

@ -10,305 +10,425 @@
(provide (provide
define-relation define-relation
define-language define-language
Var
avar
var-equal?
generate-coq generate-coq
;; private; exported for testing only ;; private; exported for testing only
(for-syntax (for-syntax
coq-defns typeset-relation
output-latex-bnf typeset-bnf
output-coq cur->coq))
new-name
fresh-name))
(begin-for-syntax
(define-syntax-class dash
(pattern x:id
#:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
"Invalid dash"))
(define-syntax-class decl (pattern (x:id (~datum :) t:id)))
;; TODO: Automatically infer decl ... by binding all free identifiers?
;; TODO: Automatically infer decl ... for meta-variables that are the
;; same as bnf grammar.
(define-syntax-class inferrence-rule
(pattern (d:decl ...
x*:expr ...
line:dash lab:id
(name:id y* ...))
#:with rule #'(lab : (-> d ... x* ... (name y* ...)))
;; TODO: convert meta-vars such as e1 to e_1
#:attr latex (format "\\inferrule~n{~a}~n{~a}"
(string-trim
(for/fold ([str ""])
([hyp (syntax->datum #'(x* ...))])
(format "~a~a \\+" str hyp))
" \\+"
#:left? #f)
(format "~a" (syntax->datum #'(name y* ...)))))))
(define-syntax (define-relation syn)
(syntax-parse syn
[(_ (n:id types* ...)
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
rules:inferrence-rule ...)
#:fail-unless (andmap (curry equal? (length (syntax->datum #'(types* ...))))
(map length (syntax->datum #'((rules.y* ...)
...))))
"Mismatch between relation declared and relation definition"
#:fail-unless (andmap (curry equal? (syntax->datum #'n))
(syntax->datum #'(rules.name ...)))
"Mismatch between relation declared name and result of inference rule"
(let ([output #`(data n : (-> types* ... Type) rules.rule ...)])
;; TODO: Pull this out into a separate function and test. Except
;; that might make using attritbutes more difficult.
(when (attribute latex-file)
(with-output-to-file (syntax->datum #'latex-file)
(thunk
(printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
(syntax->datum #'(n types* ...))
(string-trim
(for/fold ([str ""])
([rule (attribute rules.latex)])
(format "~a~a\\and~n" str rule))
"\\and"
#:left? #f))))
#:exists 'append))
#`(begin
#,@(if (attribute coq-file)
#`((generate-coq #:file coq-file #:exists
'append #,output))
#'())
#,output))]))
(begin-for-syntax
(require racket/syntax)
(define (new-name name . id*)
(apply format-id name (for/fold ([str "~a"])
([_ id*])
(string-append str "-~a")) name (map syntax->datum id*)))
(define (fresh-name id)
(datum->syntax id (gensym (syntax->datum id)))))
;; TODO: Oh, this is a mess. Rewrite it.
(begin-for-syntax
(define lang-name (make-parameter #'name))
(define nts (make-parameter (make-immutable-hash)))
(define-syntax-class nt
(pattern e:id #:fail-unless (hash-has-key? (nts) (syntax->datum #'e)) #f
#:attr name (hash-ref (nts) (syntax->datum #'e))
#:attr type (hash-ref (nts) (syntax->datum #'e))))
(define (flatten-args arg arg*)
(for/fold ([ls (syntax->list arg)])
([e (syntax->list arg*)])
(append ls (syntax->list e))))
(define-syntax-class (right-clause type)
#;(pattern (~datum var)
#:attr clause-context #`(#,(new-name (lang-name) #'var) :
(-> #,(hash-ref (nts) 'var) #,(hash-ref (nts) type)))
#:attr name #'var
#:attr arg-context #'(var))
(pattern e:nt
#:attr clause-context #`(#,(new-name #'e.name #'->
(hash-ref (nts) type)) :
(-> e.type #,(hash-ref (nts) type)))
#:attr name (fresh-name #'e.name)
#:attr arg-context #'(e.type))
(pattern x:id
#:attr clause-context #`(#,(new-name (lang-name) #'x) :
#,(hash-ref (nts) type))
#:attr name (new-name (lang-name) #'x)
#:attr arg-context #'())
(pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
#:attr name (fresh-name #'e.name)
#:attr clause-context #`(e.name : (-> #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
#,(hash-ref (nts) type)))
#:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
(define-syntax-class (right type)
(pattern ((~var r (right-clause type)) ...)
#:attr clause #'(r.clause-context ...)))
#;(define-syntax-class left
(pattern (type:id (nt*:id ...+))
#:do ))
(define-syntax-class nt-clauses
(pattern ((type:id (nt*:id ...+)
(~do (nts (for/fold ([ht (nts)])
([nt (syntax->datum #'(type nt* ...))])
(hash-set ht nt (new-name (lang-name) #'type)))))
(~datum ::=)
. (~var rhs* (right (syntax->datum #'type)))) ...)
#:with defs (with-syntax ([(name* ...)
(map (λ (x) (hash-ref (nts) x))
(syntax->datum #'(type ...)))])
#`((data name* : Type . rhs*.clause)
...)))))
(begin-for-syntax
;; TODO: More clever use of syntax-parse would enable something akin to what
;; define-relation is doing---having attributes that contain the latex
;; code for each clause.
;; TODO: convert meta-vars such as e1 to e_1
(define (output-latex-bnf vars clauses)
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(for/fold ([str ""])
([clause (syntax->list clauses)])
(syntax-parse clause
#:datum-literals (::=)
[(type:id (nonterminal:id ...) ::= exprs ...)
(format "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
(symbol->string (syntax->datum #'type))
(string-trim
(for/fold ([str ""])
([nt (syntax->datum #'(nonterminal ...))])
(format "~a~a," str nt))
","
#:left? #f)
(string-trim
(for/fold ([str ""])
([expr (syntax->datum #'(exprs ...))])
(format "~a~a \\bnfalt " str expr))
" \\bnfalt "
#:left? #f))]))))
(define (generate-latex-bnf file-name vars clauses)
(with-output-to-file file-name
(thunk (printf (output-latex-bnf vars clauses)))
#:exists 'append)))
;; TODO: For better error messages, add context, rename some of these patterns. e.g.
;; (type (meta-vars) ::= ?? )
;; TODO: Extend define-language with syntax such as ....
;; (term (e) ::= (e1 e2) ((lambda (x) e)
; #:latex "(\\lambda ,x. ,e)"))
(define-syntax (define-language syn)
(syntax-parse syn
[(_ name:id (~do (lang-name #'name))
(~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
(~optional (~seq #:vars (x*:id ...)
(~do (nts (for/fold ([ht (nts)])
([v (syntax->datum #'(x* ...))])
(hash-set ht v (hash-ref ht 'var)))))))
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
. clause*:nt-clauses)
(let ([output #`(begin . clause*.defs)])
(when (attribute latex-file)
(generate-latex-bnf (syntax->datum #'latex-file) #'vars #'clause*))
#`(begin
#,@(if (attribute coq-file)
#`((generate-coq #:file coq-file #:exists 'append #,output))
#'())
#,output))]))
(data Var : Type (avar : (-> Nat Var)))
(define (var-equal? (v1 : Var) (v2 : Var))
(match v1
[(avar (n1 : Nat))
(match v2
[(avar (n2 : Nat))
(nat-equal? n1 n2)])]))
;; See stlc.rkt for examples
;; Generate Coq from Cur: ;; Generate Coq from Cur:
(begin-for-syntax (begin-for-syntax
(define coq-defns (make-parameter "")) (define coq-defns (make-parameter ""))
(define (coq-lift-top-level str) (define (coq-lift-top-level str)
(coq-defns (format "~a~a~n" (coq-defns) str))) (coq-defns (format "~a~a~n" (coq-defns) str)))
;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
(define (constructor-args syn) (define (constructor-args syn)
(syntax-parse (type-infer/syn syn) (syntax-parse (type-infer/syn syn)
#:datum-literals (Π :) #:datum-literals (Π :)
[(Π (x:id : t) body) [(Π (x:id : t) body)
(cons #'x (constructor-args #'body))] (cons #'x (constructor-args #'body))]
[_ null])) [_ null]))
(define (sanitize-id str) (define (sanitize-id str)
(let ([replace-by `((: _) (- _))]) (let ([replace-by `((: _) (- _))])
(for/fold ([str str]) (for/fold ([str str])
([p replace-by]) ([p replace-by])
(string-replace str (symbol->string (first p)) (string-replace str (symbol->string (first p))
(symbol->string (second p)))))) (symbol->string (second p))))))
(define (output-coq syn)
(syntax-parse (cur-expand syn #'define #'begin) (define (cur->coq syn)
;; TODO: Need to add these to a literal set and export it (parameterize ([coq-defns ""])
;; Or, maybe overwrite syntax-parse (define output
#:literals (real-lambda real-forall data real-app real-elim define begin Type) (let cur->coq ([syn syn])
[(begin e ...) (syntax-parse (cur-expand syn #'define #'begin)
(for/fold ([str ""]) ;; TODO: Need to add these to a literal set and export it
([e (syntax->list #'(e ...))]) ;; Or, maybe overwrite syntax-parse
(format "~a~n" (output-coq e)))] #:literals (real-lambda real-forall data real-app real-elim define begin Type)
[(define name:id body) [(begin e ...)
(begin (for/fold ([str ""])
(coq-lift-top-level ([e (syntax->list #'(e ...))])
(format "Definition ~a := ~a.~n" (format "~a~n" (cur->coq e)))]
(output-coq #'name) [(define name:id body)
(output-coq #'body))) (begin
"")] (coq-lift-top-level
[(define (name:id (x:id : t) ...) body) (format "Definition ~a := ~a.~n"
(begin (cur->coq #'name)
(coq-lift-top-level (cur->coq #'body)))
(format "Function ~a ~a := ~a.~n" "")]
(output-coq #'name) [(define (name:id (x:id : t) ...) body)
(for/fold ([str ""]) (begin
([n (syntax->list #'(x ...))] (coq-lift-top-level
[t (syntax->list #'(t ...))]) (format "Function ~a ~a := ~a.~n"
(format "~a(~a : ~a) " str (output-coq n) (output-coq t))) (cur->coq #'name)
(output-coq #'body))) (for/fold ([str ""])
"")] ([n (syntax->list #'(x ...))]
[(real-lambda ~! (x:id (~datum :) t) body:expr) [t (syntax->list #'(t ...))])
(format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t) (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
(output-coq #'body))] (cur->coq #'body)))
[(real-forall ~! (x:id (~datum :) t) body:expr) "")]
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t) [(real-lambda ~! (x:id (~datum :) t) body:expr)
(output-coq #'body))] (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...) (cur->coq #'body))]
(begin [(real-forall ~! (x:id (~datum :) t) body:expr)
(coq-lift-top-level (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
(format "Inductive ~a : ~a :=~a." (cur->coq #'body))]
(sanitize-id (format "~a" (syntax-e #'n))) [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
(output-coq #'t) (begin
(for/fold ([strs ""]) (coq-lift-top-level
([clause (syntax->list #'((x* : t*) ...))]) (format "Inductive ~a : ~a :=~a."
(syntax-parse clause (sanitize-id (format "~a" (syntax-e #'n)))
[(x (~datum :) t) (cur->coq #'t)
(format "~a~n| ~a : ~a" strs (syntax-e #'x) (for/fold ([strs ""])
(output-coq #'t))])))) ([clause (syntax->list #'((x* : t*) ...))])
"")] (syntax-parse clause
[(Type i) "Type"] [(x (~datum :) t)
[(real-elim var t) (format "~a~n| ~a : ~a" strs (syntax-e #'x)
(format "~a_rect" (output-coq #'var))] (cur->coq #'t))]))))
[(real-app e1 e2) "")]
(format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))] [(Type i) "Type"]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))]))) [(real-elim var t)
(format "~a_rect" (cur->coq #'var))]
[(real-app e1 e2)
(format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
(format
"~a~a"
(coq-defns)
(if (regexp-match "^\\s*$" output)
""
(format "Eval compute in ~a." output))))))
(define-syntax (generate-coq syn) (define-syntax (generate-coq syn)
(syntax-parse syn (syntax-parse syn
[(_ (~optional (~seq #:file file)) [(_ (~optional (~seq #:file file))
(~optional (~seq #:exists flag)) body:expr) (~optional (~seq #:exists flag))
(parameterize ([current-output-port (if (attribute file) body:expr)
(open-output-file (syntax->datum #'file) (parameterize ([current-output-port
#:exists (if (attribute file)
(if (attribute flag) (open-output-file
;; TODO: AHH WHAT? (syntax->datum #'file)
(eval (syntax->datum #'flag)) #:exists
'error)) (if (attribute flag)
(current-output-port))] ;; TODO: AHH WHAT?
[coq-defns ""]) (eval (syntax->datum #'flag))
(define output 'error))
(let ([body (output-coq #'body)]) (current-output-port))])
(if (regexp-match "^\\s*$" body) (displayln (cur->coq #'body))
""
(format "Eval compute in ~a." body))))
(displayln (format "~a~a" (coq-defns) output))
#'(begin))])) #'(begin))]))
;; TODO: Should these display or return a string?
(begin-for-syntax
(define (display-mathpartir)
(displayln
"%% Requires mathpartir, http://pauillac.inria.fr/~remy/latex/mathpartir.html")
(displayln
"%% or mttex, https://github.com/wilbowma/mttex")
(displayln
"\\usepackage{mathpartir}"))
(define (display-bnf)
(displayln
"%% Some auxillary defs. These should deleted if using mttex, https://github.com/wilbowma/mttex")
(displayln
"\\newcommand{\\bnfdef}{{\\bf ::=}}")
(displayln
"\\newcommand{\\bnfalt}{{\\bf \\mid}}")))
;; ------------------------------------
;; define-relation
(begin-for-syntax
(define-syntax-class horizontal-line
(pattern
x:id
#:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
(define-syntax-class hypothesis
(pattern (x:id (~datum :) t))
(pattern (~not e:horizontal-line)))
;; Alias syntax-classes with names for better error messages
(define-syntax-class rule-name
(pattern x:id))
(define-syntax-class relation-name
(pattern x:id))
(define-syntax-class relation-index
(pattern e:expr))
(define-syntax-class (conclusion n args lab)
(pattern
(name:id arg:expr ...)
#:attr rule-label-symbol (syntax-e lab)
#:attr rule-name-symbol (syntax-e #'name)
#:attr relation-name-symbol (syntax-e n)
#:fail-unless (eq? (attribute rule-name-symbol) (attribute relation-name-symbol))
(format "In rule ~a, name of conclusion ~a did not match name of relation ~a"
(attribute rule-label-symbol)
(attribute rule-name-symbol)
(attribute relation-name-symbol))
#:attr rule-arg-count (length (attribute arg))
#:attr relation-arg-count (length args)
#:fail-unless (= (attribute rule-arg-count) (attribute relation-arg-count))
(format "In rule ~a, conclusion applied to ~a arguments, while relation declared to have ~a arguments"
(attribute rule-label-symbol)
(attribute rule-arg-count)
(attribute relation-arg-count))))
;; TODO: Automatically infer hypotheses that are merely declarations by binding all free identifiers?
;; TODO: Automatically infer hypotheses as above for meta-variables that are the
;; same as bnf grammar, as a simple first case
(define-syntax-class (inferrence-rule name indices)
(pattern (h:hypothesis ...
#;line:horizontal-line
(~optional line:horizontal-line)
~!
lab:rule-name
(~var t (conclusion name indices (attribute lab))))
#:with constr-decl
#'(lab : (-> h ... (t.name t.arg ...)))
;; TODO: convert meta-vars such as e1 to e_1
#:attr latex
(format
"\\inferrule~n{~a}~n{~a}"
(string-trim
(for/fold ([str ""])
;; TODO: Perhaps omit hypotheses that are merely delcarations of free variables
([hyp (syntax->datum #'(h ...))])
(format "~a~a \\+" str hyp))
" \\+"
#:left? #f)
(format "~a" (syntax->datum #'(t.name t.arg ...))))))
;; TODO: Should this display or return a string?
(define (typeset-relation form rules-latex)
(display-mathpartir)
(printf
"\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}"
form
(string-trim
(for/fold ([str ""])
([rule rules-latex])
(format "~a~a\\and~n" str rule))
"\\and"
#:left? #f))))
(define-syntax (define-relation syn)
(syntax-parse syn
[(_ (name:relation-name index:relation-index ...)
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
(~var rule (inferrence-rule (attribute name) (attribute index))) ...)
(let ([output #`(data name : (-> index ... Type) rule.constr-decl ...)])
(when (attribute latex-file)
(with-output-to-file (syntax->datum #'latex-file)
(thunk
(typeset-relation
(syntax->datum #'(name index ...))
(attribute rule.latex)))
#:exists 'append))
(when (attribute coq-file)
(with-output-to-file (syntax->datum #'coq-file)
(thunk (displayln (cur->coq output)))
#:exists 'append))
output)]))
;; ------------------------------------
;; define-language
(begin-for-syntax
;; A mutable dictionary from non-terminal meta-variables names to their types.
(define mv-map (make-parameter #f))
;; A set containing the meta-variables that represent variables.
(define vars (make-parameter #f))
;; The language name for the language currently being parsed
(define lang-name (make-parameter #f))
;; A meta-variable is any identifiers that belongs to the mv-map
(define-syntax-class meta-variable
(pattern
x:id
#:attr sym (syntax->datum #'x)
#:fail-unless (dict-has-key? (mv-map) (attribute sym)) #f
#:attr type (dict-ref (mv-map) (attribute sym))))
;; A var-meta-variable is a meta-variable that is declared to be
;; treated as a variable in the defined language.
(define-syntax-class var-meta-variable
(pattern
x:id
#:fail-unless (set-member? (vars) (syntax->datum #'x)) #f))
;; A terminal is a idnetifiers that is not a meta-variable. A terminal will always represent a constructor.
(define-syntax-class terminal
(pattern
x:id
#:attr sym (syntax->datum #'x)
#:fail-when (dict-has-key? (mv-map) (attribute sym)) #f
#:attr constructor-name
(format-id #'x "~a-~a" (lang-name) #'x)))
;; A terminal-args can appear as the argument to a terminal in
;; an expression, or as a sub-expression in a terminal-args.
;; Each terminal-args export args, a list of types the
;; terminal-args represents and the list of types the non-terminal's
;; constructor expects in this case.
(define-syntax-class (terminal-args non-terminal-type)
;; A meta-variable is a terminal-args
(pattern
e:meta-variable
#:attr args
(list #'e.type)
#:attr latex
(format "~a" (syntax-e #'e)))
;; An identifier is a terminal-args, but is treated as syntax
(pattern
x:id
#:attr args
'()
#:attr latex
(format "~a" (syntax-e #'x)))
;; So is an empty list
(pattern
()
#:attr args
'()
#:attr latex
"")
;; We use De-Bruijn indices, so binding positions are removed.
(pattern
(#:bind x:var-meta-variable . (~var t (terminal-args non-terminal-type)))
#:attr args
(attribute t.args)
#:attr latex
(format "~a ~a" (syntax-e #'x) (attribute t.latex)))
;; A terminal-args applied to other nested expressions is a terminal-args
(pattern
((~var h (terminal-args non-terminal-type))
(~var t (terminal-args non-terminal-type)) ...)
#:attr args
(for/fold ([ls (attribute h.args)])
([args (attribute t.args)])
(append ls args))
#:attr latex
(format "~a ~a" (attribute h.latex) (apply string-append (attribute t.latex)))))
;; a expression is parameterized by the name of the non-terminal to
;; which is belongs,
;; Each expression exports a constr-decl, which declares a
;; constructor for the non-terminal type.
(define-syntax-class (expression non-terminal-type)
;; A meta-variable is a valid expression.
;; Generates a conversion constructor in constr-decl, and the type of
(pattern
e:meta-variable
#:attr constructor-name
(format-id #'e "~a->~a" #'e.type non-terminal-type)
#:attr constr-decl
#`(constructor-name : (-> e.type #,non-terminal-type))
#:attr latex
(format "~a" (syntax-e #'e)))
;; An identifier is a valid expression, generating a base constructor.
(pattern
x:terminal
#:attr constr-decl
#`(x.constructor-name : #,non-terminal-type)
#:attr latex
(format "~a" (syntax-e #'x)))
;; A terminal applied to a terminal-args is a valid expression.
(pattern
(x:terminal . (~var c (terminal-args non-terminal-type)))
#:attr constr-decl
#`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))
#:attr latex
(format "(~a ~a)" (syntax-e #'x) (attribute c.latex))))
(define-syntax-class non-terminal-def
(pattern
(name:id
(meta-var:id ...+)
(~optional (~datum ::=))
;; Create a name for the type of this non-terminal, from the
;; language name and the non-terminal name.
(~bind [nt-type (format-id #'name "~a-~a" (lang-name) #'name)])
;; Imperatively update the map from meta-variables to the
;; nt-type, to be used when generating the types of the constructors
;; for this and later non-terminal.
(~do (for ([mv (syntax->datum #'(meta-var ...))])
(dict-set! (mv-map) mv (attribute nt-type))))
(~var c (expression (attribute nt-type))) ...)
;; Generates the inductive data type for this non-terminal definition.
#:attr def
#`(data nt-type : Type c.constr-decl ...)
#:attr latex
(format
"\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
(symbol->string (syntax->datum #'name))
(string-trim
(for/fold ([str ""])
([nt (syntax->datum #'(meta-var ...))])
(format "~a~a," str nt))
","
#:left? #f)
(string-trim
(for/fold ([str ""])
([expr (attribute c.latex)])
(format "~a~a \\bnfalt " str expr))
" \\bnfalt "
#:left? #f))))
;; TODO: Should this display or return a string?
(define (typeset-bnf nt-latex)
(display-mathpartir)
(display-bnf)
(printf
"\begin{displaymath}~n\\begin{array}{lrrl}~n~a~n\\end{array}~n\end{displaymath}"
(apply string-append nt-latex))))
;; TODO: For better error messages, add context
;; TODO: Extend define-language with syntax such as ....
;; (term (e) ::= (e1 e2) ((lambda (x) e)
(define-syntax (define-language syn)
(define/syntax-parse
(_ name:id
(~optional (~seq #:vars (x:id ...)))
(~optional (~seq #:output-coq coq-file:str))
(~optional (~seq #:output-latex latex-file:str))
.
non-terminal-defs)
syn)
(parameterize ([mv-map (make-hash)]
[lang-name #'name]
[vars (apply set (map syntax->datum (or (attribute x) '())))])
(cond
[(attribute x) =>
(lambda (xls)
(for ([x xls])
(dict-set! (mv-map) (syntax-e x) #'Nat)))])
(syntax-parse #'non-terminal-defs
[(def:non-terminal-def ...)
(let ([output #`(begin def.def ...)])
(when (attribute latex-file)
(with-output-to-file (syntax-e #'latex-file)
(thunk (typeset-bnf (attribute def.latex)))
#:exists 'append))
(when (attribute coq-file)
(with-output-to-file (syntax-e #'coq-file)
(thunk (displayln (cur->coq output)))
#:exists 'append))
output)])))
;; See stlc.rkt for examples

70
cur-test/cur/tests/olly.rkt
View File

@ -9,77 +9,49 @@
cur/olly) cur/olly)
(begin-for-syntax (begin-for-syntax
(require rackunit) (require rackunit))
(define (check-id-equal? v1 v2)
(check-equal?
(syntax->datum v1)
(syntax->datum v2)))
(define (check-id-match? v1 v2)
(check-regexp-match
v1
(symbol->string (syntax->datum v2))))
(check-id-match?
#px"term\\d+"
(fresh-name #'term))
(check-id-equal?
#'stlc-lambda
(new-name #'stlc #'lambda))
(check-id-match?
#px"stlc-term\\d+"
(new-name #'stlc (fresh-name #'term))))
(begin-for-syntax ;; Can't test this way anymore.
#;(begin-for-syntax
(check-equal? (check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$" (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n")) (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
(output-latex-bnf #'(x) (typeset-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
#'((term (e) ::= (e1 e2) (lambda (x) e)))))
(check-equal? (check-equal?
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$" (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
(format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n")) (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
(output-latex-bnf #'(x) (typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
#'((type (A B C) ::= unit (* A B) (+ A C))))))
(check-equal?
(var-equal? (avar z) (avar z))
true)
(check-equal?
(var-equal? (avar z) (avar (s z)))
false)
(begin-for-syntax (begin-for-syntax
(check-equal? (check-equal?
(parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns)) (format "Inductive nat : Type :=~n| z : nat.~n")
(format "Inductive nat : Type :=~n| z : nat.~n")) (cur->coq #'(data nat : Type (z : nat))))
(check-regexp-match (check-regexp-match
"(forall .+ : Type, Type)" "(forall .+ : Type, Type)"
(output-coq #'(-> Type Type))) (cur->coq #'(-> Type Type)))
(let ([t (parameterize ([coq-defns ""]) (let ([t (cur->coq
(output-coq #'(define-relation (meow gamma term type) #'(define-relation (meow gamma term type)
[(g : gamma) (e : term) (t : type) [(g : gamma) (e : term) (t : type)
--------------- T-Bla --------------- T-Bla
(meow g e t)])) (meow g e t)]))])
(coq-defns))])
(check-regexp-match (check-regexp-match
"Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :=" "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
(first (string-split t "\n"))) (first (string-split t "\n")))
(check-regexp-match (check-regexp-match
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\." "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
(second (string-split t "\n")))) (second (string-split t "\n"))))
(let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z (let ([t (cur->coq
(lambda (x : nat) (ih-x : nat) ih-x) #'(elim nat Type (lambda (x : nat) nat) z
e))]) (lambda (x : nat) (ih-x : nat) ih-x)
e))])
(check-regexp-match (check-regexp-match
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)" "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
t)) t))
(check-regexp-match (check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n" "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
(parameterize ([coq-defns ""]) (cur->coq
(output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat) #'(define thm:plus-commutes (forall (n : nat) (m : nat)
(== nat (plus n m) (plus m n))))) (== nat (plus n m) (plus m n))))))
(coq-defns)))
(check-regexp-match (check-regexp-match
"Function add1 \\(n : nat\\) := \\(s n\\).\n" "Function add1 \\(n : nat\\) := \\(s n\\).\n"
(parameterize ([coq-defns ""]) (cur->coq #'(define (add1 (n : nat)) (s n)))))
(output-coq #'(define (add1 (n : nat)) (s n)))
(coq-defns))))

126
cur-test/cur/tests/stlc.rkt
View File

@ -2,6 +2,7 @@
(require (require
rackunit rackunit
cur/stdlib/nat cur/stdlib/nat
cur/stdlib/list
cur/stdlib/sugar cur/stdlib/sugar
cur/olly cur/olly
cur/stdlib/maybe cur/stdlib/maybe
@ -15,64 +16,55 @@
(val (v) ::= true false unit) (val (v) ::= true false unit)
;; TODO: Allow datum, like 1, 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 (#:bind x : A) e) (cons e e)
(let (x x) = e in e))) (let (#:bind x #:bind x) = e in e)))
;; TODO: Abstract this over stlc-type, and provide from in OLL (define lookup-env (list-ref stlc-type))
(data Gamma : Type
(emp-gamma : Gamma)
(extend-gamma : (-> Gamma Var stlc-type Gamma)))
(define (lookup-gamma (g : Gamma) (x : Var)) (define (extend-env (g : (List stlc-type)) (t : stlc-type))
(match g (cons stlc-type t g))
[emp-gamma (none stlc-type)]
[(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
(if (var-equal? v1 x)
(some stlc-type t1)
(recur g1))]))
(define-relation (has-type Gamma stlc-term stlc-type) (define-relation (has-type (List stlc-type) stlc-term stlc-type)
#:output-coq "stlc.v" #:output-coq "stlc.v"
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
[(g : Gamma) [(g : (List stlc-type))
------------------------ T-Unit ------------------------ T-Unit
(has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)] (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
[(g : Gamma) [(g : (List stlc-type))
------------------------ T-True ------------------------ T-True
(has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)] (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
[(g : Gamma) [(g : (List stlc-type))
------------------------ T-False ------------------------ T-False
(has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)] (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
[(g : Gamma) (x : Var) (t : stlc-type) [(g : (List stlc-type)) (x : Nat) (t : stlc-type)
(== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t)) (== (Maybe stlc-type) (lookup-env g x) (some stlc-type t))
------------------------ T-Var ------------------------ T-Var
(has-type g (Var-->-stlc-term x) t)] (has-type g (Nat->stlc-term x) t)]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(has-type g e1 t1) (has-type g e1 t1)
(has-type g e2 t2) (has-type g e2 t2)
---------------------- T-Pair ---------------------- T-Pair
(has-type g (stlc-cons e1 e2) (stlc-* t1 t2))] (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(t : stlc-type) (t : stlc-type)
(x : Var) (y : Var)
(has-type g e1 (stlc-* t1 t2)) (has-type g e1 (stlc-* t1 t2))
(has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t) (has-type (extend-env (extend-env g t1) t2) e2 t)
---------------------- T-Let ---------------------- T-Let
(has-type g (stlc-let x y e1 e2) t)] (has-type g (stlc-let e1 e2) t)]
[(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var) [(g : (List stlc-type)) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
(has-type (extend-gamma g x t1) e1 t2) (has-type (extend-env g t1) e1 t2)
---------------------- T-Fun ---------------------- T-Fun
(has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))] (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(has-type g e1 (stlc--> t1 t2)) (has-type g e1 (stlc--> t1 t2))
(has-type g e2 t1) (has-type g e2 t1)
@ -84,59 +76,57 @@
;; TODO: When generating a parser, will need something like (#:name app (e e)) ;; TODO: When generating a parser, will need something like (#:name app (e e))
;; so I can name a constructor without screwing with syntax. ;; so I can name a constructor without screwing with syntax.
(begin-for-syntax (begin-for-syntax
(define index #'z)) (define (dict-shift d)
(for/fold ([d (make-immutable-hash)])
([(k v) (in-dict d)])
(dict-set d k #`(s #,v)))))
(define-syntax (begin-stlc syn) (define-syntax (begin-stlc syn)
(set! index #'z) (let stlc ([syn (syntax-case syn () [(_ e) #'e])]
(let stlc ([syn (syntax-case syn () [(_ e) #'e])]) [d (make-immutable-hash)])
(syntax-parse syn (syntax-parse syn
#:datum-literals (lambda : prj * -> quote let in cons bool) #:datum-literals (lambda : prj * -> quote let in cons bool)
[(lambda (x : t) e) [(lambda (x : t) e)
(let ([oldindex index]) #`(stlc-lambda #,(stlc #'t d) #,(stlc #'e (dict-set (dict-shift d) (syntax->datum #'x) #`z)))]
(set! index #`(s #,index))
;; Replace x with a de bruijn index, by running a CIC term at
;; compile time.
(normalize/syn
#`((lambda (x : stlc-term)
(stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
(Var-->-stlc-term (avar #,oldindex)))))]
[(quote (e1 e2)) [(quote (e1 e2))
#`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))] #`(stlc-cons #,(stlc #'e1 d) #,(stlc #'e2 d))]
[(let (x y) = e1 in e2) [(let (x y) = e1 in e2)
(let* ([y index] #`(stlc-let #,(stlc #'t d) #,(stlc #'e1 d)
[x #`(s #,y)]) #,(stlc #'e2 (dict-set* (dict-shift (dict-shift d))
(set! index #`(s (s #,index))) (syntax->datum #'x) #`z
#`((lambda (x : stlc-term) (y : stlc-term) (syntax->datum #'y) #`(s z))))]
(stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
#,(stlc #'e2)))
(Var-->-stlc-term (avar #,x))
(Var-->-stlc-term (avar #,y))))
#`(let x i #,(stlc #'e1))]
[(e1 e2) [(e1 e2)
#`(stlc-app #,(stlc #'e1) #,(stlc #'e2))] #`(stlc-app #,(stlc #'e1 d) #,(stlc #'e2 d))]
[() #'(stlc-val-->-stlc-term stlc-unit)] [() #'(stlc-val->stlc-term stlc-unit)]
[#t #'(stlc-val-->-stlc-term stlc-true)] [#t #'(stlc-val->stlc-term stlc-true)]
[#f #'(stlc-val-->-stlc-term stlc-false)] [#f #'(stlc-val->stlc-term stlc-false)]
[(t1 * t2) [(t1 * t2)
#`(stlc-* #,(stlc #'t1) #,(stlc #'t2))] #`(stlc-* #,(stlc #'t1 d) #,(stlc #'t2 d))]
[(t1 -> t2) [(t1 -> t2)
#`(stlc--> #,(stlc #'t1) #,(stlc #'t2))] #`(stlc--> #,(stlc #'t1 d) #,(stlc #'t2 d))]
[bool #`stlc-boolty] [bool #`stlc-boolty]
[e [e
(if (eq? 1 (syntax->datum #'e)) (cond
#'stlc-unitty [(eq? 1 (syntax->datum #'e))
#'e)]))) #'stlc-unitty]
[(dict-ref d (syntax->datum #'e) #f) =>
(lambda (x)
#`(Nat->stlc-term #,x))]
[else #'e])])))
(check-equal? (check-equal?
(begin-stlc (lambda (x : 1) x)) (begin-stlc (lambda (x : 1) x))
(stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))) (stlc-lambda stlc-unitty (Nat->stlc-term z)))
(check-equal? (check-equal?
(begin-stlc ((lambda (x : 1) x) ())) (begin-stlc ((lambda (x : 1) x) ()))
(stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))) (stlc-app (stlc-lambda stlc-unitty (Nat->stlc-term z))
(stlc-val-->-stlc-term stlc-unit))) (stlc-val->stlc-term stlc-unit)))
(check-equal?
(begin-stlc (lambda (x : 1) (lambda (y : 1) x)))
(stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Nat->stlc-term (s z)))))
(check-equal? (check-equal?
(begin-stlc '(() ())) (begin-stlc '(() ()))
(stlc-cons (stlc-val-->-stlc-term stlc-unit) (stlc-cons (stlc-val->stlc-term stlc-unit)
(stlc-val-->-stlc-term stlc-unit))) (stlc-val->stlc-term stlc-unit)))
(check-equal? (check-equal?
(begin-stlc #t) (begin-stlc #t)
(stlc-val-->-stlc-term stlc-true)) (stlc-val->stlc-term stlc-true))