+let empty_tables =
+ (Saturation.make_active [],
+ Saturation.make_passive [],
+ Equality.mk_equality_bag)
+
+let init_cache_and_tables dbd use_library (proof, goal) =
+ let _, metasenv, _, _ = proof in
+ let newmeta = CicMkImplicit.new_meta metasenv [] in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let eq_uri =
+ match LibraryObjects.eq_URI() with
+ | None ->assert false
+ | Some eq_uri -> eq_uri in
+ let ct = find_context_theorems context metasenv in
+ let lt =
+ if use_library then
+ find_library_theorems dbd metasenv [goal]
+ else [] in
+ (* all equations are added to the cache *)
+ prerr_endline ("ho trovato " ^ (string_of_int (List.length lt)));
+ let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in
+ let equations,others = partition_equalities (ct@lt) in
+ let bag = Equality.mk_equality_bag () in
+ let units, other_equalities, newmeta =
+ partition_unit_equalities context metasenv newmeta bag equations in
+ (* other equations are added to the cache; note that untis equalities
+ are not)*)
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ (* let equalities =
+ Saturation.simplify_equalities bag eq_uri env units in *)
+ let passive = Saturation.make_passive units in
+ let no = List.length units in
+ prerr_endline ("No = " ^ (string_of_int no));
+ let active = Saturation.make_active [] in
+ let active,passive,newmeta =
+ Saturation.pump_actives context bag newmeta active passive (no+1) infinity
+ in
+ (active,passive,bag),cache,newmeta
+
+let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast =
+ let head, metasenv, args, newmeta =
+ ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ in
+ let propositional_args =
+ HExtlib.filter_map
+ (function
+ | Cic.Meta(i,_) ->
+ let _,_,mt = CicUtil.lookup_meta i metasenv in
+ let sort,u =
+ CicTypeChecker.type_of_aux' metasenv context mt
+ CicUniv.empty_ugraph
+ in
+ let b, _ =
+ CicReduction.are_convertible ~metasenv context
+ sort (Cic.Sort Cic.Prop) u
+ in
+ if b then Some i else None
+ | _ -> assert false)
+ args
+ in
+ let results,cache,newmeta =
+ if propositional_args = [] then
+ let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+ [args,metasenv,newmetas,head,newmeta],cache,newmeta
+ else
+ let proof =
+ None,metasenv,term,term (* term non e' significativo *)
+ in
+ let flags =
+ if fast then
+ {AutoTypes.default_flags() with
+ AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+ maxwidth = 2;maxdepth = 2;
+ use_paramod=true;use_only_paramod=false}
+ else
+ {AutoTypes.default_flags() with
+ AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+ maxwidth = 2;maxdepth = 4;
+ use_paramod=true;use_only_paramod=false}
+ in
+ match auto newmeta tables cache context metasenv propositional_args flags with
+ | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
+ | substs,cache,newmeta ->
+ List.map
+ (fun subst ->
+ let metasenv =
+ CicMetaSubst.apply_subst_metasenv subst metasenv
+ in
+ let head = CicMetaSubst.apply_subst subst head in
+ let newmetas =
+ List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
+ in
+ let args = List.map (CicMetaSubst.apply_subst subst) args in
+ let newm = CicMkImplicit.new_meta metasenv subst in
+ args,metasenv,newmetas,head,max newm newmeta)
+ substs, cache, newmeta
+ in
+ results,cache,newmeta
+
+let build_equalities auto context metasenv tables cache newmeta equations =
+ List.fold_left
+ (fun (facts,cache,newmeta) (t,ty) ->
+ (* in any case we add the equation to the cache *)
+ let cache = AutoCache.cache_add_list cache context [(t,ty)] in
+ try
+ let saturated,cache,newmeta =
+ fill_hypothesis context metasenv newmeta ty tables cache auto true
+ in
+ let (active,passive,bag) = tables in
+ let eqs,bag,newmeta =
+ List.fold_left
+ (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
+ let maxmeta,equality =
+ build_equality bag head args t newmetas newmeta'
+ in
+ equality::acc,bag,maxmeta)
+ ([],bag,newmeta) saturated
+ in
+ (eqs@facts, cache, newmeta)
+ with FillingFailure (cache,newmeta) ->
+ (* if filling hypothesis fails we add the equation to
+ the cache *)
+ (facts,cache,newmeta)
+ )
+ ([],cache,newmeta) equations
+
+let close_more tables maxmeta context status auto cache =
+ let (active,passive,bag) = tables in
+ let proof, goalno = status in
+ let _, metasenv,_,_ = proof in
+ let equations = retrieve_equations cache in
+ let eqs_and_types =
+ HExtlib.filter_map
+ (fun t ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty) else None)
+ equations in
+ let units, cache, maxm =
+ build_equalities auto context metasenv tables cache maxmeta eqs_and_types in
+ prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+ string_of_int maxm);
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality e))
+ units;
+ prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+ let passive = Saturation.add_to_passive units passive in
+ let no = List.length units in
+ prerr_endline ("No = " ^ (string_of_int no));
+ let active,passive,newmeta =
+ Saturation.pump_actives context bag maxm active passive (no+1) infinity
+ in
+ (active,passive,bag),cache,newmeta
+
+let find_context_equalities
+ maxmeta bag context proof cache
+=
+ prerr_endline "find_equalities";
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker in
+ let _,metasenv,_,_ = proof in
+ let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+ (* if use_auto is true, we try to close the hypothesis of equational
+ statements using auto; a naif, and probably wrong approach *)
+ let rec aux cache index newmeta = function
+ | [] -> [], newmeta,cache
+ | (Some (_, C.Decl (term)))::tl ->
+ debug_print
+ (lazy
+ (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
+ let do_find context term =
+ match term with
+ | C.Prod (name, s, t) when is_an_equality t ->
+ (try
+
+ let term = S.lift index term in
+ let saturated,cache,newmeta =
+ fill_hypothesis context metasenv newmeta term
+ empty_tables cache default_auto false
+ in
+ let eqs,newmeta =
+ List.fold_left
+ (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
+ let newmeta, equality =
+ build_equality
+ bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
+ in
+ equality::acc, newmeta + 1)
+ ([],newmeta) saturated
+ in
+ eqs, newmeta, cache
+ with FillingFailure (cache,newmeta) ->
+ [],newmeta,cache)
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when LibraryObjects.is_eq_URI uri ->
+ let term = S.lift index term in
+ let newmeta, e =
+ build_equality bag term [] (Cic.Rel index) [] newmeta
+ in
+ [e], (newmeta+1),cache
+ | _ -> [], newmeta, cache
+ in
+ let eqs, newmeta, cache = do_find context term in
+ let rest, newmeta,cache = aux cache (index+1) newmeta tl in
+ List.map (fun x -> index,x) eqs @ rest, newmeta, cache
+ | _::tl ->
+ aux cache (index+1) newmeta tl
+ in
+ let il, maxm, cache =
+ aux cache 1 newmeta context
+ in
+ let indexes, equalities = List.split il in
+ indexes, equalities, maxm, cache
+;;
+
+(***************** applyS *******************)