final_subst, proof, open_goals
;;
-let find_equalities dbd status smart_flag ?auto cache =
+let find_equalities dbd status smart_flag auto cache =
let proof, goalno = status in
let _, metasenv,_,_ = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm, cache =
- Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache
+ Equality_retrieval.find_context_equalities 0 bag auto context proof cache
in
prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
let lib_eq_uris, library_equalities, maxm, cache =
Equality_retrieval.find_library_equalities bag
- ?auto smart_flag dbd context (proof, goalno) (maxm+2)
+ auto smart_flag dbd context (proof, goalno) (maxm+2)
cache
in
prerr_endline (">>>>>>>>>> gained from the library >>>>>>>>>>>>" ^
bag, equalities, cache, maxm
;;
-let saturate_more bag active maxmeta status smart_flag ?auto cache =
+let close_more bag active maxmeta status smart_flag auto cache =
let proof, goalno = status in
let _, metasenv,_,_ = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let eq_indexes, equalities, maxm, cache =
- Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache
+ Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
in
prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
string_of_int maxm);
let saturate
smart_flag
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width)
- ?(timeout=600.) ?auto status =
+ ?(timeout=600.) auto status =
let module C = Cic in
reset_refs ();
maxdepth := depth;
let env = (metasenv, context, ugraph) in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
let bag, equalities, cache, maxm =
- find_equalities dbd status smart_flag ?auto AutoCache.cache_empty
+ find_equalities dbd status smart_flag auto AutoCache.cache_empty
in
let res, time =
maxmeta := maxm+2;
let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let eq_uri = eq_of_goal ty in
- let bag = Equality.mk_equality_bag () in
- let eq_indexes, equalities, maxm, cache =
- Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
- in
- let lib_eq_uris, library_equalities, maxm, cache =
- Equality_retrieval.find_library_equalities bag
- false dbd context (proof, goal) (maxm+2) cache
- in
- if library_equalities = [] then prerr_endline "VUOTA!!!";
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let library_equalities = List.map snd library_equalities in
let initgoal = [], [], ty in
- let env = (metasenv, context, CicUniv.empty_ugraph) in
- let equalities =
- simplify_equalities bag eq_uri env (equalities@library_equalities)
- in
+ let eq_uri = eq_of_goal ty in
+ let bag, equalities, cache, maxm =
+ find_equalities dbd (proof,goal) false None AutoCache.cache_empty
+ in
let table =
List.fold_left
(fun tbl eq -> Indexing.index tbl eq)
let names = Utils.names_of_context context in
let bag = Equality.mk_equality_bag () in
let eq_index, equalities, maxm,cache =
- Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
+ Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty
in
let eq_what =
let what = find_in_ctx 1 target context in
let eq_uri = eq_of_goal type_of_goal in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm,cache =
- Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
+ Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in
let ugraph = CicUniv.empty_ugraph in
let env = (metasenv, context, ugraph) in
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm, cache =
- Equality_retrieval.find_library_equalities bag
+ Equality_retrieval.find_library_equalities bag None
false dbd context (proof, goal') (maxm+2) cache
in
let t2 = Unix.gettimeofday () in
let eq_uri = eq_of_goal goal in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm, cache =
- Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
+ Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in
let lib_eq_uris, library_equalities, maxm,cache =
- Equality_retrieval.find_library_equalities bag
+ Equality_retrieval.find_library_equalities bag None
false dbd context (proof, goal') (maxm+2) cache
in
let library_equalities = List.map snd library_equalities in