From ed90e027472d0250d45ae7200600c8804dd476f1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 19 Feb 2003 14:23:02 +0000 Subject: [PATCH] first tutors implementation, contains: - XML representation of available tutors - scripts to list and start/stop available tutors - script to generate simple tutors that simply use a tactic - search_pattern_apply tutor --- helm/hbugs/tutors/.cvsignore | 6 + helm/hbugs/tutors/INDEX.xml | 114 +++++++++ helm/hbugs/tutors/Makefile | 50 ++++ helm/hbugs/tutors/build_tutors.ml | 118 +++++++++ helm/hbugs/tutors/hbugs_tutor.TPL.ml | 41 ++++ helm/hbugs/tutors/hbugs_tutors_common.ml | 224 ++++++++++++++++++ helm/hbugs/tutors/hbugs_tutors_common.mli | 59 +++++ helm/hbugs/tutors/ls_tutors.ml | 55 +++++ helm/hbugs/tutors/sabba.sh | 47 ++++ .../tutors/search_pattern_apply_tutor.ml | 95 ++++++++ 10 files changed, 809 insertions(+) create mode 100644 helm/hbugs/tutors/.cvsignore create mode 100644 helm/hbugs/tutors/INDEX.xml create mode 100644 helm/hbugs/tutors/Makefile create mode 100755 helm/hbugs/tutors/build_tutors.ml create mode 100644 helm/hbugs/tutors/hbugs_tutor.TPL.ml create mode 100644 helm/hbugs/tutors/hbugs_tutors_common.ml create mode 100644 helm/hbugs/tutors/hbugs_tutors_common.mli create mode 100755 helm/hbugs/tutors/ls_tutors.ml create mode 100755 helm/hbugs/tutors/sabba.sh create mode 100644 helm/hbugs/tutors/search_pattern_apply_tutor.ml diff --git a/helm/hbugs/tutors/.cvsignore b/helm/hbugs/tutors/.cvsignore new file mode 100644 index 000000000..a3cccbc0c --- /dev/null +++ b/helm/hbugs/tutors/.cvsignore @@ -0,0 +1,6 @@ +*.cmi +*.cmo +*.cma +*.cmx +*.o +*.a diff --git a/helm/hbugs/tutors/INDEX.xml b/helm/hbugs/tutors/INDEX.xml new file mode 100644 index 000000000..9de351709 --- /dev/null +++ b/helm/hbugs/tutors/INDEX.xml @@ -0,0 +1,114 @@ + + + + + 127.0.0.1 + 50001 + Ring.ring_tac + Hbugs_types.Use_ring_Luke + Use Ring Luke + Ring tutor + + + 127.0.0.1 + 50002 + FourierR.fourier_tac + Hbugs_types.Use_fourier_Luke + Use Fourier Luke + Fourier tutor + + + 127.0.0.1 + 50003 + EqualityTactics.reflexivity_tac + Hbugs_types.Use_reflexivity_Luke + Use Reflexivity Luke + Reflexivity tutor + + + 127.0.0.1 + 50004 + EqualityTactics.symmetry_tac + Hbugs_types.Use_symmetry_Luke + Use Symmetry Luke + Symmetry tutor + + + 127.0.0.1 + 50005 + VariousTactics.assumption_tac + Hbugs_types.Use_assumption_Luke + Use Assumption Luke + Assumption tutor + + + 127.0.0.1 + 50006 + NegationTactics.contradiction_tac + Hbugs_types.Use_contradiction_Luke + Use Contradiction Luke + Contradiction tutor + + + 127.0.0.1 + 50007 + IntroductionTactics.exists_tac + Hbugs_types.Use_exists_Luke + Use Exists Luke + Exists tutor + + + 127.0.0.1 + 50008 + IntroductionTactics.split_tac + Hbugs_types.Use_split_Luke + Use Split Luke + Split tutor + + + 127.0.0.1 + 50009 + IntroductionTactics.left_tac + Hbugs_types.Use_left_Luke + Use Left Luke + Left tutor + + + 127.0.0.1 + 50010 + IntroductionTactics.right_tac + Hbugs_types.Use_right_Luke + Use Right Luke + Right tutor + + + + 127.0.0.1 + 50011 + PrimitiveTactics.apply_tac + Hbugs_types.Use_apply_Luke + Use Apply Luke (with argument) + Search pattern apply tutor + + + diff --git a/helm/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile new file mode 100644 index 000000000..6a3f718d5 --- /dev/null +++ b/helm/hbugs/tutors/Makefile @@ -0,0 +1,50 @@ +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 + diff --git a/helm/hbugs/tutors/build_tutors.ml b/helm/hbugs/tutors/build_tutors.ml new file mode 100755 index 000000000..73ac9826e --- /dev/null +++ b/helm/hbugs/tutors/build_tutors.ml @@ -0,0 +1,118 @@ +#!/usr/bin/ocamlrun /usr/bin/ocaml +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * 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 + 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 ();; + diff --git a/helm/hbugs/tutors/hbugs_tutor.TPL.ml b/helm/hbugs/tutors/hbugs_tutor.TPL.ml new file mode 100644 index 000000000..07d20c949 --- /dev/null +++ b/helm/hbugs/tutors/hbugs_tutor.TPL.ml @@ -0,0 +1,41 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * 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 () ;; + diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml new file mode 100644 index 000000000..f00b17bc0 --- /dev/null +++ b/helm/hbugs/tutors/hbugs_tutors_common.ml @@ -0,0 +1,224 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * 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 + "\n\n" ^ + "\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 + diff --git a/helm/hbugs/tutors/hbugs_tutors_common.mli b/helm/hbugs/tutors/hbugs_tutors_common.mli new file mode 100644 index 000000000..927e31b4f --- /dev/null +++ b/helm/hbugs/tutors/hbugs_tutors_common.mli @@ -0,0 +1,59 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * 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 + diff --git a/helm/hbugs/tutors/ls_tutors.ml b/helm/hbugs/tutors/ls_tutors.ml new file mode 100755 index 000000000..5ddb77d45 --- /dev/null +++ b/helm/hbugs/tutors/ls_tutors.ml @@ -0,0 +1,55 @@ +#!/usr/bin/ocamlrun /usr/bin/ocaml +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * 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 ();; + diff --git a/helm/hbugs/tutors/sabba.sh b/helm/hbugs/tutors/sabba.sh new file mode 100755 index 000000000..239cd9909 --- /dev/null +++ b/helm/hbugs/tutors/sabba.sh @@ -0,0 +1,47 @@ +#!/bin/sh +# Copyright (C) 2003: +# Stefano Zacchiroli +# 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 diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml new file mode 100644 index 000000000..531e94e0e --- /dev/null +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -0,0 +1,95 @@ + +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 () + -- 2.39.2