started a subdir for the book

17 files changed, 674 insertions, 0 deletions

diff --git a/book/examples/chapter9/Anaphora.gf b/book/examples/chapter9/Anaphora.gf
new file mode 100644
index 000000000..5cbb92c94
--- /dev/null
+++ b/book/examples/chapter9/Anaphora.gf
@@ -0,0 +1,17 @@
+abstract Anaphora = TestSemantics - [she_NP] ** {
+
+cat
+  Proof Prop ;
+
+fun
+  IfS : (A : S) -> (Proof (iS A) -> S) -> S ;
+
+  AnaNP : (A : CN) -> (a : Ind) -> Proof (iCN A a) -> NP ;
+
+  pe : (B : Ind -> Prop) -> Proof (Exist B) -> Ind ;
+  qe : (B : Ind -> Prop) -> (c : Proof (Exist B)) -> Proof (B (pe B c)) ;
+
+  pc : (A,B : Prop) -> Proof (And A B) -> Proof A ;
+  qc : (A,B : Prop) -> Proof (And A B) -> Proof B ;
+
+}
diff --git a/book/examples/chapter9/AnaphoraIta.gf b/book/examples/chapter9/AnaphoraIta.gf
new file mode 100644
index 000000000..288872160
--- /dev/null
+++ b/book/examples/chapter9/AnaphoraIta.gf
@@ -0,0 +1,17 @@
+concrete AnaphoraIta of Anaphora = TestSemanticsIta - [she_NP] ** 
+  open ResIta, Prelude, Formal in {
+
+lincat
+  Proof = {} ;
+
+lin
+  IfS A B = {s = "se" ++ A.s ++ B.s} ;
+
+  AnaNP cn _ _ = case cn.g of {
+    Masc => pronNP "lui" "lo" "gli" Masc  Sg Per3 ;
+    Fem  => pronNP "lei" "la" "le" Fem  Sg Per3
+    } ;
+
+  pe _ _ = constant [] ; ----
+
+}
diff --git a/book/examples/chapter9/Grammar.gf b/book/examples/chapter9/Grammar.gf
new file mode 100644
index 000000000..57e3f8dcc
--- /dev/null
+++ b/book/examples/chapter9/Grammar.gf
@@ -0,0 +1,39 @@
+abstract Grammar = {
+
+  flags startcat = S ;
+
+  cat 
+    S ; Cl ; NP ; VP ; AP ; CN ; 
+    Det ; N ; A ; V ; V2 ; AdA ; 
+    Tense ; Pol ;
+    Conj ;
+  data
+    UseCl   : Tense -> Pol -> Cl -> S ;
+    PredVP  : NP -> VP -> Cl ;
+    ComplV2 : V2 -> NP -> VP ;
+    DetCN   : Det -> CN -> NP ;
+    ModCN   : AP -> CN -> CN ;
+
+    CompAP  : AP -> VP ;
+    AdAP    : AdA -> AP -> AP ;
+
+    ConjS   : Conj -> S  -> S  -> S ;
+    ConjNP  : Conj -> NP -> NP -> NP ;
+
+    UseV    : V -> VP ;
+    UseN    : N -> CN ;
+    UseA    : A -> AP ;
+
+    a_Det, the_Det, every_Det : Det ;
+    this_Det, these_Det : Det ;
+    that_Det, those_Det : Det ;
+    i_NP, she_NP, we_NP : NP ;
+    very_AdA : AdA ;
+
+    Pos, Neg : Pol ;
+    Pres, Perf : Tense ;
+
+    and_Conj, or_Conj : Conj ;
+
+  
+}
diff --git a/book/examples/chapter9/GrammarIta.gf b/book/examples/chapter9/GrammarIta.gf
new file mode 100644
index 000000000..93b2b78fb
--- /dev/null
+++ b/book/examples/chapter9/GrammarIta.gf
@@ -0,0 +1,141 @@
+concrete GrammarIta of Grammar = open ResIta, Prelude in {
+  lincat  
+    S  = {s : Str} ;
+    Cl = {s : ResIta.Tense => Bool => Str} ; 
+    NP = ResIta.NP ;  
+      -- {s : Case => {clit,obj : Str ; isClit : Bool} ; a : Agr} ; 
+    VP = ResIta.VP ;  
+      -- {v : Verb ; clit : Str ; clitAgr : ClitAgr ; obj : Agr => Str} ;
+    AP = {s : Gender => Number => Str ; isPre : Bool} ;
+    CN = Noun ;           -- {s : Number => Str ; g : Gender} ;
+    Det = {s : Gender => Case => Str ; n : Number} ;
+    N = Noun ;            -- {s : Number => Str ; g : Gender} ;
+    A = Adj ;             -- {s : Gender => Number => Str ; isPre : Bool} ;
+    V = Verb ;            -- {s : VForm => Str ; aux : Aux} ;
+    V2 = Verb ** {c : Case} ;
+    AdA = {s : Str} ;
+    Pol = {s : Str ; b : Bool} ;
+    Tense = {s : Str ; t : ResIta.Tense} ;
+    Conj = {s : Str ; n : Number} ;
+  lin
+    UseCl t p cl = {s = t.s ++ p.s ++ cl.s ! t.t ! p.b} ; 
+    PredVP np vp = 
+      let 
+        subj = (np.s ! Nom).obj ;
+        obj  = vp.obj ! np.a ;
+        clit = vp.clit ;
+        verb = table {
+          Pres => agrV vp.v np.a ;
+          Perf => agrV (auxVerb vp.v.aux) np.a ++ agrPart vp.v np.a vp.clitAgr
+          }
+      in {
+        s = \\t,b => subj ++ neg b ++ clit ++ verb ! t ++ obj
+      } ;
+
+    ComplV2 v2 np = 
+      let
+        nps = np.s ! v2.c
+      in {
+        v = v2 ; 
+        clit = nps.clit ; 
+        clitAgr = case <nps.isClit,v2.c> of {
+          <True,Acc> => CAgr np.a ;
+          _ => CAgrNo
+          } ;
+        obj  = \\_ => nps.obj
+        } ;
+
+    UseV v = {
+      v = v ; 
+      clit = [] ; 
+      clitAgr = CAgrNo ;
+      obj = \\_ => []
+      } ;
+
+    DetCN det cn = {
+      s = \\c => {
+        obj = det.s ! cn.g ! c ++ cn.s ! det.n ; 
+        clit = [] ; 
+        isClit = False
+        } ;
+      a = Ag cn.g det.n Per3
+      } ;
+
+    ModCN ap cn = {
+      s = \\n => preOrPost ap.isPre (ap.s ! cn.g ! n) (cn.s ! n) ;
+      g = cn.g
+      } ;
+
+    CompAP ap = {
+      v = essere_V ; 
+      clit = [] ; 
+      clitAgr = CAgrNo ;
+      obj = \\ag => case ag of {
+        Ag g n _ => ap.s ! g ! n
+        }
+      } ;
+
+    AdAP ada ap = {
+      s = \\g,n => ada.s ++ ap.s ! g ! n ;
+      isPre = ap.isPre ;
+      } ;
+
+    ConjNP co nx ny = {
+      s = \\c => {
+        obj = (nx.s ! c).obj ++ co.s ++ (ny.s ! c).obj ; 
+        clit = [] ; 
+        isClit = False
+        } ;
+      a = conjAgr co.n nx.a ny.a
+      } ;
+
+    ConjS co x y = {s = x.s ++ co.s ++ y.s} ;
+
+    UseN n = n ;
+
+    UseA adj = adj ;
+
+    a_Det = adjDet (mkAdj "un" "una" [] [] True) Sg ;
+
+    every_Det = adjDet (regAdj "ogni") Sg ;
+
+    the_Det = {
+      s = table {
+        Masc => table {
+          Nom | Acc => elisForms "lo" "l'" "il" ;
+          Dat => elisForms "allo" "all'" "al"
+          } ;
+        Fem => table {
+          Nom | Acc => elisForms "la" "'l" "la" ;
+          Dat => elisForms "alla" "all'" "alla"
+          }
+        } ;
+      n = Sg
+      } ;
+        
+    this_Det = adjDet (regAdj "questo") Sg ;
+    these_Det = adjDet (regAdj "questo") Pl ;
+    that_Det = adjDet quello_A Sg ;
+    those_Det = adjDet quello_A Pl ;
+
+    i_NP =   pronNP "io"  "mi" "mi" Masc Sg Per1 ;
+    she_NP = pronNP "lei" "la" "le" Fem  Sg Per3 ;
+    we_NP =  pronNP "noi" "ci" "ci" Masc Pl Per1 ;
+
+    very_AdA = ss "molto" ;
+
+    Pos  = {s = [] ; b = True} ;
+    Neg  = {s = [] ; b = False} ;
+    Pres = {s = [] ; t = ResIta.Pres} ;
+    Perf = {s = [] ; t = ResIta.Perf} ;
+
+    and_Conj = {s = "e" ; n = Pl} ;
+    or_Conj  = {s = "o" ; n = Sg} ;
+
+  oper
+    quello_A : Adj = mkAdj 
+      (elisForms "quello" "quell'" "quel") "quella"
+      (elisForms "quegli" "quegli" "quei") "quelle"
+      True ;
+
+}
diff --git a/book/examples/chapter9/Logic.gf b/book/examples/chapter9/Logic.gf
new file mode 100644
index 000000000..0ce8df7e9
--- /dev/null
+++ b/book/examples/chapter9/Logic.gf
@@ -0,0 +1,9 @@
+abstract Logic = {
+  cat
+    Prop ; Ind ;
+  data
+    And, Or, If : Prop -> Prop -> Prop ;
+    Not         : Prop -> Prop ;
+    All, Exist  : (Ind -> Prop) -> Prop ;
+    Past        : Prop -> Prop ;
+}
diff --git a/book/examples/chapter9/LogicIta.gf b/book/examples/chapter9/LogicIta.gf
new file mode 100644
index 000000000..f94edc11c
--- /dev/null
+++ b/book/examples/chapter9/LogicIta.gf
@@ -0,0 +1,54 @@
+concrete LogicIta of Logic = GrammarIta ** open ResIta, Formal, Prelude in {
+
+
+lincat
+  T, I = SS ;
+lin
+  And x y = infixSS "&" x y ;
+  Or x y = infixSS "v" x y ;
+  If x y = infixSS "->" x y ;
+  Not x = prefixSS "~" x ;
+  All P = prefixSS (parenth ("A" ++ P.$0)) P ;
+  Exist P = prefixSS (parenth ("E" ++ P.$0)) P ;
+  Past P = prefixSS "Past" P ;
+
+lin
+  iN f = star (f.s ! Sg) ;
+  iA f = star (f.s ! Masc ! Sg) ;
+  iV f = star (f.s ! VInf) ;
+  iV2 f x y = star (f.s ! VInf) (cc2 x y) ;
+
+oper star : Str -> SS -> SS = \f,x -> prefixSS f (ss (parenth x.s)) ;
+
+{-
+
+lincat
+  T, I = TermPrec ;
+lin
+  And = infixl 2 "&" ;
+  Or  = infixl 2 "v" ;
+  If  = infixr 1 "->" ;
+--  Not = prefix 3 "~" ;
+--  All : (I -> T) -> T ;
+--  Exist : (I -> T) -> T ;
+--  Past : T -> T ;
+
+lin
+  iS   : S -> T ;
+  iCl  : Cl -> T ;
+  iNP  : NP -> (I -> T) -> T ;
+  iVP  : VP -> I -> T ;
+  iAP  : AP -> I -> T ;
+  iCN  : CN -> I -> T ;
+  iDet : Det -> (I -> T) -> (I -> T) -> T ;
+  iN   : N -> I -> T ;
+  iA   : A -> I -> T ;
+  iV   : V -> I -> T ;
+  iV2  : V2 -> I -> I -> T ;
+  iAdA : AdA -> (I -> T) -> I -> T ;
+  iTense : Tense -> T -> T ;
+  iPol  : Pol  -> T -> T ;
+  iConj : Conj -> T -> T -> T ;
+-}
+
+}
diff --git a/book/examples/chapter9/LogicSymb.gf b/book/examples/chapter9/LogicSymb.gf
new file mode 100644
index 000000000..14932fe9b
--- /dev/null
+++ b/book/examples/chapter9/LogicSymb.gf
@@ -0,0 +1,13 @@
+concrete LogicSymb of Logic = open Formal, Prelude in {
+
+lincat
+  Prop, Ind = TermPrec ;
+lin
+  And = infixl 2 "\\&" ;
+  Or  = infixl 2 "\\vee" ;
+  If  = infixr 1 "\\sup" ;
+  Not = prefix 3 "\\sim" ;
+  All P = prefix 3 (parenth ("\\forall" ++ P.$0)) P ;
+  Exist P = prefix 3 (parenth ("\\exists" ++ P.$0)) P ;
+  Past = prefix 3 "P" ;
+}
diff --git a/book/examples/chapter9/ParadigmsIta.gf b/book/examples/chapter9/ParadigmsIta.gf
new file mode 100644
index 000000000..010140a62
--- /dev/null
+++ b/book/examples/chapter9/ParadigmsIta.gf
@@ -0,0 +1,47 @@
+resource ParadigmsIta = GrammarIta [N,A,V] ** 
+  open ResIta, GrammarIta, Prelude in {
+
+oper
+  masculine : Gender = Masc ;
+  feminine : Gender = Fem ;
+
+  accusative : Case = Acc ;
+  dative : Case = Dat ;
+
+  mkN = overload {
+    mkN : (vino : Str) -> N 
+      = \n -> lin N (regNoun n) ;
+    mkN : (uomo, uomini : Str) -> Gender -> N 
+      = \s,p,g -> lin N (mkNoun s p g) ;
+    } ;
+
+  mkA = overload {
+    mkA : (nero : Str) -> A 
+      = \a -> lin A (regAdj a) ;
+    mkA : (buono,buona,buoni,buone : Str) -> Bool -> A 
+      = \sm,sf,pm,pf,p -> lin A (mkAdj sm sf pm pf False) ;
+    } ;
+
+  preA : A -> A
+      = \a -> lin A {s = a.s ; isPre = True} ;
+
+  mkV = overload {
+    mkV : (finire : Str) -> V 
+      = \v -> lin V (regVerb v) ;
+    mkV : (andare,vado,vadi,va,andiamo,andate,vanno,andato : Str) -> V 
+      = \i,p1,p2,p3,p4,p5,p6,p -> lin V (mkVerb i p1 p2 p3 p4 p5 p6 p Avere) ;
+    } ;
+
+  essereV : V -> V
+    = \v -> lin V {s = v.s ; aux = Essere} ;
+
+  mkV2 = overload {
+    mkV2 : Str -> V2
+      = \s -> lin V2 (regVerb s ** {c = accusative}) ;
+    mkV2 : V -> V2
+      = \v -> lin V2 (v ** {c = accusative}) ;
+    mkV2 : V -> Case -> V2
+      = \v,c -> lin V2 (v ** {c = c}) ;
+    } ;
+
+}
diff --git a/book/examples/chapter9/ResIta.gf b/book/examples/chapter9/ResIta.gf
new file mode 100644
index 000000000..f39db69f9
--- /dev/null
+++ b/book/examples/chapter9/ResIta.gf
@@ -0,0 +1,178 @@
+resource ResIta = open Prelude in {
+
+-- parameters
+
+param
+  Number = Sg | Pl ;
+  Gender = Masc | Fem ;
+  Case   = Nom | Acc | Dat ;
+  Agr    = Ag Gender Number Person ;
+  Aux    = Avere | Essere ;
+  Tense  = Pres | Perf ;
+  Person = Per1 | Per2 | Per3 ;
+
+  VForm = VInf | VPres Number Person | VPart Gender Number ;
+
+  ClitAgr = CAgrNo | CAgr Agr ;
+
+-- parts of speech
+
+oper
+  VP = {
+    v : Verb ; 
+    clit : Str ; 
+    clitAgr : ClitAgr ; 
+    obj : Agr => Str
+    } ;
+  NP = {
+    s : Case => {clit,obj : Str ; isClit : Bool} ; 
+    a : Agr
+    } ; 
+
+-- the preposition word of an abstract case
+
+  prepCase : Case -> Str = \c -> case c of {
+    Dat => "a" ;
+    _ => []
+    } ;
+
+-- for predication
+
+  agrV : Verb -> Agr -> Str = \v,a -> case a of {
+    Ag _ n p => v.s ! VPres n p
+    } ;
+
+  auxVerb : Aux -> Verb = \a -> case a of {
+    Avere => 
+      mkVerb "avere" "ho" "hai" "ha" "abbiamo" "avete" "hanno" "avuto" Avere ;
+    Essere => 
+      mkVerb "essere" "sono" "sei" "è" "siamo" "siete" "sono" "stato" Essere
+    } ;
+
+  agrPart : Verb -> Agr -> ClitAgr -> Str = \v,a,c -> case v.aux of {
+    Avere  => case c of {
+      CAgr (Ag g n _) => v.s ! VPart g n ;
+      _ => v.s ! VPart Masc Sg
+      } ;
+    Essere => case a of {
+      Ag g n _ => v.s ! VPart g n
+      }
+    } ;
+
+  neg : Bool -> Str = \b -> case b of {True => [] ; False => "non"} ;
+
+  essere_V = auxVerb Essere ;
+
+-- for coordination
+
+  conjAgr : Number -> Agr -> Agr -> Agr = \n,xa,ya -> 
+    let 
+      x = agrFeatures xa ; y = agrFeatures ya
+    in Ag 
+      (conjGender x.g y.g) 
+      (conjNumber (conjNumber x.n y.n) n)
+      (conjPerson x.p y.p) ;
+
+  agrFeatures : Agr -> {g : Gender ; n : Number ; p : Person} = \a -> 
+    case a of {Ag g n p => {g = g ; n = n ; p = p}} ;
+
+  conjGender : Gender -> Gender -> Gender = \g,h ->
+    case g of {Masc => Masc ; _ => h} ;
+
+  conjNumber : Number -> Number -> Number = \m,n ->
+    case m of {Pl => Pl ; _ => n} ;
+
+  conjPerson : Person -> Person -> Person = \p,q ->
+    case <p,q> of {
+      <Per1,_> | <_,Per1> => Per1 ;
+      <Per2,_> | <_,Per2> => Per2 ;
+      _                   => Per3
+      } ;
+
+
+
+-- for morphology
+
+  Noun : Type = {s : Number => Str ; g : Gender} ;
+  Adj  : Type = {s : Gender => Number => Str ; isPre : Bool} ;
+  Verb : Type = {s : VForm => Str ; aux : Aux} ;
+
+  mkNoun : Str -> Str -> Gender -> Noun = \vino,vini,g -> {
+    s = table {Sg => vino ; Pl => vini} ;
+    g = g
+    } ;
+
+  regNoun : Str -> Noun = \vino -> case vino of {
+    fuo + c@("c"|"g") + "o" => mkNoun vino (fuo + c + "hi") Masc ;
+    ol  + "io" => mkNoun vino (ol + "i") Masc ;
+    vin + "o" => mkNoun vino (vin + "i") Masc ;
+    cas + "a" => mkNoun vino (cas + "e") Fem ;
+    pan + "e" => mkNoun vino (pan + "i") Masc ;
+    _ => mkNoun vino vino Masc 
+    } ;
+
+  mkAdj : (_,_,_,_ : Str) -> Bool -> Adj = \buono,buona,buoni,buone,p -> {
+    s = table {
+          Masc => table {Sg => buono ; Pl => buoni} ;
+          Fem  => table {Sg => buona ; Pl => buone}
+        } ;
+    isPre = p
+    } ;
+
+  regAdj : Str -> Adj = \nero -> case nero of {
+    ner + "o"  => mkAdj nero (ner + "a") (ner + "i") (ner + "e") False ;
+    verd + "e" => mkAdj nero nero (verd + "i") (verd + "i") False ;
+    _ => mkAdj nero nero nero nero False
+    } ;
+
+  mkVerb : (_,_,_,_,_,_,_,_ : Str) -> Aux -> Verb = 
+    \amare,amo,ami,ama,amiamo,amate,amano,amato,aux -> {
+    s = table {
+          VInf          => amare ;
+          VPres Sg Per1 => amo ;
+          VPres Sg Per2 => ami ;
+          VPres Sg Per3 => ama ;
+          VPres Pl Per1 => amiamo ;
+          VPres Pl Per2 => amate ;
+          VPres Pl Per3 => amano ;
+          VPart g n     => (regAdj amato).s ! g ! n
+          } ;
+    aux = aux
+    } ;
+
+  regVerb : Str -> Verb = \amare -> case amare of {
+    am  + "are" => mkVerb amare (am+"o") (am+"i") (am+"a") 
+                     (am+"iamo") (am+"ate") (am+"ano") (am+"ato") Avere ;
+    tem + "ere" => mkVerb amare (tem+"o") (tem+"i") (tem+"e") 
+                     (tem+"iamo") (tem+"ete") (tem+"ono") (tem+"uto") Avere ;
+    fin + "ire" => mkVerb amare (fin+"isco") (fin+"isci") (fin+"isce") 
+                     (fin+"iamo") (fin+"ite") (fin+"iscono") (fin+"ito") Avere
+    } ; 
+
+-- for structural words
+
+  adjDet : Adj -> Number -> {s : Gender => Case => Str ; n : Number} = 
+  \adj,n -> {
+    s = \\g,c => prepCase c ++ adj.s ! g ! n ;
+    n = n
+    } ;
+
+  pronNP : (s,a,d : Str) -> Gender -> Number -> Person -> NP = 
+  \s,a,d,g,n,p -> {
+    s = table {
+      Nom => {clit = [] ; obj = s  ; isClit = False} ;
+      Acc => {clit = a  ; obj = [] ; isClit = True} ;
+      Dat => {clit = d  ; obj = [] ; isClit = True}
+      } ;
+    a = Ag g n p
+    } ;
+
+-- phonological auxiliaries
+
+  vowel    : pattern Str = #("a" | "e" | "i" | "o" | "u" | "h") ;
+  s_impuro : pattern Str = #("z" | "s" + ("b"|"c"|"d"|"f"|"m"|"p"|"q"|"t")) ;
+
+  elisForms : (_,_,_ : Str) -> Str = \lo,l',il ->
+    pre {#s_impuro => lo ; #vowel => l' ; _ => il} ;
+
+}
diff --git a/book/examples/chapter9/Semantics.gf b/book/examples/chapter9/Semantics.gf
new file mode 100644
index 000000000..0976caa93
--- /dev/null
+++ b/book/examples/chapter9/Semantics.gf
@@ -0,0 +1,39 @@
+abstract Semantics = Grammar, Logic ** {
+fun
+  iS     : S     -> Prop ;
+  iCl    : Cl    -> Prop ;
+  iNP    : NP    -> (Ind -> Prop) -> Prop ;
+  iVP    : VP    -> Ind -> Prop ;
+  iAP    : AP    -> Ind -> Prop ;
+  iCN    : CN    -> Ind -> Prop ;
+  iDet   : Det   -> (Ind -> Prop) -> (Ind -> Prop) -> Prop ;
+  iN     : N     -> Ind -> Prop ;
+  iA     : A     -> Ind -> Prop ;
+  iV     : V     -> Ind -> Prop ;
+  iV2    : V2    -> Ind -> Ind -> Prop ;
+  iAdA   : AdA   -> (Ind -> Prop) -> Ind -> Prop ;
+  iTense : Tense -> Prop -> Prop ;
+  iPol   : Pol   -> Prop -> Prop ;
+  iConj  : Conj  -> Prop -> Prop -> Prop ;
+def
+  iS  (UseCl t p cl) = iTense t (iPol p (iCl cl)) ;
+  iCl (PredVP np vp) = iNP np (iVP vp) ;
+  iVP (ComplV2 v2 np) i = iNP np (iV2 v2 i) ;
+  iNP (DetCN det cn) f = iDet det (iCN cn) f ;
+  iCN (ModCN ap cn) i = And (iAP ap i) (iCN cn i) ;
+  iVP (CompAP ap) i = iAP ap i ;
+  iAP (AdAP ada ap) i = iAdA ada (iAP ap) i ;
+  iS  (ConjS conj x y) = iConj conj (iS x) (iS y) ;
+  iNP (ConjNP conj x y) f = iConj conj (iNP x f) (iNP y f) ;
+  iVP (UseV v) i = iV v i ;
+  iAP (UseA a) i = iA a i ;
+  iCN (UseN n) i = iN n i ;
+  iDet a_Det d f = Exist (\x -> And (d x) (f x)) ;
+  iDet every_Det d f = All (\x -> If (d x) (f x)) ;
+  iPol Pos t = t ;
+  iPol Neg t = Not t ;
+  iTense Pres t = t ;
+  iTense Perf t = Past t ;
+  iConj and_Conj a b = And a b ;
+  iConj or_Conj  a b = Or a b ;
+}
diff --git a/book/examples/chapter9/SemanticsIta.gf b/book/examples/chapter9/SemanticsIta.gf
new file mode 100644
index 000000000..70d4b79b9
--- /dev/null
+++ b/book/examples/chapter9/SemanticsIta.gf
@@ -0,0 +1,42 @@
+concrete SemanticsIta of Semantics = GrammarIta, LogicSymb ** open ResIta, Formal, Prelude in {
+
+lin
+  iN f = star (f.s ! Sg) ;
+  iA f = star (f.s ! Masc ! Sg) ;
+  iV f = star (f.s ! VInf) ;
+  iV2 f x y = star (f.s ! VInf) (cc2 x y) ;
+
+oper star : Str -> SS -> TermPrec = \f,x -> prefix 3 (f ++ "*") (constant (parenth x.s)) ;
+
+{-
+
+lincat
+  T, I = TermPrec ;
+lin
+  And = infixl 2 "&" ;
+  Or  = infixl 2 "v" ;
+  If  = infixr 1 "->" ;
+--  Not = prefix 3 "~" ;
+--  All : (I -> T) -> T ;
+--  Exist : (I -> T) -> T ;
+--  Past : T -> T ;
+
+lin
+  iS   : S -> T ;
+  iCl  : Cl -> T ;
+  iNP  : NP -> (I -> T) -> T ;
+  iVP  : VP -> I -> T ;
+  iAP  : AP -> I -> T ;
+  iCN  : CN -> I -> T ;
+  iDet : Det -> (I -> T) -> (I -> T) -> T ;
+  iN   : N -> I -> T ;
+  iA   : A -> I -> T ;
+  iV   : V -> I -> T ;
+  iV2  : V2 -> I -> I -> T ;
+  iAdA : AdA -> (I -> T) -> I -> T ;
+  iTense : Tense -> T -> T ;
+  iPol  : Pol  -> T -> T ;
+  iConj : Conj -> T -> T -> T ;
+-}
+
+}
diff --git a/book/examples/chapter9/Syntax.gf b/book/examples/chapter9/Syntax.gf
new file mode 100644
index 000000000..01a51d0ee
--- /dev/null
+++ b/book/examples/chapter9/Syntax.gf
@@ -0,0 +1,47 @@
+interface Syntax = Grammar - 
+    [UseCl,PredVP,ComplV2,UseV,DetCN,ModCN,CompAP,AdAP,
+     ConjS,ConjNP,UseN,UseA,Pres,Perf,Pos,Neg] **
+  open Grammar in {
+
+oper
+  mkS = overload {
+    mkS : Cl -> S = UseCl Pres Pos ;
+    mkS : Tense -> Cl -> S = \t -> UseCl t Pos ;
+    mkS : Pol -> Cl -> S = UseCl Pres ;
+    mkS : Tense -> Pol -> Cl -> S = UseCl ;
+    mkS : Conj -> S -> S -> S = ConjS ;
+    } ;
+
+  mkCl = overload {
+    mkCl : NP -> V  -> Cl = \np,v -> PredVP np (UseV v) ;
+    mkCl : NP -> V2 -> NP -> Cl = \np,v,o -> PredVP np (ComplV2 v o) ;
+    mkCl : NP -> A  -> Cl = \np,a -> PredVP np (CompAP (UseA a)) ;
+    mkCl : NP -> AP -> Cl = \np,ap -> PredVP np (CompAP ap) ;
+    mkCl : NP -> VP -> Cl = PredVP ;
+    } ;
+
+  mkAP = overload {
+    mkAP : A -> AP = UseA ;
+    mkAP : AdA -> AP -> AP = AdAP ;
+    } ;
+
+  mkNP = overload {
+    mkNP : Det -> N -> NP = \d,n -> DetCN d (UseN n) ;
+    mkNP : Det -> CN -> NP = \d,n -> DetCN d n ;
+    mkNP : Conj -> NP -> NP -> NP = ConjNP ;
+    } ;
+
+  mkCN = overload {
+    mkCN : N  -> CN = UseN ;
+    mkCN : A  -> N  -> CN = \a,n -> ModCN (UseA a) (UseN n) ; 
+    mkCN : A  -> CN -> CN = \a,n -> ModCN (UseA a) n ; 
+    mkCN : AP -> N  -> CN = \a,n -> ModCN a (UseN n) ; 
+    mkCN : AP -> CN -> CN = \a,n -> ModCN a n ; 
+    } ;
+
+  presTense : Tense = Pres ;
+  perfTense : Tense = Perf ;
+  posPol : Pol = Pos ;
+  negPol : Pol = Neg ;
+
+}
diff --git a/book/examples/chapter9/SyntaxIta.gf b/book/examples/chapter9/SyntaxIta.gf
new file mode 100644
index 000000000..b4562b0de
--- /dev/null
+++ b/book/examples/chapter9/SyntaxIta.gf
@@ -0,0 +1,3 @@
+instance SyntaxIta of Syntax = GrammarIta - 
+    [PredVP,ComplV2,UseV,DetCN,ModCN,CompAP,AdAP,UseN,UseA] **
+  open GrammarIta in {} ;
diff --git a/book/examples/chapter9/Test.gf b/book/examples/chapter9/Test.gf
new file mode 100644
index 000000000..ebe55e7e0
--- /dev/null
+++ b/book/examples/chapter9/Test.gf
@@ -0,0 +1,9 @@
+abstract Test = Grammar ** {
+
+fun
+  man_N, woman_N, house_N, tree_N : N ;
+  big_A, small_A, green_A : A ;
+  walk_V, arrive_V : V ;
+  love_V2, please_V2 : V2 ;
+
+} ;
diff --git a/book/examples/chapter9/TestIta.gf b/book/examples/chapter9/TestIta.gf
new file mode 100644
index 000000000..8ae524371
--- /dev/null
+++ b/book/examples/chapter9/TestIta.gf
@@ -0,0 +1,17 @@
+concrete TestIta of Test = GrammarIta ** open ParadigmsIta in {
+
+lin
+  man_N = mkN "uomo" "uomini" masculine ;
+  woman_N = mkN "donna" ;
+  house_N = mkN "casa" ;
+  tree_N = mkN "albero" ;
+  big_A = preA (mkA "grande") ;
+  small_A = preA (mkA "piccolo") ;
+  green_A = mkA "verde" ;
+  walk_V = mkV "camminare" ;
+  arrive_V = essereV (mkV "arrivare") ;
+  love_V2 = mkV2 "amare" ;
+  please_V2 = mkV2 (essereV (mkV "piacere" "piaccio" "piaci" "piace" 
+                        "piacciamo" "piacete" "piacciono" "piaciuto")) dative ;
+
+} ;
diff --git a/book/examples/chapter9/TestSemantics.gf b/book/examples/chapter9/TestSemantics.gf
new file mode 100644
index 000000000..ce8fe4428
--- /dev/null
+++ b/book/examples/chapter9/TestSemantics.gf
@@ -0,0 +1 @@
+abstract TestSemantics = Test, Semantics ;
diff --git a/book/examples/chapter9/TestSemanticsIta.gf b/book/examples/chapter9/TestSemanticsIta.gf
new file mode 100644
index 000000000..ce6abfc09
--- /dev/null
+++ b/book/examples/chapter9/TestSemanticsIta.gf
@@ -0,0 +1 @@
+concrete TestSemanticsIta of TestSemantics = TestIta, SemanticsIta ;