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

1 files changed, 48 insertions, 59 deletions

diff --git a/examples/SUMO/Basic.gf b/examples/SUMO/Basic.gf
index 058e5a8b1..ebbc19193 100644
--- a/examples/SUMO/Basic.gf
+++ b/examples/SUMO/Basic.gf
@@ -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 ;

 

-};
\ No newline at end of file
+};