X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=1b172786a7a44a071f28079c8dbdf409a8c996ec;hb=bdbe077ddb0b377823b6806adc8bece82130c992;hp=6b25982d3bb7377b8a0a5019172e5f3f482ce678;hpb=992c6ea9d35cbdf8e9d2ce870a1b3d8f7e099e7d;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 6b25982d3..1b172786a 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1,5 +1,4 @@ (* Copyright (C) 2002, HELM Team. - * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -32,13 +31,113 @@ let debug_print s = if debug then prerr_endline (Lazy.force s);; +let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;; +let ugraph = CicUniv.oblivion_ugraph;; +let typeof = CicTypeChecker.type_of_aux';; +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 +;; + +exception NotConvertible;; + +let check_proof_is_valid proof metasenv context goalty = + if debug then + begin + try + let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in + let b,_ = CicReduction.are_convertible context ty goalty u in + if not b then raise NotConvertible else b + with _ -> + let names = + List.map (function None -> None | Some (x,_) -> Some x) context + in + debug_print (lazy ("PROOF:" ^ CicPp.pp proof names)); + (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *) + debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names)); + debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv)); + false + end + else true +;; +let assert_proof_is_valid proof metasenv context goalty = + assert (check_proof_is_valid proof metasenv context goalty) +;; + +let assert_subst_are_disjoint subst subst' = + if debug then + assert(List.for_all + (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') + subst) + else () +;; + +let split_goals_in_prop metasenv subst gl = + List.partition + (fun g -> + let _,context,ty = CicUtil.lookup_meta g metasenv in + try + let sort,u = typeof ~subst metasenv context ty ugraph in + is_propositional context sort + with + | CicTypeChecker.AssertFailure s + | CicTypeChecker.TypeCheckerFailure s -> + debug_print + (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty))); + debug_print s; + false) + (* FIXME... they should type! *) + gl +;; + +let split_goals_with_metas metasenv subst gl = + List.partition + (fun g -> + let _,context,ty = CicUtil.lookup_meta g metasenv in + let ty = CicMetaSubst.apply_subst subst ty in + CicUtil.is_meta_closed ty) + gl +;; + +let order_new_goals metasenv subst open_goals ppterm = + let prop,rest = split_goals_in_prop metasenv subst open_goals in + let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in + let closed_type, open_type = split_goals_with_metas metasenv subst rest in + let open_goals = + (List.map (fun x -> x,P) (open_prop @ closed_prop)) + @ + (List.map (fun x -> x,T) (open_type @ closed_type)) + in + let tys = + List.map + (fun (i,sort) -> + let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals + in + debug_print (lazy (" OPEN: "^ + String.concat "\n" + (List.map + (function + | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop" + | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type") + tys))); + open_goals +;; + +let is_an_equational_goal = function + | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true + | _ -> false +;; type auto_params = Cic.term list * (string * string) list @@ -48,6 +147,10 @@ let elems = ref [] ;; very naif version: it does not take dependencies properly into account *) let naif_closure ?(prefix_name="xxx_") t metasenv context = + let in_term t (i,_,_) = + List.exists (fun (j,_) -> j=i) (CicUtil.metas_of_term t) + in + let metasenv = List.filter (in_term t) metasenv in 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 @@ -72,22 +175,23 @@ let naif_closure ?(prefix_name="xxx_") t metasenv context = CicSubstitution.lift n ty,t)) (n-1,body) metasenv in - t + t, List.length metasenv ;; let lambda_close ?prefix_name t menv ctx = - let t = naif_closure ?prefix_name t menv ctx in + let t, num_lambdas = 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 + (t,num_lambdas) ctx ;; (* functions for retrieving theorems *) -exception FillingFailure of AutoCache.cache * int + +exception FillingFailure of AutoCache.cache * AutomationCache.tables let rec unfold context = function | Cic.Prod(name,s,t) -> @@ -127,7 +231,7 @@ let partition_equalities = List.partition (fun (_,ty) -> is_an_equality ty) -let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; +let default_auto tables _ cache _ _ _ _ = [],cache,tables ;; (* giusto per provare che succede let is_unit_equation context metasenv oldnewmeta term = @@ -220,7 +324,7 @@ let retrieve_equations dont_filter signature universe cache context metasenv = (only (MetadataConstraints.UriManagerSet.add eq_uri signature) context metasenv) candidates -let build_equality bag head args proof newmetas maxmeta = +let build_equality bag head args proof newmetas = match head with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> let p = @@ -231,58 +335,99 @@ let build_equality bag head args proof newmetas maxmeta = (* 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 + let bag, e = Equality.mk_equality bag (w, proof, stat, newmetas) in (* to clean the local context of metas *) - Equality.fix_metas bag maxmeta e + Equality.fix_metas bag e | _ -> assert false ;; let partition_unit_equalities context metasenv newmeta bag equations = List.fold_left - (fun (units,other,maxmeta)(t,ty) -> + (fun (bag,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 + bag, 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 + let bag, equality = + build_equality bag head args t newmetas in + bag, 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) - + bag, units,(t,ty)::other,maxmeta) + (bag,[],[],newmeta) equations +;; let init_cache_and_tables - ?dbd use_library paramod use_context dont_filter universe (proof, goal) + ?dbd ~use_library ~use_context + automation_cache restricted_univ (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 _, metasenv, _, _, _, _ = proof 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 + 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 @@ -325,11 +470,14 @@ let init_cache_and_tables 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 +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 @@ -343,10 +491,11 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u | _ -> assert false) args in - let results,cache,newmeta = + let results,cache,tables = if propositional_args = [] then - let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in - [args,metasenv,newmetas,head,newmeta],cache,newmeta + let _,_,bag = tables in + let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in + [args,metasenv,newmetas,head],cache,tables else (* let proof = @@ -364,54 +513,59 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u 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 -> + 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 = - List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv - 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 - args,metasenv,newmetas,head,max newm newmeta) - substs, cache, newmeta + 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,newmeta + results,cache,tables +;; -let build_equalities auto context metasenv tables universe cache newmeta equations = +let build_equalities auto context metasenv tables universe cache equations = List.fold_left - (fun (facts,cache,newmeta) (t,ty) -> + (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,newmeta = - fill_hypothesis context metasenv newmeta ty tables universe cache auto true + let saturated, cache, tables = + fill_hypothesis context metasenv ty tables universe cache auto true in - let (active,passive,bag) = tables in - let eqs,bag,newmeta = + let eqs, tables = List.fold_left - (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') -> - let maxmeta,equality = - build_equality bag head args t newmetas newmeta' + (fun (acc, tables) (args,metasenv,newmetas,head) -> + let actives, passives, bag = tables in + let bag, equality = + build_equality bag head args t newmetas in - equality::acc,bag,maxmeta) - ([],bag,newmeta) saturated + let tables = actives, passives, bag in + equality::acc,tables) + ([],tables) saturated in - (eqs@facts, cache, newmeta) - with FillingFailure (cache,newmeta) -> + (tables, eqs@facts, cache) + with FillingFailure (cache,tables) -> (* if filling hypothesis fails we add the equation to the cache *) - (facts,cache,newmeta) + (tables,facts,cache) ) - ([],cache,newmeta) equations + (tables,[],cache) equations -let close_more tables maxmeta context status auto universe cache = - let (active,passive,bag) = tables in +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 @@ -427,81 +581,75 @@ let close_more tables maxmeta context status auto universe cache = (* 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 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 - debug_print (lazy ("No = " ^ (string_of_int no))); - let active,passive,newmeta = - Saturation.pump_actives context bag maxm active passive (no+1) infinity + let active, passive, bag = + Saturation.pump_actives context bag active passive (no+1) infinity in - (active,passive,bag),cache,newmeta + (active,passive,bag), cache +;; -let find_context_equalities - maxmeta bag context proof (universe:Universe.universe) 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 - 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 + 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 context 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,newmeta = - fill_hypothesis context metasenv newmeta term - empty_tables universe cache default_auto false + let saturated, cache, tables = + fill_hypothesis context metasenv term + tables universe cache default_auto false in - let eqs,newmeta = + let actives, passives, bag = tables in + let bag,eqs = 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') + (fun (bag,acc) (args,metasenv,newmetas,head) -> + let bag, equality = + build_equality bag head args (Cic.Rel index) newmetas in - equality::acc, newmeta + 1) - ([],newmeta) saturated + bag, equality::acc) + (bag,[]) saturated in - eqs, newmeta, cache - with FillingFailure (cache,newmeta) -> - [],newmeta,cache) + 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 newmeta, e = - build_equality bag term [] (Cic.Rel index) [] newmeta + let actives, passives, bag = tables in + let bag, e = + build_equality bag term [] (Cic.Rel index) [] in - [e], (newmeta+1),cache - | _ -> [], newmeta, cache + let tables = actives, passives, bag in + tables, [e], cache + | _ -> tables, [], 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 + 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 cache (index+1) newmeta tl - in - let il, maxm, cache = - aux cache 1 newmeta context + aux tables cache (index+1) tl in + let tables, il, cache = aux tables cache 1 context in let indexes, equalities = List.split il in - indexes, equalities, maxm, cache + tables, indexes, equalities, cache ;; (********** PARAMETERS PASSING ***************) @@ -569,25 +717,13 @@ let flags_of_params params ?(for_applyS=false) () = AutoTypes.skip_context = skip_context; } -let universe_of_params metasenv context universe tl = - if tl = [] then universe else - let tys = - List.map - (fun term -> - fst (CicTypeChecker.type_of_aux' metasenv context term - CicUniv.oblivion_ugraph)) - tl - in - Universe.index_list Universe.empty context (List.combine tl tys) -;; - - (***************** applyS *******************) -let new_metasenv_and_unify_and_t - dbd flags universe proof goal ?tables newmeta' metasenv' +let apply_smart_aux + dbd flags automation_cache univ proof goal newmeta' metasenv' context term' ty termty goal_arity -= += +(* let ppterm = ppterm context in *) let (consthead,newmetasenv,arguments,_) = TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let term'' = @@ -623,20 +759,34 @@ let new_metasenv_and_unify_and_t (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 - let (active, passive,bag), cache, maxmeta = - init_cache_and_tables ~dbd flags.use_library true true false universe - (proof'''',newmeta) - in - Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive - max_int max_int flags.timeout + 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,_ -> + | 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 + 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 +*) ;; let rec count_prods context ty = @@ -645,7 +795,7 @@ let rec count_prods context ty = | _ -> 0 let apply_smart - ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) + ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in @@ -653,7 +803,6 @@ let apply_smart 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 universe = universe_of_params metasenv context universe univ in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -694,7 +843,7 @@ let apply_smart let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in let goal_arity = count_prods context ty in let proof, gl, active, passive = - new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables + apply_smart_aux dbd flags automation_cache univ proof goal newmeta' metasenv' context term' ty termty goal_arity in proof, gl, active, passive @@ -702,107 +851,7 @@ let apply_smart (****************** AUTO ********************) -let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;; -let ugraph = CicUniv.oblivion_ugraph;; -let typeof = CicTypeChecker.type_of_aux';; -let ppterm ctx t = - let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in - CicPp.pp t names -;; -let is_in_prop context subst metasenv ty = - let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in - is_propositional context sort -;; - -exception NotConvertible;; - -let check_proof_is_valid proof metasenv context goalty = - if debug then - begin - try - let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in - let b,_ = CicReduction.are_convertible context ty goalty u in - if not b then raise NotConvertible else b - with _ -> - let names = - List.map (function None -> None | Some (x,_) -> Some x) context - in - debug_print (lazy ("PROOF:" ^ CicPp.pp proof names)); - (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *) - debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names)); - debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv)); - false - end - else true -;; - -let assert_proof_is_valid proof metasenv context goalty = - assert (check_proof_is_valid proof metasenv context goalty) -;; - -let assert_subst_are_disjoint subst subst' = - if debug then - assert(List.for_all - (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') - subst) - else () -;; - -let split_goals_in_prop metasenv subst gl = - List.partition - (fun g -> - let _,context,ty = CicUtil.lookup_meta g metasenv in - try - let sort,u = typeof ~subst metasenv context ty ugraph in - is_propositional context sort - with - | CicTypeChecker.AssertFailure s - | CicTypeChecker.TypeCheckerFailure s -> - debug_print - (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty))); - debug_print s; - false) - (* FIXME... they should type! *) - gl -;; - -let split_goals_with_metas metasenv subst gl = - List.partition - (fun g -> - let _,context,ty = CicUtil.lookup_meta g metasenv in - let ty = CicMetaSubst.apply_subst subst ty in - CicUtil.is_meta_closed ty) - gl -;; -let order_new_goals metasenv subst open_goals ppterm = - let prop,rest = split_goals_in_prop metasenv subst open_goals in - let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in - let closed_type, open_type = split_goals_with_metas metasenv subst rest in - let open_goals = - (List.map (fun x -> x,P) (open_prop @ closed_prop)) - @ - (List.map (fun x -> x,T) (open_type @ closed_type)) - in - let tys = - List.map - (fun (i,sort) -> - let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals - in - debug_print (lazy (" OPEN: "^ - String.concat "\n" - (List.map - (function - | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop" - | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type") - tys))); - open_goals -;; - -let is_an_equational_goal = function - | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true - | _ -> false -;; (* let prop = function (_,depth,P) -> depth < 9 | _ -> false;; @@ -840,8 +889,6 @@ type goal = ProofEngineTypes.goal * int * AutoTypes.sort let candidate_no = ref 0;; type candidate = int * Cic.term Lazy.t type cache = AutoCache.cache -type tables = - Saturation.active_table * Saturation.passive_table * Equality.equality_bag type fail = (* the goal (mainly for depth) and key of the goal *) @@ -860,9 +907,9 @@ type status = * end with the same (S(g,_)) *) elem list type auto_result = - (* menv, subst, alternatives, tables, cache, maxmeta *) - | Proved of menv * subst * elem list * tables * cache * int - | Gaveup of tables * cache * int + (* menv, subst, alternatives, tables, cache *) + | Proved of menv * subst * elem list * AutomationCache.tables * cache + | Gaveup of AutomationCache.tables * cache (* the status exported to the external observer *) @@ -1168,7 +1215,9 @@ let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = let entry = goalno, (canonical_ctx, t,ty) in assert_subst_are_disjoint subst [entry]; let subst = entry :: subst in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + subst, metasenv ;; @@ -1176,7 +1225,7 @@ let mk_fake_proof metasenv subst (goalno,_,_) goalty context = None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] ;; let equational_case - tables maxm cache depth fake_proof goalno goalty subst context + tables cache depth fake_proof goalno goalty subst context flags = let active,passive,bag = tables in @@ -1191,13 +1240,13 @@ let equational_case in match - Saturation.given_clause bag maxm status active passive + Saturation.given_clause bag status active passive goal_steps saturation_steps timeout with - | None, active, passive, maxmeta -> - [], (active,passive,bag), cache, maxmeta, flags + | None, active, passive, bag -> + [], (active,passive,bag), cache, flags | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active, - passive,maxmeta -> + passive,bag -> assert_subst_are_disjoint subst subst'; let subst = subst@subst' in let open_goals = @@ -1207,19 +1256,15 @@ let equational_case 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, maxmeta, flags + [(!candidate_no,proof),metasenv,subst,open_goals], + (active,passive,bag), cache, flags end else begin debug_print (lazy ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty)); - let res, maxmeta = - Saturation.all_subsumed bag maxm status active passive - in - assert (maxmeta >= maxm); + let res = Saturation.all_subsumed bag status active passive in let res' = List.map (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) -> @@ -1235,28 +1280,30 @@ let equational_case (!candidate_no,proof),metasenv,subst,open_goals) res in - res', (active,passive,bag), cache, maxmeta, flags + res', (active,passive,bag), cache, flags end ;; let try_candidate - goalty tables maxm subst fake_proof goalno depth context cand + 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:maxm ~term:cand) + (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand) (fake_proof,goalno) in + let tables = actives, passives, Equality.push_maxmeta bag maxmeta 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 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 , maxmeta + Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables with - | ProofEngineTypes.Fail s -> None,tables, maxm - | CicUnification.Uncertain s -> None,tables, maxm + | ProofEngineTypes.Fail s -> None,tables + | CicUnification.Uncertain s -> None,tables ;; let sort_new_elems = @@ -1265,52 +1312,50 @@ let sort_new_elems = ;; let applicative_case - tables maxm depth subst fake_proof goalno goalty metasenv context universe + tables depth subst fake_proof goalno goalty metasenv context universe cache flags = let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in - let tables, elems, maxm = + let tables, elems = List.fold_left - (fun (tables,elems,maxm) cand -> + (fun (tables,elems) cand -> match try_candidate goalty - tables maxm subst fake_proof goalno depth context cand + tables subst fake_proof goalno depth context cand with - | None, tables,maxm -> tables,elems, maxm - | Some x, tables, maxm -> tables,x::elems, maxm) - (tables,[],maxm) candidates + | None, tables -> tables, elems + | Some x, tables -> tables, x::elems) + (tables,[]) candidates in let elems = sort_new_elems elems in - elems, tables, cache, maxm + elems, tables, cache ;; let equational_and_applicative_case - universe flags m s g gty tables cache maxm context + 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 if is_equational_case gty flags then - let elems,tables,cache,maxm1, flags = - equational_case tables maxm cache + let elems,tables,cache, flags = + equational_case tables cache depth fake_proof goalno gty s context flags in - let maxm = maxm1 in - let more_elems, tables, cache, maxm1 = + let more_elems, tables, cache = if flags.use_only_paramod then - [],tables, cache, maxm + [],tables, cache else applicative_case - tables maxm depth s fake_proof goalno + tables depth s fake_proof goalno gty m context universe cache flags in - let maxm = maxm1 in - elems@more_elems, tables, cache, maxm, flags + elems@more_elems, tables, cache, flags else - let elems, tables, cache, maxm = - applicative_case tables maxm depth s fake_proof goalno + let elems, tables, cache = + applicative_case tables depth s fake_proof goalno gty m context universe cache flags in - elems, tables, cache, maxm, flags + elems, tables, cache, flags ;; let rec condition_for_hint i = function | [] -> false @@ -1373,8 +1418,18 @@ let prunable menv subst ty todo = (match calculate_goal_ty g variant menv with | None -> assert false | Some (_, gty') -> - if gty = gty' then - no_progress variant tl + if gty = gty' then no_progress variant tl +(* +(prerr_endline (string_of_int n); + prerr_endline (CicPp.ppterm gty); + prerr_endline (CicPp.ppterm gty'); + prerr_endline "---------- subst"; + prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst); + prerr_endline "---------- variant"; + prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant); + prerr_endline "---------- menv"; + prerr_endline (CicMetaSubst.ppmetasenv [] menv); + no_progress variant tl) *) else false)) | _::tl -> no_progress variant tl in @@ -1393,9 +1448,9 @@ let filter_prune_hint l = if prune = [] then l else List.filter (condition_for_prune_hint prune) l ;; -let auto_main tables maxm context flags universe cache elems = +let auto_main tables context flags universe cache elems = auto_context := context; - let rec aux tables maxm flags cache (elems : status) = + let rec aux tables flags cache (elems : status) = (* pp_status context elems; *) (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration auto_status := elems; @@ -1407,23 +1462,23 @@ let auto_main tables maxm context flags universe cache elems = debug_print (lazy "skip"); (match !hint with | Some i when condition_for_hint i todo -> - aux tables maxm flags cache orlist + aux tables flags cache orlist | _ -> hint := None; - aux tables maxm flags cache elems) + aux tables flags cache elems) | [] -> (* complete failure *) debug_print (lazy "give up"); - Gaveup (tables, cache, maxm) + Gaveup (tables, cache) | (m, s, _, _, [],_)::orlist -> (* complete success *) debug_print (lazy "success"); - Proved (m, s, orlist, tables, cache, maxm) + Proved (m, s, orlist, tables, cache) | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist when not flags.AutoTypes.do_types -> (* skip since not Prop, don't even check if closed by side-effect *) debug_print (lazy "skip existential goal"); - aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist) + aux tables flags cache ((m, s, size, don, todo, fl)::orlist) | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist -> (* partial success, cache g and go on *) let cache, orlist, fl, sibling_pruned = @@ -1433,24 +1488,24 @@ let auto_main tables maxm context flags universe cache elems = debug_print (lazy (AutoCache.cache_print context cache)); let fl = remove_s_from_fl g fl in let don = if sibling_pruned then don else op::don in - aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist) + aux tables flags cache ((m, s, size, don, todo, fl)::orlist) | (m, s, size, don, todo, fl)::orlist when List.length(prop_only (d_goals todo)) > flags.maxwidth -> debug_print (lazy ("FAIL: WIDTH")); (* too many goals in and generated by last th *) let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize -> debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ " > " ^ string_of_int flags.maxsize )); (* we already have a too large proof term *) let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | _ when Unix.gettimeofday () > flags.timeout -> (* timeout *) debug_print (lazy ("FAIL: TIMEOUT")); - Gaveup (tables, cache, maxm) + Gaveup (tables, cache) | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status -> (* attack g *) debug_print (lazy "attack goal"); @@ -1458,17 +1513,17 @@ let auto_main tables maxm context flags universe cache elems = | None -> (* closed by side effect *) debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno)); - aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist) + aux tables flags cache ((m,s,size,don,todo, fl)::orlist) | Some (canonical_ctx, gty) -> let gsize, _ = Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty in if gsize > flags.maxgoalsizefactor then (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize)); - aux tables maxm flags cache orlist) + aux tables flags cache orlist) else if prunable_for_size flags s m todo then (debug_print (lazy ("POTO at depth: "^(string_of_int depth))); - aux tables maxm flags cache orlist) + aux tables flags cache orlist) else (* still to be proved *) (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty)); @@ -1477,23 +1532,23 @@ let auto_main tables maxm context flags universe cache elems = (* fail depth *) debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno)); let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | UnderInspection -> (* fail loop *) debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno)); let cache = close_failures fl cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist | Succeded t -> debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno)); let s, m = put_in_subst s m g canonical_ctx t gty in - aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist) + aux tables flags cache ((m, s, size, don,todo, fl)::orlist) | Notfound | Failed_in _ when depth > 0 -> ( (* more depth or is the first time we see the goal *) if prunable m s gty todo then (debug_print (lazy( "FAIL: LOOP: one father is equal")); - aux tables maxm flags cache orlist) + aux tables flags cache orlist) else let cache = cache_add_underinspection cache gty depth in auto_status := status; @@ -1503,14 +1558,14 @@ let auto_main tables maxm context flags universe cache elems = string_of_int gno ^ "("^ string_of_int size ^ "): "^ CicPp.ppterm gty)); (* elems are possible computations for proving gty *) - let elems, tables, cache, maxm, flags = + let elems, tables, cache, flags = equational_and_applicative_case - universe flags m s g gty tables cache maxm context + universe flags m s g gty tables cache context in if elems = [] then (* this goal has failed *) let cache = close_failures ((g,gty)::fl) cache in - aux tables maxm flags cache orlist + aux tables flags cache orlist else (* elems = (cand,m,s,gl) *) let size_gl l = List.length @@ -1540,19 +1595,19 @@ let auto_main tables maxm context flags universe cache elems = in map elems in - aux tables maxm flags cache elems) + aux tables flags cache elems) | _ -> (* no more depth *) debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno)); let cache = close_failures fl cache in - aux tables maxm flags cache orlist) + aux tables flags cache orlist) in - (aux tables maxm flags cache elems : auto_result) + (aux tables flags cache elems : auto_result) ;; let - auto_all_solutions maxm tables universe cache context metasenv gl flags + auto_all_solutions tables universe cache context metasenv gl flags = let goals = order_new_goals metasenv [] gl CicPp.ppterm in let goals = @@ -1560,20 +1615,20 @@ let (fun (x,s) -> D (x,flags.maxdepth,s)) goals in let elems = [metasenv,[],1,[],goals,[]] in - let rec aux tables maxm solutions cache elems flags = - match auto_main tables maxm context flags universe cache elems with - | Gaveup (tables,cache,maxm) -> - solutions,cache,maxm - | Proved (metasenv,subst,others,tables,cache,maxm) -> + let rec aux tables solutions cache elems flags = + match auto_main tables context flags universe cache elems with + | Gaveup (tables,cache) -> + solutions,cache, tables + | Proved (metasenv,subst,others,tables,cache) -> if Unix.gettimeofday () > flags.timeout then - ((subst,metasenv)::solutions), cache, maxm + ((subst,metasenv)::solutions), cache, tables else - aux tables maxm ((subst,metasenv)::solutions) cache others flags + aux tables ((subst,metasenv)::solutions) cache others flags in - let rc = aux tables maxm [] cache elems flags in + let rc = aux tables [] cache elems flags in match rc with - | [],cache,maxm -> [],cache,maxm - | solutions,cache,maxm -> + | [],cache,tables -> [],cache,tables + | solutions, cache,tables -> let solutions = HExtlib.filter_map (fun (subst,newmetasenv) -> @@ -1583,33 +1638,33 @@ let if opened = [] then Some subst else None) solutions in - solutions,cache,maxm + solutions,cache,tables ;; -(* }}} ****************** AUTO ***************) +(******************* AUTO ***************) let auto flags metasenv tables universe cache context metasenv gl = let initial_time = Unix.gettimeofday() 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 0 context flags universe cache elems with - | Proved (metasenv,subst,_, tables,cache,_) -> + match auto_main tables context flags universe cache elems with + | Proved (metasenv,subst,_, tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); Some (subst,metasenv), cache - | Gaveup (tables,cache,maxm) -> + | Gaveup (tables,cache) -> debug_print(lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); None,cache ;; -let applyS_tac ~dbd ~term ~params ~universe = +let applyS_tac ~dbd ~term ~params ~automation_cache = ProofEngineTypes.mk_tactic (fun status -> try let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~params ~universe status + apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status in proof, gl with @@ -1617,29 +1672,30 @@ let applyS_tac ~dbd ~term ~params ~universe = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) -let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = - let _,metasenv,_subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in +let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = let flags = flags_of_params params () in - let universe = universe_of_params metasenv context universe univ in let use_library = flags.use_library in - let tables,cache,newmeta = - init_cache_and_tables ~dbd use_library flags.use_only_paramod (not flags.skip_context) - false universe (proof, goal) in - let tables,cache,newmeta = + let universe, tables, cache = + init_cache_and_tables + ~dbd ~use_library ~use_context:(not flags.skip_context) + automation_cache univ (proof, goal) + in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let tables,cache = if flags.close_more then close_more - tables newmeta context (proof, goal) + tables context (proof, goal) auto_all_solutions universe cache - else tables,cache,newmeta in + else tables,cache in let initial_time = Unix.gettimeofday() in let (_,oldmetasenv,_subst,_,_, _) = proof in hint := None; let elem = metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] in - match auto_main tables newmeta context flags universe cache [elem] with - | Proved (metasenv,subst,_, tables,cache,_) -> + match auto_main tables context flags universe cache [elem] with + | Proved (metasenv,subst,_, tables,cache) -> debug_print (lazy ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); let proof,metasenv = @@ -1651,15 +1707,15 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = ~newmetasenv:metasenv in proof,opened - | Gaveup (tables,cache,maxm) -> + | Gaveup (tables,cache) -> debug_print (lazy ("TIME:"^ string_of_float(Unix.gettimeofday()-.initial_time))); raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; -let auto_tac ~dbd ~params ~universe = - ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);; +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 -> @@ -1669,21 +1725,20 @@ let eq_of_goal = function (* performs steps of rewrite with the universe, obtaining if possible * a trivial goal *) -let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= +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 steps = int_of_string (string params "steps" "1") in - let universe = universe_of_params metasenv context universe univ in let eq_uri = eq_of_goal ty in - let (active,passive,bag), cache, maxm = - (* we take the whole universe (no signature filtering) *) - init_cache_and_tables false true false true universe (proof,goal) - in let initgoal = [], metasenv, ty in let table = - let equalities = (Saturation.list_of_passive passive) in - (* we demodulate using both actives passives *) - List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities + 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 @@ -1705,8 +1760,8 @@ let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= (ProofEngineTypes.Fail (lazy ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) ;; -let solve_rewrite_tac ~params ~universe () = - ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params) +let solve_rewrite_tac ~params ~automation_cache () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params) ;; (* Demodulate thorem *) @@ -1765,7 +1820,7 @@ let is_subsumed univ context ty = ) None candidates ;; -let demodulate_theorem ~universe uri = +let demodulate_theorem ~automation_cache uri = let eq_uri = match LibraryObjects.eq_URI () with | Some (uri) -> uri @@ -1788,6 +1843,8 @@ let demodulate_theorem ~universe uri = 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 @@ -1810,7 +1867,7 @@ let demodulate_theorem ~universe uri = in let bag = Equality.mk_equality_bag () in - let units, _, newmeta = + let bag, units, _, newmeta = partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types in let table = @@ -1848,23 +1905,27 @@ let demodulate_theorem ~universe uri = (* NEW DEMODULATE *) -let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let universe = universe_of_params metasenv context universe univ in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let initgoal = [], metasenv, ty in +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 eq_uri = eq_of_goal ty in *) - let (active,passive,bag), cache, maxm = - init_cache_and_tables - ~dbd false false true true universe (proof,goal) - 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) @@ -1877,6 +1938,7 @@ let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= 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 @@ -1898,8 +1960,8 @@ let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd ~params ~universe = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);; +let demodulate_tac ~dbd ~params ~automation_cache = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);; let pp_proofterm = Equality.pp_proofterm;;