toy1 with classes and using resource API

1 files changed, 16 insertions, 4 deletions

diff --git a/examples/regulus/toy1/Toy1.gf b/examples/regulus/toy1/Toy1.gf
index 2478360b4..70fa5ce9f 100644
--- a/examples/regulus/toy1/Toy1.gf
+++ b/examples/regulus/toy1/Toy1.gf
@@ -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) ;
 
 }