--- /dev/null
+*.cmi
+*.cmo
+*.cma
+*.cmx
+*.o
+*.a
--- /dev/null
+<!--
+ Data used to fill template "hbugs_tutor.TPL.ml"
+
+ @ADDR@ tutor ip address
+ @PORT@ tutor tcp port
+ @TACTIC@ tactic to use (OCaml function, must have type
+ ProofEngineTypes.tactic)
+ @HINT@ hint to be sent to client (content of Hbugs_types.Eureka
+ type constructor, must have type Hbugs_types.hint, see
+ hbugs_types.ml)
+ @HINT_TYPE@ hint type (3rd argument of Hbugs_types.Register_tutor type
+ constructor, must have type Hbugs_types.hint_type)
+ @DESCRIPTION@ human readable tutor description
+
+ "source" attribute corresponding OCaml source file
+
+ INVARIANT: XML element name below are lowercase version of @TAGS@ used in
+ template
+
+ TODO: hint type isn't yet well formalized
+-->
+
+<tutors>
+ <tutor source="ring_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50001</port>
+ <tactic>Ring.ring_tac</tactic>
+ <hint>Hbugs_types.Use_ring_Luke</hint>
+ <hint_type>Use Ring Luke</hint_type>
+ <description>Ring tutor</description>
+ </tutor>
+ <tutor source="fourier_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50002</port>
+ <tactic>FourierR.fourier_tac</tactic>
+ <hint>Hbugs_types.Use_fourier_Luke</hint>
+ <hint_type>Use Fourier Luke</hint_type>
+ <description>Fourier tutor</description>
+ </tutor>
+ <tutor source="reflexivity_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50003</port>
+ <tactic>EqualityTactics.reflexivity_tac</tactic>
+ <hint>Hbugs_types.Use_reflexivity_Luke</hint>
+ <hint_type>Use Reflexivity Luke</hint_type>
+ <description>Reflexivity tutor</description>
+ </tutor>
+ <tutor source="symmetry_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50004</port>
+ <tactic>EqualityTactics.symmetry_tac</tactic>
+ <hint>Hbugs_types.Use_symmetry_Luke</hint>
+ <hint_type>Use Symmetry Luke</hint_type>
+ <description>Symmetry tutor</description>
+ </tutor>
+ <tutor source="assumption_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50005</port>
+ <tactic>VariousTactics.assumption_tac</tactic>
+ <hint>Hbugs_types.Use_assumption_Luke</hint>
+ <hint_type>Use Assumption Luke</hint_type>
+ <description>Assumption tutor</description>
+ </tutor>
+ <tutor source="contradiction_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50006</port>
+ <tactic>NegationTactics.contradiction_tac</tactic>
+ <hint>Hbugs_types.Use_contradiction_Luke</hint>
+ <hint_type>Use Contradiction Luke</hint_type>
+ <description>Contradiction tutor</description>
+ </tutor>
+ <tutor source="exists_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50007</port>
+ <tactic>IntroductionTactics.exists_tac</tactic>
+ <hint>Hbugs_types.Use_exists_Luke</hint>
+ <hint_type>Use Exists Luke</hint_type>
+ <description>Exists tutor</description>
+ </tutor>
+ <tutor source="split_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50008</port>
+ <tactic>IntroductionTactics.split_tac</tactic>
+ <hint>Hbugs_types.Use_split_Luke</hint>
+ <hint_type>Use Split Luke</hint_type>
+ <description>Split tutor</description>
+ </tutor>
+ <tutor source="left_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50009</port>
+ <tactic>IntroductionTactics.left_tac</tactic>
+ <hint>Hbugs_types.Use_left_Luke</hint>
+ <hint_type>Use Left Luke</hint_type>
+ <description>Left tutor</description>
+ </tutor>
+ <tutor source="right_tutor.ml">
+ <addr>127.0.0.1</addr>
+ <port>50010</port>
+ <tactic>IntroductionTactics.right_tac</tactic>
+ <hint>Hbugs_types.Use_right_Luke</hint>
+ <hint_type>Use Right Luke</hint_type>
+ <description>Right tutor</description>
+ </tutor>
+ <tutor source="search_pattern_apply_tutor.ml">
+ <no_auto />
+ <addr>127.0.0.1</addr>
+ <port>50011</port>
+ <tactic>PrimitiveTactics.apply_tac</tactic>
+ <hint>Hbugs_types.Use_apply_Luke</hint>
+ <hint_type>Use Apply Luke (with argument)</hint_type>
+ <description>Search pattern apply tutor</description>
+ </tutor>
+</tutors>
+
--- /dev/null
+METADIR = ../meta
+REQUIRES = threads hbugs-common helm-cic_proof_checking helm-tactics helm-getter
+COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
+OCAMLFIND = ocamlfind
+OCAMLC = $(OCAMLFIND) ocamlc $(COMMONOPTS)
+OCAMLOPT = $(OCAMLFIND) opt $(COMMONOPTS)
+LINK_OPTIONS = -thread -package threads -linkpkg
+TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
+TUTORS_INDEX = INDEX.xml
+GENERATED_TUTORS = \
+ ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \
+ assumption_tutor contradiction_tutor exists_tutor split_tutor \
+ left_tutor right_tutor
+TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor
+BUILD_TUTORS = ./build_tutors.ml
+CTL = ./sabba.sh
+TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS))
+GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS))
+COMMON = hbugs_tutors_common.cmo
+COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON))
+
+all: byte
+world: byte opt
+byte: $(TUTORS)
+opt: $(TUTORS_OPT)
+start:
+ $(CTL) start
+stop:
+ $(CTL) stop
+
+$(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX)
+ $(BUILD_TUTORS)
+%_tutor: $(COMMON) %_tutor.ml
+ $(OCAMLC) $(LINK_OPTIONS) -o $@ $^
+%_tutor.opt: $(COMMON_OPT) %_tutor.ml
+ $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $^
+
+hbugs_tutors_common.cmi: hbugs_tutors_common.mli
+ $(OCAMLC) -c $<
+$(COMMON): hbugs_tutors_common.ml hbugs_tutors_common.cmi
+ $(OCAMLC) -c $<
+$(COMMON_OPT): hbugs_tutors_common.ml
+ $(OCAMLOPT) -c $<
+
+clean:
+ rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC)
+distclean: clean
+ rm -f run/*
+.PHONY: all world byte opt clean start stop
+
--- /dev/null
+#!/usr/bin/ocamlrun /usr/bin/ocaml
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * for the HELM Team http://helm.cs.unibo.it/
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+#use "topfind";;
+#require "pcre";;
+#require "pxp";;
+open Printf;;
+open Pxp_document;;
+open Pxp_dtd;;
+open Pxp_types;;
+open Pxp_yacc;;
+
+let index = "INDEX.xml" ;;
+let template = "hbugs_tutor.TPL.ml" ;;
+
+ (* apply a set of regexp substitutions specified as a list of pairs
+ <pattern,template> to a string *)
+let rec apply_subst ~fill s =
+ match fill with
+ | [] -> s
+ | (pat, templ)::rest ->
+ apply_subst ~fill:rest (Pcre.replace ~pat ~templ s)
+;;
+ (* fill a ~template file with substitutions specified in ~fill (see
+ apply_subst) and save output to ~output *)
+let fill_template ~template ~fill ~output =
+ printf "Creating %s ... " output; flush stdout;
+ let (ic, oc) = (open_in template, open_out output) in
+ let rec fill_template' () =
+ output_string oc ((apply_subst ~fill (input_line ic)) ^ "\n");
+ fill_template' ()
+ in
+ try
+ output_string oc (sprintf
+"(*
+ THIS CODE IS GENERATED - DO NOT MODIFY!
+
+ the source of this code is template \"%s\"
+ the template was filled with data read from \"%s\"
+*)\n"
+ template index);
+ fill_template' ()
+ with End_of_file ->
+ close_in ic;
+ close_out oc;
+ printf "done!\n"; flush stdout
+;;
+let parse_xml fname =
+ parse_wfdocument_entity default_config (from_file fname) default_spec
+;;
+let is_tutor node =
+ match node#node_type with T_element "tutor" -> true | _ -> false
+;;
+let is_element node =
+ match node#node_type with T_element _ -> true | _ -> false
+;;
+exception Skip;;
+let main () =
+ (parse_xml index)#root#iter_nodes
+ (fun node ->
+ try
+ (match node with
+ | node when is_tutor node ->
+ (try (* skip hand-written tutors *)
+ ignore (find_element "no_auto" node);
+ raise Skip
+ with Not_found -> ());
+ let output =
+ try
+ (match node#attribute "source" with
+ | Value s -> s
+ | _ -> assert false)
+ with Not_found -> assert false
+ in
+ let fill =
+ List.map (* create substitution list from index data *)
+ (fun node ->
+ let name = (* node name *)
+ (match node#node_type with
+ | T_element s -> s
+ | _ -> assert false)
+ in
+ let value = node#data in (* node value *)
+ (sprintf "@%s@" (String.uppercase name), (* pattern *)
+ value)) (* substitution *)
+ (List.filter is_element node#sub_nodes)
+ in
+ fill_template ~fill ~template ~output
+ | _ -> ())
+ with Skip -> ())
+;;
+main ();;
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * for the HELM Team http://helm.cs.unibo.it/
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+module TutorDescription =
+ struct
+ let addr = "@ADDR@"
+ let port = @PORT@
+ let tactic = @TACTIC@
+ let hint = @HINT@
+ let hint_type = "@HINT_TYPE@"
+ let description = "@DESCRIPTION@"
+ end
+;;
+module Tutor = Hbugs_tutors_common.BuildTutor (TutorDescription) ;;
+Tutor.start () ;;
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * for the HELM Team http://helm.cs.unibo.it/
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Hbugs_types;;
+open Printf;;
+
+let broker_url = "localhost:49081/act";;
+
+let init_tutor = Hbugs_id_generator.new_tutor_id;;
+
+ (** register a tutor to broker *)
+let register_to_broker id url hint_type dsc =
+ try
+ let res =
+ Hbugs_messages.submit_req
+ ~url:broker_url (Register_tutor (id, url, hint_type, dsc))
+ in
+ (match res with
+ | Tutor_registered id ->
+ prerr_endline (sprintf "Tutor registered, broker id: %s" id);
+ id
+ | unexpected_msg ->
+ raise (Hbugs_messages.Unexpected_message unexpected_msg))
+ with e ->
+ failwith (sprintf "Can't register tutor to broker: uncaught exception: %s"
+ (Printexc.to_string e))
+;;
+ (** unregister a tutor from the broker *)
+let unregister_from_broker id =
+ let res = Hbugs_messages.submit_req ~url:broker_url (Unregister_tutor id) in
+ match res with
+ | Tutor_unregistered _ -> prerr_endline "Tutor unregistered!"
+ | unexpected_msg ->
+ failwith
+ (sprintf "Can't unregister from broker, received unexpected msg: %s"
+ (Hbugs_messages.string_of_msg unexpected_msg))
+;;
+
+ (* typecheck a loaded proof *)
+ (* TODO this is a cut and paste from gTopLevel.ml *)
+let typecheck_loaded_proof metasenv bo ty =
+ let module T = CicTypeChecker in
+ ignore (
+ List.fold_left
+ (fun metasenv ((_,context,ty) as conj) ->
+ ignore (T.type_of_aux' metasenv context ty) ;
+ metasenv @ [conj]
+ ) [] metasenv) ;
+ ignore (T.type_of_aux' metasenv [] ty) ;
+ ignore (T.type_of_aux' metasenv [] bo)
+;;
+
+type xml_kind = Body | Type;;
+let mk_dtdname ~ask_dtd_to_the_getter dtd =
+ if ask_dtd_to_the_getter then
+ Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+ else
+ "http://mowgli.cs.unibo.it/dtd/" ^ dtd
+;;
+ (** this function must be the inverse function of GTopLevel.strip_xml_headings
+ *)
+let add_xml_headings ~kind s =
+ let dtdname = mk_dtdname ~ask_dtd_to_the_getter:true "cic.dtd" in
+ let root =
+ match kind with
+ | Body -> "CurrentProof"
+ | Type -> "ConstantType"
+ in
+ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ^
+ "<!DOCTYPE " ^ root ^ " SYSTEM \""^ dtdname ^ "\">\n\n" ^
+ s
+;;
+
+let load_state (type_string, body_string, goal) =
+ prerr_endline "a0";
+ let ((tmp1, oc1), (tmp2, oc2)) =
+ (Filename.open_temp_file "" "", Filename.open_temp_file "" "")
+ in
+ prerr_endline "a1";
+ output_string oc1 (add_xml_headings ~kind:Type type_string);
+ output_string oc2 (add_xml_headings ~kind:Body body_string);
+ close_out oc1; close_out oc2;
+ prerr_endline (sprintf "Proof Type available in %s" tmp1);
+ prerr_endline (sprintf "Proof Body available in %s" tmp2);
+ let (proof, goal) =
+ prerr_endline "a2";
+ (match CicParser.obj_of_xml tmp1 (Some tmp2) with
+ | Cic.CurrentProof (_,metasenv,bo,ty,_) -> (* TODO il primo argomento e' una URI valida o e' casuale? *)
+ prerr_endline "a3";
+ let uri = UriManager.uri_of_string "cic:/foo.con" in
+ prerr_endline "a4";
+ typecheck_loaded_proof metasenv bo ty;
+ prerr_endline "a5";
+ ((uri, metasenv, bo, ty), goal)
+ | _ -> assert false)
+ in
+ prerr_endline "a6";
+ Sys.remove tmp1; Sys.remove tmp2;
+ (proof, goal)
+
+(* tutors creation stuff from now on *)
+
+module type HbugsTutor =
+ sig
+ val start: unit -> unit
+ end
+
+module type HbugsTutorDescription =
+ sig
+ val addr: string
+ val port: int
+ val tactic: ProofEngineTypes.tactic
+ val hint: hint
+ val hint_type: hint_type
+ val description: string
+ end
+
+module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
+ struct
+ let broker_id = ref None
+ let my_own_id = init_tutor ()
+ let my_own_addr, my_own_port = Dsc.addr, Dsc.port
+ let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
+
+ let is_authenticated id =
+ match !broker_id with
+ | None -> false
+ | Some broker_id -> id = broker_id
+
+ (* thread who do the dirty work *)
+ let slave (state, musing_id) =
+ prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
+ let (proof, goal) = load_state state in
+ let success =
+ try
+ ignore (Dsc.tactic (proof, goal));
+ true
+ with e -> false
+ in
+ let answer =
+ Musing_completed
+ (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry))
+ in
+ ignore (Hbugs_messages.submit_req ~url:broker_url answer);
+ prerr_endline
+ (sprintf "Bye, I've completed my duties (success = %b)" success)
+
+ let hbugs_callback =
+ let forbidden () =
+ prerr_endline "ignoring request from unauthorized broker";
+ Exception ("forbidden", "")
+ in
+ function
+ | Start_musing (broker_id, state) ->
+ if is_authenticated broker_id then begin
+ prerr_endline "received Start_musing";
+ let new_musing_id = Hbugs_id_generator.new_musing_id () in
+ prerr_endline
+ (sprintf "starting a new musing (id = %s)" new_musing_id);
+ ignore (Thread.create slave (state, new_musing_id));
+ Musing_started (my_own_id, new_musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | Abort_musing (broker_id, musing_id) ->
+ if is_authenticated broker_id then begin
+ prerr_endline "Ignoring 'Abort_musing' message ...";
+ Musing_aborted (my_own_id, musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | unexpected_msg ->
+ Exception ("unexpected_msg",
+ Hbugs_messages.string_of_msg unexpected_msg)
+
+ let callback (req: Http_types.request) outchan =
+ try
+ let req_msg = Hbugs_messages.msg_of_string req#body in
+ let answer = hbugs_callback req_msg in
+ Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
+ with Hbugs_messages.Parse_error (subj, reason) ->
+ Http_daemon.respond
+ ~body:(Hbugs_messages.string_of_msg
+ (Exception ("parse_error", reason)))
+ outchan
+
+ let main () =
+ try
+ Sys.catch_break true;
+ at_exit (fun () -> unregister_from_broker my_own_id);
+ broker_id :=
+ Some (register_to_broker
+ my_own_id my_own_url Dsc.hint_type Dsc.description);
+ Http_daemon.start'
+ ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
+ with Sys.Break -> () (* exit nicely, invoking at_exit functions *)
+
+ let start = main
+
+ end
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * for the HELM Team http://helm.cs.unibo.it/
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Hbugs_types;;
+
+val broker_url: string
+
+val register_to_broker:
+ tutor_id -> string -> hint_type -> string ->
+ broker_id
+val unregister_from_broker: tutor_id -> unit
+
+val init_tutor: unit -> tutor_id
+val load_state:
+ Hbugs_types.state ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal
+
+module type HbugsTutor =
+ sig
+ val start: unit -> unit
+ end
+
+module type HbugsTutorDescription =
+ sig
+ val addr: string
+ val port: int
+ val tactic: ProofEngineTypes.tactic
+ val hint: hint
+ val hint_type: hint_type
+ val description: string
+ end
+
+module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor
+
--- /dev/null
+#!/usr/bin/ocamlrun /usr/bin/ocaml
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * for the HELM Team http://helm.cs.unibo.it/
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+#use "topfind";;
+#require "pxp";;
+open Printf;;
+open Pxp_document;;
+open Pxp_dtd;;
+open Pxp_types;;
+open Pxp_yacc;;
+
+let index = "INDEX.xml" ;;
+let parse_xml fname =
+ parse_wfdocument_entity default_config (from_file fname) default_spec
+;;
+let is_tutor node =
+ match node#node_type with T_element "tutor" -> true | _ -> false
+;;
+let main () =
+ List.iter
+ (fun tutor ->
+ try
+ (match tutor#attribute "source" with
+ | Value s -> print_endline s
+ | _ -> assert false)
+ with Not_found -> assert false)
+ (List.filter is_tutor (parse_xml index)#root#sub_nodes)
+;;
+main ();;
+
--- /dev/null
+#!/bin/sh
+# Copyright (C) 2003:
+# Stefano Zacchiroli <zack@cs.unibo.it>
+# for the HELM Team http://helm.cs.unibo.it/
+#
+# This file is part of HELM, an Hypertextual, Electronic
+# Library of Mathematics, developed at the Computer Science
+# Department, University of Bologna, Italy.
+#
+# HELM is free software; you can redistribute it and/or
+# modify it under the terms of the GNU General Public License
+# as published by the Free Software Foundation; either version 2
+# of the License, or (at your option) any later version.
+#
+# HELM is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with HELM; if not, write to the Free Software
+# Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+# MA 02111-1307, USA.
+#
+# For details, see the HELM World-Wide-Web page,
+# http://helm.cs.unibo.it/
+if [ "$1" = "--help" -o "$1" = "" ]; then
+ echo "sabba.sh { start | stop | --help }"
+ exit 0
+fi
+. ../../script.sh
+./ls_tutors.ml |
+while read line; do
+ tutor=`echo $line | sed 's/\.ml//'`
+ if [ "$1" = "stop" ]; then
+ echo -n "Stopping HBugs tutor $tutor ... "
+ killall $tutor
+ echo "done!"
+ elif [ "$1" = "start" ]; then
+ echo -n "Starting HBugs tutor $tutor ... "
+ ./$tutor &> run/$tutor.LOG &
+ echo "done!"
+ else
+ echo "Uh? Try --help"
+ exit 1
+ fi
+done
--- /dev/null
+
+open Hbugs_types;;
+open Printf;;
+
+exception Empty_must;;
+
+let broker_id = ref None
+let my_own_id = Hbugs_tutors_common.init_tutor ()
+let my_own_addr, my_own_port = "127.0.0.1", 50011
+let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
+
+let is_authenticated id =
+ match !broker_id with
+ | None -> false
+ | Some broker_id -> id = broker_id
+
+ (* thread who do the dirty work *)
+let slave (state, musing_id) =
+ prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
+ let (proof, goal) = Hbugs_tutors_common.load_state state in
+ let hint =
+ try
+ let choose_must must only = (* euristic: use 2nd precision level
+ 1st is more precise but is more slow *)
+ match must with
+ | [] -> raise Empty_must
+ | _::hd::tl -> hd
+ | hd::tl -> hd
+ in
+ let uris =
+ TacticChaser.searchPattern ~choose_must () ~status:(proof, goal)
+(* ["cic:/pippo.con"; "cic:/pluto.con"] *)
+ in
+ if uris = [] then
+ Sorry
+ else
+ Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
+ with Empty_must -> Sorry
+ in
+ let answer = Musing_completed (my_own_id, musing_id, hint) in
+ ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors_common.broker_url answer);
+ prerr_endline
+ (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
+
+let hbugs_callback =
+ let forbidden () =
+ prerr_endline "ignoring request from unauthorized broker";
+ Exception ("forbidden", "")
+ in
+ function
+ | Start_musing (broker_id, state) ->
+ if is_authenticated broker_id then begin
+ prerr_endline "received Start_musing";
+ let new_musing_id = Hbugs_id_generator.new_musing_id () in
+ prerr_endline
+ (sprintf "starting a new musing (id = %s)" new_musing_id);
+ ignore (Thread.create slave (state, new_musing_id));
+ Musing_started (my_own_id, new_musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | Abort_musing (broker_id, musing_id) ->
+ if is_authenticated broker_id then begin
+ prerr_endline "Ignoring 'Abort_musing' message ...";
+ Musing_aborted (my_own_id, musing_id)
+ end else (* broker unauthorized *)
+ forbidden ();
+ | unexpected_msg ->
+ Exception ("unexpected_msg",
+ Hbugs_messages.string_of_msg unexpected_msg)
+
+let callback (req: Http_types.request) outchan =
+ try
+ let req_msg = Hbugs_messages.msg_of_string req#body in
+ let answer = hbugs_callback req_msg in
+ Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
+ with Hbugs_messages.Parse_error (subj, reason) ->
+ Http_daemon.respond
+ ~body:(Hbugs_messages.string_of_msg
+ (Exception ("parse_error", reason)))
+ outchan
+
+let main () =
+ try
+ Sys.catch_break true;
+ at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
+ broker_id :=
+ Some (Hbugs_tutors_common.register_to_broker
+ my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
+ Http_daemon.start'
+ ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
+ with Sys.Break -> () (* exit nicely, invoking at_exit functions *)
+;;
+
+main ()
+
projects / helm.git / commitdiff