diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/logic/LexTheory.gf | 8 | ||||
| -rw-r--r-- | examples/logic/LexTheoryEng.gf | 7 | ||||
| -rw-r--r-- | examples/logic/Theory.gf | 47 | ||||
| -rw-r--r-- | examples/logic/TheoryEng.gf | 10 | ||||
| -rw-r--r-- | examples/logic/TheoryI.gf | 56 |
5 files changed, 128 insertions, 0 deletions
diff --git a/examples/logic/LexTheory.gf b/examples/logic/LexTheory.gf new file mode 100644 index 000000000..8bdd715a0 --- /dev/null +++ b/examples/logic/LexTheory.gf @@ -0,0 +1,8 @@ +interface LexTheory = open Grammar in { + + oper + assume_VS : VS ; + case_N : N ; + have_V2 : V2 ; + +} diff --git a/examples/logic/LexTheoryEng.gf b/examples/logic/LexTheoryEng.gf new file mode 100644 index 000000000..556bd2b24 --- /dev/null +++ b/examples/logic/LexTheoryEng.gf @@ -0,0 +1,7 @@ +instance LexTheoryEng of LexTheory = open GrammarEng,ParadigmsEng,IrregEng in { + oper + assume_VS = mkVS (regV "assume") ; + case_N = regN "case" ; + have_V2 = dirV2 have_V ; + +} diff --git a/examples/logic/Theory.gf b/examples/logic/Theory.gf new file mode 100644 index 000000000..778e0a8ec --- /dev/null +++ b/examples/logic/Theory.gf @@ -0,0 +1,47 @@ +abstract Theory = { + + cat + Chapter ; + Jment ; + [Jment] {0} ; + Decl ; + [Decl] {0} ; + Prop ; + Proof ; + [Proof] {2} ; + Branch ; + Typ ; + Obj ; + Label ; + Ref ; + [Ref] ; + Adverb ; + Number ; + + fun + Chap : Label -> [Jment] -> Chapter ; -- title, text + + JDefObj : [Decl] -> Obj -> Obj -> Jment ; -- a = b (G) + JDefObjTyp : [Decl] -> Typ -> Obj -> Obj -> Jment ; -- a = b : A (G) + JDefProp : [Decl] -> Prop -> Prop -> Jment ; -- A = B : Prop (G) + JThm : [Decl] -> Prop -> Proof -> Jment ; -- p : P (G) + + DProp : Prop -> Decl ; -- assume P + DPropLabel : Label -> Prop -> Label ; -- assume P (h) + DTyp : Obj -> Typ -> Decl ; -- let x,y be T + + PProp : Prop -> Proof ; -- P. + PAdvProp : Adverb -> Prop -> Proof ; -- Hence, P. + PDecl : Decl -> Proof ; -- Assume P. + PBranch : Branch -> [Proof] -> Proof ; -- By cases: P1 P2 + + BCases : Number -> Branch ; -- We have n cases. + + ARef : Ref -> Adverb ; -- by Thm 2 + AHence : Adverb ; -- therefore + AAFort : Adverb ; -- a fortiori + + RLabel : Label -> Ref ; -- Thm 2 + RMany : [Ref] -> Ref ; -- Thm 2 and Lemma 4 + +} diff --git a/examples/logic/TheoryEng.gf b/examples/logic/TheoryEng.gf new file mode 100644 index 000000000..a45bc0fdd --- /dev/null +++ b/examples/logic/TheoryEng.gf @@ -0,0 +1,10 @@ +--# -path=.:mathematical:present:resource-1.0/api:prelude + +concrete TheoryEng of Theory = TheoryI with + (LexTheory = LexTheoryEng), + (Grammar = GrammarEng), + (Symbolic = SymbolicEng), + (Symbol = SymbolEng), + (Combinators = CombinatorsEng), + (Constructors = ConstructorsEng), + ;
\ No newline at end of file diff --git a/examples/logic/TheoryI.gf b/examples/logic/TheoryI.gf new file mode 100644 index 000000000..9ab457536 --- /dev/null +++ b/examples/logic/TheoryI.gf @@ -0,0 +1,56 @@ +incomplete concrete TheoryI of Theory = + open + LexTheory, + Grammar, + Symbolic, + Symbol, + Combinators, + Constructors, + (C=ConstructX), + Prelude + in { + +lincat + Chapter = Text ; + Jment = Text ; + Decl = Text ; + Prop = S ; + Branch = S ; + Proof = Text ; + [Proof] = Text ; + Typ = CN ; + Obj = NP ; + Label = NP ; + Adverb = PConj ; + Ref = NP ; + [Ref] = [NP] ; + Number = Num ; + +lin + Chap title jments = + appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ; + + JDefObj decl a b = + appendText decl (mkUtt (mkS (pred b a))) ; + + DProp p = + mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ; + DTyp a ty = --- x pro a: refresh bug + mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ; + + PProp p = mkText (mkPhr p) TEmpty ; + PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ; + PDecl d = d ; + PBranch b ps = mkText (mkPhr b) ps ; + + BCases n = + mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ; + + ARef h = mkAdv by8means_Prep h ; + AHence = therefore_PConj ; + AAFort = C.mkPConj ["a fortiori"] ; + + RLabel h = h ; + RMany rs = mkNP and_Conj rs ; + +} |