helm/hbugs/common/hbugs_types.ml

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