+let is_propositional context sort =
+ match CicReduction.whd context sort with
+ | Cic.Sort Cic.Prop
+ | Cic.Sort (Cic.CProp _) -> true
+ | _-> false
+;;
+
+
+type auto_params = Cic.term list * (string * string) list
+
+let elems = ref [] ;;
+
+(* closing a term w.r.t. its metavariables
+ very naif version: it does not take dependencies properly into account *)
+
+let naif_closure ?(prefix_name="xxx_") t metasenv context =
+ let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
+ let n = List.length metasenv in
+ let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
+ let _,with_what =
+ List.fold_left
+ (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc))
+ (n,[]) metasenv
+ in
+ let t = CicSubstitution.lift n t in
+ let body =
+ ProofEngineReduction.replace_lifting
+ ~equality:(fun c t1 t2 ->
+ match t1,t2 with
+ | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
+ | _ -> false)
+ ~context ~what ~with_what ~where:t
+ in
+ let _, t =
+ List.fold_left
+ (fun (n,t) (_,cc,ty) ->
+ n-1, Cic.Lambda(Cic.Name (prefix_name^string_of_int n),
+ CicSubstitution.lift n ty,t))
+ (n-1,body) metasenv
+ in
+ t
+;;
+
+let lambda_close ?prefix_name t menv ctx =
+ let t = naif_closure ?prefix_name t menv ctx in
+ List.fold_left
+ (fun (t,i) -> function
+ | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
+ | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
+ | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
+ (t,List.length menv) ctx
+;;
+
+(* functions for retrieving theorems *)
+
+exception FillingFailure of AutoCache.cache * int
+
+let rec unfold context = function
+ | Cic.Prod(name,s,t) ->
+ let t' = unfold ((Some (name,Cic.Decl s))::context) t in
+ Cic.Prod(name,s,t')
+ | t -> ProofEngineReduction.unfold context t
+
+let find_library_theorems dbd proof goal =
+ let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
+ let terms = List.map CicUtil.term_of_uri univ in
+ List.map
+ (fun t ->
+ (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph)))
+ terms
+
+let find_context_theorems context metasenv =
+ let l,_ =
+ List.fold_left
+ (fun (res,i) ctxentry ->
+ match ctxentry with
+ | Some (_,Cic.Decl t) ->
+ (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
+ | Some (_,Cic.Def (_,t)) ->
+ (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
+ | None -> res,i+1)
+ ([],1) context
+ in l
+
+let rec is_an_equality = function
+ | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
+ when (LibraryObjects.is_eq_URI uri) -> true
+ | Cic.Prod (_, _, t) -> is_an_equality t
+ | _ -> false
+;;
+
+let partition_equalities =
+ List.partition (fun (_,ty) -> is_an_equality ty)
+
+
+let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
+
+
+let is_unit_equation context metasenv oldnewmeta term =
+ 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.oblivion_ugraph
+ in
+ if is_propositional context sort then Some i else None
+ | _ -> assert false)
+ args
+ in
+ if propositional_args = [] then
+ let newmetas =
+ List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
+ in
+ Some (args,metasenv,newmetas,head,newmeta)
+ else None
+;;
+
+let get_candidates universe cache t =
+ let candidates=
+ (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
+ in
+ let debug_msg =
+ (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
+ (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
+ debug_print debug_msg;
+ candidates
+;;
+
+let only signature context metasenv t =
+ try
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
+ in
+ let consts = MetadataConstraints.constants_of ty in
+ let b = MetadataConstraints.UriManagerSet.subset consts signature in
+ if b then b
+ else
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ MetadataConstraints.UriManagerSet.subset consts' signature
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> assert false
+ | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
+;;
+
+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 dont_filter signature universe cache context metasenv =
+ 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
+ if dont_filter then candidates
+ else
+ let candidates = List.filter not_default_eq_term candidates in
+ List.filter (only signature context metasenv) 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) ->
+ if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
+ let _ =
+ HLog.warn
+ ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
+ ^ " since it is not meta closed")
+ in
+ units,(t,ty)::other,maxmeta
+ else
+ 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 use_context dont_filter universe (proof, goal)
+=
+ (* the local cache in initially empty *)
+ let cache = AutoCache.cache_empty in
+ let _, metasenv, _subst,_, _, _ = 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 = if use_context then find_context_theorems context metasenv else [] in
+ debug_print
+ (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
+ let lt =
+ match use_library, dbd with
+ | true, Some dbd -> find_library_theorems dbd metasenv goal
+ | _ -> []
+ in
+ debug_print
+ (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
+ let cache = cache_add_list cache context (ct@lt) in
+ let equations =
+ retrieve_equations dont_filter signature universe cache context metasenv
+ in
+ debug_print
+ (lazy ("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.oblivion_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 ProofEngineTypes.Fail _ -> None)
+ 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
+ (* SIMPLIFICATION STEP
+ let equalities =
+ let env = (metasenv, context, CicUniv.oblivion_ugraph) in
+ let eq_uri = HExtlib.unopt (LibraryObjects.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.oblivion_ugraph
+ in
+ if is_propositional context sort 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,_subst,_,_, _ = proof in
+ let signature = MetadataQuery.signature_of metasenv goalno in
+ let equations =
+ retrieve_equations false signature universe cache context metasenv
+ in
+ let eqs_and_types =
+ HExtlib.filter_map
+ (fun t ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.oblivion_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
+ debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+ string_of_int maxm));
+ List.iter
+ (fun e -> debug_print (lazy (Equality.string_of_equality e)))
+ units;
+ debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
+ let passive = Saturation.add_to_passive units passive in
+ let no = List.length units in
+ debug_print (lazy ("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,_subst,_,_, _ = 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