From 2e9230cc95280f928b15c624ee4564fffea56373 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:56:40 +0000 Subject: [PATCH] - reimplemented tacticChaser and friends in term of Metadata module and friends --- helm/ocaml/tactics/.depend | 29 +- helm/ocaml/tactics/Makefile | 6 +- helm/ocaml/tactics/eliminationTactics.ml | 51 ---- helm/ocaml/tactics/filter_auto.ml | 165 ------------ helm/ocaml/tactics/filter_auto.mli | 40 --- helm/ocaml/tactics/match_concl.ml | 242 ----------------- helm/ocaml/tactics/match_concl.mli | 49 ---- helm/ocaml/tactics/metadataQuery.ml | 52 +++- helm/ocaml/tactics/newConstraints.ml | 320 ----------------------- helm/ocaml/tactics/newConstraints.mli | 61 ----- helm/ocaml/tactics/proofEngineTypes.ml | 4 +- helm/ocaml/tactics/tacticChaser.ml | 258 ------------------ helm/ocaml/tactics/tacticChaser.mli | 41 --- helm/ocaml/tactics/variousTactics.ml | 22 +- helm/ocaml/tactics/variousTactics.mli | 3 +- 15 files changed, 74 insertions(+), 1269 deletions(-) delete mode 100644 helm/ocaml/tactics/filter_auto.ml delete mode 100644 helm/ocaml/tactics/filter_auto.mli delete mode 100644 helm/ocaml/tactics/match_concl.ml delete mode 100644 helm/ocaml/tactics/match_concl.mli delete mode 100644 helm/ocaml/tactics/newConstraints.ml delete mode 100644 helm/ocaml/tactics/newConstraints.mli delete mode 100644 helm/ocaml/tactics/tacticChaser.ml delete mode 100644 helm/ocaml/tactics/tacticChaser.mli diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 6f9e70476..6cd18ba9f 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -1,10 +1,9 @@ -filter_auto.cmi: newConstraints.cmi proofEngineHelpers.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi -tacticChaser.cmi: proofEngineTypes.cmi +metadataQuery.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi @@ -16,12 +15,6 @@ fourierR.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi -newConstraints.cmo: newConstraints.cmi -newConstraints.cmx: newConstraints.cmi -match_concl.cmo: newConstraints.cmi match_concl.cmi -match_concl.cmx: newConstraints.cmx match_concl.cmi -filter_auto.cmo: newConstraints.cmi filter_auto.cmi -filter_auto.cmx: newConstraints.cmx filter_auto.cmi proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi @@ -42,16 +35,16 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi -metadataQuery.cmo: metadataQuery.cmi -metadataQuery.cmx: metadataQuery.cmi -tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \ - primitiveTactics.cmi proofEngineTypes.cmi tacticChaser.cmi -tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \ - primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi -variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmi tacticChaser.cmi tacticals.cmi variousTactics.cmi -variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ - proofEngineTypes.cmx tacticChaser.cmx tacticals.cmx variousTactics.cmi +metadataQuery.cmo: primitiveTactics.cmi proofEngineTypes.cmi \ + metadataQuery.cmi +metadataQuery.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ + metadataQuery.cmi +variousTactics.cmo: metadataQuery.cmi primitiveTactics.cmi \ + proofEngineReduction.cmi proofEngineTypes.cmi tacticals.cmi \ + variousTactics.cmi +variousTactics.cmx: metadataQuery.cmx primitiveTactics.cmx \ + proofEngineReduction.cmx proofEngineTypes.cmx tacticals.cmx \ + variousTactics.cmi introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmi \ introductionTactics.cmi introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 65b42b301..77e61b2f4 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -1,14 +1,14 @@ PACKAGE = tactics REQUIRES = \ - pcre helm-cic_textual_parser helm-cic_proof_checking \ + pcre helm-cic_proof_checking \ helm-cic_unification helm-mathql_interpreter helm-mathql_generator \ dbi helm-metadata INTERFACE_FILES = \ - proofEngineTypes.mli newConstraints.mli match_concl.mli filter_auto.mli\ + proofEngineTypes.mli \ proofEngineReduction.mli proofEngineHelpers.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ - primitiveTactics.mli metadataQuery.mli tacticChaser.mli \ + primitiveTactics.mli metadataQuery.mli \ variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 1db11951f..b75e2da89 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -83,57 +83,6 @@ let interactive_user_uri_choice = title:string -> msg:string -> string list -> string list) ref) ;; -exception IllFormedUri of string - -let cic_textual_parser_uri_of_string uri' = - try - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then - CicTextualParser0.ConUri (UriManager.uri_of_string uri') - else - if String.sub uri' (String.length uri' - 4) 4 = ".var" then - CicTextualParser0.VarUri (UriManager.uri_of_string uri') - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in - CicTextualParser0.IndTyUri (uri'',typeno) - with - _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in - CicTextualParser0.IndConUri (uri'',typeno,consno) - ) - with - _ -> raise (IllFormedUri uri') -;; - -(* -let constructor_uri_of_string uri = - match cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false -;; - -let call_back uris = -(* N.B.: nella finestra c'e' un campo "nessuno deei precedenti, prova questo" che non ha senso? *) -(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) -(* domanda: due triple possono essere diverse solo per avere exp_named_subst diverse?? *) - let module U = UriManager in - List.map - (constructor_uri_of_string) - (!interactive_user_uri_choice - ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false - ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" - (List.map - (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)) - uris) - ) -;; -*) - let decompose_tac ?(uris_choice_callback=(function l -> l)) term = let decompose_tac uris_choice_callback term status = let (proof, goal) = status in diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml deleted file mode 100644 index b5fa2e2d7..000000000 --- a/helm/ocaml/tactics/filter_auto.ml +++ /dev/null @@ -1,165 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - - -let in_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis'" ;; - -let main_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis'" ;; - -let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'" ;; - -let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;; - -let in_body = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InBody'";; - -let escape = Str.global_replace (Str.regexp_string "\'") "\\'";; - -let hyp_const (conn:Mysql.dbd) uri = - let uri = escape uri in - (*query to obtain all the constants in the hypothesis and conclusion of the theorem*) - let query = - "select h_occurrence from refObj where source='"^uri^ - "' and (not (h_position ="^in_body^"))" in - (*prerr_endline ("$$$$$$$$$$$$$$$"^query);*) - let result = Mysql.exec conn query in - (* now we transform the result in a set *) - let f a = - match (Array.to_list a) with - [Some uri] -> uri - | _ -> assert false in - let result = Mysql.map ~f:f result in - List.fold_left - (fun set uri -> - NewConstraints.StringSet.add uri set) - NewConstraints.StringSet.empty result -;; - -(* for each uri check if its costants are a subset of - const, the set of the costants of the proof *) -let filter_new_constants (conn:Mysql.dbd) const (_,uri) = - let hyp = hyp_const conn uri in - (* prerr_endline (NewConstraints.pp_StringSet hyp);*) - NewConstraints.StringSet.subset hyp const -;; - - - - -let rec exec_query (conn:Mysql.dbd) (uris,main) k = - let add_must (n,from,where) uri = - let refObjn = "refObj" ^ (string_of_int n) in - let new_must = - [ refObjn^".h_occurrence = '" ^ uri ^ "'"; - "(not ("^refObjn^".h_position ="^in_body^"))"] in - let where' = - if n = 0 then new_must@where - else - (refObjn^".source = refObj" ^ (string_of_int (n-1)) - ^ ".source")::new_must@where in - (n+1,("refObj as "^refObjn)::from,where') - in - let (_,from,where) = - List.fold_left add_must (0,[],[]) uris in - let from,where = - ["no_concl_hyp";"refObj as main"]@from, - ["no=" ^ (string_of_int k); - "no_concl_hyp.source = refObj0.source"; - "main.source = refObj0.source"; - "main.h_occurrence = '" ^ main ^ "'"; - "main.h_position = " ^ main_conclusion]@where - in - let from = String.concat "," from in - let where = String.concat " and " where in - let query = "select distinct(refObj0.source) from " ^ from ^ " where " ^ where in - (*prerr_endline query;*) - Mysql.exec conn query -;; - -let powerset set = - let rec powerset_r set sub = - if (NewConstraints.StringSet.is_empty set) then sub - else - let a = NewConstraints.StringSet.min_elt set in - let newset = NewConstraints.StringSet.remove a set in - let newsub = NewConstraints.SetSet.union (NewConstraints.SetSet.add (NewConstraints.StringSet.singleton a) - (NewConstraints.SetSet.fold - (fun s t -> (NewConstraints.SetSet.add (NewConstraints.StringSet.add a s) t)) - sub NewConstraints.SetSet.empty)) sub in - powerset_r newset newsub in -powerset_r set NewConstraints.SetSet.empty -;; - -let setset_to_listlist setset = - let listset = NewConstraints.SetSet.elements setset in - let res = - List.map - (fun set -> - let el = NewConstraints.StringSet.elements set in - (List.length el, el)) listset in - (* ordered by descending cardinality *) -List.sort (fun (n,_) (m,_) -> m - n) res - -let exist_element list_of_uris (_,uri) = - let ex u = - if u = uri then true - else false - in -List.exists ex list_of_uris -;; - - -let filter_uris (conn:Mysql.dbd) const uris main = - let subsets_of_consts = - setset_to_listlist (powerset const) in - let ex u = - if u = main then true - else false - in - let subsets_of_consts = - List.filter - (fun (_,b) -> (List.exists ex b)) - subsets_of_consts in - let uris_of_const = - List.concat - (List.map - (fun (m,s) -> - (let res = - exec_query conn (s,main) m in - let f a = - match (Array.to_list a) with - [Some uri] -> uri - | _ -> assert false in - Mysql.map ~f:f res)) - subsets_of_consts) - in -List.filter (exist_element uris_of_const) uris -;; - -let rec power n m = - if (m = 1) then n - else n*(power n (m-1)) -;; - - diff --git a/helm/ocaml/tactics/filter_auto.mli b/helm/ocaml/tactics/filter_auto.mli deleted file mode 100644 index 699eacf62..000000000 --- a/helm/ocaml/tactics/filter_auto.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -val power: - int -> int -> int - -val filter_new_constants: - Mysql.dbd -> - NewConstraints.StringSet.t -> - int * string -> - bool - -val filter_uris: - Mysql.dbd -> - NewConstraints.StringSet.t -> - (int * string) list -> - string -> - (int * string) list diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml deleted file mode 100644 index c2266cd10..000000000 --- a/helm/ocaml/tactics/match_concl.ml +++ /dev/null @@ -1,242 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -(*********************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti, Matteo Selmi *) -(* 1/04/2004 *) -(* *) -(* *) -(*********************************************************************) - - -(* the file contains: - - functions executing must, just and only constraints on the mysql - data base; - - the general function cmatch for retrieving all statements matching - a given conclusion -*) - -type count_condition = - NIL | EQ of int | GT of int -;; - -let main_conclusion = - "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'" -;; - -let in_conclusion = - "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" -;; - -let escape = Str.global_replace (Str.regexp_string "\'") "\\'";; - - -let get_inconcl (conn:Mysql.dbd) uri = - let uri = escape uri in - let query = - "select h_occurrence from refObj where source='"^uri^ - "' and (h_position="^main_conclusion^" or h_position="^in_conclusion^")" in - prerr_endline query; - let result = Mysql.exec conn query in - (* now we transform the result in a set *) - let f a = - match (Array.to_list a) with - [Some uri] -> uri - | _ -> assert false in - let result = Mysql.map ~f:f result in - List.fold_left - (fun set uri -> - NewConstraints.StringSet.add uri set) - NewConstraints.StringSet.empty result -;; - -let test_only (conn:Mysql.dbd) only u = - let inconcl = get_inconcl conn u in - NewConstraints.StringSet.subset inconcl only -;; - -let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition) = - let add_must (n,from,where) (pos,uri) = - match pos with - `MainHypothesis _ -> assert false - | `MainConclusion None -> - let refObjn = "refObj" ^ (string_of_int n) in - let new_must = - [ refObjn^".h_occurrence = '" ^ uri ^ "'"; - refObjn^".h_position = " ^ main_conclusion] in - let where' = - if n = 0 then new_must@where - else - (refObjn^".source = refObj" ^ (string_of_int (n-1)) - ^ ".source")::new_must@where in - (n+1,("refObj as "^refObjn)::from,where') - | `MainConclusion(Some(d)) -> - let refObjn = "refObj" ^ (string_of_int n) in - let new_must = - [ refObjn^".h_occurrence = '" ^ uri ^ "'"; - refObjn^".h_position = " ^ main_conclusion; - refObjn^".h_depth = " ^ (string_of_int d)] in - let where' = - if n = 0 then new_must@where - else - (refObjn^".source = refObj" ^ (string_of_int (n-1)) - ^ ".source")::new_must@where in - (n+1,("refObj as "^refObjn)::from,where') - | `InHypothesis -> assert false - | `InConclusion -> - let refObjn = "refObj" ^ (string_of_int n) in - let new_must = - [ refObjn^".h_occurrence = '" ^ uri ^ "'"; - refObjn^".h_position = " ^ in_conclusion] in - let where' = - if n = 0 then new_must@where - else - (refObjn^".source = refObj" ^ (string_of_int (n-1)) - ^ ".source")::new_must@where in - (n+1,("refObj as "^refObjn)::from,where') - | `InBody -> assert false - in - let (_,from,where) = - List.fold_left add_must (0,[],[]) l in - let from,where = - (match cc with - NIL -> from, where - | EQ n -> - "no_inconcl_aux"::from, - ("no=" ^ (string_of_int n)):: - ("no_inconcl_aux.source = refObj0.source")::where - | GT n -> - "no_inconcl_aux"::from, - ("no>" ^ (string_of_int n)):: - ("no_inconcl_aux.source = refObj0.source")::where) in - let from = String.concat "," from in - let where = String.concat " and " where in - let query = - "select refObj0.source from " ^ from ^ " where " ^ where in - (* prerr_endline query;*) - Mysql.exec conn query -;; - - -let (must_of_prefix m s):MQGTypes.r_obj list = - let s' = List.map (fun u -> (`InConclusion, u)) s in - (`MainConclusion None,m)::s' -;; - -(* takes a list of lists and returns the list of all elements - without repetitions *) -let union l = - let rec drop_repetitions = function - [] -> [] - | [a] -> [a] - | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l) - | u::l -> u::(drop_repetitions l) in - drop_repetitions (List.sort Pervasives.compare (List.concat l)) -;; - -let critical_value = 6;; -let just_factor = 3;; - -let cmatch (conn:Mysql.dbd) t = - let eq,constants = NewConstraints.constants_of t in - (* the type of eq is not counted in constants_no *) - let constants_no = - if eq then (NewConstraints.StringSet.cardinal constants) - else (NewConstraints.StringSet.cardinal constants) in - if (constants_no > critical_value) then - let prefixes = NewConstraints.prefixes just_factor t in - (match prefixes with - Some main, all_concl -> -(* - NewConstraints.pp_prefixes all_concl; -*) - (* in some cases, max_prefix_length could be less than n *) - let max_prefix_length = - match all_concl with - [] -> assert false - | (max,_)::_ -> max in - let maximal_prefixes = - let rec filter res = function - [] -> res - | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l - | _::_-> res in - filter [] all_concl in - let greater_than :(int*string) list= - let all = - union - (List.map - (fun (m,s) -> - (let res = - exec_must conn (must_of_prefix main s) (GT (m+1)) in - let f a = - match (Array.to_list a) with - (* we tag the uri with m+1, for sorting purposes *) - [Some uri] -> (m+1,uri) - | _ -> assert false in - Mysql.map ~f:f res)) - maximal_prefixes) in - List.filter - (function (_,uri) -> test_only conn constants uri) all in - let equal_to = - List.concat - (List.map - (fun (m,s) -> - (let res = - exec_must conn (must_of_prefix main s) (EQ (m+1)) in - let f a = - match (Array.to_list a) with - (* we tag the uri with m, for sorting purposes *) - [Some uri] -> (m,uri) - | _ -> assert false in - Mysql.map ~f:f res)) - all_concl) in - greater_than @ equal_to - | _, _ -> []) - else if constants_no = 0 then [] - else - (* in this case we compute all prefixes, and we do not need - to apply the only constraints *) - let prefixes = NewConstraints.prefixes constants_no t in - (match prefixes with - Some main, all_concl -> - List.concat - (List.map - (fun (m,s) -> - (let res = - exec_must conn (must_of_prefix main s) (EQ (m+1)) in - let f a = - match (Array.to_list a) with - (* we tag the uri with m, for sorting purposes *) - [Some uri] -> (m,uri) - | _ -> assert false in - Mysql.map ~f:f res)) - all_concl) - | _, _ -> []) -;; - - diff --git a/helm/ocaml/tactics/match_concl.mli b/helm/ocaml/tactics/match_concl.mli deleted file mode 100644 index 72d384d55..000000000 --- a/helm/ocaml/tactics/match_concl.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -(*********************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti, Matteo Selmi *) -(* 1/04/2004 *) -(* *) -(* *) -(*********************************************************************) - - -type count_condition = - NIL | EQ of int | GT of int - -val exec_must : - Mysql.dbd -> - MQGTypes.r_obj list -> - count_condition -> - Mysql.result - -val cmatch : - Mysql.dbd -> - Cic.term -> - (int*string) list diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 13a73b561..619af110b 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -29,7 +29,7 @@ module Constr = MetadataConstraints let locate ~(dbh:Dbi.connection) name = let query = - dbh#prepare (sprintf "SELECT value FROM %s WHERE source = \"%s\"" + dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\"" MetadataTypes.name_tbl name) in query#execute []; @@ -73,7 +73,7 @@ let filter_uris_forward ~dbh (main, constants) uris = let full_signature = List.fold_right Constr.StringSet.add main_uris constants in - List.filter (Constr.at_most ~dbh full_signature) uris + List.filter (Constr.at_most ~dbh ~where:`Statement full_signature) uris let filter_uris_backward ~dbh signature uris = let siguris = @@ -81,6 +81,22 @@ let filter_uris_backward ~dbh signature uris = in intersect uris siguris +let compare_goal_list proof goal1 goal2 = + let _,metasenv,_,_ = proof in + let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in + let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in + let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in + let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in + let prop1 = + if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0 + else 1 + in + let prop2 = + if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0 + else 1 + in + prop1 - prop2 + let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in @@ -109,11 +125,29 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = end else filter_uris_backward ~dbh (main, other_constants) uris in - List.map - (fun uri -> - (uri, - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) - status)) - uris +prerr_endline "URIS"; +List.iter prerr_endline uris; + let rec aux = function + | [] -> [] + | uri :: tl -> + (let status' = + try + let (proof, goal_list) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) + status + in + let goal_list = + List.stable_sort (compare_goal_list proof) goal_list + in + Some (uri, (proof, goal_list)) + with ProofEngineTypes.Fail _ -> None + in + match status' with + | None -> aux tl + | Some status' -> + prerr_endline ("HO APPLICATO " ^ uri); + status' :: aux tl) + in + aux uris diff --git a/helm/ocaml/tactics/newConstraints.ml b/helm/ocaml/tactics/newConstraints.ml deleted file mode 100644 index f384e6f4d..000000000 --- a/helm/ocaml/tactics/newConstraints.ml +++ /dev/null @@ -1,320 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -(*********************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 18/03/2004 *) -(* *) -(* *) -(*********************************************************************) - -(* the file contains functions for computing prefixes and related - stuff, required by the new management of matching *) - -module SortedString = - struct - type t = string - let compare = Pervasives.compare - end -;; - -module StringSet = Set.Make (SortedString) -;; - -module SetSet = Set.Make (StringSet) -;; - - -(* - module SetSet : - sig - type elt = StringSet.t - and t = Set.Make(StringSet).t - val empty : t - val is_empty : t -> bool - val mem : elt -> t -> bool - val add : elt -> t -> t - val singleton : elt -> t - val remove : elt -> t -> t - val union : t -> t -> t - val inter : t -> t -> t - val diff : t -> t -> t - val compare : t -> t -> int - val equal : t -> t -> bool - val subset : t -> t -> bool - val iter : (elt -> unit) -> t -> unit - val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - val for_all : (elt -> bool) -> t -> bool - val exists : (elt -> bool) -> t -> bool - val filter : (elt -> bool) -> t -> t - val partition : (elt -> bool) -> t -> t * t - val cardinal : t -> int - val elements : t -> elt list - val min_elt : t -> elt - val max_elt : t -> elt - val choose : t -> elt - end -*) - -let pp_StringSet set = - if (StringSet.is_empty set) then "EMPTY" - else - "{" ^ (String.concat "," (StringSet.elements set)) ^ "}" -;; - -let pp_SetSet set = - let el = List.map pp_StringSet (SetSet.elements set) in - "{" ^ (String.concat ",\n" el) ^ "}" -;; - -let pp_prefix (n,l) = - (string_of_int n) ^ - ": {" ^ (String.concat "," l) ^ "}" - -let pp_prefixes l = - let el = List.map pp_prefix l in - "{" ^ (String.concat ",\n" el) ^ "}" - - - -let filter_by_card n = - SetSet.filter (fun t -> (StringSet.cardinal t) <= n) -;; - -let merge n a b = - let init = SetSet.union a b in - let merge_single_set s1 b = - SetSet.fold - (fun s2 res -> SetSet.add (StringSet.union s1 s2) res) - b SetSet.empty in - let res = - SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init - in - filter_by_card n res -;; - -let mutinduri u t = - (UriManager.string_of_uri u) ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ ")" -;; - -let mutconstructuri u t c = - (UriManager.string_of_uri u) - ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ "/" ^ (string_of_int c) ^ ")" -;; - -let rec inspect_children n childs = - List.fold_left - (fun res term -> merge n (inspect_conclusion n term) res) - SetSet.empty childs - -and add_root n root childs = - let childunion = inspect_children n childs in - let addroot = StringSet.add root in - SetSet.fold - (fun child newsets -> SetSet.add (addroot child) newsets) - childunion - (SetSet.singleton (StringSet.singleton root)) - -and inspect_conclusion n t = -if n = 0 then SetSet.empty -else match t with - Cic.Rel _ - | Cic.Meta _ - | Cic.Sort _ - | Cic.Implicit _ -> SetSet.empty - | Cic.Var (u,exp_named_subst) -> SetSet.empty - | Cic.Const (u,exp_named_subst) -> - SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u)) - | Cic.MutInd (u, t, exp_named_subst) -> - SetSet.singleton (StringSet.singleton (mutinduri u t)) - | Cic.MutConstruct (u, t, c, exp_named_subst) -> - SetSet.singleton (StringSet.singleton (mutconstructuri u t c)) - | Cic.Cast (t, _) -> inspect_conclusion n t - | Cic.Prod (_, s, t) -> - merge n (inspect_conclusion n s) (inspect_conclusion n t) - | Cic.Lambda (_, s, t) -> - merge n (inspect_conclusion n s) (inspect_conclusion n t) - | Cic.LetIn (_, s, t) -> - merge n (inspect_conclusion n s) (inspect_conclusion n t) - | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> - let suri = UriManager.string_of_uri u in - add_root (n-1) suri l - | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> - let suri = mutinduri u t in - add_root (n-1) suri l - | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> - let suri = mutconstructuri u t c in - add_root (n-1) suri l - | Cic.Appl l -> - SetSet.empty - | Cic.MutCase (u, t, tt, uu, m) -> - SetSet.empty - | Cic.Fix (_, m) -> - SetSet.empty - | Cic.CoFix (_, m) -> - SetSet.empty -;; - -let rec inspect_term n t = -if n = 0 then assert false -else match t with - Cic.Rel _ - | Cic.Meta _ - | Cic.Sort _ - | Cic.Implicit _ -> None, SetSet.empty - | Cic.Var (u,exp_named_subst) -> None, SetSet.empty - | Cic.Const (u,exp_named_subst) -> - Some (UriManager.string_of_uri u), SetSet.empty - | Cic.MutInd (u, t, exp_named_subst) -> - Some (mutinduri u t), SetSet.empty - | Cic.MutConstruct (u, t, c, exp_named_subst) -> - Some (mutconstructuri u t c), SetSet.empty - | Cic.Cast (t, _) -> inspect_term n t - | Cic.Prod (_, _, t) -> inspect_term n t - | Cic.LetIn (_, _, t) -> inspect_term n t - | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> - let suri = UriManager.string_of_uri u in - let childunion = inspect_children (n-1) l in - Some suri, childunion - | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> - let suri = mutinduri u t in - if u = HelmLibraryObjects.Logic.eq_URI && n>1 then - (* equality is handled in a special way: in particular, - the type, if defined, is always added to the prefix, - and n is not decremented - it should have been n-2 *) - match l with - Cic.Const (u1,exp_named_subst1)::l1 -> - let suri1 = UriManager.string_of_uri u1 in - let inconcl = add_root (n-1) suri1 l1 in - Some suri, inconcl - | Cic.MutInd (u1, t1, exp_named_subst1)::l1 -> - let suri1 = mutinduri u1 t1 in - let inconcl = add_root (n-1) suri1 l1 in - Some suri, inconcl - | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 -> - let suri1 = mutconstructuri u1 t1 c1 in - let inconcl = add_root (n-1) suri1 l1 in - Some suri, inconcl - | _ :: _ -> Some suri, SetSet.empty - | _ -> assert false (* args number must be > 0 *) - else - let childunion = inspect_children (n-1) l in - Some suri, childunion - | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> - let suri = mutconstructuri u t c in - let childunion = inspect_children (n-1) l in - Some suri, childunion - | _ -> None, SetSet.empty - -let rec add uri children = - List.fold_left - (fun acc t -> - StringSet.union (constants_concl t) acc) - (StringSet.singleton uri) children - -(* this function creates the set of all different constants appearing in - the conclusion of the term *) -and constants_concl = - function - Cic.Rel _ - | Cic.Meta _ - | Cic.Sort _ - | Cic.Implicit _ -> StringSet.empty - | Cic.Var (u,exp_named_subst) -> StringSet.empty - | Cic.Const (u,exp_named_subst) -> - StringSet.singleton (UriManager.string_of_uri u) - | Cic.MutInd (u, t, exp_named_subst) -> - StringSet.singleton (mutinduri u t) - | Cic.MutConstruct (u, t, c, exp_named_subst) -> - StringSet.singleton (mutconstructuri u t c) - | Cic.Cast (t, _) -> constants_concl t - | Cic.Prod (_, s, t) -> - StringSet.union (constants_concl s) (constants_concl t) - | Cic.Lambda (_, s, t) -> - StringSet.union (constants_concl s) (constants_concl t) - | Cic.LetIn (_, s, t) -> - StringSet.union (constants_concl s) (constants_concl t) - | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> - let suri = UriManager.string_of_uri u in - add suri l - | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> - let suri = mutinduri u t in - add suri l - | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> - let suri = mutconstructuri u t c in - add suri l - | Cic.Appl l -> - StringSet.empty - | Cic.MutCase (u, t, tt, uu, m) -> - StringSet.empty - | Cic.Fix (_, m) -> - StringSet.empty - | Cic.CoFix (_, m) -> - StringSet.empty -;; - -(* (constants_of t) returns a pair (b,n) where n is the number of - constants in the conclusion of t, and b is true if in MainConclusion - we have an equality *) - -let rec constants_of = function - | Cic.Cast (t, _) -> constants_of t - | Cic.Prod (_, _, t) -> constants_of t - | Cic.LetIn (_, _, t) -> constants_of t - | (Cic.Appl ((Cic.MutInd (u, _, _))::l)) as t when - u = HelmLibraryObjects.Logic.eq_URI -> - (true, constants_concl t) - | t -> (false, constants_concl t) -;; - - -let add_cardinality s = - let l = SetSet.elements s in - let res = - List.map - (fun set -> - let el = StringSet.elements set in - (List.length el, el)) l in - (* ordered by descending cardinality *) - List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res) -;; - -let prefixes n t = - match inspect_term n t with - Some a, set -> Some a, add_cardinality set - | None, set when (SetSet.is_empty set) -> None, [] - | _, _ -> assert false -;; - -let mainandcons t = - let const = constants_concl t in - match prefixes 1 t with - Some main, _ -> main, const - | _,_ -> assert false -;; - diff --git a/helm/ocaml/tactics/newConstraints.mli b/helm/ocaml/tactics/newConstraints.mli deleted file mode 100644 index 52c2d7169..000000000 --- a/helm/ocaml/tactics/newConstraints.mli +++ /dev/null @@ -1,61 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -(*********************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 18/03/2004 *) -(* *) -(* *) -(*********************************************************************) - - -module StringSet : Set.S with type elt = string - -module SetSet : Set.S with type elt = StringSet.t - -val pp_SetSet : SetSet.t -> string - -val pp_StringSet : StringSet.t -> string - - - -val inspect_term : int -> Cic.term -> string option * SetSet.t - -val prefixes : int -> Cic.term -> string option * ((int * (StringSet.elt list)) list) - -(* (constants_of t) returns a pair (b,n) where n is the set of the - constants in the conclusion of t, and b is true if in MainConclusion - we have an equality *) - -val constants_of : Cic.term -> bool * StringSet.t - -val constants_concl : Cic.term -> StringSet.t - -val pp_prefixes : ((int * (StringSet.elt list)) list) -> string - -val mainandcons : Cic.term -> (string * StringSet.t) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 8d1def22e..b4992aca3 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -67,7 +67,9 @@ let apply_tactic t status = let saved_univ = CicUniv.get_working() in try t status - with Fail s -> CicUniv.set_working saved_univ; raise (Fail s) + with Fail s -> + CicUniv.set_working saved_univ; + raise (Fail s) (** constraint: the returned value will always be constructed by Cic.Name **) type mk_fresh_name_type = diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml deleted file mode 100644 index 2235670a0..000000000 --- a/helm/ocaml/tactics/tacticChaser.ml +++ /dev/null @@ -1,258 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -(*****************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 18/02/2003 *) -(* *) -(* *) -(*****************************************************************************) - -module MQI = MQueryInterpreter -module MQIC = MQIConn -module I = MQueryInterpreter -module U = MQGUtil -module G = MQueryGenerator - - (* search arguments on which Apply tactic doesn't fail *) -let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status = - let ((_, metasenv, _, _), metano) = status in - let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in - let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in -match list_of_must with - [] -> [] -|_ -> - let must = choose_must list_of_must only in - let result = - I.execute mqi_handle - (G.query_of_constraints - (Some CGMatchConclusion.universe) - (must,[],[]) (Some only,None,None)) in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri - ) result - in - let uris = - (* TODO ristretto per ragioni di efficienza *) - prerr_endline "STO FILTRANDO"; - List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris - in - prerr_endline "HO FILTRATO"; - let uris',exc = - let rec filter_out = - function - [] -> [],"" - | uri::tl -> - let tl',exc = filter_out tl in - try - if - let time = Unix.gettimeofday() in - (try - ignore(ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac - ~term:(MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri))) - status); - let time1 = Unix.gettimeofday() in - prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) ); - true - with ProofEngineTypes.Fail _ -> - let time1 = Unix.gettimeofday() in - prerr_endline (Printf.sprintf "%1.3f" (time1 -. time)); false) - then - uri::tl',exc - else - tl',exc - with - (ProofEngineTypes.Fail _) as e -> - let exc' = - "

^ Exception raised trying to apply " ^ - uri ^ ": " ^ Printexc.to_string e ^ "

" ^ exc - in - tl',exc' - in - filter_out uris - in - let html' = - "

Objects that can actually be applied:

" ^ - String.concat "
" uris' ^ exc ^ - "

Number of false matches: " ^ - string_of_int (List.length uris - List.length uris') ^ "

" ^ - "

Number of good matches: " ^ - string_of_int (List.length uris') ^ "

" - in - output_html html' ; - uris' -;; - - -(*matchConclusion modificata per evitare una doppia apply*) -let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status = - let ((_, metasenv, _, _), metano) = status in - let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in - let conn = - match mqi_handle.MQIConn.pgc with - MQIConn.MySQL_C conn -> conn - | _ -> assert false in - let uris = Match_concl.cmatch conn ty in - (* List.iter - (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *) - (* delete all .var uris *) - let isvar (_,s) = - let len = String.length s in - let suffix = String.sub s (len-4) 4 in - not (suffix = ".var") in - let uris = List.filter isvar uris in - (* delete all not "cic:/Coq" uris *) - (* - let uris = - (* TODO ristretto per ragioni di efficienza *) - List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in - *) - (* concl_cost are the costants in the conclusion of the proof - while hyp_const are the constants in the hypothesis *) - let (main_concl,concl_const) = NewConstraints.mainandcons ty in - prerr_endline ("Ne sono rimasti" ^ string_of_int (List.length uris)); - let hyp t set = - match t with - Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t)) - | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t)) - | _ -> set in - let hyp_const = - List.fold_right hyp ey NewConstraints.StringSet.empty in - prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const)); - (* uris with new constants in the proof are filtered *) - let all_const = NewConstraints.StringSet.union hyp_const concl_const in - let uris = - if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const)))) - then - (prerr_endline("metodo vecchio");List.filter (Filter_auto.filter_new_constants conn all_const) uris) - else Filter_auto.filter_uris conn all_const uris main_concl in -(* - let uris = - (* ristretto all cache *) - prerr_endline "SOLO CACHE"; - List.filter - (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris - in - prerr_endline "HO FILTRATO2"; -*) - let uris = - List.map - (fun (n,u) -> - (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) - uris in - let uris' = - let rec filter_out = - function - [] -> [] - | (m,uri)::tl -> - let tl' = filter_out tl in - try - prerr_endline ("STO APPLICANDO " ^ uri); - let res = (m, - (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac - ~term:(MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri))) - status))::tl' in - prerr_endline ("OK");res - (* with ProofEngineTypes.Fail _ -> tl' *) - (* patch to cover CSC's exportation bug *) - with _ -> prerr_endline ("FAIL");tl' - in - prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris)); - filter_out uris - in - prerr_endline ("Ne sono rimasti 3 " ^ string_of_int (List.length uris')); - - uris' -;; - -(*funzione che sceglie il penultimo livello di profondita' dei must*) - -(* -let choose_must list_of_must only= -let n = (List.length list_of_must) - 1 in - List.nth list_of_must n -;;*) - -(* questa prende solo il main *) -let choose_must list_of_must only = - List.nth list_of_must 0 - -(* livello 1 -let choose_must list_of_must only = - try - List.nth list_of_must 1 - with _ -> - List.nth list_of_must 0 *) - -let searchTheorems mqi_handle (proof,goal) = - let subproofs = - matchConclusion2 mqi_handle ~choose_must() (proof, goal) in - let res = - List.sort - (fun (n1,(_,gl1)) (n2,(_,gl2)) -> - let l1 = List.length gl1 in - let l2 = List.length gl2 in - (* if the list of subgoals have the same lenght we use the - prefix tag, where higher tags have precedence *) - if l1 = l2 then n2 - n1 - else l1 - l2) - subproofs - in - (* now we may drop the prefix tag *) - (*let res' = - List.map snd res in*) - let order_goal_list proof goal1 goal2 = - let _,metasenv,_,_ = proof in - let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in - let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in -(* - prerr_endline "PRIMA DELLA PRIMA TYPE OF " ; -*) - let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in -(* - prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2)); -*) - let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in -(* - prerr_endline "DOPO LA SECONDA TYPE OF " ; -*) - let prop1 = if CicReduction.are_convertible - ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0 - else 1 in - let prop2 = if CicReduction.are_convertible - ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0 - else 1 in - prop1 - prop2 in - List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res -;; - diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli deleted file mode 100644 index d4f8a2c54..000000000 --- a/helm/ocaml/tactics/tacticChaser.mli +++ /dev/null @@ -1,41 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * 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://cs.unibo.it/helm/. - *) - -val matchConclusion : MQIConn.handle -> - ?output_html:(string -> unit) -> - choose_must:(MQGTypes.r_obj list list -> - MQGTypes.r_obj list -> - MQGTypes.r_obj list) -> - unit -> ProofEngineTypes.status -> string list - - -(* TODO: OLD CODE TO BE REMOVED -val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list -*) - -val searchTheorems: - MQIConn.handle -> ProofEngineTypes.status -> - (ProofEngineTypes.proof * ProofEngineTypes.goal list) list - diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 9293d1439..f986bc867 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -181,12 +181,12 @@ let new_search_theorems f proof goal depth gtl = exception NoOtherChoices;; -let rec auto_new mqi_handle = function +let rec auto_new dbh = function [] -> raise NoOtherChoices | (proof, [])::tl -> (proof, [])::tl - | (proof, (goal,0)::gtl)::tl -> auto_new mqi_handle tl + | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl | (proof, (goal,depth)::gtl)::tl -> - let _,metasenv,_,_ = proof in + let _,metasenv,proof_obj,_ = proof in let meta_inf = (try let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in @@ -196,12 +196,14 @@ let rec auto_new mqi_handle = function Some (ey, ty) -> prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); + prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj)); let local_choices = new_search_theorems search_theorems_in_context proof goal (depth-1) gtl in let global_choices = new_search_theorems - (TacticChaser.searchTheorems mqi_handle) + (fun status -> List.map snd (MetadataQuery.hint ~dbh status)) +(* (TacticChaser.searchTheorems mqi_handle) *) proof goal (depth-1) gtl in let all_choices = local_choices@global_choices@tl in @@ -214,17 +216,17 @@ let rec auto_new mqi_handle = function let reorder = List.stable_sort sorting_list all_choices in - auto_new mqi_handle reorder - | None -> auto_new mqi_handle ((proof,gtl)::tl) + auto_new dbh reorder + | None -> auto_new dbh ((proof,gtl)::tl) ;; -let auto_tac mqi_handle = +let auto_tac ~(dbh:Dbi.connection) = (* CicMetaSubst.reset_counters (); *) - let auto_tac mqi_handle (proof,goal) = + let auto_tac dbh (proof,goal) = prerr_endline "Entro in Auto"; try - (match auto_new mqi_handle [(proof, [(goal,depth)])] with + (match auto_new dbh [(proof, [(goal,depth)])] with | (proof,_)::_ -> prerr_endline "AUTO_TAC HA FINITO"; (* CicMetaSubst.print_counters (); *) @@ -235,7 +237,7 @@ let auto_tac mqi_handle = prerr_endline("Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") in - ProofEngineTypes.mk_tactic (auto_tac mqi_handle) + ProofEngineTypes.mk_tactic (auto_tac dbh) ;; (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index a4d471e3b..ebbf84332 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -32,5 +32,6 @@ val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list -> ProofEngineTypes.tactic -val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic +(* val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic *) +val auto_tac : dbh:Dbi.connection -> ProofEngineTypes.tactic -- 2.39.2