From 48760756c64bcc5a3290cb381c98ef477f5e639f Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Thu, 27 Nov 2008 00:45:45 +0000
Subject: [PATCH] svn: r12604

---
 collects/redex/examples/contracts.ss | 154 +++++++++++++++++++++++++++
 1 file changed, 154 insertions(+)
 create mode 100644 collects/redex/examples/contracts.ss

diff --git a/collects/redex/examples/contracts.ss b/collects/redex/examples/contracts.ss
new file mode 100644
index 0000000000..70b9a34d6b
--- /dev/null
+++ b/collects/redex/examples/contracts.ss
@@ -0,0 +1,154 @@
+#lang scheme
+
+#|
+
+A core contract calculus, including blame, 
+with function contracts, (eager) pair contracts, 
+and a few numeric predicates
+
+|#
+
+(require redex redex/examples/subst)
+
+(reduction-steps-cutoff 10)
+
+(define-language lang
+  (e (e e ...)
+     x
+     number
+     (λ (x ...) e)
+     
+     (if e e e)
+     #t #f
+     
+     cons car cdr
+     
+     -> or/c
+     ac
+     pred?
+     (blame l)
+     l)
+  (pred? number?
+         odd?
+         positive?)
+  (E (v ... E e ...)
+     (if E e e)
+     hole)
+  (v number
+     (λ (x ...) e)
+     cons car cdr
+     (cons v v)
+     pred?
+     -> or/c ac
+     (-> v ...)
+     (or/c v ...)
+     #t #f
+     l)
+
+  (l + -) ;; blame labels
+  
+  (x variable-not-otherwise-mentioned))
+
+(define reds
+  (reduction-relation
+   lang
+   (--> (in-hole E ((λ (x ...) e) v ...))
+        (in-hole E (subst-n ((x v) ... e)))
+        (side-condition (= (length (term (x ...)))
+                           (length (term (v ...)))))
+        βv)
+   
+   (--> (in-hole E (if #t e_1 e_2)) (in-hole E e_1) ift)
+   (--> (in-hole E (if #f e_1 e_2)) (in-hole E e_2) iff)
+   
+   (--> (in-hole E (number? number)) (in-hole E #t))
+   (--> (in-hole E (number? v))
+        (in-hole E #f)
+        (side-condition (not (number? (term v)))))
+
+   (--> (in-hole E (car (cons v_1 v_2))) 
+        (in-hole E v_1))
+   (--> (in-hole E (cdr (cons v_1 v_2))) 
+        (in-hole E v_2))
+   
+   (--> (in-hole E (odd? number))
+        (in-hole E #t)
+        (side-condition (odd? (term number))))
+   (--> (in-hole E (odd? v))
+        (in-hole E #f)
+        (side-condition (or (not (number? (term v)))
+                            (not (odd? (term v))))))
+   
+   (--> (in-hole E (positive? number))
+        (in-hole E #t)
+        (side-condition (positive? (term number))))
+   (--> (in-hole E (positive? v))
+        (in-hole E #f)
+        (side-condition (or (not (number? (term v)))
+                            (not (positive? (term v))))))
+
+   
+   (--> (in-hole E (blame l)) 
+        (blame l)
+        (side-condition (not (equal? (term E) (term hole)))))
+   
+   (--> (in-hole E (ac pred? v l))
+        (in-hole E (if (pred? v) v (blame l))))
+   (--> (in-hole E (ac (-> v_dom ... v_rng) (λ (x ...) e) l))
+        (in-hole E (λ (x ...) (ac v_rng ((λ (x ...) e) (ac v_dom x l_2) ...) l)))
+        (where l_2 (¬ l)))
+   
+   (--> (in-hole E (ac (cons v_1 v_2) (cons v_3 v_4) l))
+        (in-hole E (cons (ac v_1 v_3 l) (ac v_2 v_4 l))))
+   
+   (--> (in-hole E (ac (or/c pred? v_1 v_2 ...) v_3 l))
+        (in-hole E (if (pred? v_3) 
+                       v_3
+                       (ac (or/c v_1 v_2 ...) v_3 l))))
+   (--> (in-hole E (ac (or/c v_1) v_2 l))
+        (in-hole E (ac v_1 v_2 l)))
+   ))
+
+(define-metafunction lang
+  [(¬ +) -]
+  [(¬ -) +])
+
+(test--> reds (term ((λ (x y) x) 1 2)) 1)
+(test--> reds (term ((λ (x y) y) 1 2)) 2)
+(test--> reds (term (if (if #t #f #t) #f #t)) (term #t))
+(test--> reds (term (positive? 1)) #t)
+(test--> reds (term (positive? -1)) #f)
+(test--> reds (term (positive? (λ (x) x))) #f)
+(test--> reds (term (odd? 1)) #t)
+(test--> reds (term (odd? 2)) #f)
+(test--> reds (term (odd? (λ (x) x))) #f)
+(test--> reds (term (car (cdr (cdr (cons 1 (cons 2 (cons 3 #f))))))) 3)
+
+(test--> reds (term ((λ (x) x) (blame -))) (term (blame -)))
+(test--> reds (term (ac number? 1 +)) 1)
+(test--> reds (term (ac number? (λ (x) x) +)) (term (blame +)))
+(test--> reds (term ((ac (-> number? number?) (λ (x) x) +) 1)) 1)
+(test--> reds 
+         (term ((ac (-> number? number?) (λ (x) x) +) #f)) 
+         (term (blame -)))
+(test--> reds 
+         (term ((ac (-> number? number?) (λ (x) #f) +) 1))
+         (term (blame +)))
+(test--> reds
+         (term (ac (or/c odd? positive?) 1 +))
+         1)
+(test--> reds
+         (term (ac (or/c odd? positive?) -1 +))
+         -1)
+(test--> reds
+         (term (ac (or/c odd? positive?) 2 +))
+         2)
+(test--> reds
+         (term (ac (or/c odd? positive?) -2 +))
+         (term (blame +)))
+
+(test--> reds
+         (term (ac (cons odd? positive?) (cons 3 1) +))
+         (term (cons 3 1)))
+
+(test-results)
\ No newline at end of file