X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;fp=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=689102fe2439c982d94f756087375c2da6116c2e;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml deleted file mode 100644 index 689102fe2..000000000 --- a/helm/ocaml/tactics/tacticChaser.ml +++ /dev/null @@ -1,230 +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 - prerr_endline "123"; - let result = - I.execute mqi_handle - (G.query_of_constraints - (Some CGMatchConclusion.universe) - (must,[],[]) (Some only,None,None)) in - prerr_endline "456"; - 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 - (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 result = Match_concl.cmatch conn ty in - (* Stampa il risultato della query - List.iter - (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result; - *) - let uris = - List.map - (fun (n,u) -> - (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) - result in - (* 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 (_,concl_const) = NewConstraints.constants_of 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 uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) 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 - [] -> [] - | (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 ("Ne sono rimasti " ^ string_of_int (List.length uris)); - filter_out uris - in - prerr_endline ("Ne sono rimasti " ^ 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) = -(*prerr_endline "1";*) - 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 *) - List.map snd res -;; -