From 44b4f5ca818794e0ab9f5e506a7666bd507c5e5b Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 2 Oct 2015 18:06:33 -0400
Subject: [PATCH] Add type-inferring constructors

Convention: /i denotes a type-inferring version of something.
---
 stdlib/maybe.rkt | 11 ++++++++++-
 stdlib/prop.rkt  | 16 +++++++++++++---
 2 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt
index 7f9b5ff..2550871 100644
--- a/stdlib/maybe.rkt
+++ b/stdlib/maybe.rkt
@@ -1,13 +1,22 @@
 #lang s-exp "../cur.rkt"
 (require "sugar.rkt")
-(provide Maybe none some)
+(provide Maybe none some some/i)
 
 (data Maybe : (forall (A : Type) Type)
   (none : (forall (A : Type) (Maybe A)))
   (some : (forall* (A : Type) (a : A) (Maybe A))))
 
+(define-syntax (some/i syn)
+  (syntax-case syn ()
+   [(_ a)
+    (let ([a-ty (type-infer/syn #'a)])
+      #`(some #,a-ty a))]))
+
 (module+ test
   (require rackunit "bool.rkt")
+  (check-equal?
+   (some/i true)
+   (some Bool true))
   ;; Disabled until #22 fixed
   #;(check-equal?
     (case* Maybe Type (some Bool true) (Bool)
diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt
index 143c4a9..738949d 100644
--- a/stdlib/prop.rkt
+++ b/stdlib/prop.rkt
@@ -8,7 +8,7 @@
   False
   Not
   And
-  conj
+  conj conj/i
   thm:and-is-symmetric proof:and-is-symmetric
   thm:proj1 proof:proj1
   thm:proj2 proof:proj2
@@ -28,6 +28,13 @@
   (conj : (forall* (A : Type) (B : Type)
             (x : A) (y : B) (And A B))))
 
+(define-syntax (conj/i syn)
+  (syntax-case syn ()
+    [(_ a b)
+     (let ([a-type (type-infer/syn #'a)]
+           [b-type (type-infer/syn #'b)])
+       #`(conj #,a-type #,b-type a b))]))
+
 (define-theorem thm:and-is-symmetric
   (forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
 
@@ -36,7 +43,7 @@
     (case* And Type ab (P Q)
       (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)))))
+      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
 (qed thm:and-is-symmetric proof:and-is-symmetric)
 
@@ -94,4 +101,7 @@
          true
          true
          (refl Bool true))
-    z))
+    z)
+  (check-equal?
+   (conj/i (conj/i T T) T)
+   (conj (And True True) True (conj True True T T) T)))