summaryrefslogtreecommitdiff
path: root/examples/tutorial/smart
diff options
context:
space:
mode:
Diffstat (limited to 'examples/tutorial/smart')
-rw-r--r--examples/tutorial/smart/House.gf35
-rw-r--r--examples/tutorial/smart/HouseEng.gf76
-rw-r--r--examples/tutorial/smart/LexSmart.gf12
-rw-r--r--examples/tutorial/smart/LexSmartSwe.gf12
-rw-r--r--examples/tutorial/smart/Smart.gf47
-rw-r--r--examples/tutorial/smart/SmartEng.gf84
-rw-r--r--examples/tutorial/smart/SmartFre.gf95
-rw-r--r--examples/tutorial/smart/SmartI.gf50
-rw-r--r--examples/tutorial/smart/SmartSwe.gf5
9 files changed, 416 insertions, 0 deletions
diff --git a/examples/tutorial/smart/House.gf b/examples/tutorial/smart/House.gf
new file mode 100644
index 000000000..e156792f1
--- /dev/null
+++ b/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 ;
+
+
+}
+
diff --git a/examples/tutorial/smart/HouseEng.gf b/examples/tutorial/smart/HouseEng.gf
new file mode 100644
index 000000000..d36122c51
--- /dev/null
+++ b/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"
+ } ;
+
+
+}
+
diff --git a/examples/tutorial/smart/LexSmart.gf b/examples/tutorial/smart/LexSmart.gf
new file mode 100644
index 000000000..0bbe7aa7c
--- /dev/null
+++ b/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 ;
+
+}
diff --git a/examples/tutorial/smart/LexSmartSwe.gf b/examples/tutorial/smart/LexSmartSwe.gf
new file mode 100644
index 000000000..6a9ea38ef
--- /dev/null
+++ b/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" ;
+
+}
diff --git a/examples/tutorial/smart/Smart.gf b/examples/tutorial/smart/Smart.gf
new file mode 100644
index 000000000..f88b40f12
--- /dev/null
+++ b/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) ;
+
+}
+
diff --git a/examples/tutorial/smart/SmartEng.gf b/examples/tutorial/smart/SmartEng.gf
new file mode 100644
index 000000000..384e50060
--- /dev/null
+++ b/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 ;
+
+}
+
diff --git a/examples/tutorial/smart/SmartFre.gf b/examples/tutorial/smart/SmartFre.gf
new file mode 100644
index 000000000..c5d903519
--- /dev/null
+++ b/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 [] ;
+
+}
+
diff --git a/examples/tutorial/smart/SmartI.gf b/examples/tutorial/smart/SmartI.gf
new file mode 100644
index 000000000..2b46ba0fe
--- /dev/null
+++ b/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 [] ;
+
+
+}
diff --git a/examples/tutorial/smart/SmartSwe.gf b/examples/tutorial/smart/SmartSwe.gf
new file mode 100644
index 000000000..a537639d6
--- /dev/null
+++ b/examples/tutorial/smart/SmartSwe.gf
@@ -0,0 +1,5 @@
+--# -path=.:alltenses:prelude
+
+concrete SmartSwe of Smart = SmartI with
+ (Syntax = SyntaxSwe),
+ (LexSmart = LexSmartSwe) ;
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 12:55:44 +0000