+ let _, metasenv, _, _, _, _ = proof in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ if restricted_univ = [] then
+ let ct =
+ if use_context then find_context_theorems context metasenv else []
+ in
+ let lt =
+ match use_library, dbd with
+ | true, Some dbd -> find_library_theorems dbd metasenv goal
+ | _ -> []
+ in
+ let cache = AutoCache.cache_empty in
+ let cache = cache_add_list cache context (ct@lt) in
+ let tables =
+ let env = metasenv, context, CicUniv.oblivion_ugraph in
+ List.fold_left
+ (fun (a,p,b) (t,ty) ->
+ let mes = CicUtil.metas_of_term ty in
+ Saturation.add_to_active b a p env ty t
+ (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
+ automation_cache.AutomationCache.tables ct
+ in
+(* AutomationCache.pp_cache { automation_cache with AutomationCache.tables =
+ * tables }; *)
+ automation_cache.AutomationCache.univ, tables, cache
+ else
+ let metasenv, t_ty, s_t_ty, _ =
+ List.fold_left
+ (fun (metasenv,acc, sacc, maxmeta) t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+ in
+ let head, metasenv, args, maxmeta =
+ TermUtil.saturate_term maxmeta metasenv context ty 0
+ in
+ let st = if args = [] then t else Cic.Appl (t::args) in
+ metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
+ (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ
+ in
+ let automation_cache = AutomationCache.empty () in
+ let automation_cache =
+ let universe = automation_cache.AutomationCache.univ in
+ let universe =
+ Universe.index_list universe context t_ty
+ in
+ { automation_cache with AutomationCache.univ = universe }
+ in
+ let automation_cache =
+ List.fold_left
+ (fun c (t,ty) ->
+ AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
+ automation_cache s_t_ty
+ in
+(* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache_add_list cache_empty context t_ty
+;;
+ (*
+(* let signature = MetadataQuery.signature_of metasenv goal in *)
+(* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
+ let equations =
+ retrieve_equations dont_filter (* true *) 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 term tables (universe:Universe.universe) cache auto fast =
+ let actives, passives, bag = tables in
+ let bag, head, metasenv, args =
+ Equality.saturate_term bag metasenv context term
+ in
+ let tables = actives, passives, bag 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,tables =
+ if propositional_args = [] then
+ let _,_,bag = tables in
+ let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
+ [args,metasenv,newmetas,head],cache,tables
+ 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 tables universe cache context metasenv propositional_args flags with
+ | [],cache,tables -> raise (FillingFailure (cache,tables))
+ | substs,cache,tables ->
+ let actives, passaives, bag = tables in
+ let bag, res =
+ List.fold_right
+ (fun subst (bag,acc) ->
+ let metasenv =
+ CicMetaSubst.apply_subst_metasenv subst metasenv
+ in
+ let head = CicMetaSubst.apply_subst subst head in
+ let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
+ let args = List.map (CicMetaSubst.apply_subst subst) args in
+ let newm = CicMkImplicit.new_meta metasenv subst in
+ let bag = Equality.push_maxmeta bag newm in
+ bag, ((args,metasenv,newmetas,head) :: acc))
+ substs (bag,[])
+ in
+ let tables = actives, passives, bag in
+ res, cache, tables
+ in
+ results,cache,tables
+;;
+
+let build_equalities auto context metasenv tables universe cache equations =
+ List.fold_left
+ (fun (tables,facts,cache) (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, tables =
+ fill_hypothesis context metasenv ty tables universe cache auto true
+ in
+ let eqs, tables =
+ List.fold_left
+ (fun (acc, tables) (args,metasenv,newmetas,head) ->
+ let actives, passives, bag = tables in
+ let bag, equality =
+ build_equality bag head args t newmetas
+ in
+ let tables = actives, passives, bag in
+ equality::acc,tables)
+ ([],tables) saturated
+ in
+ (tables, eqs@facts, cache)
+ with FillingFailure (cache,tables) ->
+ (* if filling hypothesis fails we add the equation to
+ the cache *)
+ (tables,facts,cache)
+ )
+ (tables,[],cache) equations
+
+let close_more tables context status auto universe cache =
+ 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 tables, units, cache =
+ build_equalities auto context metasenv tables universe cache eqs_and_types
+ in
+ let active,passive,bag = tables in
+ let passive = Saturation.add_to_passive units passive in
+ let no = List.length units in
+ let active, passive, bag =
+ Saturation.pump_actives context bag active passive (no+1) infinity
+ in
+ (active,passive,bag), cache
+;;
+
+let find_context_equalities tables 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
+ (* 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 tables cache index = function
+ | [] -> tables, [], cache
+ | (Some (_, C.Decl (term)))::tl ->
+ debug_print
+ (lazy
+ (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
+ let do_find tables 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, tables =
+ fill_hypothesis context metasenv term
+ tables universe cache default_auto false
+ in
+ let actives, passives, bag = tables in
+ let bag,eqs =
+ List.fold_left
+ (fun (bag,acc) (args,metasenv,newmetas,head) ->
+ let bag, equality =
+ build_equality bag head args (Cic.Rel index) newmetas
+ in
+ bag, equality::acc)
+ (bag,[]) saturated
+ in
+ let tables = actives, passives, bag in
+ tables, eqs, cache
+ with FillingFailure (cache,tables) ->
+ tables, [], cache)
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when LibraryObjects.is_eq_URI uri ->
+ let term = S.lift index term in
+ let actives, passives, bag = tables in
+ let bag, e =
+ build_equality bag term [] (Cic.Rel index) []
+ in
+ let tables = actives, passives, bag in
+ tables, [e], cache
+ | _ -> tables, [], cache
+ in
+ let tables, eqs, cache = do_find tables context term in
+ let tables, rest, cache = aux tables cache (index+1) tl in
+ tables, List.map (fun x -> index,x) eqs @ rest, cache
+ | _::tl ->
+ aux tables cache (index+1) tl
+ in
+ let tables, il, cache = aux tables cache 1 context in
+ let indexes, equalities = List.split il in
+ tables, indexes, equalities, cache
+;;
+
+(********** PARAMETERS PASSING ***************)
+
+let bool params name default =
+ try
+ let s = List.assoc name params in
+ if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+ else if s = "0" || s = "false" || s = "no" || s= "off" then false
+ else
+ let msg = "Unrecognized value for parameter "^name^"\n" in
+ let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
+ raise (ProofEngineTypes.Fail (lazy msg))
+ with Not_found -> default
+;;
+
+let string params name default =
+ try List.assoc name params with
+ | Not_found -> default
+;;
+
+let int params name default =
+ try int_of_string (List.assoc name params) with
+ | Not_found -> default
+ | Failure _ ->
+ raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
+;;
+
+let flags_of_params params ?(for_applyS=false) () =
+ let int = int params in
+ let bool = bool params in
+ let close_more = bool "close_more" false in
+ let use_paramod = bool "use_paramod" true in
+ let skip_trie_filtering = bool "skip_trie_filtering" false in
+ let skip_context = bool "skip_context" false in
+ let use_only_paramod =
+ if for_applyS then true else bool "paramodulation" false in
+ let use_library = bool "library"
+ ((AutoTypes.default_flags()).AutoTypes.use_library) in
+ let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+ let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
+ let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
+ let do_type = bool "type" false in
+ let timeout = int "timeout" 0 in
+ { AutoTypes.maxdepth =
+ if use_only_paramod then 2 else depth;
+ AutoTypes.maxwidth = width;
+ AutoTypes.maxsize = size;
+ AutoTypes.timeout =
+ if timeout = 0 then
+ if for_applyS then Unix.gettimeofday () +. 30.0
+ else
+ infinity
+ else
+ Unix.gettimeofday() +. (float_of_int timeout);
+ AutoTypes.use_library = use_library;
+ AutoTypes.use_paramod = use_paramod;
+ AutoTypes.use_only_paramod = use_only_paramod;
+ AutoTypes.close_more = close_more;
+ AutoTypes.dont_cache_failures = false;
+ AutoTypes.maxgoalsizefactor = gsize;
+ AutoTypes.do_types = do_type;
+ AutoTypes.skip_trie_filtering = skip_trie_filtering;
+ AutoTypes.skip_context = skip_context;
+ }
+
+(***************** applyS *******************)
+
+let apply_smart_aux
+ dbd flags automation_cache univ proof goal newmeta' metasenv'
+ context term' ty termty goal_arity
+=
+(* let ppterm = ppterm context in *)