X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=34b305ba54d06e7d3f514e9dc2b018bf783805db;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=1b172786a7a44a071f28079c8dbdf409a8c996ec;hpb=bdbe077ddb0b377823b6806adc8bece82130c992;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 1b172786a..34b305ba5 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -38,12 +38,14 @@ let ppterm ctx t = let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in CicPp.pp t names ;; + let is_propositional context sort = match CicReduction.whd context sort with | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true | _-> false ;; + let is_in_prop context subst metasenv ty = let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in is_propositional context sort @@ -366,8 +368,15 @@ let init_cache_and_tables ?dbd ~use_library ~use_context automation_cache restricted_univ (proof, goal) = - let _, metasenv, _, _, _, _ = proof in + 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 if restricted_univ = [] then let ct = if use_context then find_context_theorems context metasenv else [] @@ -379,103 +388,47 @@ let init_cache_and_tables 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 + let automation_cache = + add_list_to_tables metasenv subst automation_cache ct in -(* AutomationCache.pp_cache { automation_cache with AutomationCache.tables = - * tables }; *) - automation_cache.AutomationCache.univ, tables, cache +(* AutomationCache.pp_cache automation_cache; *) + automation_cache.AutomationCache.univ, + automation_cache.AutomationCache.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 + 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 = AutomationCache.empty () in *) let automation_cache = - let universe = automation_cache.AutomationCache.univ in + 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 = - List.fold_left - (fun c (t,ty) -> - AutomationCache.add_term_to_active c metasenv [] context t (Some ty)) - automation_cache s_t_ty + add_list_to_tables metasenv subst automation_cache ct in -(* AutomationCache.pp_cache automation_cache; *) + (* AutomationCache.pp_cache automation_cache; *) automation_cache.AutomationCache.univ, automation_cache.AutomationCache.tables, - cache_add_list cache_empty context t_ty + cache_empty ;; - (* -(* 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 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 context term + Equality.saturate_term bag metasenv subst context term in let tables = actives, passives, bag in let propositional_args = @@ -537,14 +490,14 @@ let fill_hypothesis context metasenv term tables (universe:Universe.universe) ca results,cache,tables ;; -let build_equalities auto context metasenv tables universe cache equations = +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 ty tables universe cache auto true + fill_hypothesis context metasenv subst ty tables universe cache auto true in let eqs, tables = List.fold_left @@ -565,10 +518,9 @@ let build_equalities auto context metasenv tables universe cache equations = ) (tables,[],cache) equations -let close_more tables context status auto universe cache = +let close_more tables context status auto signature universe cache = let proof, goalno = status in - let _, metasenv,_subst,_,_, _ = proof in - let signature = MetadataQuery.signature_of metasenv goalno in + let _, metasenv,subst,_,_, _ = proof in let equations = retrieve_equations false signature universe cache context metasenv in @@ -582,7 +534,7 @@ let close_more tables context status auto universe cache = 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 + 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 @@ -593,12 +545,12 @@ let close_more tables context status auto universe cache = (active,passive,bag), cache ;; -let find_context_equalities tables context proof (universe:Universe.universe) 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 + 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 @@ -613,7 +565,7 @@ let find_context_equalities tables context proof (universe:Universe.universe) ca (try let term = S.lift index term in let saturated, cache, tables = - fill_hypothesis context metasenv term + fill_hypothesis context metasenv subst term tables universe cache default_auto false in let actives, passives, bag = tables in @@ -717,92 +669,408 @@ let flags_of_params params ?(for_applyS=false) () = 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 flags automation_cache univ proof goal newmeta' metasenv' - context term' ty termty goal_arity + dbd automation_cache params proof goal newmeta' metasenv' subst + context term' ty termty goal_arity = -(* let ppterm = ppterm context in *) - let (consthead,newmetasenv,arguments,_) = + let consthead,newmetasenv,arguments,_ = TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let term'' = - match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) + match arguments with + | [] -> term' + | _ -> Cic.Appl (term'::arguments) in - let proof',oldmetasenv = - let (puri,metasenv,_subst,pbo,pty, attrs) = proof in - (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv + let consthead = + let rec aux t = function + | [] -> + let t = CicReduction.normalize ~delta:false context t in + (match t, ty with + | Cic.Appl (hd1::_), Cic.Appl (hd2::_) when hd1 <> hd2 -> + let t = ProofEngineReduction.unfold context t in + (match t with + | Cic.Appl (hd1'::_) when hd1' = hd2 -> t + | _ -> raise (ProofEngineTypes.Fail (lazy "incompatible head"))) + | _ -> t) + | arg :: tl -> + match CicReduction.whd context t with + | Cic.Prod (_,_,tgt) -> + aux (CicSubstitution.subst arg tgt) tl + | _ -> assert false + in + aux termty arguments in let goal_for_paramod = match LibraryObjects.eq_URI () with | Some uri -> - Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty] + Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Implicit (Some `Type); consthead; ty] | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) in - let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in - let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in - let proof'' = - let uri,_,_subst,p,ty, attrs = proof' in - uri,metasenv_for_paramod,_subst,p,ty, attrs - in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let proof''',goals = - ProofEngineTypes.apply_tactic - (EqualityTactics.rewrite_tac ~direction:`RightToLeft - ~pattern:(ProofEngineTypes.conclusion_pattern None) - (Cic.Meta(newmeta,irl)) []) - (proof'',goal) - in - let goal = match goals with [g] -> g | _ -> assert false in - let proof'''', _ = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac term'') - (proof''',goal) - in - let universe, tables, cache = - init_cache_and_tables ~dbd ~use_library:flags.use_library - ~use_context:true automation_cache univ (proof'''',newmeta) - in - let active, passive, bag = tables in - match - Saturation.given_clause bag (proof'''',newmeta) active passive - 20 10 flags.timeout - with - | None, _,_,_ -> - raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) - | Some (_,proof''''',_), active,passive,bag -> - proof''''', - ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive -(* - debug_print - (lazy - ("SUBSUMPTION SU: " ^ string_of_int newmeta ^ " " ^ ppterm goal_for_paramod)); - let res, maxmeta = - Saturation.all_subsumed bag maxm (proof'''',newmeta) active passive + try + let goal_for_paramod, _, newmetasenv, subst, _ = + CicRefine.type_of newmetasenv subst context goal_for_paramod + CicUniv.oblivion_ugraph + in + let newmeta = CicMkImplicit.new_meta newmetasenv subst in + let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in + let proof'' = + let uri,_,_,p,ty, attrs = proof in + uri,metasenv_for_paramod,subst,p,ty, attrs + in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in +(* + prerr_endline ("------ prima di rewrite su ------ " ^ string_of_int goal); + prerr_endline ("menv:\n"^CicMetaSubst.ppmetasenv [] metasenv_for_paramod); + prerr_endline ("subst:\n"^CicMetaSubst.ppsubst + ~metasenv:(metasenv_for_paramod) + subst); +*) + + let (proof''',goals) = + ProofEngineTypes.apply_tactic + (EqualityTactics.rewrite_tac ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) + (Cic.Meta(newmeta,irl)) []) (proof'',goal) + in + let goal = match goals with [g] -> g | _ -> assert false in + let proof'''', _ = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac term'') + (proof''',goal) + in + + + let (_,m,_,_,_,_ as p) = + let pu,metasenv,subst,proof,px,py = proof'''' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + let proof'''' = pu,metasenv,subst,proof,px,py in + let univ, params = params in + let use_context = bool params "use_context" true in + let universe, (active,passive,bag), cache = + init_cache_and_tables ~use_library:false ~use_context + automation_cache univ (proof'''',newmeta) in - if res = [] then - raise (ProofEngineTypes.Fail (lazy("BUM"))) - else let (_,proof''''',_) = List.hd res in - proof''''',ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive + match + Saturation.solve_narrowing bag (proof'''',newmeta) active passive + 1 (*0 infinity*) + with + | None, active, passive, bag -> + raise (ProofEngineTypes.Fail (lazy ("paramod fails"))) + | Some(subst',(pu,metasenv,_,proof,px, py),open_goals),active, + passive,bag -> + assert_subst_are_disjoint subst subst'; + let subst = subst@subst' in + pu,metasenv,subst,proof,px,py + in + +(* + let (_,m,_,_,_,_ as p),_ = + solve_rewrite ~params ~automation_cache (proof'''',newmeta) + in *) -;; -let rec count_prods context ty = - match CicReduction.whd context ty with - Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t - | _ -> 0 + let open_goals = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m + in + p, open_goals + with + CicRefine.RefineFailure msg -> + raise (ProofEngineTypes.Fail msg) +;; let apply_smart - ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal) + ~dbd ~term ~automation_cache ~params (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_subst,_,_, _) = proof in + let (_,metasenv,subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let flags = flags_of_params params ~for_applyS:true () in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -838,24 +1106,35 @@ let apply_smart in let metasenv' = metasenv@newmetasenvfragment in let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph + CicTypeChecker.type_of_aux' + metasenv' ~subst context term' CicUniv.oblivion_ugraph in let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in - let goal_arity = count_prods context ty in - let proof, gl, active, passive = - apply_smart_aux dbd flags automation_cache univ proof goal - newmeta' metasenv' context term' ty termty goal_arity + let goal_arity = + let rec count_prods context ty = + match CicReduction.whd ~subst context ty with + | Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + in + count_prods context ty in - proof, gl, active, passive + apply_smart_aux dbd automation_cache params proof goal + newmeta' metasenv' subst context term' ty termty goal_arity ;; -(****************** AUTO ********************) - +let applyS_tac ~dbd ~term ~params ~automation_cache = + ProofEngineTypes.mk_tactic + (fun status -> + try + apply_smart ~dbd ~term ~params ~automation_cache status + with + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (ProofEngineTypes.Fail msg)) +;; -(* -let prop = function (_,depth,P) -> depth < 9 | _ -> false;; -*) +(****************** AUTO ********************) let calculate_timeout flags = if flags.timeout = 0. then @@ -868,20 +1147,10 @@ let is_equational_case goalty flags = let ensure_equational t = if is_an_equational_goal t then true else false - (* - let msg="Not an equational goal.\nYou cant use the paramodulation flag"in - raise (ProofEngineTypes.Fail (lazy msg)) - *) in (flags.use_paramod && is_an_equational_goal goalty) || (flags.use_only_paramod && ensure_equational goalty) ;; -(* -let cache_add_success sort cache k v = - if sort = P then cache_add_success cache k v else cache_remove_underinspection - cache k -;; -*) type menv = Cic.metasenv type subst = Cic.substitution @@ -951,7 +1220,8 @@ let calculate_closed_goal_ty (goalno,_,_) s = let cc,_,goalty = List.assoc goalno s in (* XXX applicare la subst al contesto? *) Some (cc, CicMetaSubst.apply_subst s goalty) - with Not_found -> None + with Not_found -> + None ;; let pp_status ctx status = @@ -1207,8 +1477,11 @@ let add_to_cache_and_del_from_orlist_if_green_cut let close_failures (fl : fail list) (cache : cache) = List.fold_left (fun cache ((gno,depth,_),gty) -> - debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno)); - cache_add_failure cache gty depth) + if CicUtil.is_meta_closed gty then + ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno)); + cache_add_failure cache gty depth) + else + cache) cache fl ;; let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = @@ -1224,6 +1497,7 @@ let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = let mk_fake_proof metasenv subst (goalno,_,_) goalty context = None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] ;; + let equational_case tables cache depth fake_proof goalno goalty subst context flags @@ -1238,7 +1512,6 @@ let equational_case let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in - match Saturation.given_clause bag status active passive goal_steps saturation_steps timeout @@ -1261,9 +1534,47 @@ let equational_case end else begin - debug_print - (lazy - ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty)); + debug_print (lazy ("NARROWING DEL GOAL: " ^ + string_of_int goalno ^ " " ^ ppterm goalty )); + let goal_steps, saturation_steps, timeout = + 1,0,flags.timeout + in + match + Saturation.solve_narrowing bag status active passive goal_steps + with + | None, active, passive, bag -> + [], (active,passive,bag), cache, flags + | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active, + passive,bag -> + assert_subst_are_disjoint subst subst'; + let subst = subst@subst' in + let open_goals = + order_new_goals metasenv subst open_goals ppterm + in + let open_goals = + List.map (fun (x,sort) -> x,depth-1,sort) open_goals + in + incr candidate_no; + [(!candidate_no,proof),metasenv,subst,open_goals], + (active,passive,bag), cache, flags + end +(* + begin + let params = ([],["use_context","false"]) in + let automation_cache = { + AutomationCache.tables = tables ; + AutomationCache.univ = Universe.empty; } + in + try + let ((_,metasenv,subst,_,_,_),open_goals) = + + solve_rewrite ~params ~automation_cache + (fake_proof, goalno) + in + let proof = lazy (Cic.Meta (-1,[])) in + [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags + with ProofEngineTypes.Fail _ -> [], tables, cache, flags +(* let res = Saturation.all_subsumed bag status active passive in let res' = List.map @@ -1281,20 +1592,34 @@ let equational_case res in res', (active,passive,bag), cache, flags +*) end +*) ;; -let try_candidate +let sort_new_elems = + List.sort (fun (_,_,_,l1) (_,_,_,l2) -> + let p1 = List.length (prop_only l1) in + let p2 = List.length (prop_only l2) in + if p1 = p2 then List.length l1 - List.length l2 else p1-p2) +;; + + +let try_candidate dbd goalty tables subst fake_proof goalno depth context cand = let ppterm = ppterm context in try let actives, passives, bag = tables in - let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta = - (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand) + let (_,metasenv,subst,_,_,_), open_goals = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:cand) (fake_proof,goalno) in - let tables = actives, passives, Equality.push_maxmeta bag maxmeta in + let tables = actives, passives, + Equality.push_maxmeta bag + (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst)) + in debug_print (lazy (" OK: " ^ ppterm cand)); let metasenv = CicRefine.pack_coercion_metasenv metasenv in let open_goals = order_new_goals metasenv subst open_goals ppterm in @@ -1306,21 +1631,33 @@ let try_candidate | CicUnification.Uncertain s -> None,tables ;; -let sort_new_elems = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> - List.length (prop_only l1) - List.length (prop_only l2)) -;; - -let applicative_case - tables depth subst fake_proof goalno goalty metasenv context universe - cache flags +let applicative_case dbd + tables depth subst fake_proof goalno goalty metasenv context + signature universe cache flags = - let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in + (* let goalty_aux = + match goalty with + | Cic.Appl (hd::tl) -> + Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) + | _ -> goalty + in *) + let goalty_aux = goalty in + let candidates = + get_candidates flags.skip_trie_filtering universe cache goalty_aux + in + (* if the goal is an equality we skip the congruence theorems *) + let candidates = + if is_equational_case goalty flags + then List.filter not_default_eq_term candidates + else candidates + in + let candidates = List.filter (only signature context metasenv) candidates + in let tables, elems = List.fold_left (fun (tables,elems) cand -> match - try_candidate goalty + try_candidate dbd goalty tables subst fake_proof goalno depth context cand with | None, tables -> tables, elems @@ -1331,8 +1668,105 @@ let applicative_case elems, tables, cache ;; -let equational_and_applicative_case - universe flags m s g gty tables cache context +let try_smart_candidate dbd + goalty tables subst fake_proof goalno depth context cand += + let ppterm = ppterm context in + try + let params = ([],[]) in + let automation_cache = { + AutomationCache.tables = tables ; + AutomationCache.univ = Universe.empty; } + in + debug_print (lazy ("candidato per " ^ string_of_int goalno + ^ ": " ^ CicPp.ppterm cand)); +(* + let (_,metasenv,subst,_,_,_) = fake_proof in + prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv); + prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst); +*) + let ((_,metasenv,subst,_,_,_),open_goals) = + apply_smart ~dbd ~term:cand ~params ~automation_cache + (fake_proof, goalno) + in + let metasenv = CicRefine.pack_coercion_metasenv metasenv in + let open_goals = order_new_goals metasenv subst open_goals ppterm in + let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in + incr candidate_no; + Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables + with + | ProofEngineTypes.Fail s -> None,tables + | CicUnification.Uncertain s -> None,tables +;; + +let smart_applicative_case dbd + tables depth subst fake_proof goalno goalty metasenv context signature + universe cache flags += + let goalty_aux = + match goalty with + | Cic.Appl (hd::tl) -> + Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) + | _ -> goalty + in + let smart_candidates = + get_candidates flags.skip_trie_filtering universe cache goalty_aux + in + let candidates = + get_candidates flags.skip_trie_filtering universe cache goalty + in + let smart_candidates = + List.filter + (fun x -> not(List.mem x candidates)) smart_candidates + in + let debug_msg = + (lazy ("smart_candidates" ^ " = " ^ + (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in + debug_print debug_msg; + let candidates = List.filter (only signature context metasenv) candidates in + let smart_candidates = + List.filter (only signature context metasenv) smart_candidates + in +(* + let penalty cand depth = + if only signature context metasenv cand then depth else ((prerr_endline ( + "penalizzo " ^ CicPp.ppterm cand));depth -1) + in +*) + let tables, elems = + List.fold_left + (fun (tables,elems) cand -> + match + try_candidate dbd goalty + tables subst fake_proof goalno depth context cand + with + | None, tables -> + (* if normal application fails we try to be smart *) + (match try_smart_candidate dbd goalty + tables subst fake_proof goalno depth context cand + with + | None, tables -> tables, elems + | Some x, tables -> tables, x::elems) + | Some x, tables -> tables, x::elems) + (tables,[]) candidates + in + let tables, smart_elems = + List.fold_left + (fun (tables,elems) cand -> + match + try_smart_candidate dbd goalty + tables subst fake_proof goalno depth context cand + with + | None, tables -> tables, elems + | Some x, tables -> tables, x::elems) + (tables,[]) smart_candidates + in + let elems = sort_new_elems (elems @ smart_elems) in + elems, tables, cache +;; + +let equational_and_applicative_case dbd + signature universe flags m s g gty tables cache context = let goalno, depth, sort = g in let fake_proof = mk_fake_proof m s g gty context in @@ -1345,15 +1779,20 @@ let equational_and_applicative_case if flags.use_only_paramod then [],tables, cache else - applicative_case + applicative_case dbd tables depth s fake_proof goalno - gty m context universe cache flags + gty m context signature universe cache flags in elems@more_elems, tables, cache, flags else let elems, tables, cache = - applicative_case tables depth s fake_proof goalno - gty m context universe cache flags + match LibraryObjects.eq_URI () with + | Some _ -> + smart_applicative_case dbd tables depth s fake_proof goalno + gty m context signature universe cache flags + | None -> + applicative_case dbd tables depth s fake_proof goalno + gty m context signature universe cache flags in elems, tables, cache, flags ;; @@ -1442,21 +1881,24 @@ let condition_for_prune_hint prune (m, s, size, don, todo, fl) = in List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s ;; -let filter_prune_hint l = +let filter_prune_hint c l = let prune = !prune_hint in prune_hint := []; (* possible race... *) - if prune = [] then l - else List.filter (condition_for_prune_hint prune) l + if prune = [] then c,l + else + cache_reset_underinspection c, + List.filter (condition_for_prune_hint prune) l ;; -let auto_main tables context flags universe cache elems = + +let auto_main dbd tables context flags signature universe cache elems = auto_context := context; let rec aux tables flags cache (elems : status) = -(* pp_status context elems; *) + pp_status context elems; (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration auto_status := elems; check_pause (); *) - let elems = filter_prune_hint elems in + let cache, elems = filter_prune_hint cache elems in match elems with | (m, s, size, don, todo, fl)::orlist when !hint <> None -> debug_print (lazy "skip"); @@ -1559,8 +2001,8 @@ let auto_main tables context flags universe cache elems = CicPp.ppterm gty)); (* elems are possible computations for proving gty *) let elems, tables, cache, flags = - equational_and_applicative_case - universe flags m s g gty tables cache context + equational_and_applicative_case dbd + signature universe flags m s g gty tables cache context in if elems = [] then (* this goal has failed *) @@ -1607,8 +2049,16 @@ let auto_main tables context flags universe cache elems = let - auto_all_solutions tables universe cache context metasenv gl flags + auto_all_solutions dbd tables universe cache context metasenv gl flags = + let signature = + List.fold_left + (fun set g -> + MetadataConstraints.UriManagerSet.union set + (MetadataQuery.signature_of metasenv g) + ) + MetadataConstraints.UriManagerSet.empty gl + in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map @@ -1616,7 +2066,7 @@ let in let elems = [metasenv,[],1,[],goals,[]] in let rec aux tables solutions cache elems flags = - match auto_main tables context flags universe cache elems with + match auto_main dbd tables context flags signature universe cache elems with | Gaveup (tables,cache) -> solutions,cache, tables | Proved (metasenv,subst,others,tables,cache) -> @@ -1643,12 +2093,21 @@ let (******************* AUTO ***************) -let auto flags metasenv tables universe cache context metasenv gl = - let initial_time = Unix.gettimeofday() in + +let auto dbd flags metasenv tables universe cache context metasenv gl = + let initial_time = Unix.gettimeofday() in + let signature = + List.fold_left + (fun set g -> + MetadataConstraints.UriManagerSet.union set + (MetadataQuery.signature_of metasenv g) + ) + MetadataConstraints.UriManagerSet.empty gl + in let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in let elems = [metasenv,[],1,[],goals,[]] in - match auto_main tables context flags universe cache elems with + match auto_main dbd tables context flags signature universe cache elems with | Proved (metasenv,subst,_, tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); @@ -1659,19 +2118,6 @@ let auto flags metasenv tables universe cache context metasenv gl = None,cache ;; -let applyS_tac ~dbd ~term ~params ~automation_cache = - ProofEngineTypes.mk_tactic - (fun status -> - try - let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status - in - proof, gl - with - | CicUnification.UnificationFailure msg - | CicTypeChecker.TypeCheckerFailure msg -> - raise (ProofEngineTypes.Fail msg)) - let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = let flags = flags_of_params params () in let use_library = flags.use_library in @@ -1680,21 +2126,34 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ~dbd ~use_library ~use_context:(not flags.skip_context) automation_cache univ (proof, goal) in - let _,metasenv,_subst,_,_, _ = proof in + let _,metasenv,subst,_,_, _ = proof in let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let signature = MetadataQuery.signature_of metasenv goal in + let signature = + List.fold_left + (fun set t -> + let ty, _ = + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.oblivion_ugraph + in + MetadataConstraints.UriManagerSet.union set + (MetadataConstraints.constants_of ty) + ) + signature univ + in let tables,cache = if flags.close_more then close_more tables context (proof, goal) - auto_all_solutions universe cache + (auto_all_solutions dbd) signature universe cache else tables,cache in let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_subst,_,_, _) = proof in - hint := None; + let (_,oldmetasenv,_,_,_, _) = proof in + hint := None; let elem = - metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] + metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[] in - match auto_main tables context flags universe cache [elem] with + match auto_main dbd tables context flags signature universe cache [elem] with | Proved (metasenv,subst,_, tables,cache) -> debug_print (lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); @@ -1717,252 +2176,6 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa let auto_tac ~dbd ~params ~automation_cache = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);; -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_tac ~automation_cache ~params:(univ,params) (proof,goal as status)= - let steps = int_of_string (string params "steps" "1") in - let universe, tables, cache = - init_cache_and_tables ~use_library:false ~use_context:false - automation_cache univ (proof,goal) - in - let actives, passives, bag = tables in - let _,metasenv,_subst,_,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv 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 - match Indexing.solve_demodulating bag env table initgoal steps with - | Some (proof, metasenv, newty) -> - let refl = - match newty with - | Cic.Appl[Cic.MutInd _;eq_ty;left;_] -> - Equality.Exact (Equality.refl_proof eq_uri eq_ty left) - | _ -> assert false - in - let proofterm,_ = - Equality.build_goal_proof - bag eq_uri proof refl newty [] context metasenv - in - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) status - | None -> - raise - (ProofEngineTypes.Fail (lazy - ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) -;; -let solve_rewrite_tac ~params ~automation_cache () = - ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params) -;; - -(* 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 subst,((_,metasenv,_,_,_,_), open_goals),maxmeta = - (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~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_tac ~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 [] in - let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in - let proofterm,_ = - Equality.build_goal_proof (~contextualize:false) bag - eq_uri newproof opengoal ty [] context metasenv - in - let extended_metasenv = (maxm,context,newty)::metasenv in - let extended_status = - (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) - 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*) -;; - -let demodulate_tac ~dbd ~params ~automation_cache = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);; - let pp_proofterm = Equality.pp_proofterm;; let revision = "$Revision$";;