[Broken] rewriting the rest of olly
Rewriting the rest of olly, including the latex and coq generators, and the define-relation form. Unfortunately, managed to break parsing somehow.
This commit is contained in:
William J. Bowman
parent
d613b53700
commit
0e46da74ab
|
|
@ -14,105 +14,240 @@
|
|||
|
||||
;; private; exported for testing only
|
||||
(for-syntax
|
||||
coq-defns
|
||||
output-latex-bnf
|
||||
output-coq))
|
||||
typeset-relation
|
||||
typeset-bnf
|
||||
cur->coq))
|
||||
|
||||
;; Generate Coq from Cur:
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class dash
|
||||
(define coq-defns (make-parameter ""))
|
||||
|
||||
(define (coq-lift-top-level 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
|
||||
;; TODO: Think the above TODO was fixed; consult git log
|
||||
(define (constructor-args syn)
|
||||
(syntax-parse (type-infer/syn syn)
|
||||
#:datum-literals (Π :)
|
||||
[(Π (x:id : t) body)
|
||||
(cons #'x (constructor-args #'body))]
|
||||
[_ null]))
|
||||
|
||||
(define (sanitize-id str)
|
||||
(let ([replace-by `((: _) (- _))])
|
||||
(for/fold ([str str])
|
||||
([p replace-by])
|
||||
(string-replace str (symbol->string (first p))
|
||||
(symbol->string (second p))))))
|
||||
|
||||
(define (cur->coq syn)
|
||||
(parameterize ([coq-defns ""])
|
||||
(define output
|
||||
(let cur->coq ([syn syn])
|
||||
(syntax-parse (cur-expand syn #'define #'begin)
|
||||
;; TODO: Need to add these to a literal set and export it
|
||||
;; Or, maybe overwrite syntax-parse
|
||||
#:literals (real-lambda real-forall data real-app real-elim define begin Type)
|
||||
[(begin e ...)
|
||||
(for/fold ([str ""])
|
||||
([e (syntax->list #'(e ...))])
|
||||
(format "~a~n" (cur->coq e)))]
|
||||
[(define name:id body)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Definition ~a := ~a.~n"
|
||||
(cur->coq #'name)
|
||||
(cur->coq #'body)))
|
||||
"")]
|
||||
[(define (name:id (x:id : t) ...) body)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Function ~a ~a := ~a.~n"
|
||||
(cur->coq #'name)
|
||||
(for/fold ([str ""])
|
||||
([n (syntax->list #'(x ...))]
|
||||
[t (syntax->list #'(t ...))])
|
||||
(format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
|
||||
(cur->coq #'body)))
|
||||
"")]
|
||||
[(real-lambda ~! (x:id (~datum :) t) body:expr)
|
||||
(format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
|
||||
(cur->coq #'body))]
|
||||
[(real-forall ~! (x:id (~datum :) t) body:expr)
|
||||
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
|
||||
(cur->coq #'body))]
|
||||
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Inductive ~a : ~a :=~a."
|
||||
(sanitize-id (format "~a" (syntax-e #'n)))
|
||||
(cur->coq #'t)
|
||||
(for/fold ([strs ""])
|
||||
([clause (syntax->list #'((x* : t*) ...))])
|
||||
(syntax-parse clause
|
||||
[(x (~datum :) t)
|
||||
(format "~a~n| ~a : ~a" strs (syntax-e #'x)
|
||||
(cur->coq #'t))]))))
|
||||
"")]
|
||||
[(Type i) "Type"]
|
||||
[(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)
|
||||
(syntax-parse syn
|
||||
[(_ (~optional (~seq #:file file))
|
||||
(~optional (~seq #:exists flag))
|
||||
body:expr)
|
||||
(parameterize ([current-output-port
|
||||
(if (attribute file)
|
||||
(open-output-file
|
||||
(syntax->datum #'file)
|
||||
#:exists
|
||||
(if (attribute flag)
|
||||
;; TODO: AHH WHAT?
|
||||
(eval (syntax->datum #'flag))
|
||||
'error))
|
||||
(current-output-port))])
|
||||
(displayln (cur->coq #'body))
|
||||
#'(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
|
||||
#:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x))) "Invalid dash"))
|
||||
#:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
|
||||
|
||||
(define-syntax-class decl (pattern (x:id (~datum :) t)))
|
||||
(define-syntax-class declaration
|
||||
(pattern (x:id (~datum :) t)))
|
||||
|
||||
;; Alias syntax-classes with names for better error messages
|
||||
(define-syntax-class hypothesis
|
||||
(pattern (~not e:horizontal-line)))
|
||||
|
||||
(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 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-class (inferrence-rule name indices)
|
||||
(pattern (d:declaration ...
|
||||
(~peek (~not declaration))
|
||||
~!
|
||||
h:hypothesis ...
|
||||
line:horizontal-line
|
||||
#;(~optional line:horizontal-line)
|
||||
lab:rule-name
|
||||
(~var t (conclusion name indices (attribute lab))))
|
||||
#:with constr-decl
|
||||
#'(lab : (-> d ... 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 ""])
|
||||
([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
|
||||
[(_ (n:id types* ...)
|
||||
[(_ (name:relation-name index:relation-index ...)
|
||||
(~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.
|
||||
(~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
|
||||
(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))))
|
||||
(typeset-relation
|
||||
(syntax->datum #'(name index ...))
|
||||
(attribute rule.latex)))
|
||||
#:exists 'append))
|
||||
#`(begin
|
||||
#,@(if (attribute coq-file)
|
||||
#`((generate-coq #:file coq-file #:exists
|
||||
'append #,output))
|
||||
#'())
|
||||
#,output))]))
|
||||
(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
|
||||
;; 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 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 clauses)
|
||||
(with-output-to-file file-name
|
||||
(thunk (printf (output-latex-bnf clauses)))
|
||||
#:exists 'append)))
|
||||
|
||||
(begin-for-syntax
|
||||
;; A mutable dictionary from non-terminal meta-variables names to their types.
|
||||
(define mv-map (make-parameter #f))
|
||||
|
|
@ -157,25 +292,33 @@
|
|||
(pattern
|
||||
e:meta-variable
|
||||
#:attr args
|
||||
(list #'e.type))
|
||||
(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))
|
||||
(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
|
||||
|
|
@ -184,7 +327,9 @@
|
|||
#:attr args
|
||||
(for/fold ([ls (attribute h.args)])
|
||||
([args (attribute t.args)])
|
||||
(append ls 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,
|
||||
|
|
@ -198,19 +343,25 @@
|
|||
#:attr constructor-name
|
||||
(format-id #'e "~a->~a" #'e.type non-terminal-type)
|
||||
#:attr constr-decl
|
||||
#`(constructor-name : (-> e.type #,non-terminal-type)))
|
||||
#`(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))
|
||||
#`(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))))
|
||||
#`(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
|
||||
|
|
@ -228,7 +379,31 @@
|
|||
(~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 ...))))
|
||||
#`(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 ....
|
||||
|
|
@ -251,110 +426,16 @@
|
|||
(for ([x xls])
|
||||
(dict-set! (mv-map) (syntax-e x) #'Nat)))])
|
||||
(syntax-parse #'non-terminal-defs
|
||||
[((~var defs non-terminal-def) ...)
|
||||
(let ([output #`(begin defs.def ...)])
|
||||
;; TODO: Should do this via attributes
|
||||
[(def:non-terminal-def ...)
|
||||
(let ([output #`(begin def.def ...)])
|
||||
(when (attribute latex-file)
|
||||
(generate-latex-bnf (syntax->datum #'latex-file) #'(defs ...)))
|
||||
#`(begin
|
||||
;; TODO: generate-coq should also export a compile-time function.
|
||||
#,@(if (attribute coq-file)
|
||||
#`((generate-coq #:file coq-file #:exists 'append #,output))
|
||||
#'())
|
||||
#,output))])))
|
||||
(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
|
||||
|
||||
;; Generate Coq from Cur:
|
||||
|
||||
(begin-for-syntax
|
||||
(define coq-defns (make-parameter ""))
|
||||
(define (coq-lift-top-level 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
|
||||
;; TODO: Think the above TODO was fixed; consult git log
|
||||
(define (constructor-args syn)
|
||||
(syntax-parse (type-infer/syn syn)
|
||||
#:datum-literals (Π :)
|
||||
[(Π (x:id : t) body)
|
||||
(cons #'x (constructor-args #'body))]
|
||||
[_ null]))
|
||||
(define (sanitize-id str)
|
||||
(let ([replace-by `((: _) (- _))])
|
||||
(for/fold ([str str])
|
||||
([p replace-by])
|
||||
(string-replace str (symbol->string (first p))
|
||||
(symbol->string (second p))))))
|
||||
(define (output-coq syn)
|
||||
(syntax-parse (cur-expand syn #'define #'begin)
|
||||
;; TODO: Need to add these to a literal set and export it
|
||||
;; Or, maybe overwrite syntax-parse
|
||||
#:literals (real-lambda real-forall data real-app real-elim define begin Type)
|
||||
[(begin e ...)
|
||||
(for/fold ([str ""])
|
||||
([e (syntax->list #'(e ...))])
|
||||
(format "~a~n" (output-coq e)))]
|
||||
[(define name:id body)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Definition ~a := ~a.~n"
|
||||
(output-coq #'name)
|
||||
(output-coq #'body)))
|
||||
"")]
|
||||
[(define (name:id (x:id : t) ...) body)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Function ~a ~a := ~a.~n"
|
||||
(output-coq #'name)
|
||||
(for/fold ([str ""])
|
||||
([n (syntax->list #'(x ...))]
|
||||
[t (syntax->list #'(t ...))])
|
||||
(format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
|
||||
(output-coq #'body)))
|
||||
"")]
|
||||
[(real-lambda ~! (x:id (~datum :) t) body:expr)
|
||||
(format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
|
||||
(output-coq #'body))]
|
||||
[(real-forall ~! (x:id (~datum :) t) body:expr)
|
||||
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
|
||||
(output-coq #'body))]
|
||||
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
|
||||
(begin
|
||||
(coq-lift-top-level
|
||||
(format "Inductive ~a : ~a :=~a."
|
||||
(sanitize-id (format "~a" (syntax-e #'n)))
|
||||
(output-coq #'t)
|
||||
(for/fold ([strs ""])
|
||||
([clause (syntax->list #'((x* : t*) ...))])
|
||||
(syntax-parse clause
|
||||
[(x (~datum :) t)
|
||||
(format "~a~n| ~a : ~a" strs (syntax-e #'x)
|
||||
(output-coq #'t))]))))
|
||||
"")]
|
||||
[(Type i) "Type"]
|
||||
[(real-elim var t)
|
||||
(format "~a_rect" (output-coq #'var))]
|
||||
[(real-app e1 e2)
|
||||
(format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
|
||||
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
|
||||
|
||||
(define-syntax (generate-coq syn)
|
||||
(syntax-parse syn
|
||||
[(_ (~optional (~seq #:file file))
|
||||
(~optional (~seq #:exists flag)) body:expr)
|
||||
(parameterize ([current-output-port (if (attribute file)
|
||||
(open-output-file (syntax->datum #'file)
|
||||
#:exists
|
||||
(if (attribute flag)
|
||||
;; TODO: AHH WHAT?
|
||||
(eval (syntax->datum #'flag))
|
||||
'error))
|
||||
(current-output-port))]
|
||||
[coq-defns ""])
|
||||
(define output
|
||||
(let ([body (output-coq #'body)])
|
||||
(if (regexp-match "^\\s*$" body)
|
||||
""
|
||||
(format "Eval compute in ~a." body))))
|
||||
(displayln (format "~a~a" (coq-defns) output))
|
||||
#'(begin))]))
|
||||
|
|
|
|||
|
|
@ -11,49 +11,47 @@
|
|||
(begin-for-syntax
|
||||
(require rackunit))
|
||||
|
||||
(begin-for-syntax
|
||||
;; Can't test this way anymore.
|
||||
#;(begin-for-syntax
|
||||
(check-equal?
|
||||
(format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
|
||||
(format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
|
||||
(output-latex-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
|
||||
(typeset-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
|
||||
(check-equal?
|
||||
(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"))
|
||||
(output-latex-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
|
||||
(typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
|
||||
|
||||
(begin-for-syntax
|
||||
(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
|
||||
"(forall .+ : Type, Type)"
|
||||
(output-coq #'(-> Type Type)))
|
||||
(let ([t (parameterize ([coq-defns ""])
|
||||
(output-coq #'(define-relation (meow gamma term type)
|
||||
[(g : gamma) (e : term) (t : type)
|
||||
--------------- T-Bla
|
||||
(meow g e t)]))
|
||||
(coq-defns))])
|
||||
(cur->coq #'(-> Type Type)))
|
||||
(let ([t (cur->coq
|
||||
#'(define-relation (meow gamma term type)
|
||||
[(g : gamma) (e : term) (t : type)
|
||||
--------------- T-Bla
|
||||
(meow g e t)]))])
|
||||
(check-regexp-match
|
||||
"Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
|
||||
(first (string-split t "\n")))
|
||||
(check-regexp-match
|
||||
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
|
||||
(second (string-split t "\n"))))
|
||||
(let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
|
||||
(lambda (x : nat) (ih-x : nat) ih-x)
|
||||
e))])
|
||||
(let ([t (cur->coq
|
||||
#'(elim nat Type (lambda (x : nat) nat) z
|
||||
(lambda (x : nat) (ih-x : nat) ih-x)
|
||||
e))])
|
||||
(check-regexp-match
|
||||
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
|
||||
t))
|
||||
(check-regexp-match
|
||||
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
|
||||
(parameterize ([coq-defns ""])
|
||||
(output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
|
||||
(== nat (plus n m) (plus m n)))))
|
||||
(coq-defns)))
|
||||
(cur->coq
|
||||
#'(define thm:plus-commutes (forall (n : nat) (m : nat)
|
||||
(== nat (plus n m) (plus m n))))))
|
||||
(check-regexp-match
|
||||
"Function add1 \\(n : nat\\) := \\(s n\\).\n"
|
||||
(parameterize ([coq-defns ""])
|
||||
(output-coq #'(define (add1 (n : nat)) (s n)))
|
||||
(coq-defns))))
|
||||
(cur->coq #'(define (add1 (n : nat)) (s n)))))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user