AdvS and for_Prep in resource (except Russian)

examples/logic/LogicI.gf

@@ -16,11 +16,16 @@ lincat
   Text  = Section ;
 
 lin
+  ThmWithProof = theorem ;
+
   Disj A B = coord or_Conj A B ;
   Impl A B = coord ifthen_DConj A B ;
 
   Abs = mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
 
+  Univ A B = 
+    mkS (mkAdv for_Prep (mkNP all_Predet (mkNP (mkDet IndefArt (mkCN A $0))))) B ;
+
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
   DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
 

examples/logic/Prooftext.gf

@@ -34,6 +34,9 @@ oper
     = \decl,a,b -> 
         appendText decl (mkUtt (mkS (pred b a))) ;
 
+  theorem : Prop -> Proof -> Section 
+    = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
+
   assumption : Prop -> Decl 
     = \p -> 
         mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
@@ -45,6 +48,8 @@ oper
   proof = overload {
     proof : Prop -> Proof 
       = \p -> mkText (mkPhr p) TEmpty ;
+    proof : Str -> Proof
+      = \s -> {s = s ++ "." ; lock_Text = <>} ;
     proof : Adverb -> Prop -> Proof
       = \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
     proof : Decl -> Proof
@@ -76,4 +81,6 @@ oper
   refs : Refs -> Ref
     = \rs -> mkNP and_Conj rs ;
 
+  mkLabel : Str -> Label ;
+
 }

examples/logic/ProoftextEng.gf

@@ -1,12 +1,19 @@
 --# -path=.:mathematical:present:resource-1.0/api:prelude
 
-instance ProoftextEng of Prooftext = open 
+instance ProoftextEng of Prooftext = 
-  LexTheoryEng, 
+  open 
-  GrammarEng, 
+    LexTheoryEng, 
-  SymbolicEng, 
+    GrammarEng, 
-  SymbolEng, 
+    SymbolicEng, 
-  (C=ConstructX),
+    SymbolEng, 
-  CombinatorsEng, 
+    (C=ConstructX),
-  ConstructorsEng in {
+    CombinatorsEng, 
-  }
+    ConstructorsEng,
-  ;
+    (P=ParadigmsEng)
+  in {
+
+oper
+  mkLabel : Str -> Label = \s -> UsePN (P.regPN s) ;
+
+
+}

lib/resource-1.0/abstract/Sentence.gf

@@ -61,6 +61,10 @@ abstract Sentence = Cat ** {
     UseQCl : Tense -> Ant -> Pol -> QCl -> QS ;
     UseRCl : Tense -> Ant -> Pol -> RCl -> RS ;
 
+-- An adverb can be added to the beginning of a sentence.
+
+    AdvS   : Adv -> S  -> S ;            -- today, I will go home
+
 }
 
 --.

lib/resource-1.0/abstract/Structural.gf

@@ -38,6 +38,7 @@ abstract Structural = Cat ** {
   everywhere_Adv : Adv ;
   first_Ord : Ord ;
   few_Det : Det ;
+  for_Prep : Prep ;
   from_Prep : Prep ;
   he_Pron : Pron ;
   here_Adv : Adv ;

lib/resource-1.0/api/Constructors.gf

@@ -67,8 +67,8 @@ incomplete resource Constructors = open Grammar in {
       mkS : Conj -> S -> S -> S ;            -- John walks and Mary talks   
       mkS : DConj -> S -> S -> S ;           -- either I leave or you come
       mkS : Conj -> ListS -> S ;             -- John walks, Mary talks, and Bob runs
-      mkS : DConj -> ListS -> S              -- either I leave, you come, or he runs
+      mkS : DConj -> ListS -> S ;            -- either I leave, you come, or he runs
-
+      mkS : Adv -> S -> S                    -- today, I will sleep
       } ;
 
     mkCl : overload {
@@ -522,7 +522,9 @@ incomplete resource Constructors = open Grammar in {
       mkS : Conj -> ListS -> S
                                         = \c,xy -> ConjS c xy ;
       mkS : DConj -> ListS -> S
-                                        = \c,xy -> DConjS c xy
+                                        = \c,xy -> DConjS c xy ;
+      mkS : Adv -> S -> S 
+                                        = AdvS
 
       } ;
 

lib/resource-1.0/danish/StructuralDan.gf

@@ -30,6 +30,7 @@ concrete StructuralDan of Structural = CatDan **
   everywhere_Adv = ss "overalt" ;
   few_Det  = {s = \\_,_ => "få" ; n = Pl ; det = DDef Indef} ;
   first_Ord = {s = "første" ; isDet = True} ;
+  for_Prep = ss "for" ;
   from_Prep = ss "fra" ;
   he_Pron = MorphoDan.mkNP "han"  "ham"  "hans" "hans" "hans"  SgUtr P3 ;
   here_Adv = ss "her" ;

lib/resource-1.0/english/SentenceEng.gf

@@ -48,6 +48,8 @@ concrete SentenceEng of Sentence = CatEng ** open Prelude, ResEng in {
       c = cl.c
       } ;
 
+    AdvS a s = {s = a.s ++ "," ++ s.s} ;
+
   oper
     ctr = contrNeg True ;  -- contracted negations
 }

lib/resource-1.0/english/StructuralEng.gf

@@ -32,6 +32,7 @@ concrete StructuralEng of Structural = CatEng **
   everywhere_Adv = ss "everywhere" ;
   few_Det = mkDeterminer Pl "few" ;
   first_Ord = ss "first" ;
+  for_Prep = ss "for" ;
   from_Prep = ss "from" ;
   he_Pron = mkNP "he" "him" "his" Sg P3 ;
   here_Adv = ss "here" ;

lib/resource-1.0/finnish/SentenceFin.gf

@@ -64,4 +64,6 @@ concrete SentenceFin of Sentence = CatFin ** open Prelude, ResFin in {
       c = cl.c
       } ;
 
+    AdvS a s = {s = a.s ++ "," ++ s.s} ;
+
 }

lib/resource-1.0/finnish/StructuralFin.gf

@@ -39,6 +39,7 @@ concrete StructuralFin of Structural = CatFin **
   everywhere_Adv = ss "kaikkialla" ;
   few_Det  = mkDet Sg (regN "harva") ;
   first_Ord = {s = \\n,c => (regN "ensimmäinen").s ! NCase n c} ;
+  for_Prep = casePrep allative ;
   from_Prep = casePrep elative ;
   he_Pron = mkPronoun "hän" "hänen" "häntä"  "hänenä" "häneen" Sg P3 ;
   here_Adv = ss "täällä" ;

lib/resource-1.0/french/StructuralFre.gf

@@ -35,6 +35,7 @@ lin
   everywhere_Adv = ss "partout" ;
   few_Det  = {s = \\g,c => prepCase c ++ "peu" ++ elisDe ; n = Pl} ;
   first_Ord = {s = \\ag => (regA "premier").s ! Posit ! AF ag.g ag.n} ;
+  for_Prep = mkPreposition "pour" ;
   from_Prep = complGen ; ---
   he_Pron = 
     mkPronoun

lib/resource-1.0/german/SentenceGer.gf

@@ -44,4 +44,6 @@ concrete SentenceGer of Sentence = CatGer ** open ResGer in {
       c = cl.c
       } ;
 
+    AdvS a s = {s = \\o => a.s ++ "," ++ s.s ! o} ;
+
 }

lib/resource-1.0/german/StructuralGer.gf

@@ -35,6 +35,7 @@ concrete StructuralGer of Structural = CatGer **
   everywhere_Adv = ss "überall" ;
   few_Det = detLikeAdj Pl "wenig" ;
   first_Ord = {s = (regA "erst").s ! Posit} ;
+  for_Prep = mkPrep "für" Acc ;
   from_Prep = mkPrep "aus" Dat ;
   he_Pron = mkPronPers "er" "ihn" "ihm" "seiner" "sein"  Masc Sg P3 ;
   here7to_Adv = ss ["hierher"] ;

lib/resource-1.0/italian/StructuralIta.gf

@@ -33,6 +33,7 @@ lin
   everywhere_Adv = ss "dappertutto" ;
   few_Det  = {s = \\g,c => prepCase c ++ genForms "pochi" "poche" ! g ; n = Pl} ;
   first_Ord = {s = \\ag => (regA "primo").s ! Posit ! AF ag.g ag.n} ;
+  for_Prep = mkPrep "per" ;
   from_Prep = complGen ; ---
   he_Pron = 
     mkPronoun

lib/resource-1.0/norwegian/StructuralNor.gf

@@ -30,6 +30,7 @@ concrete StructuralNor of Structural = CatNor **
   everywhere_Adv = ss "overalt" ;
   few_Det  = {s = \\_,_ => "få" ; n = Pl ; det = DDef Indef} ;
   first_Ord = {s = "første" ; isDet = True} ;
+  for_Prep = ss "for" ;
   from_Prep = ss "fra" ;
   he_Pron = MorphoNor.mkNP "han"  "ham"  "hans" "hans" "hans"  SgUtr P3 ;
   here_Adv = ss "her" ;

lib/resource-1.0/romance/SentenceRomance.gf

@@ -50,4 +50,6 @@ incomplete concrete SentenceRomance of Sentence =
       c = cl.c
       } ;
 
+    AdvS a s = {s = \\o => a.s ++ "," ++ s.s ! o} ;
+
 }

lib/resource-1.0/scandinavian/SentenceScand.gf

@@ -47,4 +47,5 @@ incomplete concrete SentenceScand of Sentence =
       c = cl.c
       } ;
 
+    AdvS a s = {s = \\o => a.s ++ "," ++ s.s ! o} ;
 }

lib/resource-1.0/spanish/StructuralSpa.gf

@@ -33,6 +33,7 @@ lin
   everywhere_Adv = ss ["en todas partes"] ;
   few_Det  = {s = \\g,c => prepCase c ++ genForms "pocos" "pocas" ! g ; n = Pl} ;
   first_Ord = {s = \\ag => (regA "primero").s ! Posit ! AF ag.g ag.n} ;
+  for_Prep = mkPrep "por" ;
   from_Prep = complGen ; ---
   he_Pron = 
     mkPronoun 

lib/resource-1.0/swedish/StructuralSwe.gf

@@ -30,6 +30,7 @@ concrete StructuralSwe of Structural = CatSwe **
   everywhere_Adv = ss "överallt" ;
   few_Det  = {s = \\_,_ => "få" ; n = Pl ; det = DDef Indef} ;
   first_Ord = {s = "första" ; isDet = True} ;
+  for_Prep = ss "för" ;
   from_Prep = ss "från" ;
   he_Pron = MorphoSwe.mkNP "han"  "honom"  "hans" "hans" "hans"  SgUtr P3 ;
   here_Adv = ss "här" ;