added examples/SUMO

examples/SUMO/Basic.gf

@@ -0,0 +1,103 @@
+--# -path=.:englishExtended:common:prelude:abstract
+abstract Basic = open Conjunction in {
+cat Class;
+   El Class;
+   Ind Class;
+   SubClassC (c1,c2 : Class) (Var c2 -> Formula);
+   SubClass (c1,c2 : Class);
+   Inherits Class Class ;
+   [El Class];
+   [Class];
+   Formula;
+   Desc Class;
+   Var Class;
+   Stmt ;
+   
+-- inheritance between classes   
+data 
+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;
+
+
+-- 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 
+not : Formula -> Formula;
+and : Formula -> Formula -> Formula;
+or : Formula -> Formula -> Formula;
+impl : Formula -> Formula -> Formula;
+equiv : Formula -> Formula -> Formula;
+
+
+-- quantification over instances of a Class
+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 desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c2 ;
+
+fun descClass : (c : Class) -> Desc c -> Class ;
+def descClass _ (desc c _ _) = c ;
+
+fun descInh : (c : Class) -> (p : Desc c) -> Inherits (descClass c p) c ;
+--def descInh c1 (desc c2 c1 i) = i ;
+
+fun desc2desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c1 -> Desc c2 ;
+--def desc2desc _ _ inh dsc = desc ? ? (plusInh ? ? ? inh (descInh ? dsc)) ;
+
+--fun plusInh : (c1,c2,c3 : Class) -> Inherits c1 c2 -> Inherits c2 c3 -> Inherits c1 c3 ;
+--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 ;
+
+
+
+};