X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=d3ba1d2a3e1130ac9abc7e3d6a0071169fe8c2b1;hb=6150b8ef905aaea17b47ff466c067054f976cd8f;hp=76a58091da7899dea84f55847538e6c383b16db9;hpb=a8f512296b650595549fe3e125930657d20bb99c;p=helm.git diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 76a58091d..d3ba1d2a3 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -33,74 +33,266 @@ (* *) (******************************************************************************) +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 searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status = +let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status = let ((_, metasenv, _, _), metano) = status in - let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let list_of_must,only = MQueryLevels.out_restr metasenv ey ty 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 torigth_restriction (u,b) = - let p = - if b then - "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" - else - "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" - in - (u,p,None) - in - let rigth_must = List.map torigth_restriction must in - let rigth_only = Some (List.map torigth_restriction only) in + prerr_endline "123"; let result = - MQueryInterpreter.execute mqi_handle - (MQueryGenerator.query_of_constraints - (Some - ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ; - "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"]) - (rigth_must,[],[]) (rigth_only,None,None)) in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri - ) result in - let uris',exc = - let rec filter_out = - function - [] -> [],"" - | uri::tl -> - let tl',exc = filter_out tl in - try - if - (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) - then - uri::tl',exc - else - tl',exc - with + 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' + 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 + 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 *) + +(* OLD CODE: TO BE REMOVED +(*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*) +(*Mi serve per ritornare la posizione del teo che produce meno subgoal*) + +exception NotInTheList;; + + +let position n = + let rec aux k = + function + [] -> raise NotInTheList + | m::_ when m=n -> k + | _::tl -> aux (k+1) tl in + aux 1 +;; + + + +(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *) +(*generate the less number of subgoals*) + +let searchTheorem (proof,goal) = + let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *) + in + let mqi_handle = MQIC.init mqi_flags prerr_string +in + let uris' = + matchConclusion + mqi_handle ~choose_must() (proof, goal) + in + 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 + let list_proofgoal = + List.map + (function term -> + PrimitiveTactics.apply_tac ~term (proof,goal)) + list_of_termin + in + let (list_of_subgoal: int list list) = + List.map snd list_proofgoal + in + let list_of_num = + List.map List.length list_of_subgoal + in + let list_sort = + List.sort Pervasives.compare list_of_num + in (*ordino la lista in modo cresc*) + let min= List.nth list_sort 0 (*prendo il minimo*) + in + let uri' = (*cerco il teo di pos k*) + List.nth list_of_termin (position min list_of_num) + in + (* let teo= + String.sub uri' 4 (String.length uri' - 4) + + (* modifico la str in modo che sia accettata da apply*) + in*) + PrimitiveTactics.apply_tac ~term:uri' (proof,goal) +;; +*) + + +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 + + ;;