From be2fd4a6afd64de2a01ebd67597ec757ee26e70b Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Wed, 4 Feb 2015 18:47:15 -0500
Subject: [PATCH] Reorganized stdlib; fixed some tests

---
 maybe.rkt                     |  7 -------
 oll.rkt                       |  8 ++++----
 proofs-for-free.rkt           |  2 +-
 redex-curnel.rkt              |  2 +-
 bool.rkt => stdlib/bool.rkt   |  2 +-
 stdlib/maybe.rkt              | 16 ++++++++++++++++
 nat.rkt => stdlib/nat.rkt     |  2 +-
 prop.rkt => stdlib/prop.rkt   |  2 +-
 sugar.rkt => stdlib/sugar.rkt |  4 ++--
 stlc.rkt                      |  3 ++-
 10 files changed, 29 insertions(+), 19 deletions(-)
 delete mode 100644 maybe.rkt
 rename bool.rkt => stdlib/bool.rkt (91%)
 create mode 100644 stdlib/maybe.rkt
 rename nat.rkt => stdlib/nat.rkt (97%)
 rename prop.rkt => stdlib/prop.rkt (97%)
 rename sugar.rkt => stdlib/sugar.rkt (95%)

diff --git a/maybe.rkt b/maybe.rkt
deleted file mode 100644
index 5640ff2..0000000
--- a/maybe.rkt
+++ /dev/null
@@ -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))))
diff --git a/oll.rkt b/oll.rkt
index 1906dbe..9c22cc4 100644
--- a/oll.rkt
+++ b/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"))))))
diff --git a/proofs-for-free.rkt b/proofs-for-free.rkt
index 91e2af4..3232eee 100644
--- a/proofs-for-free.rkt
+++ b/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
diff --git a/redex-curnel.rkt b/redex-curnel.rkt
index 9213f58..f2dc72f 100644
--- a/redex-curnel.rkt
+++ b/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)))
diff --git a/bool.rkt b/stdlib/bool.rkt
similarity index 91%
rename from bool.rkt
rename to stdlib/bool.rkt
index b2f188f..e900a43 100644
--- a/bool.rkt
+++ b/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
diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt
new file mode 100644
index 0000000..5ce02ad
--- /dev/null
+++ b/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))
diff --git a/nat.rkt b/stdlib/nat.rkt
similarity index 97%
rename from nat.rkt
rename to stdlib/nat.rkt
index 7cd02ed..1a80012 100644
--- a/nat.rkt
+++ b/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.
diff --git a/prop.rkt b/stdlib/prop.rkt
similarity index 97%
rename from prop.rkt
rename to stdlib/prop.rkt
index 4a533e4..7c1aef7 100644
--- a/prop.rkt
+++ b/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
diff --git a/sugar.rkt b/stdlib/sugar.rkt
similarity index 95%
rename from sugar.rkt
rename to stdlib/sugar.rkt
index 7502e39..afcb6c7 100644
--- a/sugar.rkt
+++ b/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]))
 
 
diff --git a/stlc.rkt b/stlc.rkt
index c09206a..d034c98 100644
--- a/stlc.rkt
+++ b/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)