diff options
Diffstat (limited to 'examples-3.0/tutorial/smart/Smart.gf')
| -rw-r--r-- | examples-3.0/tutorial/smart/Smart.gf | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/examples-3.0/tutorial/smart/Smart.gf b/examples-3.0/tutorial/smart/Smart.gf new file mode 100644 index 000000000..f88b40f12 --- /dev/null +++ b/examples-3.0/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) ; + +} + |