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 +}; diff --git a/examples/SUMO/BasicEng.gf b/examples/SUMO/BasicEng.gf index 41f483e8c..8f25d2012 100644 --- a/examples/SUMO/BasicEng.gf +++ b/examples/SUMO/BasicEng.gf @@ -1,96 +1,99 @@ --# -path=.:englishExtended:abstract:common: -concrete BasicEng of Basic = CatEng - [Text] ** open DictLangEng, ParadigmsEng, ResEng, Coordination, Prelude, ParamBasic, NounEng in{ +concrete BasicEng of Basic = CatEng - [Text] ** open DictLangEng, ParadigmsEng, ResEng, Coordination, Prelude, ParamBasic, NounEng in { + lincat - Class = CN ; - El = NP ; - Ind = NP ; - Var = PN ; - SubClass = {} ; - SubClassC = {} ; - Inherits = {} ; - Desc = CN ; - Formula = PolSentence; - [El] = [NP]; - [Class] = [CN]; - Stmt = StmtS ; - lin -BaseClass = {s1,s2 = \\_,_ => ""; - g = Neutr; - lock_ListCN=<>}; -ConsClass xs x = ConsCN xs x ; + Class = CN ; + El = NP ; + Ind = NP ; + Var = PN ; + SubClass = {} ; + SubClassC = {} ; + Inherits = {} ; + Desc = CN ; + Formula = PolSentence; + [El] = [NP]; + [Class] = [CN]; + Stmt = StmtS ; + +lin + BaseClass = {s1,s2 = \\_,_ => ""; + g = Neutr; + lock_ListCN=<>}; + ConsClass xs x = ConsCN xs x ; - -BaseEl c = {s1,s2 = \\_ => ""; - a = agrP3 Sg; - lock_ListNP=<>}; + BaseEl c = {s1,s2 = \\_ => ""; + a = agrP3 Sg; + lock_ListNP=<>}; -ConsEl c xs x = ConsNP xs x ; + ConsEl c xs x = ConsNP xs x ; - -and f1 f2 = {s = \\f,c => f1.s ! Indep ! c ++ "and" ++ f2.s ! Indep ! c; flag = NothingS; lock_PolSentence = <>}; -or f1 f2 = {s = \\f,c => f1.s ! Indep ! c ++ "or" ++ f2.s ! Indep ! c; flag = NothingS; lock_PolSentence = <>}; -not f1 = {s = \\f,c => case c of - {Neg => f1.s ! f ! Pos ; - Pos => f1.s ! Indep ! Neg }; - flag = f1.flag; - lock_PolSentence = <>}; -impl f1 f2 = {s = \\f,c => "if" ++ f1.s ! Indep ! c ++ "then" ++ f2.s ! Indep ! c; flag = NothingS; lock_PolSentence = <>}; + and f1 f2 = {s = \\f,c => f1.s ! Indep ! c ++ "and" ++ f2.s ! Indep ! c; flag = NothingS; lock_PolSentence = <>}; + or f1 f2 = {s = \\f,c => f1.s ! Indep ! c ++ "or" ++ f2.s ! Indep ! c; flag = NothingS; lock_PolSentence = <>}; + not f1 = {s = \\f,c => case c of { + Neg => f1.s ! f ! Pos ; + Pos => f1.s ! Indep ! Neg + }; + flag = f1.flag; + lock_PolSentence = <> + }; + impl f1 f2 = {s = \\f,c => "if" ++ f1.s ! Indep ! c ++ "then" ++ f2.s ! Indep ! c; flag = NothingS; lock_PolSentence = <>}; -equiv f1 f2 = {s = \\f,c => f1.s ! Indep ! c ++ "is" ++ "equivalent" ++ "to" ++ f2.s ! Indep ! c; flag = NothingS; - lock_PolSentence = <>}; + equiv f1 f2 = {s = \\f,c => f1.s ! Indep ! c ++ "is" ++ "equivalent" ++ "to" ++ f2.s ! Indep ! c; flag = NothingS; + lock_PolSentence = <>}; -el c1 c2 i e = e; -var c1 c2 i e = UsePN e; + el c1 c2 i e = e; + var c1 c2 i e = UsePN e; -exists C f = let np = DetCN (DetQuant IndefArt NumSg) C - in - {s = \\form,c => case