GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-22 19:22:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

changes in SUMO: formatting and fixes for lots of lots of small problems

Browse Source
This commit is contained in:
krasimir
2010-06-06 11:06:44 +00:00
parent ae79d4e4b2
commit 455d955841
41 changed files with 56990 additions and 61448 deletions
Download Patch File Download Diff File Expand all files Collapse all files

107
examples/SUMO/Basic.gf
View File

@@ -1,79 +1,73 @@
--# -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 ;
abstract Basic = {
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;
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 ;
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;
el : (c1, c2 : Class) -> Inherits c1 c2 -> Ind c1 -> El c2;
-- class-forming operations
data
both : Class -> Class -> Class ;
either : Class -> Class -> Class ;
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;
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;
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 ;
-- (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);
-- relationship with other subclasses
bothC : (c1, c2, c3 : Class) -> Inherits c3 c1 -> Inherits c3 c2 -> Inherits c3 (both c1 c2);
-- axioms for either
-- 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);
-- (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 ;
-- 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 ;
data
desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c2 ;
fun descClass : (c : Class) -> Desc c -> Class ;
def descClass _ (desc c _ _) = c ;
@@ -88,16 +82,11 @@ 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 ;
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 ;
};
};