mathtext examples from Bonn

24 files changed, 413 insertions, 0 deletions

diff --git a/examples/mathtext/Geometry.gf b/examples/mathtext/Geometry.gf
new file mode 100644
index 000000000..c43654b9b
--- /dev/null
+++ b/examples/mathtext/Geometry.gf
@@ -0,0 +1,12 @@
+abstract Geometry = Logic ** {
+fun
+  Line, Point, Circle : Dom ;
+  Intersect, Parallel : Ind -> Ind -> Atom ;
+  Vertical : Ind -> Atom ;
+  Centre : Ind -> Ind ;
+
+  Horizontal : Pred1 ;
+  Diverge : Pred1 ;
+
+  Contain : Pred2 ;
+}
diff --git a/examples/mathtext/GeometryEng.gf b/examples/mathtext/GeometryEng.gf
new file mode 100644
index 000000000..bb8243527
--- /dev/null
+++ b/examples/mathtext/GeometryEng.gf
@@ -0,0 +1,18 @@
+--# -path=alltenses
+
+concrete GeometryEng of Geometry = LogicEng ** 
+  open SyntaxEng, ParadigmsEng in {
+lin
+  Line = mkN "line" ;
+  Point = mkN "point" ; 
+  Circle = mkN "circle" ;
+  Intersect = pred (mkV2 "intersect") ;
+  Parallel = pred (mkA2 (mkA "parallel") (mkPrep "to")) ;
+  Vertical = pred (mkA "vertical") ;
+  Centre = app (mkN2 (mkN "centre") (mkPrep "of")) ;
+
+  Horizontal = mkVP (mkA "horizontal") ;
+  Diverge = mkVP (mkV "diverge") ;
+
+  Contain = mkVPSlash (mkV2 "contain") ;
+}
diff --git a/examples/mathtext/GeometryFre.gf b/examples/mathtext/GeometryFre.gf
new file mode 100644
index 000000000..97502a650
--- /dev/null
+++ b/examples/mathtext/GeometryFre.gf
@@ -0,0 +1,18 @@
+--# -path=alltenses
+
+concrete GeometryFre of Geometry = LogicFre ** 
+  open SyntaxFre, ParadigmsFre, IrregFre in {
+lin
+  Line = mkN "ligne" ;
+  Point = mkN "point" ; 
+  Circle = mkN "cercle" masculine ;
+  Intersect = pred (mkV2 "couper") ;
+  Parallel = pred (mkA2 (mkA "parallèle") dative) ;
+  Vertical = pred (mkA "vertical") ;
+  Centre = app (mkN2 (mkN "centre" masculine) genitive) ;
+
+  Horizontal = mkVP (mkA "horizontel") ;
+  Diverge = mkVP (mkV "diverger") ;
+
+  Contain = mkVPSlash contenir_V2 ;
+}
diff --git a/examples/mathtext/GeometryGer.gf b/examples/mathtext/GeometryGer.gf
new file mode 100644
index 000000000..25c2cf965
--- /dev/null
+++ b/examples/mathtext/GeometryGer.gf
@@ -0,0 +1,19 @@
+--# -path=alltenses
+
+concrete GeometryGer of Geometry = LogicGer ** 
+  open SyntaxGer, ParadigmsGer, IrregGer in {
+lin
+  Line = mkN "Gerade" ;
+  Point = mkN "Punkt" ; 
+  Circle = mkN "Kreis" ;
+  Intersect = pred (mkV2 (mkV "schneiden")) ;
+  Parallel = pred (mkA2 (mkA "parallel") (mkPrep "zu" dative)) ;
+  Vertical = pred (mkA "vertikal") ;
+  Centre = app (mkN2 (mkN "Mittelpunkt") (mkPrep [] genitive)) ;
+
+  Horizontal = mkVP (mkA "horizontal") ;
+  Diverge = mkVP (mkV "divergieren") ;
+
+  Contain = mkVPSlash (mkV2 (fixprefixV "ent" halten_V)) ;
+
+}
diff --git a/examples/mathtext/LexLogic.gf b/examples/mathtext/LexLogic.gf
new file mode 100644
index 000000000..c80ff27bc
--- /dev/null
+++ b/examples/mathtext/LexLogic.gf
@@ -0,0 +1,20 @@
+interface LexLogic = open Syntax, Prelude in {
+
+oper
+  case_N : N ; -- it is not the case that
+  such_A : A ; -- number such that 
+  by_Prep : Prep ; -- by Thm 5
+  all_Det : Det ; -- the article with "all"
+  axiom_N : N ;
+  theorem_N : N ;
+  definition_N : N ;
+  define_V3 : V3 ;  -- we define a as b
+  define_V2V : V2V ;  -- we define x to be f if p
+  iff_Subj : Subj ; -- if and only if
+oper
+  indef : Bool -> CN -> NP = \b -> case b of {
+    True => mkNP aPl_Det ;
+    False => mkNP aSg_Det
+    } ;
+
+}
diff --git a/examples/mathtext/LexLogicEng.gf b/examples/mathtext/LexLogicEng.gf
new file mode 100644
index 000000000..efb8c4a8d
--- /dev/null
+++ b/examples/mathtext/LexLogicEng.gf
@@ -0,0 +1,15 @@
+instance LexLogicEng of LexLogic = open SyntaxEng, ParadigmsEng, 
+  (MS = MakeStructuralEng), Prelude in {
+
+oper
+  case_N = mkN "case" ;
+  such_A = mkA "such" ;
+  by_Prep = mkPrep "by" ;
+  all_Det = aPl_Det ;
+  axiom_N = mkN "axiom" ;
+  theorem_N = mkN "theorem" ;
+  definition_N = mkN "definition" ;
+  define_V3 = mkV3 (mkV "define") (mkPrep [] ) (mkPrep "as") ;
+  define_V2V = mkV2V (mkV "define") (mkPrep [] ) (mkPrep []) ;
+  iff_Subj = MS.mkSubj "if and only if" ;
+}
diff --git a/examples/mathtext/LexLogicFre.gf b/examples/mathtext/LexLogicFre.gf
new file mode 100644
index 000000000..94036039c
--- /dev/null
+++ b/examples/mathtext/LexLogicFre.gf
@@ -0,0 +1,16 @@
+instance LexLogicFre of LexLogic = open SyntaxFre, ParadigmsFre, 
+  (MS = MakeStructuralFre), Prelude in {
+
+oper
+  case_N = mkN "cas" ;
+  such_A = mkA "tel" "telle" ;
+  by_Prep = mkPrep "par" ;
+  all_Det = thePl_Det ;
+  axiom_N = mkN "axiome" masculine ;
+  theorem_N = mkN "théorème" masculine ;
+  definition_N = mkN "définition" feminine ;
+  define_V3 = mkV3 (mkV "définir") (mkPrep []) (mkPrep "comme") ;
+  define_V2V = mkV2V (mkV "définir") (mkPrep []) genitive ;
+  iff_Subj = MS.mkSubj ("si et seulement" ++ if_Subj.s) ; --- .s
+
+}
diff --git a/examples/mathtext/LexLogicGer.gf b/examples/mathtext/LexLogicGer.gf
new file mode 100644
index 000000000..a2d8e8431
--- /dev/null
+++ b/examples/mathtext/LexLogicGer.gf
@@ -0,0 +1,16 @@
+instance LexLogicGer of LexLogic = open SyntaxGer, ParadigmsGer, 
+  (MS = MakeStructuralGer), Prelude in {
+
+oper
+  case_N = mkN "Fall" "Fälle" masculine ;
+  such_A = invarA "derart" ; ----
+  by_Prep = mkPrep "durch" accusative ;
+  all_Det = aPl_Det ;
+  axiom_N = mkN "Axiom" ;
+  theorem_N = mkN "Theorem" ;
+  definition_N = mkN "Definition" ;
+  define_V3 = 
+    mkV3 (mkV "definieren") (mkPrep [] accusative) (mkPrep "als" accusative) ;
+  define_V2V = mkV2V (mkV "definieren") (mkPrep [] accusative) ;
+  iff_Subj = MS.mkSubj "wenn und nur wenn" ;
+}
diff --git a/examples/mathtext/Logic.gf b/examples/mathtext/Logic.gf
new file mode 100644
index 000000000..161660154
--- /dev/null
+++ b/examples/mathtext/Logic.gf
@@ -0,0 +1,24 @@
+abstract Logic = Symbols ** {
+
+-- flags startcat = Prop ;
+
+cat
+  Prop ; Atom ; Ind ; Dom ; Var ; [Prop] {2} ; [Var] {1} ;
+fun
+  And, Or : [Prop] -> Prop ;
+  If, Iff : Prop -> Prop -> Prop ;
+  Not : Prop -> Prop ;
+  All, Exist : [Var] -> Dom -> Prop -> Prop ;
+  PAtom : Atom -> Prop ;
+  NAtom : Atom -> Prop ;
+  MkVar : String -> Var ;
+
+  PExp : Exp -> Prop ;
+  IExp : Exp -> Ind ;
+
+cat
+  Pred1 ; Pred2 ;
+fun 
+  PredPred1 : Pred1 -> Ind -> Atom ; 
+  PredPred2 : Pred2 -> Ind -> Ind -> Atom ; 
+}
diff --git a/examples/mathtext/LogicEng.gf b/examples/mathtext/LogicEng.gf
new file mode 100644
index 000000000..f4a747e26
--- /dev/null
+++ b/examples/mathtext/LogicEng.gf
@@ -0,0 +1,5 @@
+concrete LogicEng of Logic = SymbolsX ** LogicI with
+  (LexLogic = LexLogicEng),
+  (Lang = LangEng),
+  (Syntax = SyntaxEng),
+  (Symbolic = SymbolicEng) ;
diff --git a/examples/mathtext/LogicFre.gf b/examples/mathtext/LogicFre.gf
new file mode 100644
index 000000000..325d48f1f
--- /dev/null
+++ b/examples/mathtext/LogicFre.gf
@@ -0,0 +1,15 @@
+concrete LogicFre of Logic = SymbolsX ** LogicI - [Exist] with
+  (LexLogic = LexLogicFre),
+  (Lang = LangFre),
+  (Syntax = SyntaxFre),
+  (Symbolic = SymbolicFre) ** open SyntaxFre in {
+
+lin
+  --- to get the mood of the that clause correct
+  Exist xs A B = 
+    Lang.SSubjS
+    (mkS (mkCl (indef xs.p2 
+      (mkCN such_A (mkCN A xs.p1)))))
+    that_Subj B ;
+
+} ;
diff --git a/examples/mathtext/LogicGer.gf b/examples/mathtext/LogicGer.gf
new file mode 100644
index 000000000..66e7c5001
--- /dev/null
+++ b/examples/mathtext/LogicGer.gf
@@ -0,0 +1,15 @@
+concrete LogicGer of Logic = SymbolsX ** LogicI - [Exist] with
+  (LexLogic = LexLogicGer),
+  (Lang = LangGer),
+  (Syntax = SyntaxGer),
+  (Symbolic = SymbolicGer) ** open SyntaxGer, (P = ParadigmsGer) in {
+
+lin
+  --- to get the extraposited clause in correct place
+  Exist xs A B = 
+    Lang.SSubjS
+    (mkS (mkCl (indef xs.p2 
+      (mkCN (mkCN A xs.p1) (P.mkAdv "derart")))))
+    that_Subj B ;
+
+} ;
diff --git a/examples/mathtext/LogicI.gf b/examples/mathtext/LogicI.gf
new file mode 100644
index 000000000..e84861550
--- /dev/null
+++ b/examples/mathtext/LogicI.gf
@@ -0,0 +1,48 @@
+incomplete concrete LogicI of Logic = SymbolsX ** open 
+  LexLogic, 
+  Syntax, 
+  Symbolic, 
+  (Lang = Lang), -- for SSubjS
+  Prelude in {
+lincat
+  Prop = S ; 
+  Atom = Cl ; 
+  Ind = NP ; 
+  Dom = N ; 
+  Var = NP ; 
+  [Prop] = [S] ; 
+  [Var] = NP * Bool ;
+lin
+  And = mkS and_Conj ;
+  Or = mkS or_Conj ;
+  If A B = mkS (mkAdv if_Subj A) B ;
+  Iff A B = Lang.SSubjS A iff_Subj B ;
+  Not A = 
+    Lang.SSubjS
+      (mkS negativePol (mkCl 
+        (mkVP (mkNP the_Quant case_N)))) that_Subj A ; 
+  All xs A B = mkS (mkAdv for_Prep (mkNP all_Predet 
+                 (mkNP all_Det (mkCN A xs.p1)))) B ;
+  Exist xs A B = mkS (mkCl (indef xs.p2 
+                   (mkCN (mkCN A xs.p1) (mkAP (mkAP such_A) B)))) ;
+  PAtom = mkS ;
+  NAtom = mkS negativePol ;
+  MkVar s = symb (dollar s.s) ;
+  BaseProp = mkListS ;
+  ConsProp = mkListS ;
+  BaseVar x = <x,False> ;
+  ConsVar x xs = <mkNP and_Conj (mkListNP x xs.p1), True> ;
+
+  PExp e = symb (mkSymb (dollar e.s)) ;
+  IExp e = symb (dollar e.s) ;
+
+lincat
+  Pred1 = VP ;
+  Pred2 = VPSlash ;
+lin
+  PredPred1 f x = mkCl x f ;
+  PredPred2 f x y = mkCl x (mkVP f y) ;
+
+oper 
+  dollar : Str -> Str = \s -> "$" ++ s ++ "$" ;
+}
diff --git a/examples/mathtext/MathGeom.gf b/examples/mathtext/MathGeom.gf
new file mode 100644
index 000000000..7eee1ae95
--- /dev/null
+++ b/examples/mathtext/MathGeom.gf
@@ -0,0 +1 @@
+abstract MathGeom = Geometry, MathText ;
diff --git a/examples/mathtext/MathGeomEng.gf b/examples/mathtext/MathGeomEng.gf
new file mode 100644
index 000000000..a04c56282
--- /dev/null
+++ b/examples/mathtext/MathGeomEng.gf
@@ -0,0 +1,4 @@
+--# -path=.:present
+
+concrete MathGeomEng of MathGeom = GeometryEng, MathTextEng ;
+
diff --git a/examples/mathtext/MathGeomFre.gf b/examples/mathtext/MathGeomFre.gf
new file mode 100644
index 000000000..d4e3ff23c
--- /dev/null
+++ b/examples/mathtext/MathGeomFre.gf
@@ -0,0 +1,4 @@
+--# -path=.:present
+
+concrete MathGeomFre of MathGeom = GeometryFre, MathTextFre ;
+
diff --git a/examples/mathtext/MathGeomGer.gf b/examples/mathtext/MathGeomGer.gf
new file mode 100644
index 000000000..f4147b419
--- /dev/null
+++ b/examples/mathtext/MathGeomGer.gf
@@ -0,0 +1,4 @@
+--# -path=.:present
+
+concrete MathGeomGer of MathGeom = GeometryGer, MathTextGer ;
+
diff --git a/examples/mathtext/MathText.gf b/examples/mathtext/MathText.gf
new file mode 100644
index 000000000..88357e67e
--- /dev/null
+++ b/examples/mathtext/MathText.gf
@@ -0,0 +1,45 @@
+abstract MathText = Logic ** {
+
+flags startcat = Book ;
+
+cat
+  Book ;
+  Section ;
+  [Section] {1} ;
+  Paragraph ;
+  [Paragraph] {1} ;
+  Statement ;
+  Declaration ;
+  [Declaration] {0} ;
+  Ident ;
+  Proof ;
+  Case ;
+  [Case] {2} ;
+  Number ;
+ 
+fun
+  MkBook : [Section] -> Book ;
+  
+  ParAxiom   : Ident -> Statement -> Section ;
+  ParTheorem : Ident -> Statement -> Proof -> Section ;
+
+  ParDefInd   : [Declaration] -> Ind -> Ind -> Section ;
+  ParDefPred1 : [Declaration] -> Ind -> Pred1 -> Prop -> Section ;
+  ParDefPred2 : [Declaration] -> Ind -> Pred2 -> Ind -> Prop -> Section ;
+
+  StProp : [Declaration] -> Prop -> Statement ;
+
+  DecVar  : [Var] -> Dom -> Declaration ;
+  DecProp : Prop -> Declaration ;
+
+  PrEnd  : Proof ;
+  PrStep : Statement -> Proof -> Proof ;
+  PrBy   : Ident -> Prop -> Proof -> Proof ;
+  PrCase : Number -> [Case] -> Proof ;
+  CProof : Ident -> Proof -> Case ;
+
+  IdStr  : String -> Ident ;
+
+  Two, Three, Four, Five : Number ;
+
+}
diff --git a/examples/mathtext/MathTextEng.gf b/examples/mathtext/MathTextEng.gf
new file mode 100644
index 000000000..4577fff24
--- /dev/null
+++ b/examples/mathtext/MathTextEng.gf
@@ -0,0 +1,5 @@
+concrete MathTextEng of MathText = LogicEng ** MathTextI with
+  (LexLogic = LexLogicEng),
+  (Syntax = SyntaxEng),
+  (Lang = LangEng), ---- ImpP3
+  (Symbolic = SymbolicEng) ;
diff --git a/examples/mathtext/MathTextFre.gf b/examples/mathtext/MathTextFre.gf
new file mode 100644
index 000000000..035ff00d5
--- /dev/null
+++ b/examples/mathtext/MathTextFre.gf
@@ -0,0 +1,5 @@
+concrete MathTextFre of MathText = LogicFre ** MathTextI with
+  (LexLogic = LexLogicFre),
+  (Syntax = SyntaxFre),
+  (Lang = LangFre), ---- ImpP3
+  (Symbolic = SymbolicFre) ;
diff --git a/examples/mathtext/MathTextGer.gf b/examples/mathtext/MathTextGer.gf
new file mode 100644
index 000000000..b608dde63
--- /dev/null
+++ b/examples/mathtext/MathTextGer.gf
@@ -0,0 +1,5 @@
+concrete MathTextGer of MathText = LogicGer ** MathTextI with
+  (LexLogic = LexLogicGer),
+  (Syntax = SyntaxGer),
+  (Lang = LangGer), ---- for ImpP3
+  (Symbolic = SymbolicGer) ;
diff --git a/examples/mathtext/MathTextI.gf b/examples/mathtext/MathTextI.gf
new file mode 100644
index 000000000..88c554245
--- /dev/null
+++ b/examples/mathtext/MathTextI.gf
@@ -0,0 +1,74 @@
+incomplete concrete MathTextI of MathText = Logic **
+  open 
+    Syntax,
+    (Lang = Lang), ---- for ImpP3, SSubjS 
+    Symbolic, 
+    LexLogic in {
+
+lincat
+  Book = Text ;
+  Section = Text ;
+  [Section] = Text ;
+  Paragraph = Text ;
+  [Paragraph] = Text ;
+  Statement = Text ;
+  Declaration = Utt ;
+  [Declaration] = Text ;
+  Ident = NP ;
+  Proof = Text ;
+  Case = Text ;
+  [Case] = Text ;
+  Number = Card ;
+ 
+lin
+  MkBook ss = ss ;
+  
+  ParAxiom   id stm = mkText (mkText (Lang.UttCN (mkCN axiom_N id))) stm ;
+  ParTheorem id stm pr = 
+    mkText (mkText (mkText (Lang.UttCN (mkCN theorem_N id))) stm) pr ;
+
+  ParDefInd  cont dum dens = 
+    definition (mkText cont (mkText (mkCl (mkNP we_Pron) define_V3 dum dens))) ;
+  ParDefPred1 cont arg dum dens = 
+    definition (mkText cont (mkText (Lang.SSubjS 
+      (mkS (mkCl (mkNP we_Pron) define_V2V arg dum)) 
+      if_Subj dens))) ;
+  ParDefPred2 cont arg dum obj dens = 
+    definition (mkText cont (mkText (Lang.SSubjS 
+      (mkS (mkCl (mkNP we_Pron) define_V2V arg (mkVP dum obj))) 
+      if_Subj dens))) ;
+
+  BaseSection s = s ;
+  ConsSection s ss = mkText s ss ;
+  BaseParagraph s = s ;
+  ConsParagraph s ss = mkText s ss ;
+  BaseCase s t = mkText s t ;
+  ConsCase s ss = mkText s ss ;
+  BaseDeclaration = emptyText ;
+  ConsDeclaration s ss = mkText (mkPhr s) ss ;
+
+
+  StProp ds prop = mkText ds (mkText prop) ;
+
+  DecVar xs dom = 
+    Lang.ImpP3 xs.p1 (mkVP (indef xs.p2 (mkCN dom))) ; 
+ --   mkUtt (mkImp (mkVP let_V2V xs.p1 (mkVP (indef xs.p2 (mkCN dom))))) ; 
+  DecProp prop = mkUtt prop ;
+
+  PrEnd  = emptyText ;
+  PrStep st pr = mkText st pr ;
+  PrBy id prop proof = mkText (mkText (mkS (mkAdv by_Prep id) prop)) proof ;
+  PrCase num cs = 
+    mkText (mkPhr (mkCl (mkNP we_Pron) have_V2 (mkNP num case_N))) cs ;
+  CProof id proof = mkText (mkPhr (mkUtt (mkNP (mkCN case_N id)))) proof ;
+
+  IdStr s = symb s.s ;
+
+  Two = mkCard n2_Numeral ;
+  Three = mkCard n3_Numeral ;
+  Four = mkCard n4_Numeral ;
+  Five = mkCard n5_Numeral ;
+
+oper
+  definition : Text -> Text = mkText (mkText (Lang.UttCN (mkCN definition_N))) ;
+}
diff --git a/examples/mathtext/Symbols.gf b/examples/mathtext/Symbols.gf
new file mode 100644
index 000000000..b56718a01
--- /dev/null
+++ b/examples/mathtext/Symbols.gf
@@ -0,0 +1,10 @@
+abstract Symbols = {
+
+cat 
+  Exp ; 
+
+fun 
+--  EInt : Int -> Expp ; --- clashes with EVar...
+  EVar : String -> Exp ;
+  EIn, EPlus, ETimes, EEq, EGt, ELt : Exp -> Exp -> Exp ;
+}
diff --git a/examples/mathtext/SymbolsX.gf b/examples/mathtext/SymbolsX.gf
new file mode 100644
index 000000000..be362f5e9
--- /dev/null
+++ b/examples/mathtext/SymbolsX.gf
@@ -0,0 +1,15 @@
+concrete SymbolsX of Symbols = open Formal in {
+
+lincat 
+  Exp = TermPrec ; 
+
+lin 
+--  EInt i = constant i.s ;
+  EVar x = constant x.s ;
+  EIn = infixn 0 "\\in" ;
+  EPlus = infixl 2 "+" ;
+  ETimes = infixl 3 "*" ;
+  EEq = infixn 0 "=" ;
+  EGt = infixn 0 ">" ;
+  ELt = infixn 0 "<" ;
+}