SUMO: remove the uggly SubClassC and use KappaFn instead

1 files changed, 32 insertions, 26 deletions

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 ;