From d508d9bcff3d5c68867eb3a74f38fa22c2c69cc3 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Thu, 22 Jan 2015 12:37:48 -0500
Subject: [PATCH] Started factoring into libraries.

---
 coq-extraction.rkt | 72 ++++++++++++++++++++++++++++++++++++++++++++++
 example.rkt        | 54 ----------------------------------
 pltools.rkt        | 53 ++++++++++++++++++++++++++++++++++
 redex-core.rkt     |  2 ++
 sugar.rkt          | 51 ++++++++++++++++++++++++++++++++
 5 files changed, 178 insertions(+), 54 deletions(-)
 create mode 100644 coq-extraction.rkt
 create mode 100644 pltools.rkt
 create mode 100644 sugar.rkt

diff --git a/coq-extraction.rkt b/coq-extraction.rkt
new file mode 100644
index 0000000..ef0c78a
--- /dev/null
+++ b/coq-extraction.rkt
@@ -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"))))))
diff --git a/example.rkt b/example.rkt
index 2fca3b3..f03a1dc 100644
--- a/example.rkt
+++ b/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)]))
diff --git a/pltools.rkt b/pltools.rkt
new file mode 100644
index 0000000..eafa2b8
--- /dev/null
+++ b/pltools.rkt
@@ -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)))
diff --git a/redex-core.rkt b/redex-core.rkt
index 0cf7845..50d5c2e 100644
--- a/redex-core.rkt
+++ b/redex-core.rkt
@@ -613,7 +613,9 @@
     #%module-begin
     #%datum
     require
+    provide
     for-syntax
+    module+
     (rename-out
       [dep-lambda lambda]
       [dep-lambda λ]
diff --git a/sugar.rkt b/sugar.rkt
new file mode 100644
index 0000000..021b77e
--- /dev/null
+++ b/sugar.rkt
@@ -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))