Module language, positivity checking, more tests

* redex-core is now a module language, complete with fancyness. For
  documentation, TODO.
* Added examples file using the module language.

example.rkt

@@ -0,0 +1,30 @@
+#lang s-exp "redex-core.rkt"
+
+(define-syntax (-> syn)
+  (syntax-case syn ()
+    [(_ t1 t2)
+     (with-syntax ([(x) (generate-temporaries '(1))])
+       #'(forall (x : t1) t2))]))
+
+(data true : Type
+  (TT : true))
+
+(data nat : Type
+  (z : nat)
+  (s : (-> nat nat)))
+
+(lambda (nat : Type)
+  ((lambda (x : (forall (y : Type) Type)) (x nat))
+   (lambda (y : Type) y)))
+
+(lambda (nat : Type) nat)
+
+(lambda (y : (-> nat nat))
+  (lambda (x : nat) (y x)))
+
+(define y (lambda (x : true) x))
+(define (y1 (x : true)) x)
+y1
+
+(define (y2 (x1 : true) (x2 : true)) x1)
+(y2 TT TT)

redex-core.rkt

@@ -1,17 +1,11 @@
-#lang racket/base
+#lang racket
 
+(module core racket
   (require
     (only-in racket/set set=?)
-  (only-in racket curry)
     redex/reduction-semantics)
-
+  (provide
-#;(provide
+    (all-defined-out))
-  define-constructor-for
-  match
-  define-fun
-  define-rec
-  lambda)
-
 
   ;; References:
   ;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
@@ -80,6 +74,7 @@
   ;; NB: Substitution is hard
   (define-metafunction dtracketL
     subst : t x t -> t
+    [(subst U x t) U]
     [(subst x x t) t]
     [(subst x_0 x t) x_0]
     [(subst (Π (x : t_0) t_1) x t) (Π (x : t_0) t_1)]
@@ -205,6 +200,49 @@
     (check-true
       (term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat))))
 
+  (define-metafunction dtracketL
+    positive : t any -> #t or #f
+    ;; Type; not a inductive constructor
+    [(positive U any) #t]
+    ;; nat
+    [(positive x_0 x_0) #t]
+    ;; nat -> t_1 ... -> nat
+    [(positive (Π (x : x_1) t_1) x_0)
+     (positive t_1 x_0)]
+    ;; Type -> t_1 ... -> nat
+    [(positive (Π (x : U) t_1) x_0)
+     (positive t_1 x_0)]
+    ;; (t_0 -> t_2) -> t_1 ... -> nat
+    [(positive (Π (x : (Π (x_1 : t_0) t_2)) t_1) x_0)
+     ,(and (term (copositive (Π (x_1 : t_0) t_2) x_0)) (term (positive t_1 x_0)))])
+
+  (define-metafunction dtracketL
+    copositive : t any -> #t or #f
+    [(copositive U any) #t]
+    [(copositive x_0 x_0) #f]
+    [(copositive (Π (x : x_0) t_1) x_0) #f]
+    ;; x_1 -> t_1 ... -> nat
+    [(copositive (Π (x : x_1) t_1) x_0)
+     (positive t_1 x_0)]
+    [(copositive (Π (x : U) t_1) x_0)
+     (positive t_1 x_0)]
+    [(copositive (Π (x : (Π (x_1 : t_0) t_2)) t_1) x_0)
+     ,(and (term (positive (Π (x_1 : t_0) t_2) x_0)) (term (copositive t_1 x_0)))])
+
+  (module+ test
+    (check-true (term (positive nat nat)))
+    (check-true (term (positive (Π (x : nat) nat) nat)))
+    ;; (nat -> nat) -> nat
+    (check-false (term (positive (Π (x : (Π (y : nat) nat)) nat) nat)))
+    ;; (Type -> nat) -> nat
+    (check-true (term (positive (Π (x : (Π (y : Type) nat)) nat) nat)))
+    ;; (((nat -> Type) -> nat) -> nat)
+    (check-true (term (positive (Π (x : (Π (y : (Π (x : nat) Type)) nat)) nat) nat)))
+    (check-false (term (positive (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat) nat)))
+
+    (check-true (term (positive Type #f)))
+    )
+
   (define-judgment-form dtracket-typingL
     #:mode (wf I I)
     #:contract (wf Σ Γ)
@@ -217,6 +255,7 @@
      (wf Σ (Γ x : t))]
 
     [(types Σ ∅ t U)
+     (side-condition (positive t (result-type Σ t)))
      -----------------
      (wf (Σ x : t) ∅)])
   (module+ test
@@ -332,7 +371,29 @@
                     (types (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat))
                            ∅
                            (case zero (zero (s zero)))
-                         nat))))
+                           nat)))
+    (define Σ0 (term ∅))
+    (define lam (term (λ (nat : Type) nat)))
+    (check-equal?
+      (term (Π (nat : Type) Type))
+      (judgment-holds (types ,Σ0 ∅ ,lam t) t))
+    (define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat))))
+    (check-equal?
+      (term (Π (nat : Type) Type))
+      (judgment-holds (types ,Σ2 ∅ ,lam t) t))
+    (check-equal?
+      (term (Π (x : (Π (y : Type) y)) nat))
+      (judgment-holds (types (∅ nat : Type) ∅ (λ (x : (Π (y : Type) y)) (x nat))
+                            t) t))
+    (check-equal?
+      (term (Π (y : Type) Type))
+      (judgment-holds (types (∅ nat : Type) ∅ (λ (y : Type) y) t) t))
+    (check-equal?
+      (term Type)
+      (judgment-holds (types (∅ nat : Type) ∅
+                            ((λ (x : (Π (y : Type) Type)) (x nat))
+                             (λ (y : Type) y))
+                            t) t)))
 
   (define-judgment-form dtracket-typingL
     #:mode (type-check I I I)
@@ -377,35 +438,143 @@
 
     [(check Γ e t)
      ----------------- "DTR-SAnnotate"
-   (synth Γ (e : t) t)])
+     (synth Γ (e : t) t)]) )
 
-#;(define-judgment-form dtracket-typingL
+(module sugar racket
-  #:mode (check I I I)
+  (require
-  #:contract (check Γ t t)
+    racket/trace
+    racket/pretty
+    (submod ".." core)
+    redex/reduction-semantics
+    (for-syntax
+      racket
+      racket/pretty
+      racket/trace
+      (except-in (submod ".." core) remove)
+      redex/reduction-semantics))
+  (provide
+    ;; Basic syntax
+    #%module-begin
+    (rename-out
+      [dep-lambda lambda]
+      [dep-lambda λ]
+      [dep-app #%app]
 
-  [(check (Γ x : t_0) e t_1)
+      [dep-forall forall]
-   ----------------- "DTR-Abstraction"
+      [dep-forall ∀]
-   (check Γ (λ x e) (Π (x : t_0) t_1))]
 
-  [(synth Γ e t)
+      [dep-inductive data]
-   ----------------- "DTR-SSynth"
+      [dep-case case]
-   (check Γ e t)])
-#;(module+ test
-  (check-equal?
-    (list (term (Unv 0)))
-    (judgment-holds (synth ∅ Type U) U))
-  (check-equal?
-    (list (term Unv 0))
-    (judgment-holds (synth (∅ x : Type) Type U)))
-  (check-equal?
-    (list (term Type))
-    (judgment-holds (synth (∅ x : Type) x U)))
-  (check-equal?
-    (list (term Type))
-    (judgment-holds (synth ((∅ x_0 : Type) x_1 : Type) (Π (x_3 : x_0) x_1) U)))
 
-  (check-equal?
+      [dep-var #%top])
-    (list ())
+    ;; DYI syntax extension
-    (judgment-holds (synth ∅ (λ (x : Type) x) (Π (x : Type) Type))))
+    define-syntax
-  (check-true (judgment-holds (types ∅ (λ (y : Type) (λ (x : y) x))
+    (rename-out [dep-define define])
-                                     (Π (y : Type) (Π (x : y) y))))))
+    syntax-case
+    syntax-rules
+    (for-syntax (all-from-out racket)))
+
+  (begin-for-syntax
+    (current-trace-notify
+      (parameterize ([pretty-print-depth #f]
+                     [pretty-print-columns 'infinity])
+        (lambda (x)
+          (pretty-display x)
+          (newline))))
+    (current-trace-print-args
+      (let ([cwtpr (current-trace-print-args)])
+        (lambda (s l kw l2 n)
+          (cwtpr s (map syntax->datum l) kw l2 n))))
+    (current-trace-print-results
+      (let ([cwtpr (current-trace-print-results)])
+        (lambda (s l n)
+         (cwtpr s (map syntax->datum l) n)))))
+
+  ;; WEEEEEEE
+  (define gamma
+    (make-parameter (term ∅)
+      (lambda (x)
+        (unless (redex-match? dtracket-typingL Γ x)
+          (error 'core-error "We build a bad gamma ~s" x))
+        x)))
+  (define sigma
+    (make-parameter (term ∅)#;(term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat)))
+      (lambda (x)
+        (unless (redex-match? dtracket-typingL Σ x)
+          (error 'core-error "We build a bad sigma ~s" x))
+        x)))
+  #;(define-syntax (-> syn)
+    (syntax-case syn ()
+      [(_ t1 t2)
+       (with-syntax ([(x) (generate-temporaries '(1))])
+         #'(dep-forall (x : t1) t2))]))
+
+  (define-syntax (dep-lambda syn)
+    (syntax-case syn (:)
+      [(_ (x : t) e)
+       #`(let* ([lam (term (λ (x : ,t)
+                              ,(let ([x (term x)])
+                                 (parameterize ([gamma (term (,(gamma) ,x : ,t))])
+                                   e))))])
+           (unless (judgment-holds (types ,(sigma) ,(gamma) ,lam t_0))
+             (error 'type-checking "Term is ill-typed: ~s" lam))
+           lam)]))
+
+  (define-syntax (curry-app syn)
+    (syntax-case syn ()
+      [(_ e1 e2) #'(term (,e1 ,e2))]
+      [(_ e1 e2 e3 ...)
+       #'(curry-app (term (,e1 ,e2)) e3 ...)]))
+
+  (define-syntax (dep-app syn)
+    (syntax-case syn ()
+      [(_ e1 e2 ...)
+       #'(term (reduce ,(curry-app e1 e2 ...))) ]))
+
+  (define-syntax-rule (dep-case e (x0 e0) ...)
+    (term (case ,e (,x0 ,e0) ...)))
+
+  (define-syntax (dep-inductive syn)
+    (syntax-case syn (:)
+      [(_ i : ti (x1 : t1) ...)
+       #'(begin
+           (sigma (term (,(sigma) i : ,ti)))
+           (for ([x (list (term x1) ...)]
+                 [t (list (term ,t1) ...)])
+             (sigma (term (,(sigma) ,x : ,t)))))]))
+
+  ;; TODO: Lots of shared code with dep-lambda
+  (define-syntax (dep-forall syn)
+    (syntax-case syn (:)
+      [(_ (x : t) e)
+       #`(let ([tmp (term (Π (x : ,t)
+                             ,(let ([x (term x)])
+                                 (parameterize ([gamma (term (,(gamma) ,x : ,t))])
+                                   e))))])
+           (unless (judgment-holds (types ,(sigma) ,(gamma) ,tmp U_0))
+             (error 'type-checking "Term is ill-typed: ~s" tmp))
+           tmp)]))
+
+  (define-syntax (dep-var syn)
+    (syntax-case syn ()
+      [(_ . id)
+       #'(let ()
+           (unless (judgment-holds (types ,(sigma) ,(gamma) ,(term id) t_0))
+             (error 'unbound "Unbound variable: ~s" (term id)))
+           (term id))]))
+
+  (define-syntax (curry-lambda syn)
+    (syntax-case syn (:)
+      [(_ ((x : t) (xr : tr) ...) e)
+       #'(dep-lambda (x : t) (curry-lambda ((xr : tr) ...) e))]
+      [(_ () e) #'e]))
+  ;; TODO: Syntax-parse
+  (define-syntax (dep-define syn)
+    (syntax-case syn (:)
+      [(_ (name (x : t) ...) e)
+       #'(define name (curry-lambda ((x : t) ...) e))]
+      [(_ id e)
+       #'(define id e)])))
+
+(require 'sugar)
+(provide (all-from-out 'sugar))