Reorganized stdlib; fixed some tests

maybe.rkt

@@ -1,7 +0,0 @@
-#lang s-exp "redex-curnel.rkt"
-(require "sugar.rkt")
-(provide maybe none some)
-
-(data maybe : (forall (A : Type) Type)
-  (none : (forall (A : Type) (maybe A)))
-  (some : (forall* (A : Type) (a : A) (maybe A))))

oll.rkt

@@ -2,7 +2,7 @@
 ;; OLL: The OTT-Like Library
 ;; TODO: Add latex extraction
 ;; TODO: Automagically create a parser from bnf grammar
-(require "sugar.rkt" "nat.rkt" racket/trace)
+(require "stdlib/sugar.rkt" "stdlib/nat.rkt" racket/trace)
 
 (provide define-relation define-language var avar var-equal?)
 
@@ -192,7 +192,7 @@
        #'Type)]))
 
 (module+ test
-  (require "sugar.rkt")
+  (require "stdlib/sugar.rkt")
   (begin-for-syntax
     (require rackunit)
     (check-equal?
@@ -207,8 +207,8 @@
                               --------------- T-Bla
                               (meow g e t)]))])
       (check-regexp-match
-        "Inductive meow : (forall temp. : gamma, (forall temp. : term, (forall temp. : type, Type))) :="
+        "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))))\\."
+        "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
         (second (string-split t "\n"))))))

proofs-for-free.rkt

@@ -1,5 +1,5 @@
 #lang s-exp "redex-curnel.rkt"
-(require "sugar.rkt" "prop.rkt")
+(require "stdlib/sugar.rkt" "stdlib/prop.rkt")
 
 ;; ---------
 (begin-for-syntax

redex-curnel.rkt

@@ -1013,6 +1013,6 @@
          #'(void))])))
 
 (require (rename-in 'sugar [module+ dep-module+]))
-(provide (all-from-out 'sugar))
+(provide (rename-out [dep-module+ module+]) (all-from-out 'sugar))
 (module+ test
   (require (submod ".." core test)))

stdlib/bool.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "redex-curnel.rkt"
+#lang s-exp "../redex-curnel.rkt"
 (provide bool btrue bfalse if bnot)
 
 (data bool : Type

stdlib/maybe.rkt

@@ -0,0 +1,16 @@
+#lang s-exp "../redex-curnel.rkt"
+(require "sugar.rkt")
+(provide maybe none some)
+
+(data maybe : (forall (A : Type) Type)
+  (none : (forall (A : Type) (maybe A)))
+  (some : (forall* (A : Type) (a : A) (maybe A))))
+
+(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))

stdlib/nat.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "redex-curnel.rkt"
+#lang s-exp "../redex-curnel.rkt"
 (require "sugar.rkt" "bool.rkt")
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.

stdlib/prop.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "redex-curnel.rkt"
+#lang s-exp "../redex-curnel.rkt"
 (require "sugar.rkt")
 ;; TODO: Handle multiple provide forms properly
 ;; TODO: Handle (all-defined-out) properly

stdlib/sugar.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "redex-curnel.rkt"
+#lang s-exp "../redex-curnel.rkt"
 (provide ->
          ->*
          forall*
@@ -12,7 +12,7 @@
          real-app
          define-rec)
 
-(require (only-in "redex-curnel.rkt" [#%app real-app]
+(require (only-in "../redex-curnel.rkt" [#%app real-app]
                   [define real-define]))
 
 

stlc.rkt

@@ -1,5 +1,6 @@
 #lang s-exp "redex-curnel.rkt"
-(require racket/trace "nat.rkt" "sugar.rkt" "oll.rkt" "maybe.rkt")
+(require racket/trace "stdlib/nat.rkt" "stdlib/sugar.rkt" "oll.rkt"
+         "stdlib/maybe.rkt")
 
 (define-language stlc
   #:vars (x)