msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

toy1 with classes and using resource API

Browse Source
This commit is contained in:
aarne
2007-06-11 14:53:08 +00:00
parent 2b438a6284
commit 75a9ea71a2
9 changed files with 313 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
examples/regulus/toy1/Toy1.gf
View File

@@ -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) ;
}