toy1 with classes and using resource API

9 files changed, 313 insertions, 8 deletions

diff --git a/examples/regulus/toy1/LexToy1.gf b/examples/regulus/toy1/LexToy1.gf
new file mode 100644
index 000000000..d48e43a3b
--- /dev/null
+++ b/examples/regulus/toy1/LexToy1.gf
@@ -0,0 +1,12 @@
+interface LexToy1 = 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 ;
+
+}
\ No newline at end of file
diff --git a/examples/regulus/toy1/LexToy1Swe.gf b/examples/regulus/toy1/LexToy1Swe.gf
new file mode 100644
index 000000000..3930a4728
--- /dev/null
+++ b/examples/regulus/toy1/LexToy1Swe.gf
@@ -0,0 +1,12 @@
+instance LexToy1Swe of LexToy1 = 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" ;
+
+}
diff --git a/examples/regulus/toy1/Toy1.gf b/examples/regulus/toy1/Toy1.gf
index 2478360b4..70fa5ce9f 100644
--- a/examples/regulus/toy1/Toy1.gf
+++ b/examples/regulus/toy1/Toy1.gf
@@ -11,12 +11,16 @@ cat
   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) -> Action k -> Device k -> Question ;
+  QAction : (k : Kind) -> (a : Action k) -> Statelike k a -> Device k -> Question ;
 
   DKindOne  : (k : Kind) -> Device k ;
   DKindMany : (k : Kind) -> Device k ;
@@ -24,12 +28,20 @@ fun
 
   light, fan : Kind ;
 
-  switchOn, switchOff : (k : Kind) -> Action k ;
+  switchOn, switchOff : (k : Kind) -> Switchable k -> Action k ;
 
-  dim : Action light ;
+  dim : (k : Kind) -> Dimmable k -> Action k ;
 
   kitchen, livingRoom : Location ;
-  
+
+-- proof objects
+
+  switchable_light : Switchable light ;
+  switchable_fan : Switchable fan ;
+  dimmable_fan : Dimmable fan ;
+
+  statelike_switchOn  : (k : Kind) -> (s : Switchable k) -> Statelike k (switchOn k s) ;
+  statelike_switchOff : (k : Kind) -> (s : Switchable k) -> Statelike k (switchOff k s) ;
 
 }
 
diff --git a/examples/regulus/toy1/Toy1Eng.gf b/examples/regulus/toy1/Toy1Eng.gf
index 1d71eabf1..30e861f44 100644
--- a/examples/regulus/toy1/Toy1Eng.gf
+++ b/examples/regulus/toy1/Toy1Eng.gf
@@ -24,7 +24,7 @@ lin
   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) ;
+  QAction _ act st dev = ss (be dev.n ++ dev.s ++ act.s ! VPart ++ act.part ++ st.s) ;
 
   DKindOne  k = {
     s = "the" ++ k.s ! Sg ; 
@@ -42,10 +42,10 @@ lin
   light = mkNoun "light" ;
   fan = mkNoun "fan" ;
 
-  switchOn _ = mkVerb "switch" "swithced" "on" ;
-  switchOff _ = mkVerb "switch" "swithced" "off" ;
+  switchOn _ _ = mkVerb "switch" "swithced" "on" ;
+  switchOff _ _ = mkVerb "switch" "swithced" "off" ;
 
-  dim = mkVerb "dim" "dimmed" [] ;
+  dim _ _ = mkVerb "dim" "dimmed" [] ;
 
   kitchen = ss "kitchen" ;
   livingRoom = ss ["living room"] ;
@@ -71,6 +71,14 @@ oper
     Pl => "are"
     } ;
 
+lin
+  switchable_light = ss [] ;
+  switchable_fan  = ss [] ;
+  dimmable_fan  = ss [] ;
+
+  statelike_switchOn _ _ = ss [] ;
+  statelike_switchOff _ _ = ss [] ;
+
 
 }
 
diff --git a/examples/regulus/toy1/Toy1Fre.gf b/examples/regulus/toy1/Toy1Fre.gf
new file mode 100644
index 000000000..73ac9aa97
--- /dev/null
+++ b/examples/regulus/toy1/Toy1Fre.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_fan  = ss [] ;
+
+  statelike_switchOn _ _ = ss [] ;
+  statelike_switchOff _ _ = ss [] ;
+
+}
+
diff --git a/examples/regulus/toy1/Toy1I.gf b/examples/regulus/toy1/Toy1I.gf
new file mode 100644
index 000000000..03193d5b7
--- /dev/null
+++ b/examples/regulus/toy1/Toy1I.gf
@@ -0,0 +1,50 @@
+--# -path=.:present:prelude
+
+incomplete concrete Toy1I of Toy1 = open Syntax, LexToy1, 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_fan  = ss [] ;
+
+  statelike_switchOn _ _ = ss [] ;
+  statelike_switchOff _ _ = ss [] ;
+
+
+}
diff --git a/examples/regulus/toy1/Toy1Swe.gf b/examples/regulus/toy1/Toy1Swe.gf
new file mode 100644
index 000000000..0e23994c8
--- /dev/null
+++ b/examples/regulus/toy1/Toy1Swe.gf
@@ -0,0 +1,5 @@
+--# -path=.:alltenses:prelude
+
+concrete Toy1Swe of Toy1 = Toy1I with
+  (Syntax = SyntaxSwe),
+  (LexToy1 = LexToy1Swe) ;
diff --git a/examples/regulus/toy1/Toy1a.gf b/examples/regulus/toy1/Toy1a.gf
new file mode 100644
index 000000000..2478360b4
--- /dev/null
+++ b/examples/regulus/toy1/Toy1a.gf
@@ -0,0 +1,35 @@
+abstract Toy1 = {
+
+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 ;
+  
+
+}
+
diff --git a/examples/regulus/toy1/Toy1aEng.gf b/examples/regulus/toy1/Toy1aEng.gf
new file mode 100644
index 000000000..1d71eabf1
--- /dev/null
+++ b/examples/regulus/toy1/Toy1aEng.gf
@@ -0,0 +1,76 @@
+--# -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 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" "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"
+    } ;
+
+
+}
+