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

Fixed coq generator for elim

Browse Source
This commit is contained in:
William J. Bowman 2015-09-25 18:08:20 -04:00
parent f4d38dec51
commit f353ad8991
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 8 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
oll.rkt
View File

@ -4,7 +4,7 @@
(require (require
"stdlib/sugar.rkt" "stdlib/sugar.rkt"
"stdlib/nat.rkt" "stdlib/nat.rkt"
(only-in "curnel/redex-lang.rkt" [#%app real-app])) (only-in "curnel/redex-lang.rkt" [#%app real-app] [elim real-elim]))
(provide (provide
define-relation define-relation
@ -279,7 +279,7 @@
#'begin) #'begin)
;; TODO: Need to add these to a literal set and export it ;; TODO: Need to add these to a literal set and export it
;; Or, maybe overwrite syntax-parse ;; Or, maybe overwrite syntax-parse
#:literals (lambda forall data real-app elim define-theorem #:literals (lambda forall data real-app real-elim define-theorem
define qed begin Type) define qed begin Type)
[(begin e ...) [(begin e ...)
(for/fold ([str ""]) (for/fold ([str ""])
@ -338,14 +338,8 @@
(output-coq #'t))])))) (output-coq #'t))]))))
"")] "")]
[(Type i) "Type"] [(Type i) "Type"]
[(elim var e P m ...) [(real-elim var t)
(format "(~a_rect ~a~a ~a)" (format "~a_rect" (output-coq #'var))]
(output-coq #'var)
(output-coq #'P)
(for/fold ([x ""])
([m (syntax->list #'(m ...))])
(format "~a ~a" x (output-coq m)))
(output-coq #'e))]
[(real-app e1 e2) [(real-app e1 e2)
(format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))] (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))]))) [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
@ -391,10 +385,11 @@
(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 e (lambda (x : nat) nat) z (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
(lambda* (x : nat) (ih-x : nat) ih-x)))]) (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
"Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n" "Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"