X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=ce4b9357e389da2588ae4b7932b681c1a0cb2c6d;hb=5c10d402b5de7233bc83d7f685b274832e383212;hp=a01ca86913eedfbe9789997c54d3e9c0576bfb24;hpb=b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index a01ca8691..ce4b9357e 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 @@ -191,7 +190,8 @@ let lambda_close ?prefix_name t menv 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) -> @@ -231,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 = @@ -324,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 = @@ -335,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 @@ -429,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 @@ -447,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 = @@ -468,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 @@ -531,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 ***************) @@ -673,23 +717,10 @@ 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 automation_cache 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 *) @@ -728,20 +759,18 @@ let new_metasenv_and_unify_and_t (PrimitiveTactics.apply_tac term'') (proof''',goal) in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let (active, passive,bag), cache, maxm = - init_cache_and_tables ~dbd flags.use_library false (* was true *) - true false universe - (proof'''',newmeta) - 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 maxm (proof'''',newmeta) active passive + 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 @@ -766,7 +795,7 @@ let rec count_prods context ty = | _ -> 0 let apply_smart - ~dbd ~term ~subst ~automation_cache ?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 @@ -774,11 +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 - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ in - let universe = universe_of_params metasenv context universe univ in - let automation_cache = { automation_cache with AutomationCache.univ = universe } in - let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -819,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 automation_cache 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 @@ -865,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 *) @@ -885,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 *) @@ -1203,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 @@ -1218,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 = @@ -1234,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) -> @@ -1262,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 = @@ -1292,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 @@ -1430,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; @@ -1444,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 = @@ -1470,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"); @@ -1495,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)); @@ -1514,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; @@ -1540,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 @@ -1577,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 = @@ -1597,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) -> @@ -1620,7 +1638,7 @@ let if opened = [] then Some subst else None) solutions in - solutions,cache,maxm + solutions,cache,tables ;; (******************* AUTO ***************) @@ -1630,12 +1648,12 @@ let auto flags metasenv tables universe cache context metasenv gl = 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 @@ -1655,30 +1673,29 @@ let applyS_tac ~dbd ~term ~params ~automation_cache = raise (ProofEngineTypes.Fail msg)) let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = - let _,metasenv,_subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params () in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ 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 = @@ -1690,7 +1707,7 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa ~newmetasenv:metasenv in proof,opened - | Gaveup (tables,cache,maxm) -> + | Gaveup (tables,cache) -> debug_print (lazy ("TIME:"^ string_of_float(Unix.gettimeofday()-.initial_time))); @@ -1708,23 +1725,21 @@ let eq_of_goal = function (* 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 _,metasenv,_subst,_,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in +let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal)= let steps = int_of_string (string params "steps" "1") in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ 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) + 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 eq_uri = eq_of_goal ty 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 @@ -1739,6 +1754,11 @@ let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as sta Equality.build_goal_proof bag eq_uri proof refl newty [] context metasenv in + let proofterm, _, metasenv, _ = + CicRefine.type_of_aux' metasenv 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 -> @@ -1853,7 +1873,7 @@ let demodulate_theorem ~automation_cache 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 = @@ -1892,22 +1912,20 @@ let demodulate_theorem ~automation_cache uri = (* NEW DEMODULATE *) let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* XXX automation_cache *) - let universe = automation_cache.AutomationCache.univ 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 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 @@ -1926,14 +1944,19 @@ let demodulate_tac ~dbd ~automation_cache ~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 eq_uri newproof opengoal ty [] context metasenv in - let extended_metasenv = (maxm,context,newty)::metasenv in + let metasenv = (maxm,context,newty)::metasenv in + let proofterm, _, metasenv, _ = + CicRefine.type_of_aux' metasenv context proofterm + CicUniv.oblivion_ugraph + in let extended_status = - (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in + (curi,metasenv,_subst,pbo,pty, attrs),goal in let (status,newgoals) = ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac ~term:proofterm) @@ -1950,6 +1973,14 @@ let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= let demodulate_tac ~dbd ~params ~automation_cache = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);; +let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache = + let all = bool flags "all" false in + if all then + solve_rewrite_tac ~params ~automation_cache () + else + demodulate_tac ~dbd ~params ~automation_cache +;; + let pp_proofterm = Equality.pp_proofterm;; let revision = "$Revision$";;