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

Reorganizing "pltools" to be more suggestive

Browse Source
This commit is contained in:
William J. Bowman 2015-01-27 19:10:54 -05:00
parent 9ebc1723c6
commit 96f9343029
3 changed files with 74 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

72
coq-extraction.rkt
View File

@ -1,72 +0,0 @@
#lang s-exp "cur-redex.rkt"
(begin-for-syntax
(define orig-insp (variable-reference->module-declaration-inspector
(#%variable-reference)))
(define (disarm syn) (syntax-disarm syn orig-insp))
;; TODO: Pull expand, perhaps list of literals, into a library.
(define (expand syn)
(disarm (local-expand syn 'expression (syntax-e #'(lambda forall data case fix Type #%app #%top)))))
(define (output-coq syn)
(syntax-parse (expand syn)
[((~literal lambda) ~! (x:id (~datum :) t) body:expr)
(format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t)
(output-coq #'body))]
[((~literal forall) ~! (x:id (~datum :) t) body:expr)
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
(output-coq #'body))]
[((~literal data) ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
(format "Inductive ~a : ~a :=~n~a."
(syntax-e #'n)
(output-coq #'t)
(string-trim
(for/fold ([strs ""])
([clause (syntax->list #'((x* : t*) ...))])
(syntax-parse clause
[(x (~datum :) t)
(format "~a~a : ~a~n| " strs (syntax-e #'x)
(output-coq #'t))]))
#px"\\s\\| $"
#:left? #f))]
;; TODO: Add "case". Will be slightly tricky since the syntax is
;; quite different from Coq.
[(e1 e* ...)
(format "(~a~a)" (output-coq #'e1)
(for/fold ([strs ""])
([arg (syntax->list #'(e* ...))])
(format "~a ~a" strs (output-coq arg))))]
[e:id (format "~a" (syntax->datum #'e))])))
(define-syntax (generate-coq syn)
(syntax-parse syn
[(_ (~optional (~seq #:file file)) body:expr)
(parameterize ([current-output-port (if (attribute file)
(syntax->datum #'file)
(current-output-port))])
(displayln (output-coq #'body))
#'Type)]))
(module+ test
(require "sugar.rkt" "pltools.rkt")
(begin-for-syntax
(require rackunit)
(check-equal?
(format "Inductive nat : Type :=~nz : nat.")
(output-coq #'(data nat : Type (z : nat))))
(check-regexp-match
"(forall .+ : Type, Type)"
(output-coq #'(-> Type Type)))
;; TODO: Not sure why these tests are failing.
(let ([t (output-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 temp. : gamma, (forall temp. : term, (forall temp. : 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"))))))

73
pltools.rkt → oll.rkt
View File

@ -1,5 +1,7 @@
#lang s-exp "cur-redex.rkt"
;; OLL: The OTT-Like Library
(require "sugar.rkt" "nat.rkt")
;; TODO: Can't export var, avar because technically these aren't
;; defined....
;; REALLY NEED TO FIX THAT
@ -163,3 +165,74 @@
(stlc-val-->-stlc-term : (-> stlc-val stlc-term))
(stlc-term2151 : (->* stlc-term stlc-term stlc-term))
(stlc-lambda : (->* var stlc-type stlc-term stlc-term))))
(begin-for-syntax
(define orig-insp (variable-reference->module-declaration-inspector
(#%variable-reference)))
(define (disarm syn) (syntax-disarm syn orig-insp))
;; TODO: Pull expand, perhaps list of literals, into a library.
(define (expand syn)
(disarm (local-expand syn 'expression (syntax-e #'(lambda forall data case fix Type #%app #%top)))))
(define (output-coq syn)
(syntax-parse (expand syn)
[((~literal lambda) ~! (x:id (~datum :) t) body:expr)
(format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t)
(output-coq #'body))]
[((~literal forall) ~! (x:id (~datum :) t) body:expr)
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
(output-coq #'body))]
[((~literal data) ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
(format "Inductive ~a : ~a :=~n~a."
(syntax-e #'n)
(output-coq #'t)
(string-trim
(for/fold ([strs ""])
([clause (syntax->list #'((x* : t*) ...))])
(syntax-parse clause
[(x (~datum :) t)
(format "~a~a : ~a~n| " strs (syntax-e #'x)
(output-coq #'t))]))
#px"\\s\\| $"
#:left? #f))]
;; TODO: Add "case". Will be slightly tricky since the syntax is
;; quite different from Coq.
[(e1 e* ...)
(format "(~a~a)" (output-coq #'e1)
(for/fold ([strs ""])
([arg (syntax->list #'(e* ...))])
(format "~a ~a" strs (output-coq arg))))]
[e:id (format "~a" (syntax->datum #'e))])))
(define-syntax (generate-coq syn)
(syntax-parse syn
[(_ (~optional (~seq #:file file)) body:expr)
(parameterize ([current-output-port (if (attribute file)
(syntax->datum #'file)
(current-output-port))])
(displayln (output-coq #'body))
#'Type)]))
(module+ test
(require "sugar.rkt")
(begin-for-syntax
(require rackunit)
(check-equal?
(format "Inductive nat : Type :=~nz : nat.")
(output-coq #'(data nat : Type (z : nat))))
(check-regexp-match
"(forall .+ : Type, Type)"
(output-coq #'(-> Type Type)))
;; TODO: Not sure why these tests are failing.
(let ([t (output-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 temp. : gamma, (forall temp. : term, (forall temp. : 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"))))))

1
proofs-for-free-v2.rkt
View File

@ -1,4 +1,5 @@
#lang s-exp "cur-redex.rkt"
;; Ignore this file.
(require rackunit racket/trace (for-syntax racket/syntax))
;; TODO: Move to standard library