gf-book/examples/chapter6/Classes.gf


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

abstract Classes = {

flags 
  startcat = Command ;

cat
  Command ;
  Kind ;
  Class ;
  Instance Class Kind ;
  Action Class ;
  Device Kind ;

fun
  Act  : (c : Class) -> (k : Kind) -> Instance c k -> Action c -> Device k -> Command ;
  The : (k : Kind) -> Device k ;

  Light, Fan : Kind ;
  Switchable, Dimmable : Class ;
  
  SwitchOn, SwitchOff : Action Switchable ;
  Dim : Action Dimmable ;

  switchable_Light : Instance Switchable Light ;
  switchable_Fan : Instance Switchable Fan ;
  dimmable_Light : Instance Dimmable Light ;

}