From 5e812d5d92dac3e2b82eec5a4b6b1033b458f3f3 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 19 Feb 2003 14:04:17 +0000 Subject: [PATCH] - 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 --- helm/hbugs/common/hbugs_types.ml | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) 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 *) -- 2.39.2