diff --git a/examples/SUMO/Basic.gf b/examples/SUMO/Basic.gf new file mode 100644 index 000000000..058e5a8b1 --- /dev/null +++ b/examples/SUMO/Basic.gf @@ -0,0 +1,103 @@ +--# -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 ; + +-- 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 ; + + +-- 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; + + +-- quantification over instances of a Class +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 desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c2 ; + +fun descClass : (c : Class) -> Desc c -> Class ; +def descClass _ (desc c _ _) = c ; + +fun descInh : (c : Class) -> (p : Desc c) -> Inherits (descClass c p) c ; +--def descInh c1 (desc c2 c1 i) = i ; + +fun desc2desc : (c1,c2 : Class) -> Inherits c1 c2 -> Desc c1 -> Desc c2 ; +--def desc2desc _ _ inh dsc = desc ? ? (plusInh ? ? ? inh (descInh ? dsc)) ; + +--fun plusInh : (c1,c2,c3 : Class) -> Inherits c1 c2 -> Inherits c2 c3 -> Inherits c1 c3 ; +--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 ; + + + +}; \ No newline at end of file diff --git a/examples/SUMO/BasicEng.gf b/examples/SUMO/BasicEng.gf new file mode 100644 index 000000000..1521857c0 --- /dev/null +++ b/examples/SUMO/BasicEng.gf @@ -0,0 +1,96 @@ +--# -path=.:englishExtended:abstract:common: +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 = SS ; + lin +BaseClass = {s1,s2 = \\_,_ => ""; + g = Neutr; + lock_ListCN=<>}; +ConsClass xs x = ConsCN xs x ; + + +BaseEl c = {s1,s2 = \\_ => ""; + a = agrP3 Sg; + lock_ListNP=<>}; + +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 = <>}; + +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; + +exists C f = let np = DetCN (DetQuant IndefArt NumSg) C + in + {s = \\form,c => case