Started factoring into libraries.
This commit is contained in:
William J. Bowman
parent
f4a47cc7d6
commit
d508d9bcff
72
coq-extraction.rkt
Normal file
72
coq-extraction.rkt
Normal file
|
|
@ -0,0 +1,72 @@
|
|||
#lang s-exp "redex-core.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"))))))
|
||||
54
example.rkt
54
example.rkt
|
|
@ -431,57 +431,3 @@
|
|||
(has-type g e2 t1)
|
||||
---------------------- T-App
|
||||
(has-type g (app e1 e2) t2)])
|
||||
|
||||
(begin-for-syntax
|
||||
(define orig-insp (variable-reference->module-declaration-inspector
|
||||
(#%variable-reference)))
|
||||
|
||||
(define (disarm syn) (syntax-disarm syn orig-insp))
|
||||
|
||||
(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))]
|
||||
[(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)]))
|
||||
|
||||
(generate-coq (data nat : Type (z : nat)))
|
||||
(generate-coq (-> Type Type))
|
||||
(generate-coq
|
||||
(define-relation (meow gamma term type)
|
||||
[(g : gamma) (e : term) (t : type)
|
||||
--------------- T-Bla
|
||||
(meow g e t)]))
|
||||
|
|
|
|||
53
pltools.rkt
Normal file
53
pltools.rkt
Normal file
|
|
@ -0,0 +1,53 @@
|
|||
#lang s-exp "redex-core.rkt"
|
||||
(require "sugar.rkt")
|
||||
(provide define-relation)
|
||||
|
||||
(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?
|
||||
(define-syntax-class inferrence-rule
|
||||
(pattern (d:decl ...
|
||||
x*:expr ...
|
||||
line:dash lab:id
|
||||
(name:id y* ...))
|
||||
#:with rule #'(lab : (forall* d ...
|
||||
(->* x* ... (name y* ...)))))))
|
||||
(define-syntax (define-relation syn)
|
||||
(syntax-parse syn
|
||||
[(_ (n:id types* ...) 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"
|
||||
#`(data n : (->* types* ... Type)
|
||||
rules.rule ...)]))
|
||||
|
||||
;; TODO: Add BNF syntax, with binders?
|
||||
;; (define-language name
|
||||
; #:literal (-> lambda)
|
||||
; #:var (x)
|
||||
; (v : val ::= true false)
|
||||
; (t : type ::= bool (-> t t))
|
||||
; (e : term ::= var (e e) (lambda (x : t) e)))
|
||||
; =>
|
||||
; (data var : Type (avar : (-> nat var)))
|
||||
; (also generate gamma, function, etc.)
|
||||
; (data name-val : Type
|
||||
; (name-true : val)
|
||||
; (name-false : val))
|
||||
; (data name-term : Type
|
||||
; (name-term-var : (-> var name-term))
|
||||
; (name-term1 : (->* name-term name-term name-term))
|
||||
; (name-lambda : (->* var name-type name-term name-term)))
|
||||
; (data name-type : Type
|
||||
; (name-bool : type)
|
||||
; (name--> : (-> name-type name-type)))
|
||||
|
|
@ -613,7 +613,9 @@
|
|||
#%module-begin
|
||||
#%datum
|
||||
require
|
||||
provide
|
||||
for-syntax
|
||||
module+
|
||||
(rename-out
|
||||
[dep-lambda lambda]
|
||||
[dep-lambda λ]
|
||||
|
|
|
|||
51
sugar.rkt
Normal file
51
sugar.rkt
Normal file
|
|
@ -0,0 +1,51 @@
|
|||
#lang s-exp "redex-core.rkt"
|
||||
(provide ->
|
||||
->*
|
||||
forall*
|
||||
lambda*
|
||||
case*
|
||||
define-theorem
|
||||
qed)
|
||||
|
||||
(define-syntax (-> syn)
|
||||
(syntax-case syn ()
|
||||
[(_ t1 t2)
|
||||
(with-syntax ([(x) (generate-temporaries '(1))])
|
||||
#`(forall (x : t1) t2))]))
|
||||
|
||||
(define-syntax ->*
|
||||
(syntax-rules ()
|
||||
[(->* a) a]
|
||||
[(->* a a* ...)
|
||||
(-> a (->* a* ...))]))
|
||||
|
||||
(define-syntax forall*
|
||||
(syntax-rules (:)
|
||||
[(_ (a : t) (ar : tr) ... b)
|
||||
(forall (a : t)
|
||||
(forall* (ar : tr) ... b))]
|
||||
[(_ b) b]))
|
||||
|
||||
(define-syntax lambda*
|
||||
(syntax-rules (:)
|
||||
[(_ (a : t) (ar : tr) ... b)
|
||||
(lambda (a : t)
|
||||
(lambda* (ar : tr) ... b))]
|
||||
[(_ b) b]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define (rewrite-clause clause)
|
||||
(syntax-case clause (:)
|
||||
[((con (a : A) ...) body) #'(con (lambda* (a : A) ... body))]
|
||||
[(e body) #'(e body)])))
|
||||
|
||||
(define-syntax (case* syn)
|
||||
(syntax-case syn ()
|
||||
[(_ e clause* ...)
|
||||
#`(case e #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
|
||||
|
||||
(define-syntax-rule (define-theorem name prop)
|
||||
(define name prop))
|
||||
|
||||
(define-syntax-rule (qed thm pf)
|
||||
((lambda (x : thm) T) pf))
|
||||
Loading…
Reference in New Issue
Block a user