+let not_default_eq_term t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ not (LibraryObjects.in_eq_URIs uri)
+ with Invalid_argument _ -> true
+
+let retrieve_equations signature universe cache context=
+ match LibraryObjects.eq_URI() with
+ | None -> []
+ | Some eq_uri ->
+ let eq_uri = UriManager.strip_xpointer eq_uri in
+ let fake= Cic.Meta(-1,[]) in
+ let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
+ let candidates = get_candidates universe cache fake_eq in
+ (* defaults eq uris are built-in in auto *)
+ let candidates = List.filter not_default_eq_term candidates in
+ let candidates = List.filter (only signature context) candidates in
+ List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
+ candidates
+
+let build_equality bag head args proof newmetas maxmeta =
+ match head with
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
+ let p =
+ if args = [] then proof else Cic.Appl (proof::args)
+ in
+ let o = !Utils.compare_terms t1 t2 in
+ let stat = (ty,t1,t2,o) in
+ (* let w = compute_equality_weight stat in *)
+ let w = 0 in
+ let proof = Equality.Exact p in
+ let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
+ (* to clean the local context of metas *)
+ Equality.fix_metas bag maxmeta e
+ | _ -> assert false
+;;
+
+let partition_unit_equalities context metasenv newmeta bag equations =
+ List.fold_left
+ (fun (units,other,maxmeta)(t,ty) ->
+ match is_unit_equation context metasenv maxmeta ty with
+ | Some (args,metasenv,newmetas,head,newmeta') ->
+ let maxmeta,equality =
+ build_equality bag head args t newmetas newmeta' in
+ equality::units,other,maxmeta
+ | None ->
+ units,(t,ty)::other,maxmeta)
+ ([],[],newmeta) equations
+
+let empty_tables =
+ (Saturation.make_active [],
+ Saturation.make_passive [],
+ Equality.mk_equality_bag)
+
+let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
+ (* the local cache in initially empty *)
+ let cache = AutoCache.cache_empty in
+ let _, metasenv, _, _, _ = proof in
+ let signature = MetadataQuery.signature_of metasenv goal in
+ let newmeta = CicMkImplicit.new_meta metasenv [] in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let ct = find_context_theorems context metasenv in
+ prerr_endline
+ ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
+ let lt =
+ if use_library then
+ find_library_theorems dbd metasenv goal
+ else [] in
+ prerr_endline
+ ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
+ let cache = cache_add_list cache context (ct@lt) in
+ let equations =
+ retrieve_equations signature universe cache context in
+ prerr_endline
+ ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
+ 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
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with _ -> None) (* catturare l'eccezione giusta di unfold *)
+ equations in
+ let bag = Equality.mk_equality_bag () in
+ let units, other_equalities, newmeta =
+ partition_unit_equalities context metasenv newmeta bag eqs_and_types in
+ (* let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let equalities =
+ let eq_uri =
+ match LibraryObjects.eq_URI() with
+ | None ->assert false
+ | Some eq_uri -> eq_uri in
+ Saturation.simplify_equalities bag eq_uri env units in *)
+ let passive = Saturation.make_passive units in
+ let no = List.length units in
+ let active = Saturation.make_active [] in
+ let active,passive,newmeta =
+ if paramod then active,passive,newmeta
+ else
+ 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 (universe:Universe.universe) cache auto fast =
+ let head, metasenv, args, newmeta =
+ TermUtil.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 universe 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 universe 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 universe 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 universe cache =
+ let (active,passive,bag) = tables in
+ let proof, goalno = status in
+ let _, metasenv,_,_, _ = proof in
+ let signature = MetadataQuery.signature_of metasenv goalno in
+ let equations = retrieve_equations signature universe cache context 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 universe 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 (universe:Universe.universe) cache
+=
+ 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 universe 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
+;;