msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

SUMO: remove the uggly SubClassC and use KappaFn instead

Browse Source
This commit is contained in:
krasimir
2010-06-06 11:44:51 +00:00
parent 8c9b63236f
commit db3eb23d5f
5 changed files with 131 additions and 134 deletions
Download Patch File Download Diff File Expand all files Collapse all files

70
examples/SUMO/Basic.gf
View File

@@ -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
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 ;
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) -> 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;
-- 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 ;