Fixed latex output

Not sure the resulting Coq code will actually type check, due to
differences in the types of Cur eliminators and Coq eliminators.

oll.rkt

@@ -53,14 +53,14 @@
         (when (attribute latex-file)
           (with-output-to-file (syntax->datum #'latex-file)
             (thunk
-              (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)))
+              (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))))
             #:exists 'append))
         #`(begin
             #,@(if (attribute coq-file)
@@ -187,7 +187,7 @@
                      #:left? #f))]))))
   (define (generate-latex-bnf file-name vars clauses)
     (with-output-to-file file-name
-      (thunk (output-latex-bnf vars clauses))
+      (thunk (printf (output-latex-bnf vars clauses)))
       #:exists 'append)))
 (module+ test
   (require "stdlib/sugar.rkt")
@@ -231,11 +231,19 @@
 (data var : Type (avar : (-> nat var)))
 
 (define (var-equal? (v1 : var) (v2 : var))
-  (case* v1
-    [(avar (n1 : nat))
-     (case* v2
-       [(avar (n2 : nat))
+  (case* var v1 (lambda* (v : var) bool)
+    [(avar (n1 : nat)) IH: ()
+     (case* var v2 (lambda* (v : var) bool)
+       [(avar (n2 : nat)) IH: ()
         (nat-equal? n1 n2)])]))
+(module+ test
+  (require rackunit)
+  (check-equal?
+    (var-equal? (avar z) (avar z))
+    btrue)
+  (check-equal?
+    (var-equal? (avar z) (avar (s z)))
+    bfalse))
 
 ;; See stlc.rkt for examples
 
@@ -263,7 +271,7 @@
                               #'begin)
        ;; TODO: Need to add these to a literal set and export it
        ;; Or, maybe overwrite syntax-parse
-       #:literals (lambda forall data real-app case define-theorem
+       #:literals (lambda forall data real-app elim define-theorem
                           define qed begin Type)
        [(begin e ...)
         (for/fold ([str ""])
@@ -303,7 +311,7 @@
                     (output-coq #'body)))
           "")]
        [(lambda ~! (x:id (~datum :) t) body:expr)
-        (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t)
+        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
                 (output-coq #'body))]
        [(forall ~! (x:id (~datum :) t) body:expr)
         (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
@@ -322,21 +330,14 @@
                           (output-coq #'t))]))))
           "")]
        [(Type i) "Type"]
-       [(case e (ec eb) ...)
-        (format "(match ~a with~n~aend)"
-                (output-coq #'e)
-                (for/fold ([strs ""])
-                          ([con   (syntax->list #'(ec ...))]
-                           [body  (syntax->list #'(eb ...))])
-                  (let* ([ids (generate-temporaries (constructor-args con))]
-                         [names (map (compose ~a syntax->datum) ids)])
-                    (format "~a| (~a) => ~a~n" strs
-                      (for/fold ([str (output-coq con)])
-                                ([n names])
-                        (format "~a ~a" str n))
-                      (for/fold ([body (output-coq body)])
-                                ([n names])
-                        (format "(~a ~a)" body n))))))]
+       [(elim var e P m ...)
+        (format "(~a_rect ~a~a ~a)"
+          (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)
         (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
        [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
@@ -377,14 +378,15 @@
                                 (meow g e t)]))
                (coq-defns))])
       (check-regexp-match
-        "Inductive meow : \\(forall temp. : gamma, \\(forall temp. : term, \\(forall temp. : type, Type\\)\\)\\) :="
+        "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 #'(case z (z z) (s (lambda (n : nat) (s n)))))])
+    (let ([t (output-coq #'(elim nat e (lambda (x : nat) nat) z
+                             (lambda* (x : nat) (ih-x : nat) ih-x)))])
       (check-regexp-match
-        "\\(match z with\n\\| \\(z\\) => z\n\\| \\(s .+\\) => \\(\\(fun n : nat => \\(s n\\)\\) .+\\)\nend\\)"
+        "\\(nat_rect \\(fun x : nat => nat\\) z \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\) e\\)"
         t))
     (check-regexp-match
       "Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"

proofs-for-free.rkt

@@ -77,6 +77,7 @@
 (define (CPSf-relation (f1 : CPSf) (f2 : CPSf))
   ;; TODO: Fix run so I can simply use (run CPSf) to perform
   ;; substitution
+  (translate (run CPSf))
   (translate (forall* (ans : Type) (k : (-> X ans)) ans)))
 #;(module+ test
   (require rackunit)

stdlib/bool.rkt

@@ -8,9 +8,10 @@
 (define-syntax (if syn)
   (syntax-case syn ()
     [(_ t s f)
-     #'(case t
-         [btrue s]
-         [bfalse f])]))
+     ;; Compute the motive
+     (let ([M #`(lambda (x : #,(type-infer/syn #'t))
+                  #,(type-infer/syn #'s))])
+       (quasisyntax/loc syn (elim bool t #,M s f)))]))
 
 (define (bnot (x : bool)) (if x bfalse btrue))
 (module+ test

stdlib/maybe.rkt

@@ -8,9 +8,12 @@
 
 (module+ test
   (require rackunit "bool.rkt")
-  ;; TODO: Dependent pattern matching doesn't work yet
-  #;(check-equal? (case* (some bool btrue)
-                  [(none (A : Type)) bfalse]
-                  [(some (A : Type) (x : bool))
-                   (if x btrue bfalse)])
-                btrue))
+  #;(check-equal?
+    (case* maybe (some bool btrue)
+      (lambda (x : (maybe bool)) bool)
+      [(none (A : Type)) IH: ()
+       bfalse]
+      [(some (A : Type) (x : A)) IH: ()
+       ;; TODO: Don't know how to use dependency yet
+       (if x btrue bfalse)])
+    btrue))

stdlib/nat.rkt

@@ -2,7 +2,7 @@
 (require "sugar.rkt" "bool.rkt")
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.
-(provide nat z s add1 sub1 plus nat-equal?)
+(provide nat z s add1 sub1 plus )
 (module+ test
   (require rackunit))
 
@@ -15,33 +15,37 @@
   (check-equal? (add1 (s z)) (s (s z))))
 
 (define (sub1 (n : nat))
-  (case n
+  (case* nat n (lambda (x : nat) nat)
     [z z]
-    [s (lambda (x : nat) x)]))
+    [(s (x : nat)) IH: ((ih-n : nat)) x]))
 (module+ test
   (check-equal? (sub1 (s z)) z))
 
-(define plus
-  (fix (plus : (forall* (n1 : nat) (n2 : nat) nat))
-    (lambda (n1 : nat)
-      (lambda (n2 : nat)
-        (case n1
-          [z n2]
-          [s (λ (x : nat) (plus x (s n2)))])))))
+(define (plus (n1 : nat) (n2 : nat))
+  (case* nat n1 (lambda (x : nat) nat)
+    [z n2]
+    [(s (x : nat)) IH: ((ih-n1 : nat))
+     (s ih-n1)]))
 (module+ test
   (check-equal? (plus z z) z)
   (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
 
-(define-rec (nat-equal? (n1 : nat) (n2 : nat) : bool)
-  (case* n1
-    [z (case* n2
-         [z btrue]
-         [(s (n3 : nat)) bfalse])]
-    [(s (n3 : nat))
-       (case* n2
-         [z btrue]
-         [(s (n4 : nat)) (nat-equal? n3 n4)])]))
+;; Credit to this function goes to Max
+(define (nat-equal? (n1 : nat))
+  (elim nat n1 (lambda (x : nat) (-> nat bool))
+    (lambda (n2 : nat)
+      (elim nat n2 (lambda (x : nat) bool)
+        btrue
+        (lambda* (x : nat) (ih-n2 : bool) bfalse)))
+    (lambda* (x : nat) (ih : (-> nat bool))
+      (lambda (n2 : nat)
+        (elim nat n2 (lambda (x : nat) bool)
+          bfalse
+          (lambda* (x : nat) (ih-bla : bool)
+            (ih x)))))))
 (module+ test
-  (check-equal? btrue (nat-equal? z z))
-  (check-equal? bfalse (nat-equal? z (s z)))
-  (check-equal? btrue (nat-equal? (s z) (s z))))
+  (check-equal? (nat-equal? z z) btrue)
+  (check-equal? (nat-equal? z (s z)) bfalse)
+  (check-equal? (nat-equal? (s z) (s z)) btrue))
+
+

stdlib/prop.rkt

@@ -18,7 +18,7 @@
 
 (define-theorem thm:anything-implies-true (forall (P : Type) true))
 
-(qed (run thm:anything-implies-true) (lambda (P : Type) T))
+(qed thm:anything-implies-true (lambda (P : Type) T))
 
 (data false : Type)
 
@@ -31,20 +31,23 @@
 (define-theorem thm:and-is-symmetric
   (forall* (P : Type) (Q : Type) (ab : (and P Q)) (and Q P)))
 
-;; TODO: BAH! pattern matching on inductive families is still broken.
 (define proof:and-is-symmetric
   (lambda* (P : Type) (Q : Type) (ab : (and P Q))
-    (case* ab
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x)))))
+    (case* and ab
+      (lambda* (P : Type) (Q : Type) (ab : (and P Q))
+         (and Q P))
+      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj Q P y x)))))
 
-#;(qed thm:and-is-symmetric proof:and-is-symmetric)
+(qed thm:and-is-symmetric proof:and-is-symmetric)
 
 (define-theorem thm:proj1
   (forall* (A : Type) (B : Type) (c : (and A B)) A))
 
 (define proof:proj1
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) a)))))
+    (case* and c
+      (lambda* (A : Type) (B : Type) (c : (and A B)) A)
+      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
 (qed thm:proj1 proof:proj1)
 
@@ -53,7 +56,9 @@
 
 (define proof:proj2
   (lambda* (A : Type) (B : Type) (c : (and A B))
-    (case c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) b)))))
+    (case* and c
+      (lambda* (A : Type) (B : Type) (c : (and A B)) B)
+      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
 (qed thm:proj2 proof:proj2)
 

stdlib/sugar.rkt

@@ -66,22 +66,30 @@
     [(_ (name (a : t) ... : t_res) body)
      #'(define name (fix (name : (forall* (a : t) ... t_res))
                       (lambda* (a : t) ... body)))]))
+
 (begin-for-syntax
   (define (rewrite-clause clause)
-    (syntax-case clause (:)
-      [((con (a : A) ...) body) #'(con (lambda* (a : A) ... body))]
-      [(e body) #'(e body)])))
+    (syntax-case clause (: IH:)
+      [((con (a : A) ...) IH: ((x : t) ...) body)
+       #'(lambda* (a : A) ... (x : t) ... body)]
+      [(e body) #'body])))
 
+;; TODO: Expects clauses in same order as constructors as specified when
+;; TODO: inductive D is defined.
 (define-syntax (case* syn)
   (syntax-case syn ()
-    [(_ e clause* ...)
-     #`(case e #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
+    [(_ D e P clause* ...)
+     #`(elim D e P #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
 
 (define-syntax-rule (define-theorem name prop)
   (define name prop))
 
-;; TODO: Current implementation doesn't do beta/eta while type-checking
-;; because reasons. So manually insert a run in the type annotation
-(define-syntax-rule (qed thm pf)
-  ((lambda (x : (run thm)) Type) pf))
+(define-syntax (qed stx)
+  (syntax-case stx ()
+    [(_ t pf)
+     (begin
+       (unless (type-check/syn? #'pf #'t)
+         (raise-syntax-error 'qed "Invalid proof"
+           #'pf #'t))
+       #'pf)]))
 

stlc.rkt

@@ -17,13 +17,14 @@
   (emp-gamma : gamma)
   (extend-gamma : (->* gamma var stlc-type gamma)))
 
-(define-rec (lookup-gamma (g : gamma) (x : var) : (maybe stlc-type))
-  (case* g
+(define (lookup-gamma (g : gamma) (x : var))
+  (case* gamma g (lambda* (g : gamma) (maybe stlc-type))
     [emp-gamma (none stlc-type)]
     [(extend-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type))
+     IH: ((ih-g1 : (maybe stlc-type)))
      (if (var-equal? v1 x)
          (some stlc-type t1)
-         (lookup-gamma g1 x))]))
+         ih-g1)]))
 
 (define-relation (has-type gamma stlc-term stlc-type)
   #:output-coq "stlc.v"