let inter = Constr.UriManagerSet.inter set1 set2 in
List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
+let at_most =
+ let profiler = CicUtil.profile "at_most" in
+ fun ~dbd ~where uri -> profiler (Constr.at_most ~dbd ~where) uri
+
+let sigmatch =
+ let profiler = CicUtil.profile "sigmatch" in
+ fun ~dbd ~facts ~where signature ->
+ profiler (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+
let filter_uris_forward ~dbd (main, constants) uris =
let main_uris =
match main with
let full_signature =
List.fold_right Constr.UriManagerSet.add main_uris constants
in
- List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
+ List.filter (at_most ~dbd ~where:`Statement full_signature) uris
let filter_uris_backward ~dbd ~facts signature uris =
let siguris =
List.map snd
- (MetadataConstraints.sigmatch ~dbd ~facts ~where:`Statement signature)
+ (sigmatch ~dbd ~facts ~where:`Statement signature)
in
intersect uris siguris
Constr.UriManagerSet.union bag (Constr.constants_of ty))
s s
+let apply_tac_verbose =
+ let profiler = CicUtil.profile "apply_tac_verbose" in
+ fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
+
+let sigmatch =
+ let profiler = CicUtil.profile "sigmatch" in
+ fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler (Constr.sigmatch ~dbd ~facts ~where) signature
+
+let cmatch' =
+ let profiler = CicUtil.profile "cmatch'" in
+ fun ~dbd ~facts signature -> profiler (Constr.cmatch' ~dbd ~facts) signature
+
+let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+ let set = signature_of_hypothesis context in
+ let set =
+ match main with
+ None -> set
+ | Some (main,l) ->
+ List.fold_right Constr.UriManagerSet.add (main::l) set in
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let all_constants_closed = close_with_types set metasenv context in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+
let experimental_hint
~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
let (_, metasenv, _, _) = proof in
let (uris, (main, sig_constants)) =
match signature with
| Some signature ->
- (Constr.sigmatch ~dbd ~facts signature, signature)
+ (sigmatch ~dbd ~facts signature, signature)
| None ->
- (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty)
+ (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
in
let uris = List.filter nonvar (List.map snd uris) in
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
try
let (subst,(proof, goal_list)) =
(* debug_print ("STO APPLICANDO" ^ uri); *)
- PrimitiveTactics.apply_tac_verbose
+ apply_tac_verbose
+ ~term:(CicUtil.term_of_uri uri)
+ status
+ in
+ let goal_list =
+ List.stable_sort (compare_goal_list proof) goal_list
+ in
+ Some (uri, (subst,(proof, goal_list)))
+ with ProofEngineTypes.Fail _ -> None
+ in
+ match status' with
+ | None -> aux tl
+ | Some status' -> status' :: aux tl)
+ in
+ List.stable_sort
+ (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
+ Pervasives.compare (List.length goals1) (List.length goals2))
+ (aux uris)
+
+let new_experimental_hint
+ ~(dbd:Mysql.dbd) ?(facts=false) ?signature ~universe
+ ((proof, goal) as status)
+=
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let (uris, (main, sig_constants)) =
+ match signature with
+ | Some signature ->
+ (sigmatch ~dbd ~facts signature, signature)
+ | None ->
+ (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in
+ let universe =
+ List.fold_left
+ (fun res u -> Constr.UriManagerSet.add u res)
+ Constr.UriManagerSet.empty universe in
+ let uris =
+ List.fold_left
+ (fun res (_,u) -> Constr.UriManagerSet.add u res)
+ Constr.UriManagerSet.empty uris in
+ let uris = Constr.UriManagerSet.inter uris universe in
+ let uris = Constr.UriManagerSet.elements uris in
+ let rec aux = function
+ | [] -> []
+ | uri :: tl ->
+ (let status' =
+ try
+ let (subst,(proof, goal_list)) =
+ (* debug_print ("STO APPLICANDO" ^ uri); *)
+ apply_tac_verbose
~term:(CicUtil.term_of_uri uri)
status
in