From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 19 Feb 2003 14:04:17 +0000 (+0000)
Subject: - formalized proof engine status
X-Git-Tag: V_0_0_4_1~26
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e812d5d92dac3e2b82eec5a4b6b1033b458f3f3;p=helm.git

- 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 f2b2f2018..3f5b2f4cb 100644
--- 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 *)