helm/hbugs/common/hbugs_types.ml

   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 = string             (* TODO stato del proof assistant *)
  36
  37 type hint = string              (* TODO consiglio per l'utente *)
  38 type hint_type = string              (* TODO consiglio per l'utente *)
  39
  40 type musing_result =
  41   | Eureka of string            (* extra information, if any, parsed depending
  42                                 on tutor's hint_type *)
  43   | Sorry
  44
  45   (* for each message, first component is an ID that identify the sender *)
  46 type message =
  47
  48   (* general purpose *)
  49   | Help  (* help request *)
  50   | Usage of string (* help response *)       (* usage string *)
  51   | Exception of string * string              (* name, value *)
  52
  53   (* client -> broker *)
  54   | Register_client of client_id * string     (* client id, client url *)
  55   | Unregister_client of client_id            (* client id *)
  56   | List_tutors of client_id                  (* client_id *)
  57   | Subscribe of client_id * tutor_id list    (* client id, tutor id list *)
  58   | State_change of client_id * state         (* client_id, new state *)
  59
  60   (* tutor -> broker *)
  61   | Register_tutor of tutor_id * string * hint_type * string
  62                                               (* tutor id, tutor url, hint type,
  63                                               tutor description *)
  64   | Unregister_tutor of tutor_id              (* tutor id *)
  65   | Musing_started of tutor_id * musing_id    (* tutor id, musing id *)
  66   | Musing_aborted of tutor_id * musing_id    (* tutor id, musing id *)
  67   | Musing_completed of tutor_id * musing_id * musing_result
  68                                               (* tutor id, musing id, result *)
  69
  70   (* broker -> client *)
  71   | Client_registered of broker_id            (* broker id *)
  72   | Client_unregistered of broker_id          (* broker id *)
  73   | Tutor_list of broker_id * tutor_dsc list  (* broker id, tutor list *)
  74   | Subscribed of broker_id * tutor_id list   (* broker id, tutor list *)
  75   | State_accepted of broker_id * musing_id list * musing_id list
  76                                               (* broker id, stopped musing ids,
  77                                               started musing ids *)
  78   | Hint of broker_id * hint                  (* broker id, hint *)
  79
  80   (* broker -> tutor *)
  81   | Tutor_registered of broker_id             (* broker id *)
  82   | Tutor_unregistered of broker_id           (* broker id *)
  83   | Start_musing of broker_id * state         (* broker id, state *)
  84   | Abort_musing of broker_id * musing_id     (* broker id, musing id *)
  85   | Thanks of broker_id * musing_id           (* broker id, musing id *)
  86