gf-book web page index and toc

12 files changed, 0 insertions, 326 deletions

diff --git a/book/examples/chapter6/Aggregation.gf b/book/examples/chapter6/Aggregation.gf
deleted file mode 100644
index 28cbd39ef..000000000
--- a/book/examples/chapter6/Aggregation.gf
+++ /dev/null
@@ -1,33 +0,0 @@
-abstract Aggregation = {
-  cat S ; NP ; VP ;
-  data 
-    PredVP : NP -> VP -> S ;
-    ConjS  : S -> S -> S ;
-    ConjVP : VP -> VP -> VP ;
-    ConjNP : NP -> NP -> NP ;
-    Run, Walk : VP ;
-    John, Mary : NP ;
-
-  fun aggr : S -> S ; -- main aggregation function
-  def aggr (ConjS (PredVP x X) (PredVP y Y)) = 
-    ifS (eqNP x y) 
-      (PredVP x (ConjVP X Y)) 
-      (ifS (eqVP X Y) 
-         (PredVP (ConjNP x y) X)
-         (ConjS (PredVP x X) (PredVP y Y))) ;
-  fun ifS : Bool -> S -> S -> S ; -- if b then x else y 
-  def
-    ifS True  x _ = x ;
-    ifS False _ y = y ;
-  fun eqNP : NP -> NP -> Bool ;  -- x == y
-  def 
-    eqNP John John = True ;
-    eqNP Mary Mary = True ;
-    eqNP _ _ = False ;
-  fun eqVP : VP -> VP -> Bool ;  -- X == Y
-  def 
-    eqVP Run  Run  = True ;
-    eqVP Walk Walk = True ;
-    eqVP _ _ = False ;
-  cat Bool ; data True, False : Bool ;
-}
diff --git a/book/examples/chapter6/AggregationEng.gf b/book/examples/chapter6/AggregationEng.gf
deleted file mode 100644
index 9ed403c79..000000000
--- a/book/examples/chapter6/AggregationEng.gf
+++ /dev/null
@@ -1,17 +0,0 @@
-concrete AggregationEng of Aggregation = {
-
-lincat S, NP, VP = Str ;
-
-lin 
-  PredVP x y = x ++ y ;
-  ConjS  a b = a ++ "or" ++ b ;
-  ConjVP a b = a ++ "or" ++ b ;
-  ConjNP a b = a ++ "or" ++ b ;
-
-  Run = "runs" ;
-  Walk = "walks" ;
-  John = "John" ;
-  Mary = "Mary" ;
-
-}
-
diff --git a/book/examples/chapter6/Arithm.gf b/book/examples/chapter6/Arithm.gf
deleted file mode 100644
index 685627745..000000000
--- a/book/examples/chapter6/Arithm.gf
+++ /dev/null
@@ -1,30 +0,0 @@
-abstract Arithm = {
-  cat
-    Prop ;                        -- proposition
-    Nat ;                         -- natural number
-  data
-    Zero : Nat ;                  -- 0
-    Succ : Nat -> Nat ;           -- the successor of x
-  fun
-    Even : Nat -> Prop ;          -- x is even
-    And  : Prop -> Prop -> Prop ; -- A and B
-
-  cat Less Nat Nat ; 
-  data LessZ : (y : Nat) -> Less Zero (Succ y) ;
-  data LessS : (x,y : Nat) -> Less x y -> Less (Succ x) (Succ y) ;
-
-  cat Span ;
-  data FromTo : (m,n : Nat) -> Less m n -> Span ;
-
-  fun one : Nat ;
-  def one = Succ Zero ;
-
-  fun twice : Nat -> Nat ;
-  def twice x = plus x x ;
-
-  fun plus : Nat -> Nat -> Nat ;
-  def 
-    plus x Zero = x ;
-    plus x (Succ y) = Succ (plus x y) ;
-
-} 
diff --git a/book/examples/chapter6/Bin.gf b/book/examples/chapter6/Bin.gf
deleted file mode 100644
index c181656f8..000000000
--- a/book/examples/chapter6/Bin.gf
+++ /dev/null
@@ -1,50 +0,0 @@
-abstract Bin = {
-
-cat Nat ; Bin ; Pos ;
-
-data 
-  Zero : Nat ; 
-  Succ : Nat -> Nat ;
-
-  BZero : Bin ;         -- 0
-  BPos  : Pos -> Bin ;  -- p
-  BOne  : Pos ;         -- 1
-  AZero : Pos -> Pos ;  -- p0
-  AOne  : Pos -> Pos ;  -- p1
-
-fun
-  bin2nat : Bin -> Nat ;
-def
-  bin2nat BZero = Zero ;
-  bin2nat (BPos p) = pos2nat p ;
-fun 
-  pos2nat : Pos -> Nat ;
-def
-  pos2nat BOne = one ;
-  pos2nat (AZero p) = twice (pos2nat p) ;
-  pos2nat (AOne  p) = Succ (twice (pos2nat p)) ;
-fun one : Nat ;
-def one = Succ Zero ;
-fun twice : Nat -> Nat ;
-def 
-  twice Zero = Zero ;
-  twice (Succ n) = Succ (Succ (twice n)) ;
-
-fun
-  nat2bin : Nat -> Bin ;
-def
-  nat2bin Zero = BZero ;
-  nat2bin (Succ n) = bSucc (nat2bin n) ;
-fun
-  bSucc : Bin -> Bin ;
-def
-  bSucc BZero = BPos BOne ;
-  bSucc (BPos p) = BPos (pSucc p) ;
-fun
-  pSucc : Pos -> Pos ;
-def
-  pSucc BOne = AZero BOne ;
-  pSucc (AZero p) = AOne p ;
-  pSucc (AOne p) = AZero (pSucc p) ;
-
-}
\ No newline at end of file
diff --git a/book/examples/chapter6/Classes.gf b/book/examples/chapter6/Classes.gf
deleted file mode 100644
index ac7430d25..000000000
--- a/book/examples/chapter6/Classes.gf
+++ /dev/null
@@ -1,28 +0,0 @@
-abstract Classes = {
-
-flags 
-  startcat = Command ;
-
-cat
-  Command ;
-  Kind ;
-  Class ;
-  Instance Class Kind ;
-  Action Class ;
-  Device Kind ;
-
-fun
-  Act  : (c : Class) -> (k : Kind) -> Instance c k -> Action c -> Device k -> Command ;
-  The : (k : Kind) -> Device k ;
-
-  Light, Fan : Kind ;
-  Switchable, Dimmable : Class ;
-  
-  SwitchOn, SwitchOff : Action Switchable ;
-  Dim : Action Dimmable ;
-
-  switchable_Light : Instance Switchable Light ;
-  switchable_Fan : Instance Switchable Fan ;
-  dimmable_Light : Instance Dimmable Light ;
-
-}
diff --git a/book/examples/chapter6/ClassesEng.gf b/book/examples/chapter6/ClassesEng.gf
deleted file mode 100644
index 5bdf80c35..000000000
--- a/book/examples/chapter6/ClassesEng.gf
+++ /dev/null
@@ -1,29 +0,0 @@
---# -path=.:present
-
-concrete ClassesEng of Classes = open SyntaxEng, ParadigmsEng in {
-
-lincat
-  Command = Utt ;
-  Kind = CN ;
-  Class = {} ;
-  Instance = {} ;
-  Action = V2 ;
-  Device = NP ;
-
-lin
-  Act _ _ _ a d = mkUtt (mkImp a d) ;
-  The k = mkNP the_Det k ;
-
-  Light = mkCN (mkN "light") ;
-  Fan = mkCN (mkN "fan") ;
-  Switchable, Dimmable = <> ;
-  
-  SwitchOn = mkV2 (partV (mkV "switch") "on") ;
-  SwitchOff = mkV2 (partV (mkV "switch") "off") ;
-  Dim = mkV2 (mkV "dim") ;
-
-  switchable_Light = <> ;
-  switchable_Fan = <> ;
-  dimmable_Light = <> ;
-
-}
diff --git a/book/examples/chapter6/DShopping.gf b/book/examples/chapter6/DShopping.gf
deleted file mode 100644
index a5a06e070..000000000
--- a/book/examples/chapter6/DShopping.gf
+++ /dev/null
@@ -1,24 +0,0 @@
-abstract DShopping = {
-  flags startcat = Comment ;
-  cat
-    Comment ; 
-    Dom ;
-    Item Dom ; 
-    Kind Dom ; 
-    Quality Dom ;
-  fun
-    DFood, DCloth : Dom ;
-
-    Pred : (d : Dom) -> Item d -> Quality d -> Comment ;
-    This, That : (d : Dom) -> Kind d -> Item d ;
-    Mod : (d : Dom) -> Quality d -> Kind d -> Kind d ;
-    Wine, Cheese, Fish : Kind DFood ;
-    Very : (d : Dom) -> Quality d -> Quality d ;
-    Fresh, Warm, Delicious, Boring : Quality DFood ;
-
-    Shirt, Jacket : Kind DCloth ;
-    Comfortable : Quality DCloth ;
-
-    Italian, Expensive, Elegant : (d : Dom) -> Quality d ;
-
-}
diff --git a/book/examples/chapter6/DShoppingEng.gf b/book/examples/chapter6/DShoppingEng.gf
deleted file mode 100644
index 3dc3a2cc2..000000000
--- a/book/examples/chapter6/DShoppingEng.gf
+++ /dev/null
@@ -1,33 +0,0 @@
---# -path=.:present
-
-concrete DShoppingEng of DShopping = open SyntaxEng, ParadigmsEng in {
-
-  lincat
-    Comment = Cl ; 
-    Item = NP ;
-    Kind = CN ;
-    Quality = AP ;
-  lin
-    Pred _ item quality = mkCl item quality ;
-    This _ kind = mkNP this_QuantSg kind ;
-    That _ kind = mkNP that_QuantSg kind ;
-    Mod _ quality kind = mkCN quality kind ;
-    Very _ quality = mkAP very_AdA quality ;
-
-    Shirt = mkCN (mkN "shirt") ;
-    Jacket = mkCN (mkN "jacket") ;
-    Wine = mkCN (mkN "wine") ;
-    Cheese = mkCN (mkN "cheese") ;
-    Fish = mkCN (mkN "fish" "fish") ;
-    Fresh = mkAP (mkA "fresh") ;
-    Warm = mkAP (mkA "warm") ;
-    Italian _ = mkAP (mkA "Italian") ;
-    Expensive _ = mkAP (mkA "expensive") ;
-    Elegant _ = mkAP (mkA "elegant") ;
-    Delicious = mkAP (mkA "delicious") ;
-    Boring = mkAP (mkA "boring") ;
-    Comfortable = mkAP (mkA "comfortable") ;
-
-    DFood, DCloth = {s = []} ;
-
-}
diff --git a/book/examples/chapter6/Nat.gf b/book/examples/chapter6/Nat.gf
deleted file mode 100644
index ba0dfe4a1..000000000
--- a/book/examples/chapter6/Nat.gf
+++ /dev/null
@@ -1,22 +0,0 @@
-abstract Nat = {
-  cat
-    Prop ;                        -- proposition
-    Nat ;                         -- natural number
-  data
-    Zero : Nat ;                  -- 0
-    Succ : Nat -> Nat ;           -- the successor of x
-  fun
-    Even : Nat -> Prop ;          -- x is even
-    And  : Prop -> Prop -> Prop ; -- A and B
-
-  fun one : Nat ;
-  def one = Succ Zero ;
-
-  fun twice : Nat -> Nat ;
-  def twice x = plus x x ;
-
-  fun plus : Nat -> Nat -> Nat ;
-  def 
-    plus x Zero = x ;
-    plus x (Succ y) = Succ (plus x y) ;
-}
diff --git a/book/examples/chapter6/Smart.gf b/book/examples/chapter6/Smart.gf
deleted file mode 100644
index 6fc3e0bc5..000000000
--- a/book/examples/chapter6/Smart.gf
+++ /dev/null
@@ -1,16 +0,0 @@
-abstract Smart = {
-
-  cat
-    Command ;
-    Kind ; 
-    Device Kind ; 
-    Action Kind ; 
-
-  fun 
-    Act : (k : Kind) -> Action k -> Device k -> Command ;
-    The : (k : Kind) -> Device k ;  -- the light
-    Light, Fan : Kind ;
-    Dim : Action Light ;
-    SwitchOn, SwitchOff : (k : Kind) -> Action k ;
-
-}
diff --git a/book/examples/chapter6/Verbs.gf b/book/examples/chapter6/Verbs.gf
deleted file mode 100644
index 371450aeb..000000000
--- a/book/examples/chapter6/Verbs.gf
+++ /dev/null
@@ -1,22 +0,0 @@
-abstract Verbs = {
-
-cat
-  S ; NP ; Subcat ; V Subcat ; Args Subcat ;
-
-fun
-  cIntr : Subcat ;
-  cTr   : Subcat ;
-  cS    : Subcat ;
-
-  aIntr : NP -> Args cIntr ;
-  aTr   : NP -> NP -> Args cTr ;
-  aS    : NP -> S  -> Args cS ;
-
-  pred  : (s : Subcat) -> V s -> Args s -> S ;
-
-  john, mary : NP ;
-  walk : V cIntr ;
-  love : V cTr ;
-  know : V cS ;
-
-}
\ No newline at end of file
diff --git a/book/examples/chapter6/VerbsEng.gf b/book/examples/chapter6/VerbsEng.gf
deleted file mode 100644
index b235178d9..000000000
--- a/book/examples/chapter6/VerbsEng.gf
+++ /dev/null
@@ -1,22 +0,0 @@
-concrete VerbsEng of Verbs = {
-
-lincat
-  S, NP, Subcat, V = Str ; Args = Str * Str ;
-
-lin
-  cIntr = [] ;
-  cTr   = [] ;
-  cS    = [] ;
-
-  aIntr su    = <su,[]> ;
-  aTr   su ob = <su,ob> ;
-  aS    su s  = <su,"that" ++ s> ;
-
-  pred _ v xs = xs.p1 ++ v ++ xs.p2 ;
-
-  john = "John" ; mary = "Mary" ;
-  walk = "walks" ;
-  love = "loves" ;
-  know = "knows" ;
-
-}