From: Andrea Asperti Date: Mon, 10 May 2004 09:40:33 +0000 (+0000) Subject: Adding file match_concl X-Git-Tag: V_0_0_9~57 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5930f13b2d863abbff240ffa985bcc064c7a5ab8;p=helm.git Adding file match_concl 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 --- diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 608260c83..581663cd2 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -16,6 +16,10 @@ proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi proofEngineHelpers.cmx: proofEngineHelpers.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 tacticals.cmo: proofEngineTypes.cmo tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi @@ -30,8 +34,10 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi -tacticChaser.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi -tacticChaser.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi +tacticChaser.cmo: match_concl.cmi primitiveTactics.cmi proofEngineTypes.cmo \ + tacticChaser.cmi +tacticChaser.cmx: match_concl.cmx primitiveTactics.cmx proofEngineTypes.cmx \ + tacticChaser.cmi variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ proofEngineTypes.cmo tacticChaser.cmi tacticals.cmi variousTactics.cmi variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index b5430999e..c5ab120c1 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -5,6 +5,7 @@ REQUIRES = \ INTERFACE_FILES = \ proofEngineReduction.mli proofEngineHelpers.mli \ + newConstraints.mli match_concl.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli tacticChaser.mli variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml new file mode 100644 index 000000000..4f36f3ee5 --- /dev/null +++ b/helm/ocaml/tactics/match_concl.ml @@ -0,0 +1,239 @@ +(* 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 new file mode 100644 index 000000000..72d384d55 --- /dev/null +++ b/helm/ocaml/tactics/match_concl.mli @@ -0,0 +1,49 @@ +(* 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/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 5851b1467..edb69bf50 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -66,7 +66,7 @@ match list_of_must with prerr_endline "STO FILTRANDO"; List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in - prerr_endline "HO FILTRATO"; + prerr_endline "HO FILTRATO"; let uris',exc = let rec filter_out = function @@ -74,15 +74,20 @@ match list_of_must with | uri::tl -> let tl',exc = filter_out tl in try - if + if + let time = Unix.gettimeofday() in (try ignore - (PrimitiveTactics.apply_tac - ~term:(MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri)) - status); - true - with ProofEngineTypes.Fail _ -> false) + (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 @@ -112,49 +117,61 @@ match list_of_must with (*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 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 ((_, 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 result = Match_concl.cmatch conn ty in + List.iter + (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result; let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri - ) result - in + List.map + (fun (n,u) -> + (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) + result in + 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 + let uris = + (* TODO ristretto per ragioni di efficienza *) + prerr_endline "STO FILTRANDO2"; + List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in +(* let uris = (* TODO ristretto per ragioni di efficienza *) prerr_endline "STO FILTRANDO2"; List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in - 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 + 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' = let rec filter_out = function [] -> [] - | uri::tl -> - let tl' = filter_out tl in - try - ((PrimitiveTactics.apply_tac - ~term:(MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri)) - status)::tl') - with ProofEngineTypes.Fail _ -> tl' + | (m,uri)::tl -> + let tl' = filter_out tl in + try + (m, + (prerr_endline ("STO APPLICANDO " ^ uri); + (PrimitiveTactics.apply_tac + ~term:(MQueryMisc.term_of_cic_textual_parser_uri + (MQueryMisc.cic_textual_parser_uri_of_string uri)) + status)))::tl' + (* with ProofEngineTypes.Fail _ -> tl' *) + (* patch to cover CSC's exportation bug *) + with _ -> tl' in - prerr_endline (string_of_int (List.length uris)); + prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris)); filter_out uris in uris' @@ -162,14 +179,22 @@ match list_of_must with (*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 = - List.nth list_of_must 0 + try + List.nth list_of_must 1 + with _ -> + List.nth list_of_must 0 *) (* OLD CODE: TO BE REMOVED (*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*) @@ -241,29 +266,22 @@ in let searchTheorems mqi_handle (proof,goal) = (*prerr_endline "1";*) - let uris' = + let subproofs = matchConclusion2 mqi_handle ~choose_must() (proof, goal) in -prerr_endline (string_of_int (List.length uris')); -(*prerr_endline "2";*) -(* let list_of_termin = - List.map - (function string -> - (MQueryMisc.term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string string))) - uris' in -prerr_endline "3"; - let list_proofgoal = - List.map - (function term -> - PrimitiveTactics.apply_tac ~term (proof,goal)) list_of_termin in*) -(*prerr_endline "4";*) -let res = + let res = List.sort - (fun (_,gl1) (_,gl2) -> - Pervasives.compare (List.length gl1) (List.length gl2)) - uris' - in -(*prerr_endline "5";*) -res + (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 *) + List.map snd res + + ;; diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 98c13e80b..bb5be64d8 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -51,53 +51,87 @@ let search_theorems_in_context status = prerr_endline ("SIAM QUI = " ^ s); [] ;; - +exception NotAProposition;; exception NotApplicableTheorem;; exception MaxDepth;; -let depth = 5;; +let depth = 3;; -let rec auto_tac mqi_handle level proof goal = -prerr_endline "Entro in Auto_rec"; +let rec auto_tac_aux mqi_handle level proof goal = +prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level)); if level = 0 then (* (proof, [goal]) *) - (prerr_endline ("NON ci credo"); + (prerr_endline ("MaxDepth"); raise MaxDepth) else - (* choices is a list of pairs proof and goallist *) - let choices = - (search_theorems_in_context (proof,goal))@ - (TacticChaser.searchTheorems mqi_handle (proof,goal)) - in - let rec try_choices = function - [] -> raise NotApplicableTheorem - | (proof,goallist)::tl -> + (* let us verify that the metavariable is still an open goal -- + it could have been closed by closing other goals -- and that + it is of sort Prop *) + let _,metasenv,_,_ = proof in + let meta_inf = + (try + let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in + Some (ey, ty) + with _ -> None) in + match meta_inf with + Some (ey, ty) -> + prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); + (* + let time1 = Unix.gettimeofday() in + let _, all_paths = NewConstraints.prefixes 5 ty in + let time2 = Unix.gettimeofday() in + prerr_endline + (Printf.sprintf "TEMPO DI CALCOLO = %1.3f" (time2 -. time1) ); + prerr_endline + ("ALL PATHS: n = " ^ string_of_int + (List.length all_paths)); + prerr_endline (NewConstraints.pp_prefixes all_paths); + *) + (* if the goal does not have a sort Prop we return the + current proof and a list containing the goal *) + let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in + if CicReduction.are_convertible + ey (Cic.Sort Cic.Prop) ty_sort then + (* sort Prop *) + (* choices is a list of pairs proof and goallist *) + let choices = + (search_theorems_in_context (proof,goal))@ + (TacticChaser.searchTheorems mqi_handle (proof,goal)) + in + let rec try_choices = function + [] -> raise NotApplicableTheorem + | (proof,goallist)::tl -> prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist)); - (try - List.fold_left - (fun proof goal -> - (* It may happen that to close the first open goal - also some other goals are closed *) - let _,metasenv,_,_ = proof in - if List.exists (fun (i,_,_) -> i = goal) metasenv then - let newproof = - auto_tac mqi_handle (level-1) proof goal - in - newproof - else - (* goal already closed *) - proof) - proof goallist - with - | MaxDepth - | NotApplicableTheorem -> - try_choices tl) in - try_choices choices;; + (try + List.fold_left + (fun proof goal -> + auto_tac_aux mqi_handle (level-1) proof goal) + proof goallist + with + | MaxDepth + | NotApplicableTheorem + | NotAProposition -> + try_choices tl) in + try_choices choices + else + (* CUT AND PASTE DI PROVA !! *) + let choices = + (search_theorems_in_context (proof,goal))@ + (TacticChaser.searchTheorems mqi_handle (proof,goal)) + in + let rec try_choices = function + [] -> raise NotApplicableTheorem + | (proof,[])::tl -> proof + | _::tl -> try_choices tl in + try_choices choices + (* raise NotAProposition *) + | None -> proof +;; let auto_tac mqi_handle (proof,goal) = prerr_endline "Entro in Auto"; try - let proof = auto_tac mqi_handle depth proof goal in + let proof = auto_tac_aux mqi_handle depth proof goal in prerr_endline "AUTO_TAC HA FINITO"; (proof,[]) with