helm/ocaml/hbugs/hbugs_types.mli

   1 (*
   2  * Copyright (C) 2003:
   3  *    Stefano Zacchiroli <zack@cs.unibo.it>
   4  *    for the HELM Team http://helm.cs.unibo.it/
   5  *
   6  *  This file is part of HELM, an Hypertextual, Electronic
   7  *  Library of Mathematics, developed at the Computer Science
   8  *  Department, University of Bologna, Italy.
   9  *
  10  *  HELM is free software; you can redistribute it and/or
  11  *  modify it under the terms of the GNU General Public License
  12  *  as published by the Free Software Foundation; either version 2
  13  *  of the License, or (at your option) any later version.
  14  *
  15  *  HELM is distributed in the hope that it will be useful,
  16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
  17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  18  *  GNU General Public License for more details.
  19  *
  20  *  You should have received a copy of the GNU General Public License
  21  *  along with HELM; if not, write to the Free Software
  22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  23  *  MA  02111-1307, USA.
  24  *
  25  *  For details, see the HELM World-Wide-Web page,
  26  *  http://helm.cs.unibo.it/
  27  *)
  28
  29 type broker_id = string
  30 type client_id = string
  31 type musing_id = string
  32 type tutor_id = string
  33 type tutor_dsc = tutor_id * string  (* tutor id, tutor description *)
  34
  35 type state =  (* proof assitant's state: proof type, proof body, goal *)
  36   string * string * int
  37
  38 type hint =
  39     (* tactics usage related hints *)
  40   | Use_ring
  41   | Use_fourier
  42   | Use_reflexivity
  43   | Use_symmetry
  44   | Use_assumption
  45   | Use_contradiction
  46   | Use_exists
  47   | Use_split
  48   | Use_left
  49   | Use_right
  50   | Use_apply of string        (* use apply tactic on embedded term *)
  51     (* hints list *)
  52   | Hints of hint list
  53
  54 type hint_type = string              (* TODO tipo di consiglio per l'utente *)
  55
  56 type musing_result =
  57   | Eureka of hint            (* extra information, if any, parsed depending
  58                                 on tutor's hint_type *)
  59   | Sorry
  60
  61   (* for each message, first component is an ID that identify the sender *)
  62 type message =
  63
  64   (* general purpose *)
  65   | Help  (* help request *)
  66   | Usage of string (* help response *)       (* usage string *)
  67   | Exception of string * string              (* name, value *)
  68
  69   (* client -> broker *)
  70   | Register_client of client_id * string     (* client id, client url *)
  71   | Unregister_client of client_id            (* client id *)
  72   | List_tutors of client_id                  (* client_id *)
  73   | Subscribe of client_id * tutor_id list    (* client id, tutor id list *)
  74   | State_change of client_id * state option  (* client_id, new state *)
  75   | Wow of client_id                          (* client_id *)
  76
  77   (* tutor -> broker *)
  78   | Register_tutor of tutor_id * string * hint_type * string
  79                                               (* tutor id, tutor url, hint type,
  80                                               tutor description *)
  81   | Unregister_tutor of tutor_id              (* tutor id *)
  82   | Musing_started of tutor_id * musing_id    (* tutor id, musing id *)
  83   | Musing_aborted of tutor_id * musing_id    (* tutor id, musing id *)
  84   | Musing_completed of tutor_id * musing_id * musing_result
  85                                               (* tutor id, musing id, result *)
  86
  87   (* broker -> client *)
  88   | Client_registered of broker_id            (* broker id *)
  89   | Client_unregistered of broker_id          (* broker id *)
  90   | Tutor_list of broker_id * tutor_dsc list  (* broker id, tutor list *)
  91   | Subscribed of broker_id * tutor_id list   (* broker id, tutor list *)
  92   | State_accepted of broker_id * musing_id list * musing_id list
  93                                               (* broker id, stopped musing ids,
  94                                               started musing ids *)
  95   | Hint of broker_id * hint                  (* broker id, hint *)
  96
  97   (* broker -> tutor *)
  98   | Tutor_registered of broker_id             (* broker id *)
  99   | Tutor_unregistered of broker_id           (* broker id *)
 100   | Start_musing of broker_id * state         (* broker id, state *)
 101   | Abort_musing of broker_id * musing_id     (* broker id, musing id *)
 102   | Thanks of broker_id * musing_id           (* broker id, musing id *)
 103   | Too_late of broker_id * musing_id         (* broker id, musing id *)
 104