From e76b78d1d80796de1b8f6a469741cbd26cd4d822 Mon Sep 17 00:00:00 2001 From: Matteo Selmi Date: Fri, 21 May 2004 16:44:53 +0000 Subject: [PATCH] Added a sort function to decide the order of theorems to try in the tactic "auto". --- helm/ocaml/tactics/filter_auto.ml | 4 ++-- helm/ocaml/tactics/tacticChaser.ml | 10 +++++++--- helm/ocaml/tactics/variousTactics.ml | 27 +++++++++++++-------------- 3 files changed, 22 insertions(+), 19 deletions(-) diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml index 73eaed638..73494c8e3 100644 --- a/helm/ocaml/tactics/filter_auto.ml +++ b/helm/ocaml/tactics/filter_auto.ml @@ -41,7 +41,7 @@ let hyp_const (conn:Mysql.dbd) uri = "select h_occurrence from refObj where source='"^uri^ "' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^ "or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in - prerr_endline ("$$$$$$$$$$$$$$$"^query); +(* prerr_endline ("$$$$$$$$$$$$$$$"^query);*) let result = Mysql.exec conn query in (* now we transform the result in a set *) let f a = @@ -59,7 +59,7 @@ let hyp_const (conn:Mysql.dbd) uri = 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); + (* prerr_endline (NewConstraints.pp_StringSet hyp);*) NewConstraints.StringSet.subset hyp const ;; diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 689102fe2..e917555ce 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -48,13 +48,11 @@ 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,_ -> @@ -140,9 +138,15 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st 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 + List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in + *) + (* + let uris = + List.filter (fun _,uri -> not (Pcre.pmatch ~pat:"^cic:/Coq/ring" 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 diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 0df44420c..daf461c5b 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -106,18 +106,7 @@ else Some (ey, ty) -> prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); - (* - 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 + (* 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 @@ -196,7 +185,9 @@ let rec auto_new mqi_handle = function Some (ey, ty) with _ -> None) in match meta_inf with - Some _ -> + Some (ey, ty) -> + prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); + prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); let local_choices = new_search_theorems search_theorems_in_context proof goal (depth-1) gtl in @@ -206,7 +197,15 @@ let rec auto_new mqi_handle = function proof goal (depth-1) gtl in let all_choices = local_choices@global_choices@tl in - let reorder = all_choices in + let sorting_list (_,g1) (_,g2) = + let l1 = List.length g1 in + let l2 = List.length g2 in + if (l1 = l2 && not(l1 = 0)) then + (snd(List.nth g2 0)) - (snd(List.nth g1 0)) + else l1 - l2 in + let reorder = + List.stable_sort sorting_list all_choices + in auto_new mqi_handle reorder | None -> auto_new mqi_handle ((proof,gtl)::tl) ;; -- 2.39.2