From 455d9558417a759fae3ccbe5cde5c9f5064a08d2 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Sun, 6 Jun 2010 11:06:44 +0000
Subject: changes in SUMO: formatting and fixes for lots of lots of small
 problems

---
 examples/SUMO/Basic.gf | 107 ++++++++++++++++++++++---------------------------
 1 file changed, 48 insertions(+), 59 deletions(-)

(limited to 'examples/SUMO/Basic.gf')

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
+};
-- 
cgit v1.2.3