Rewrite test file with new features

test.sigma

 
-type A ::= [ a : [] ].
+print "\nExamples from Abadi and Cardelli.\n".
 
-type Bool ::= [ if : A ; then : A ; else : A ].
+type A ::= [ a : [] ].
+type B ::= [ b : [] ].
 
-type Arrow ::= [ arg : A ; val : A ].
+print "\nChecking if true then t else e = t.\n".
+check (λ(t : A) λ(e : A) if true(A) then t else e) = (λ(t : A) λ(e : A) t) : A -> A -> A.
 
-let true : Bool ::= [ if = ς(x : Bool) x.then ;
-                      then = ς(x : Bool) x.then ;
-                      else = ς(x : Bool) x.else ].
+print "\nChecking if false then t else e = e.\n".
+check (λ(t : A) λ(e : A) if false(A) then t else e) = (λ(t : A) λ(e : A) e) : A -> A -> A.
 
-let false : Bool ::= [ if = ς(x : Bool) x.else ;
-                       then = ς(x : Bool) x.then ;
-                       else = ς(x : Bool) x.else ].
-let if : Bool -> A -> A -> A ::=
-       λ(b : Bool) λ(t : A) λ(e : A) ((b.then := t).else := e).if.
+print "\nChecking β-reduction.\n".
+check (λ(a : A) λ(f : A -> B) ((λ(x : A) f x) a))
+    = (λ(a : A) λ(f : A -> B) f a) : A -> (A -> B) -> B.
 
-type Nat ::= [ iszero : Bool ;
+type Nat ::= [ iszero : Bool(A);
                pred : A ].
 
-let 0 : Nat ::= [ iszero = ς(x : Nat) true ;
+let 0 : Nat ::= [ iszero = ς(x : Nat) true(A) ;
                   pred = ς(x : Nat) x.pred ].
 
-let 42 : Nat ::= [ iszero = ς(x : Nat) false ;
-                  pred = ς(x : Nat) x.pred ].
+let 42 : Nat ::= [ iszero = ς(x : Nat) false(A) ;
+                   pred = ς(x : Nat) x.pred ].
+
+type Point ::= [ x : Nat ;
+                 y : Nat ].
+
+type Color ::= [ red : Bool(A); green : Bool(A); blue : Bool(A) ].
+
+let rgb_color : Bool(A) -> Bool(A) -> Bool(A) -> Color ::=
+  λ(r : Bool(A)) λ(g : Bool(A)) λ(b : Bool(A)) [ red = ς(self : Color) r;
+                                                 green = ς(self : Color) g;
+                                                 blue = ς(self : Color) b ].
+
+let red : Color ::= rgb_color (true(A)) (false(A)) (false(A)).
+
+type ColorPoint ::= [ x : Nat ;
+                      y : Nat ;
+                      c : Color ].
+
+let point_of_colorpoint : ColorPoint -> Point ::= λ(p : ColorPoint) p.
+
+print "\nChecking reduction with coercions: (coerce ColorPoint Point [x = 42; y = 0; c = red]).x = 42.\n".
+check (point_of_colorpoint [ x = ς(s : ColorPoint) 42;
+                             y = ς(s : ColorPoint) 0;
+                             c = ς(s : ColorPoint) red ]).x = 42 : Nat.
 
 type RomCell ::= [ get : Nat ].
+
+print "\nChecking reduction of select.\n".
+check [ get = ς(self : RomCell) 42 ].get = 42 : Nat.
+
 type PromCell ::= [ get : Nat ; set : Nat -> RomCell ].
 
-let myCell : PromCell ::= [ get = ς( self : PromCell ) 0 ;
-                            set = ς( self : PromCell ) λ(n : Nat) self.get := n ].
+let myPromCell : PromCell ::= [ get = ς( self : PromCell ) 0 ;
+                                set = ς( self : PromCell ) λ(n : Nat) self.get := n ].
+
+print "\nSubtyping: Checking (myPromCell.set 42).get = 42 : Nat.\n".
+check (myPromCell.set 42).get = 42 : Nat.
+
+print "\nChecking myPromCell.get = 0 : Nat.\n".
+check myPromCell.get = 0 : Nat.
+
+type PrivateCell ::= [ get : Nat ;
+                       set : Nat -> RomCell ;
+                       contents : Nat ].
 
+let myCell : PromCell ::= [ get = ς(self : PrivateCell) self.contents;
+                            set = ς(self : PrivateCell) λ(n : Nat) self.contents := n;
+                            contents = ς(self : PrivateCell) 0 ].
+
+norm myCell.
+
+print "\nSubtyping: Checking (myCell.set 42).get = 42 : Nat.\n".
 check (myCell.set 42).get = 42 : Nat.
+
+print "\nChecking myCell.get = 0 : Nat.\n".
+check myCell.get = 0 : Nat.
+
+print "\nEnd of examples.\n".