+ let _, metasenv, subst, _, _, _ = proof in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let add_list_to_tables metasenv subst automation_cache ct =
+ List.fold_left
+ (fun automation_cache (t,_) ->
+ AutomationCache.add_term_to_active automation_cache
+ metasenv subst context t None)
+ automation_cache ct
+ in
+ match restricted_univ with
+ | None ->
+ 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 automation_cache =
+ add_list_to_tables metasenv subst automation_cache ct
+ in
+(* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache
+ | Some restricted_univ ->
+ let t_ty =
+ List.map
+ (fun t ->
+ let ty, _ = CicTypeChecker.type_of_aux'
+ metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+ in
+ t, ty)
+ restricted_univ
+ in
+ (* let automation_cache = AutomationCache.empty () in *)
+ let automation_cache =
+ let universe = Universe.empty in
+ let universe =
+ Universe.index_list universe context t_ty
+ in
+ { automation_cache with AutomationCache.univ = universe }
+ in
+ let ct =
+ if use_context then find_context_theorems context metasenv else t_ty
+ in
+ let automation_cache =
+ add_list_to_tables metasenv subst automation_cache ct
+ in
+ (* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache_empty
+;;
+
+let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast =
+ let actives, passives, bag = tables in
+ let bag, head, metasenv, args =
+ Equality.saturate_term bag metasenv subst 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 subst 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 subst 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 signature universe cache =
+ let proof, goalno = status in
+ let _, metasenv,subst,_,_, _ = proof 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 subst 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 dbd 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 subst 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;
+ }
+
+
+let eq_of_goal = function
+ | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
+ uri
+ | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
+(* performs steps of rewrite with the universe, obtaining if possible
+ * a trivial goal *)
+let solve_rewrite ~automation_cache ~params:(univ,params) (proof,goal)=
+ let steps = int_of_string (string params "steps" "4") in
+ let use_context = bool params "use_context" true in
+ let universe, tables, cache =
+ init_cache_and_tables ~use_library:false ~use_context
+ automation_cache univ (proof,goal)
+ in
+ let actives, passives, bag = tables in
+ let pa,metasenv,subst,pb,pc,pd = proof in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ let eq_uri = eq_of_goal ty in
+ let initgoal = [], metasenv, ty in
+ let table =
+ let equalities = (Saturation.list_of_passive passives) in
+ List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities
+ in
+ let env = metasenv,context,CicUniv.oblivion_ugraph in
+ debug_print (lazy ("demod to solve: " ^ CicPp.ppterm ty));
+ match Indexing.solve_demodulating bag env table initgoal steps with
+ | Some (bag, gproof, metasenv, sub_subst, proof) ->
+ let subst_candidates,extra_infos =
+ List.split
+ (HExtlib.filter_map
+ (fun (i,c,_) ->
+ if i <> goal && c = context then Some (i,(c,ty)) else None)
+ metasenv)
+ in
+ let proofterm,proto_subst =
+ let proof = Equality.add_subst sub_subst proof in
+ Equality.build_goal_proof
+ bag eq_uri gproof proof ty subst_candidates context metasenv
+ in
+ let proofterm = Subst.apply_subst sub_subst proofterm in
+ let extrasubst =
+ HExtlib.filter_map
+ (fun (i,((c,ty),t)) ->
+ match t with
+ | Cic.Meta (j,_) when i=j -> None
+ | _ -> Some (i,(c,t,ty)))
+ (List.combine subst_candidates
+ (List.combine extra_infos proto_subst))
+ in
+ let subst = subst @ extrasubst in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let proofterm, _, metasenv,subst, _ =
+ CicRefine.type_of metasenv subst context proofterm
+ CicUniv.oblivion_ugraph
+ in
+ let status = (pa,metasenv,subst,pb,pc,pd), goal in
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) status
+ | None ->
+ raise
+ (ProofEngineTypes.Fail (lazy
+ ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
+;;
+
+(* Demodulate thorem *)
+let open_type ty bo =
+ let rec open_type_aux context ty k args =
+ match ty with
+ | Cic.Prod (n,s,t) ->
+ let n' =
+ FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
+ let entry = match n' with
+ | Cic.Name _ -> Some (n',(Cic.Decl s))
+ | Cic.Anonymous -> None
+ in
+ open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
+ | Cic.LetIn (n,s,sty,t) ->
+ let entry = Some (n,(Cic.Def (s,sty)))
+ in
+ open_type_aux (entry::context) t (k+1) args
+ | _ -> context, ty, args
+ in
+ let context, ty, args = open_type_aux [] ty 1 [] in
+ match args with
+ | [] -> context, ty, bo
+ | _ -> context, ty, Cic.Appl (bo::args)
+;;
+
+let rec close_type bo ty context =
+ match context with
+ | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
+ | Some (n,(Cic.Decl s))::tl ->
+ close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
+ | Some (n,(Cic.Def (s,sty)))::tl ->
+ close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
+ | _ -> assert false
+;;
+
+let is_subsumed univ context ty =
+ let candidates = Universe.get_candidates univ ty in
+ List.fold_left
+ (fun res cand ->
+ match res with
+ | Some found -> Some found
+ | None ->
+ try
+ let mk_irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable in
+ let metasenv = [(0,context,ty)] in
+ let fake_proof =
+ None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[]
+ in
+ let (_,metasenv,subst,_,_,_), open_goals =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:cand)
+ (fake_proof,0)
+ in
+ let prop_goals, other =
+ split_goals_in_prop metasenv subst open_goals
+ in
+ if prop_goals = [] then Some cand else None
+ with
+ | ProofEngineTypes.Fail s -> None
+ | CicUnification.Uncertain s -> None
+ ) None candidates
+;;
+
+let demodulate_theorem ~automation_cache uri =
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
+ let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ let context,ty,bo =
+ match obj with
+ | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
+ | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
+ in
+ if CicUtil.is_closed ty then
+ raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
+ let initgoal = [], [], ty in
+ (* compute the signature *)
+ let signature =
+ let ty_set = MetadataConstraints.constants_of ty in
+ let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
+ let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
+ MetadataQuery.close_with_types set [] context
+ in
+ (* retrieve equations from the universe universe *)
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
+ let equations =
+ retrieve_equations true signature universe AutoCache.cache_empty context []
+ 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' [] 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 bag, units, _, newmeta =
+ partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
+ in
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ Indexing.empty units
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ Indexing.demod bag
+ ([],context,CicUniv.oblivion_ugraph) table initgoal in
+ if changed then
+ begin
+ let oldproof = Equality.Exact bo in
+ let proofterm,_ =
+ Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
+ eq_uri newproof oldproof ty [] context newmetasenv
+ in
+ if newmetasenv <> [] then
+ raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
+ else
+ begin
+ assert_proof_is_valid proofterm newmetasenv context newty;
+ match is_subsumed universe context newty with
+ | Some t -> raise
+ (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
+ | None -> close_type proofterm newty context
+ end
+ end
+ else (* if newty = ty then *)
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+ (*else ProofEngineTypes.apply_tactic
+ (ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
+;;
+
+
+(* NEW DEMODULATE *)
+let demodulate ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
+ let universe, tables, cache =
+ init_cache_and_tables
+ ~dbd ~use_library:false ~use_context:true
+ automation_cache univ (proof,goal)
+ in
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
+ let active, passive, bag = tables in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let initgoal = [], metasenv, ty in
+ let equalities = (Saturation.list_of_passive passive) in
+ (* we demodulate using both actives passives *)
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities)));
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
+ equalities;
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ (snd active) equalities
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ (* Indexing.demodulation_goal bag *)
+ Indexing.demod bag
+ (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
+ in
+ if changed then
+ begin
+ let maxm = CicMkImplicit.new_meta metasenv subst in
+ let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
+ let subst_candidates = List.map (fun (i,_,_) -> i) metasenv in
+ let subst_candidates = List.filter (fun x-> x <> goal) subst_candidates in
+ let proofterm, proto_subst =
+ Equality.build_goal_proof (~contextualize:false) bag
+ eq_uri newproof opengoal ty subst_candidates context metasenv
+ in
+ (* XXX understan what to do with proto subst *)
+ let metasenv = (maxm,context,newty)::metasenv in
+ let proofterm, _, metasenv, subst, _ =
+ CicRefine.type_of metasenv subst context proofterm
+ CicUniv.oblivion_ugraph
+ in
+ let extended_status = (curi,metasenv,subst,pbo,pty, attrs),goal in
+ let proof,gl =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) extended_status
+ in
+ proof,maxm::gl
+ end
+ else
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+;;
+
+let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ let all = bool flags "all" false in
+ if all then
+ solve_rewrite ~params ~automation_cache status
+ else
+ demodulate ~dbd ~params ~automation_cache status)
+;;
+(***************** applyS *******************)
+
+let apply_smart_aux
+ dbd automation_cache (params:auto_params) proof goal newmeta' metasenv' subst
+ context term' ty termty goal_arity
+=
+ let consthead,newmetasenv,arguments,_ =
+ TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in