From 54f40a135f2dff103a531fe0e71d4c55f17d6a3e Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Sun, 6 Jun 2010 11:44:51 +0000
Subject: SUMO: remove the uggly SubClassC and use KappaFn instead

---
 examples/SUMO/Basic.gf | 58 ++++++++++++++++++++++++++++----------------------
 1 file changed, 32 insertions(+), 26 deletions(-)

(limited to 'examples/SUMO/Basic.gf')

diff --git a/examples/SUMO/Basic.gf b/examples/SUMO/Basic.gf
index ebbc19193..f5962d43e 100644
--- a/examples/SUMO/Basic.gf
+++ b/examples/SUMO/Basic.gf
@@ -5,7 +5,6 @@ cat
   Class;
   El Class;
   Ind Class;
-  SubClassC (c1,c2 : Class) (Var c2 -> Formula);
   SubClass (c1,c2 : Class);
   Inherits Class Class ;
   [El Class];
@@ -15,24 +14,48 @@ cat
   Var Class;
   Stmt ;
 
--- inheritance between classes   
+
+-- class-forming operations
 data 
+  both : Class -> Class -> Class ;
+  either : Class -> Class -> Class ;
+  
+  KappaFn : (c : Class) -> (Var c -> Formula) -> Class ;
+
+
+-- inheritance between classes   
+data
+  -- simple sub-class relations
   inhz : (c : Class) -> Inherits c c;
-  inhs : (c1, c2, c3 : Class) -> (p : Var c2 -> Formula) -> SubClassC c1 c2 p -> Inherits c2 c3 -> Inherits c1 c3;
-  inhsC : (c1, c2, c3 : Class) -> SubClass c1 c2 -> Inherits c2 c3 -> Inherits c1 c3;
+  inhs : (c1, c2, c3 : Class) -> SubClass c1 c2 -> Inherits c2 c3 -> Inherits c1 c3;
+
+  -- (both c1 c2) is subclass of c1 and of c2
+  bothL : (c1, c2 : Class) -> Inherits (both c1 c2) c1 ;
+  bothR : (c1, c2 : Class) -> Inherits (both c1 c2) c2 ; 
+
+  -- relationship with other subclasses
+  bothC : (c1, c2, c3 : Class) -> Inherits c3 c1 -> Inherits c3 c2 -> Inherits c3 (both c1 c2);
+
+  -- (either c1 c2) is superclass of c1 and of c2
+  eitherL : (c1, c2 : Class) -> Inherits c1 (either c1 c2);
+  eitherR : (c1, c2 : Class) -> Inherits c2 (either c1 c2);
+
+  -- relationship with other subclasses
+  eitherC : (c1,c2,c3 : Class) -> Inherits c1 c3 -> Inherits c2 c3 -> Inherits (either c1 c2) c3 ; 
+
+  -- sub-class axiom for KappaFn
+  kappa : (c : Class) -> (p : Var c -> Formula) -> Inherits (KappaFn c p) c ;
+
 
 -- coercion from Var to El
 data 
   var : (c1 , c2 : Class) -> Inherits c1 c2 -> Var c1 -> El c2 ;
 
+
 -- coercion from Ind to El 
 data 
   el : (c1, c2 : Class) -> Inherits c1 c2 -> Ind c1 -> El c2;
 
--- class-forming operations
-data 
-  both : Class -> Class -> Class ;
-  either : Class -> Class -> Class ;
 
 -- first-order logic operations for Formula
 data 
@@ -47,23 +70,6 @@ data
   exists : (c : Class) -> (Var c -> Formula) -> Formula;
   forall : (c : Class) -> (Var c -> Formula) -> Formula;
 
--- axioms for both
-data 
-  -- (both c1 c2) is subclass of c1 and of c2
-  bothL : (c1, c2 : Class) -> Inherits (both c1 c2) c1 ;
-  bothR : (c1, c2 : Class) -> Inherits (both c1 c2) c2 ; 
-
-  -- relationship with other subclasses
-  bothC : (c1, c2, c3 : Class) -> Inherits c3 c1 -> Inherits c3 c2 -> Inherits c3 (both c1 c2);
-
- -- axioms for either 
-data 
-  -- (either c1 c2) is superclass of c1 and of c2
-  eitherL : (c1, c2 : Class) -> Inherits c1 (either c1 c2);
-  eitherR : (c1, c2 : Class) -> Inherits c2 (either c1 c2);
-
-  -- relationship with other subclasses
-  eitherC : (c1,c2,c3 : Class) -> Inherits c1 c3 -> Inherits c2 c3 -> Inherits (either c1 c2) c3 ; 
 
 -- Desc category
 data
@@ -82,10 +88,10 @@ fun desc2desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c1 -> Desc c2 ;
 --def plusInh _ _ _ inhz                 inh2 = inh2 ;
 --    plusInh _ _ _ (inhs _ _ _ sc inh1) inh2 = inhs ? ? ? sc (plusInh ? ? ? inh1 inh2) ;
 
+
 -- statements 
 data 
   subClassStm : (c1,c2 : Class) -> SubClass c1 c2 -> Stmt ;
-  subClassCStm : (c1,c2 : Class) -> (p : Var c2 -> Formula) -> SubClassC c1 c2 p -> Stmt ;
   instStm : (c : Class) -> Ind c -> Stmt ;
   formStm : Formula -> Stmt ;
 
-- 
cgit v1.2.3