last adjustments of examples before course

examples/tutorial/smart/House.gf

@@ -0,0 +1,35 @@
+abstract House = {
+
+flags startcat = Utterance ;
+
+cat 
+  Utterance ; 
+  Command ; 
+  Question ; 
+  Kind ; 
+  Action Kind ; 
+  Device Kind ; 
+  Location ;
+
+fun
+  UCommand  : Command -> Utterance ;
+  UQuestion : Question -> Utterance ;
+
+  CAction : (k : Kind) -> Action k -> Device k -> Command ;
+  QAction : (k : Kind) -> Action k -> Device k -> Question ;
+
+  DKindOne  : (k : Kind) -> Device k ;
+  DKindMany : (k : Kind) -> Device k ;
+  DLoc  : (k : Kind) -> Device k -> Location -> Device k ;
+
+  light, fan : Kind ;
+
+  switchOn, switchOff : (k : Kind) -> Action k ;
+
+  dim : Action light ;
+
+  kitchen, livingRoom : Location ;
+  
+
+}
+

examples/tutorial/smart/HouseEng.gf

@@ -0,0 +1,76 @@
+--# -path=.:prelude
+
+concrete HouseEng of House = open Prelude in {
+
+-- grammar Toy1 from the Regulus book
+
+flags startcat = Utterance ;
+
+param
+  Number = Sg | Pl ;
+  VForm = VImp | VPart ;
+
+lincat 
+  Utterance = SS ;
+  Command = SS ;
+  Question = SS ;
+  Kind = {s : Number => Str} ; 
+  Action = {s : VForm => Str ; part : Str} ;
+  Device = {s : Str ; n : Number} ;
+  Location = SS ;
+
+lin
+  UCommand  c = c ;
+  UQuestion q = q ;
+
+  CAction _ act dev = ss (act.s ! VImp ++ bothWays act.part dev.s) ;
+  QAction _ act dev = ss (be dev.n ++ dev.s ++ act.s ! VPart ++ act.part) ;
+
+  DKindOne  k = {
+    s = "the" ++ k.s ! Sg ; 
+    n = Sg
+    } ;
+  DKindMany k = {
+    s = "the" ++ k.s ! Pl ; 
+    n = Pl
+    } ;
+  DLoc _ dev loc = {
+    s = dev.s ++ "in" ++ "the" ++ loc.s ; 
+    n = dev.n
+    } ;
+
+  light = mkNoun "light" ;
+  fan = mkNoun "fan" ;
+
+  switchOn _ = mkVerb "switch" "switched" "on" ;
+  switchOff _ = mkVerb "switch" "switched" "off" ;
+
+  dim = mkVerb "dim" "dimmed" [] ;
+
+  kitchen = ss "kitchen" ;
+  livingRoom = ss ["living room"] ;
+  
+oper
+  mkNoun : Str -> {s : Number => Str} = \dog -> {
+    s = table {
+      Sg => dog ;
+      Pl => dog + "s"
+      }
+    } ;
+  
+  mkVerb : (_,_,_ : Str) -> {s : VForm => Str ; part : Str} = \go,gone,away -> {
+    s = table {
+      VImp => go ;
+      VPart => gone
+      } ;
+    part = away
+    } ;
+
+  be : Number -> Str = \n -> case n of {
+    Sg => "is" ;
+    Pl => "are"
+    } ;
+
+
+}
+

examples/tutorial/smart/LexSmart.gf

@@ -0,0 +1,12 @@
+interface LexSmart = open Syntax in {
+
+oper
+  dim_V2 : V2 ;
+  fan_N : N ;
+  kitchen_N : N ;
+  light_N : N ;
+  livingRoom_N : N ;
+  switchOff_V2 : V2 ;
+  switchOn_V2 : V2 ;
+
+}

examples/tutorial/smart/LexSmartSwe.gf

@@ -0,0 +1,12 @@
+instance LexSmartSwe of LexSmart = open SyntaxSwe, ParadigmsSwe in {
+
+oper
+  dim_V2 = mkV2 "dämpa" ;
+  fan_N = mkN "fläkt" ;
+  kitchen_N = mkN "kök" neutrum ;
+  light_N = mkN "lampa" ;
+  livingRoom_N = mkN "vardagsrum" "vardagsrummet" "vardagsrum" "vardagsrummen" ;
+  switchOff_V2 = mkV2 "släcker" ;
+  switchOn_V2 = mkV2 "tänder" ;
+
+}

examples/tutorial/smart/Smart.gf

@@ -0,0 +1,47 @@
+abstract Smart = {
+
+flags startcat = Utterance ;
+
+cat 
+  Utterance ; 
+  Command ; 
+  Question ; 
+  Kind ; 
+  Action Kind ; 
+  Device Kind ; 
+  Location ;
+
+  Switchable Kind ;
+  Dimmable Kind ;
+  Statelike (k : Kind) (Action k) ;
+
+fun
+  UCommand  : Command -> Utterance ;
+  UQuestion : Question -> Utterance ;
+
+  CAction : (k : Kind) -> Action k -> Device k -> Command ;
+  QAction : (k : Kind) -> (a : Action k) -> Statelike k a -> Device k -> Question ;
+
+  DKindOne  : (k : Kind) -> Device k ;
+  DKindMany : (k : Kind) -> Device k ;
+  DLoc  : (k : Kind) -> Device k -> Location -> Device k ;
+
+  light, fan : Kind ;
+
+  switchOn, switchOff : (k : Kind) -> Switchable k -> Action k ;
+
+  dim : (k : Kind) -> Dimmable k -> Action k ;
+
+  kitchen, livingRoom : Location ;
+
+-- proof objects
+
+  switchable_light : Switchable light ;
+  switchable_fan : Switchable fan ;
+  dimmable_light : Dimmable light ;
+
+  statelike_switchOn  : (k : Kind) -> (s : Switchable k) -> Statelike k (switchOn k s) ;
+  statelike_switchOff : (k : Kind) -> (s : Switchable k) -> Statelike k (switchOff k s) ;
+
+}
+

examples/tutorial/smart/SmartEng.gf

@@ -0,0 +1,84 @@
+--# -path=.:prelude
+
+concrete Toy1Eng of Toy1 = open Prelude in {
+
+-- grammar Toy1 from the Regulus book
+
+flags startcat = Utterance ;
+
+param
+  Number = Sg | Pl ;
+  VForm = VImp | VPart ;
+
+lincat 
+  Utterance = SS ;
+  Command = SS ;
+  Question = SS ;
+  Kind = {s : Number => Str} ; 
+  Action = {s : VForm => Str ; part : Str} ;
+  Device = {s : Str ; n : Number} ;
+  Location = SS ;
+
+lin
+  UCommand  c = c ;
+  UQuestion q = q ;
+
+  CAction _ act dev = ss (act.s ! VImp ++ bothWays act.part dev.s) ;
+  QAction _ act st dev = ss (be dev.n ++ dev.s ++ act.s ! VPart ++ act.part ++ st.s) ;
+
+  DKindOne  k = {
+    s = "the" ++ k.s ! Sg ; 
+    n = Sg
+    } ;
+  DKindMany k = {
+    s = "the" ++ k.s ! Pl ; 
+    n = Pl
+    } ;
+  DLoc _ dev loc = {
+    s = dev.s ++ "in" ++ "the" ++ loc.s ; 
+    n = dev.n
+    } ;
+
+  light = mkNoun "light" ;
+  fan = mkNoun "fan" ;
+
+  switchOn _ _ = mkVerb "switch" "swithced" "on" ;
+  switchOff _ _ = mkVerb "switch" "swithced" "off" ;
+
+  dim _ _ = mkVerb "dim" "dimmed" [] ;
+
+  kitchen = ss "kitchen" ;
+  livingRoom = ss ["living room"] ;
+  
+oper
+  mkNoun : Str -> {s : Number => Str} = \dog -> {
+    s = table {
+      Sg => dog ;
+      Pl => dog + "s"
+      }
+    } ;
+  
+  mkVerb : (_,_,_ : Str) -> {s : VForm => Str ; part : Str} = \go,gone,away -> {
+    s = table {
+      VImp => go ;
+      VPart => gone
+      } ;
+    part = away
+    } ;
+
+  be : Number -> Str = \n -> case n of {
+    Sg => "is" ;
+    Pl => "are"
+    } ;
+
+  hidden : SS = ss [] ;
+lin
+  switchable_light = hidden ;
+  switchable_fan = hidden ;
+  dimmable_light = hidden ;
+
+  statelike_switchOn _ _ = hidden ;
+  statelike_switchOff _ _ = hidden ;
+
+}
+

examples/tutorial/smart/SmartFre.gf

@@ -0,0 +1,95 @@
+--# -path=.:prelude
+
+concrete Toy1Fre of Toy1 = open Prelude in {
+
+-- grammar Toy1 from the Regulus book
+
+flags startcat = Utterance ;
+
+param
+  Number = Sg | Pl ;
+  Gender = Masc | Fem ;
+  VForm  = VInf | VPart Gender Number ;
+
+lincat 
+  Utterance = SS ;
+  Command = SS ;
+  Question = SS ;
+  Kind = {s : Number => Str ; g : Gender} ; 
+  Action = {s : VForm => Str} ;
+  Device = {s : Str ; g : Gender ; n : Number} ;
+  Location = {s : Number => Str ; g : Gender} ; 
+
+lin
+  UCommand  c = c ;
+  UQuestion q = q ;
+
+  CAction _ act dev = ss (act.s ! VInf ++ dev.s) ;
+  QAction _ act st dev = 
+    ss (dev.s ++ est dev.g dev.n ++ act.s ! VPart dev.g dev.n ++ st.s) ;
+
+  DKindOne  k = {
+    s = defArt k.g ++ k.s ! Sg ; 
+    g = k.g ;
+    n = Sg
+    } ;
+  DKindMany k = {
+    s = "les" ++ k.s ! Pl ; 
+    g = k.g ;
+    n = Pl
+    } ;
+  DLoc _ dev loc = {
+    s = dev.s ++ "dans" ++ defArt loc.g ++ loc.s ! Sg ;
+    g = dev.g ; 
+    n = dev.n
+    } ;
+
+  light = mkNoun "lampe" Fem ;
+  fan = mkNoun "ventilateur" Masc ;
+
+  switchOn _ _ = mkVerb "allumer" "allumé" ;
+  switchOff _ _ = mkVerb "éteindre" "éteint" ;
+
+  dim _ _ = mkVerb "baisser" "baissé" ;
+
+  kitchen = mkNoun "cuisine" Fem ;
+  livingRoom = mkNoun "salon" Masc ;
+  
+oper
+  mkNoun : Str -> Gender -> {s : Number => Str ; g : Gender} = \dog,g -> {
+    s = table {
+      Sg => dog ;
+      Pl => dog + "s"
+      } ;
+    g = g
+    } ;
+  
+  mkVerb : (_,_ : Str) -> {s : VForm => Str} = \venir,venu -> {
+    s = table {
+      VInf => venir ;
+      VPart Masc Sg => venu ;
+      VPart Masc Pl => venu + "s" ;
+      VPart Fem  Sg => venu + "e" ;
+      VPart Fem  Pl => venu + "es"
+      }
+    } ;
+
+  est : Gender -> Number -> Str = \g,n -> case <g,n> of {
+    <Masc,Sg> => "est-il" ;
+    <Fem, Sg> => "est-elle" ;
+    <Masc,Pl> => "sont-ils" ;
+    <Fem, Pl> => "sont-elles"
+    } ;
+
+  defArt : Gender -> Str = \g -> case g of {Masc => "le" ; Fem => "la"} ;
+
+lin
+  switchable_light = ss [] ;
+  switchable_fan  = ss [] ;
+  dimmable_light  = ss [] ;
+
+  statelike_switchOn _ _ = ss [] ;
+  statelike_switchOff _ _ = ss [] ;
+
+}
+

examples/tutorial/smart/SmartI.gf

@@ -0,0 +1,50 @@
+--# -path=.:present:prelude
+
+incomplete concrete SmartI of Smart = open Syntax, LexSmart, Prelude in {
+
+-- grammar Toy1 from the Regulus book
+
+flags startcat = Utterance ;
+
+lincat 
+  Utterance = Utt ;
+  Command = Imp ;
+  Question = QS ;
+  Kind = N ;
+  Action = V2 ;
+  Device = NP ;
+  Location = N ;
+
+lin
+  UCommand  c = mkUtt politeImpForm c ;
+  UQuestion q = mkUtt q ;
+
+  CAction _ act dev = mkImp act dev ;
+  QAction _ act st dev = 
+    mkQS anteriorAnt (mkQCl (mkCl dev (passiveVP act))) ; ---- show empty proof
+
+  DKindOne k = mkNP defSgDet k ;
+  DKindMany k = mkNP defPlDet k ;
+  DLoc _ dev loc = mkNP dev (mkAdv in_Prep (mkNP defSgDet loc)) ;
+
+  light = light_N ;
+  fan = fan_N ;
+
+  switchOn _ _ = switchOn_V2 ;
+  switchOff _ _ = switchOff_V2 ;
+
+  dim _ _ = dim_V2 ;
+
+  kitchen = kitchen_N ;
+  livingRoom = livingRoom_N ;
+  
+lin
+  switchable_light = ss [] ;
+  switchable_fan  = ss [] ;
+  dimmable_light  = ss [] ;
+
+  statelike_switchOn _ _ = ss [] ;
+  statelike_switchOff _ _ = ss [] ;
+
+
+}

examples/tutorial/smart/SmartSwe.gf

@@ -0,0 +1,5 @@
+--# -path=.:alltenses:prelude
+
+concrete SmartSwe of Smart = SmartI with
+  (Syntax = SyntaxSwe),
+  (LexSmart = LexSmartSwe) ;