diff options
| author | krasimir <krasimir@chalmers.se> | 2010-02-17 11:07:24 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-02-17 11:07:24 +0000 |
| commit | f7f0112256b738a7c640c37d5bcbfc8a33bdb307 (patch) | |
| tree | e75a57edda742cbda74326331655cdf31e943649 /examples/SUMO/Basic.gf | |
| parent | a4d41ef3e32af4f5e2fb2f5e97ff7024aa4dd068 (diff) | |
added examples/SUMO
Diffstat (limited to 'examples/SUMO/Basic.gf')
| -rw-r--r-- | examples/SUMO/Basic.gf | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/examples/SUMO/Basic.gf b/examples/SUMO/Basic.gf new file mode 100644 index 000000000..058e5a8b1 --- /dev/null +++ b/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 ;
+
+
+
+};
\ No newline at end of file |