- formalized proof engine status

- formalized hints and hints list
- added Wow and Too_late broker -> tutor messages
- fixed Eureka message contents to carry a real life hint

diff --git a/helm/hbugs/common/hbugs_types.ml b/helm/hbugs/common/hbugs_types.ml
index f2b2f20189f372fe5be3f4bd5c3c87ad72c476ff..3f5b2f4cb5a4320f029bbe2e676047ba74f277f0 100644 (file)
--- a/helm/hbugs/common/hbugs_types.ml
+++ b/helm/hbugs/common/hbugs_types.ml
@@ -32,13 +32,29 @@ type musing_id = string
 type tutor_id = string
 type tutor_dsc = tutor_id * string  (* tutor id, tutor description *)
 
-type state = string             (* TODO stato del proof assistant *)
+type state =  (* proof assitant's state: proof type, proof body, goal *)
+  string * string * int
 
-type hint = string              (* TODO consiglio per l'utente *)
-type hint_type = string              (* TODO consiglio per l'utente *)
+type hint =
+    (* tactics usage related hints *)
+  | Use_ring_Luke
+  | Use_fourier_Luke
+  | Use_reflexivity_Luke
+  | Use_symmetry_Luke
+  | Use_assumption_Luke
+  | Use_contradiction_Luke
+  | Use_exists_Luke
+  | Use_split_Luke
+  | Use_left_Luke
+  | Use_right_Luke
+  | Use_apply_Luke of string        (* use apply tactic on embedded term *)
+    (* hints list *)
+  | Hints of hint list
+
+type hint_type = string              (* TODO tipo di consiglio per l'utente *)
 
 type musing_result =
-  | Eureka of string            (* extra information, if any, parsed depending
+  | Eureka of hint            (* extra information, if any, parsed depending
                                 on tutor's hint_type *)
   | Sorry
 
@@ -56,6 +72,7 @@ type message =
   | List_tutors of client_id                  (* client_id *)
   | Subscribe of client_id * tutor_id list    (* client id, tutor id list *)
   | State_change of client_id * state         (* client_id, new state *)
+  | Wow of client_id                          (* client_id *)
 
   (* tutor -> broker *)
   | Register_tutor of tutor_id * string * hint_type * string
@@ -83,4 +100,5 @@ type message =
   | Start_musing of broker_id * state         (* broker id, state *)
   | Abort_musing of broker_id * musing_id     (* broker id, musing id *)
   | Thanks of broker_id * musing_id           (* broker id, musing id *)
+  | Too_late of broker_id * musing_id         (* broker id, musing id *)