diff options
Diffstat (limited to 'examples/mathtext')
24 files changed, 0 insertions, 413 deletions
diff --git a/examples/mathtext/Geometry.gf b/examples/mathtext/Geometry.gf deleted file mode 100644 index c43654b9b..000000000 --- a/examples/mathtext/Geometry.gf +++ /dev/null @@ -1,12 +0,0 @@ -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 deleted file mode 100644 index bb8243527..000000000 --- a/examples/mathtext/GeometryEng.gf +++ /dev/null @@ -1,18 +0,0 @@ ---# -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 deleted file mode 100644 index 97502a650..000000000 --- a/examples/mathtext/GeometryFre.gf +++ /dev/null @@ -1,18 +0,0 @@ ---# -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 deleted file mode 100644 index 25c2cf965..000000000 --- a/examples/mathtext/GeometryGer.gf +++ /dev/null @@ -1,19 +0,0 @@ ---# -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 deleted file mode 100644 index c80ff27bc..000000000 --- a/examples/mathtext/LexLogic.gf +++ /dev/null @@ -1,20 +0,0 @@ -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 deleted file mode 100644 index efb8c4a8d..000000000 --- a/examples/mathtext/LexLogicEng.gf +++ /dev/null @@ -1,15 +0,0 @@ -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 deleted file mode 100644 index 94036039c..000000000 --- a/examples/mathtext/LexLogicFre.gf +++ /dev/null @@ -1,16 +0,0 @@ -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 deleted file mode 100644 index a2d8e8431..000000000 --- a/examples/mathtext/LexLogicGer.gf +++ /dev/null @@ -1,16 +0,0 @@ -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 deleted file mode 100644 index 161660154..000000000 --- a/examples/mathtext/Logic.gf +++ /dev/null @@ -1,24 +0,0 @@ -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 deleted file mode 100644 index f4a747e26..000000000 --- a/examples/mathtext/LogicEng.gf +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 325d48f1f..000000000 --- a/examples/mathtext/LogicFre.gf +++ /dev/null @@ -1,15 +0,0 @@ -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 deleted file mode 100644 index 66e7c5001..000000000 --- a/examples/mathtext/LogicGer.gf +++ /dev/null @@ -1,15 +0,0 @@ -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 deleted file mode 100644 index e84861550..000000000 --- a/examples/mathtext/LogicI.gf +++ /dev/null @@ -1,48 +0,0 @@ -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 deleted file mode 100644 index 7eee1ae95..000000000 --- a/examples/mathtext/MathGeom.gf +++ /dev/null @@ -1 +0,0 @@ -abstract MathGeom = Geometry, MathText ; diff --git a/examples/mathtext/MathGeomEng.gf b/examples/mathtext/MathGeomEng.gf deleted file mode 100644 index a04c56282..000000000 --- a/examples/mathtext/MathGeomEng.gf +++ /dev/null @@ -1,4 +0,0 @@ ---# -path=.:present - -concrete MathGeomEng of MathGeom = GeometryEng, MathTextEng ; - diff --git a/examples/mathtext/MathGeomFre.gf b/examples/mathtext/MathGeomFre.gf deleted file mode 100644 index d4e3ff23c..000000000 --- a/examples/mathtext/MathGeomFre.gf +++ /dev/null @@ -1,4 +0,0 @@ ---# -path=.:present - -concrete MathGeomFre of MathGeom = GeometryFre, MathTextFre ; - diff --git a/examples/mathtext/MathGeomGer.gf b/examples/mathtext/MathGeomGer.gf deleted file mode 100644 index f4147b419..000000000 --- a/examples/mathtext/MathGeomGer.gf +++ /dev/null @@ -1,4 +0,0 @@ ---# -path=.:present - -concrete MathGeomGer of MathGeom = GeometryGer, MathTextGer ; - diff --git a/examples/mathtext/MathText.gf b/examples/mathtext/MathText.gf deleted file mode 100644 index 88357e67e..000000000 --- a/examples/mathtext/MathText.gf +++ /dev/null @@ -1,45 +0,0 @@ -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 deleted file mode 100644 index 4577fff24..000000000 --- a/examples/mathtext/MathTextEng.gf +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 035ff00d5..000000000 --- a/examples/mathtext/MathTextFre.gf +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index b608dde63..000000000 --- a/examples/mathtext/MathTextGer.gf +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index 88c554245..000000000 --- a/examples/mathtext/MathTextI.gf +++ /dev/null @@ -1,74 +0,0 @@ -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 deleted file mode 100644 index b56718a01..000000000 --- a/examples/mathtext/Symbols.gf +++ /dev/null @@ -1,10 +0,0 @@ -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 deleted file mode 100644 index be362f5e9..000000000 --- a/examples/mathtext/SymbolsX.gf +++ /dev/null @@ -1,15 +0,0 @@ -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 "<" ; -} |