blob: f88b40f125ae1be61dbbe9cad277c8f89ea28def (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
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) ;
}
|
