From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- tactics/auto.ml | 574 +++++++++++++++++++++++++++++++++----------------------- 1 file changed, 341 insertions(+), 233 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 066ed786..1212656b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: auto.ml 11739 2009-01-02 19:33:19Z herbelin $ *) open Pp open Util @@ -59,6 +59,8 @@ type pri_auto_tactic = { code : auto_tactic (* the tactic to apply when the concl matches pat *) } +type hint_entry = global_reference option * pri_auto_tactic + let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2 let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2 @@ -110,34 +112,60 @@ module Constr_map = Map.Make(struct let compare = Pervasives.compare end) +let is_transparent_gr (ids, csts) = function + | VarRef id -> Idpred.mem id ids + | ConstRef cst -> Cpred.mem cst csts + | IndRef _ | ConstructRef _ -> false + +let fmt_autotactic = + function + | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c) + | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c) + | Give_exact c -> (str"exact " ++ pr_lconstr c) + | Res_pf_THEN_trivial_fail (c,clenv) -> + (str"apply " ++ pr_lconstr c ++ str" ; trivial") + | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) + | Extern tac -> + (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) + +let pr_autotactic = fmt_autotactic + module Hint_db = struct type t = { hintdb_state : Names.transparent_state; use_dn : bool; - hintdb_map : search_entry Constr_map.t + hintdb_map : search_entry Constr_map.t; + (* A list of unindexed entries starting with an unfoldable constant + or with no associated pattern. *) + hintdb_nopat : stored_data list } - let empty use_dn = { hintdb_state = empty_transparent_state; - use_dn = use_dn; - hintdb_map = Constr_map.empty } + let empty st use_dn = { hintdb_state = st; + use_dn = use_dn; + hintdb_map = Constr_map.empty; + hintdb_nopat = [] } let find key db = try Constr_map.find key db.hintdb_map with Not_found -> empty_se - + let map_all k db = let (l,l',_) = find k db in - Sort.merge pri_order l l' + Sort.merge pri_order (db.hintdb_nopat @ l) l' let map_auto (k,c) db = let st = if db.use_dn then Some db.hintdb_state else None in - lookup_tacs (k,c) st (find k db) - + let l' = lookup_tacs (k,c) st (find k db) in + Sort.merge pri_order db.hintdb_nopat l' + let is_exact = function | Give_exact _ -> true | _ -> false + let rebuild_db st' db = + { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map } + let add_one (k,v) db = let st',rebuild = match v.code with @@ -148,27 +176,43 @@ module Hint_db = struct | EvalConstRef cst -> (ids, Cpred.add cst csts)), true | _ -> db.hintdb_state, false in - let dnst, db = - if db.use_dn then - Some st', { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map } - else None, db + let dnst, db, k = + if db.use_dn then + let db', k' = + if rebuild then rebuild_db st' db, k + else (* not an unfold *) + (match k with + | Some gr -> db, if is_transparent_gr st' gr then None else k + | None -> db, None) + in + (Some st', db', k') + else None, db, k in - let oval = find k db in let pat = if not db.use_dn && is_exact v.code then None else v.pat in - { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map; - hintdb_state = st' } + match k with + | None -> + if not (List.mem v db.hintdb_nopat) then + { db with hintdb_nopat = v :: db.hintdb_nopat } + else db + | Some gr -> + let oval = find gr db in + { db with hintdb_map = Constr_map.add gr (add_tac pat v dnst oval) db.hintdb_map; + hintdb_state = st' } let add_list l db = List.fold_right add_one l db - let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db.hintdb_map + let iter f db = + f None db.hintdb_nopat; + Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map let transparent_state db = db.hintdb_state - let set_transparent_state db st = { db with hintdb_state = st } + let set_transparent_state db st = + let db = if db.use_dn then rebuild_db st db else db in + { db with hintdb_state = st } - let set_rigid db cst = - let (ids,csts) = db.hintdb_state in - { db with hintdb_state = (ids, Cpred.remove cst csts) } + let use_dn db = db.use_dn + end module Hintdbmap = Gmap @@ -235,21 +279,21 @@ let make_exact_entry pri (c,cty) = let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type ce in let pat = Pattern.pattern_of_constr c' in - (head_of_constr_reference (List.hd (head_constr cty)), + (Some (head_of_constr_reference (fst (head_constr cty))), { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) -let make_apply_entry env sigma (eapply,verbose) pri (c,cty) = - let cty = hnf_constr env sigma cty in - match kind_of_term cty with +let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = + let cty = if hnf then hnf_constr env sigma cty else cty in + match kind_of_term cty with | Prod _ -> let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type ce in let pat = Pattern.pattern_of_constr c' in let hd = (try head_pattern_bound pat - with BoundPattern -> failwith "make_apply_entry") in + with BoundPattern -> failwith "make_apply_entry") in let nmiss = List.length (clenv_missing ce) in if nmiss = 0 then - (hd, + (Some hd, { pri = (match pri with None -> nb_hyp cty | Some p -> p); pat = Some pat; code = Res_pf(c,{ce with env=empty_env}) }) @@ -258,14 +302,14 @@ let make_apply_entry env sigma (eapply,verbose) pri (c,cty) = if verbose then warn (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); - (hd, + (Some hd, { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); pat = Some pat; code = ERes_pf(c,{ce with env=empty_env}) }) end | _ -> failwith "make_apply_entry" -(* flags is (e,v) with e=true if eapply and v=true if verbose +(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose c is a constr cty is the type of constr *) @@ -279,14 +323,14 @@ let make_resolves env sigma flags pri c = if ents = [] then errorlabstrm "Hint" (pr_lconstr c ++ spc() ++ - (if fst flags then str"cannot be used as a hint." + (if pi1 flags then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); ents (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma (hname,_,htyp) = try - [make_apply_entry env sigma (true, false) None + [make_apply_entry env sigma (true, true, false) None (mkVar hname, htyp)] with | Failure _ -> [] @@ -294,23 +338,23 @@ let make_resolve_hyp env sigma (hname,_,htyp) = (* REM : in most cases hintname = id *) let make_unfold (ref, eref) = - (ref, + (Some ref, { pri = 4; pat = None; code = Unfold_nth eref }) let make_extern pri pat tacast = - let hdconstr = try_head_pattern pat in + let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri=pri; - pat = Some pat; + pat = pat; code= Extern tacast }) let make_trivial env sigma c = let t = hnf_constr env sigma (type_of env sigma c) in - let hd = head_of_constr_reference (List.hd (head_constr t)) in + let hd = head_of_constr_reference (fst (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in - (hd, { pri=1; + (Some hd, { pri=1; pat = Some (Pattern.pattern_of_constr (clenv_type ce)); code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) @@ -328,15 +372,29 @@ let add_hint dbname hintlist = let db' = Hint_db.add_list hintlist db in searchtable_add (dbname,db') with Not_found -> - let db = Hint_db.add_list hintlist (Hint_db.empty false) in + let db = Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false) in searchtable_add (dbname,db) -type hint_action = CreateDB of bool | UpdateDB of (global_reference * pri_auto_tactic) list +let add_transparency dbname grs b = + let db = searchtable_map dbname in + let st = Hint_db.transparent_state db in + let st' = + List.fold_left (fun (ids, csts) gr -> + match gr with + | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) + | EvalVarRef v -> (if b then Idpred.add else Idpred.remove) v ids, csts) + st grs + in searchtable_add (dbname, Hint_db.set_transparent_state db st') + +type hint_action = | CreateDB of bool * transparent_state + | AddTransparency of evaluable_global_reference list * bool + | AddTactic of (global_reference option * pri_auto_tactic) list let cache_autohint (_,(local,name,hints)) = match hints with - | CreateDB b -> searchtable_add (name, Hint_db.empty b) - | UpdateDB hints -> add_hint name hints + | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) + | AddTransparency (grs, b) -> add_transparency name grs b + | AddTactic hints -> add_hint name hints let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for auto") @@ -351,11 +409,15 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = code = code ; } in - let subst_hint (lab,data as hint) = - let lab',elab' = subst_global subst lab in - let lab' = - try head_of_constr_reference (List.hd (head_constr_bound elab' [])) - with Tactics.Bound -> lab' in + let subst_key gr = + let (lab'', elab') = subst_global subst gr in + let gr' = + (try head_of_constr_reference (fst (head_constr_bound elab')) + with Tactics.Bound -> lab'') + in if gr' == gr then gr else gr' + in + let subst_hint (k,data as hint) = + let k' = Option.smartmap subst_key k in let data' = match data.code with | Res_pf (c, clenv) -> let c' = subst_mps subst c in @@ -383,18 +445,21 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = if tac==tac' then data else trans_data data (Extern tac') in - if lab' == lab && data' == data then hint else - (lab',data') + if k' == k && data' == data then hint else + (k',data') in match hintlist with | CreateDB _ -> obj - | UpdateDB hintlist -> + | AddTransparency (grs, b) -> + let grs' = list_smartmap (subst_evaluable_reference subst) grs in + if grs==grs' then obj else (local, name, AddTransparency (grs', b)) + | AddTactic hintlist -> let hintlist' = list_smartmap subst_hint hintlist in if hintlist' == hintlist then obj else - (local,name,UpdateDB hintlist') + (local,name,AddTactic hintlist') let classify_autohint (_,((local,name,hintlist) as obj)) = - if local or hintlist = (UpdateDB []) then Dispose else Substitute obj + if local or hintlist = (AddTactic []) then Dispose else Substitute obj let export_autohint ((local,name,hintlist) as obj) = if local then None else Some obj @@ -408,8 +473,8 @@ let (inAutoHint,outAutoHint) = export_function = export_autohint } -let create_hint_db l n b = - Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB b)) +let create_hint_db l n st b = + Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st))) (**************************************************************************) (* The "Hint" vernacular command *) @@ -419,29 +484,40 @@ let add_resolves env sigma clist local dbnames = (fun dbname -> Lib.add_anonymous_leaf (inAutoHint - (local,dbname, UpdateDB - (List.flatten (List.map (fun (x, y) -> - make_resolves env sigma (true,Flags.is_verbose()) x y) clist))))) + (local,dbname, AddTactic + (List.flatten (List.map (fun (x, hnf, y) -> + make_resolves env sigma (true,hnf,Flags.is_verbose()) x y) clist))))) dbnames let add_unfolds l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf - (inAutoHint (local,dbname, UpdateDB (List.map make_unfold l)))) + (inAutoHint (local,dbname, AddTactic (List.map make_unfold l)))) + dbnames + +let add_transparency l b local dbnames = + List.iter + (fun dbname -> Lib.add_anonymous_leaf + (inAutoHint (local,dbname, AddTransparency (l, b)))) dbnames -let add_extern pri (patmetas,pat) tacast local dbname = +let add_extern pri pat tacast local dbname = (* We check that all metas that appear in tacast have at least one occurence in the left pattern pat *) let tacmetas = [] in - match (list_subtract tacmetas patmetas) with - | i::_ -> - errorlabstrm "add_extern" - (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") - | [] -> + match pat with + | Some (patmetas,pat) -> + (match (list_subtract tacmetas patmetas) with + | i::_ -> + errorlabstrm "add_extern" + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") + | [] -> + Lib.add_anonymous_leaf + (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast]))) + | None -> Lib.add_anonymous_leaf - (inAutoHint(local,dbname, UpdateDB [make_extern pri pat tacast])) + (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast])) let add_externs pri pat tacast local dbnames = List.iter (add_extern pri pat tacast local) dbnames @@ -450,7 +526,7 @@ let add_trivials env sigma l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf ( - inAutoHint(local,dbname, UpdateDB (List.map (make_trivial env sigma) l)))) + inAutoHint(local,dbname, AddTactic (List.map (make_trivial env sigma) l)))) dbnames let forward_intern_tac = @@ -464,7 +540,7 @@ let add_hints local dbnames0 h = let f = Constrintern.interp_constr sigma env in match h with | HintsResolve lhints -> - add_resolves env sigma (List.map (fun (pri, x) -> pri, f x) lhints) local dbnames + add_resolves env sigma (List.map (fun (pri, b, x) -> pri, b, f x) lhints) local dbnames | HintsImmediate lhints -> add_trivials env sigma (List.map f lhints) local dbnames | HintsUnfold lhints -> @@ -478,21 +554,35 @@ let add_hints local dbnames0 h = (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference.") in - if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + Dumpglob.add_glob (loc_of_reference r) gr; (gr,r') in add_unfolds (List.map f lhints) local dbnames + | HintsTransparency (lhints, b) -> + let f r = + let gr = Syntax_def.global_with_alias r in + let r' = match gr with + | ConstRef c -> EvalConstRef c + | VarRef c -> EvalVarRef c + | _ -> + errorlabstrm "evalref_of_ref" + (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ + str "to an evaluable reference.") + in + Dumpglob.add_glob (loc_of_reference r) gr; + r' in + add_transparency (List.map f lhints) b local dbnames | HintsConstructors lqid -> let add_one qid = let env = Global.env() and sigma = Evd.empty in let isp = inductive_of_reference qid in let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in let lcons = list_tabulate - (fun i -> None, mkConstruct (isp,i+1)) (Array.length consnames) in + (fun i -> None, true, mkConstruct (isp,i+1)) (Array.length consnames) in add_resolves env sigma lcons local dbnames in List.iter add_one lqid | HintsExtern (pri, patcom, tacexp) -> - let pat = Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in - let tacexp = !forward_intern_tac (fst pat) tacexp in + let pat = Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in + let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in add_externs pri pat tacexp local dbnames | HintsDestruct(na,pri,loc,pat,code) -> if dbnames0<>[] then @@ -503,7 +593,7 @@ let add_hints local dbnames0 h = (* Functions for printing the hints *) (**************************************************************************) -let fmt_autotactic = +let pr_autotactic = function | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c) | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c) @@ -514,19 +604,19 @@ let fmt_autotactic = | Extern tac -> (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) -let fmt_hint v = - (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) +let pr_hint v = + (pr_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) -let fmt_hint_list hintlist = - (str " " ++ hov 0 (prlist fmt_hint hintlist) ++ fnl ()) +let pr_hint_list hintlist = + (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ()) -let fmt_hints_db (name,db,hintlist) = +let pr_hints_db (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ if hintlist = [] then (str " nothing" ++ fnl ()) - else (fnl () ++ fmt_hint_list hintlist)) + else (fnl () ++ pr_hint_list hintlist)) (* Print all hints associated to head c in any database *) -let fmt_hint_list_for_head c = +let pr_hint_list_for_head c = let dbs = Hintdbmap.to_list !searchtable in let valid_dbs = map_succeed @@ -538,19 +628,16 @@ let fmt_hint_list_for_head c = else hov 0 (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++ - hov 0 (prlist fmt_hints_db valid_dbs)) + hov 0 (prlist pr_hints_db valid_dbs)) -let fmt_hint_ref ref = fmt_hint_list_for_head ref +let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let print_hint_ref ref = ppnl(fmt_hint_ref ref) +let print_hint_ref ref = ppnl(pr_hint_ref ref) -let fmt_hint_term cl = +let pr_hint_term cl = try - let (hdc,args) = match head_constr_bound cl [] with - | hdc::args -> (hdc,args) - | [] -> assert false - in + let (hdc,args) = head_constr_bound cl in let hd = head_of_constr_reference hdc in let dbs = Hintdbmap.to_list !searchtable in let valid_dbs = @@ -568,14 +655,14 @@ let fmt_hint_term cl = (str "No hint applicable for current goal") else (str "Applicable Hints :" ++ fnl () ++ - hov 0 (prlist fmt_hints_db valid_dbs)) + hov 0 (prlist pr_hints_db valid_dbs)) with Bound | Match_failure _ | Failure _ -> (str "No hint applicable for current goal") let error_no_such_hint_database x = error ("No such Hint database: "^x^".") -let print_hint_term cl = ppnl (fmt_hint_term cl) +let print_hint_term cl = ppnl (pr_hint_term cl) (* print all hints that apply to the concl of the current goal *) let print_applicable_hint () = @@ -591,9 +678,15 @@ let print_hint_db db = str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); Hint_db.iter (fun head hintlist -> - msg (hov 0 - (str "For " ++ pr_global head ++ str " -> " ++ - fmt_hint_list hintlist))) + match head with + | Some head -> + msg (hov 0 + (str "For " ++ pr_global head ++ str " -> " ++ + pr_hint_list hintlist)) + | None -> + msg (hov 0 + (str "For any goal -> " ++ + pr_hint_list hintlist))) db let print_hint_db_by_name dbname = @@ -618,7 +711,10 @@ let print_searchtable () = (* tactics with a trace mechanism for automatic search *) (**************************************************************************) -let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l) +let priority l = List.filter (fun (_,hint) -> hint.pri = 0) l + +let select_unfold_extern = + List.filter (function (_,{code = (Unfold_nth _ | Extern _)}) -> true | _ -> false) (* tell auto not to reuse already instantiated metas in unification (for compatibility, since otherwise, apply succeeds oftener) *) @@ -633,25 +729,33 @@ let auto_unif_flags = { (* Try unification with the precompiled clause, then use registered Apply *) -let unify_resolve_nodelta (c,clenv) gls = - let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in - h_simplest_apply c gls +let unify_resolve_nodelta (c,clenv) gl = + let clenv' = connect_clenv gl clenv in + let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in + h_simplest_apply c gl -let unify_resolve flags (c,clenv) gls = - let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver false ~flags clenv' gls in - h_apply true false [c,NoBindings] gls +let unify_resolve flags (c,clenv) gl = + let clenv' = connect_clenv gl clenv in + let _ = clenv_unique_resolver false ~flags clenv' gl in + h_apply true false [inj_open c,NoBindings] gl +let unify_resolve_gen = function + | None -> unify_resolve_nodelta + | Some flags -> unify_resolve flags (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types *) -let make_local_hint_db eapply lems g = - let sign = pf_hyps g in - let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in - let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in - Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty false)) +let add_hint_lemmas eapply lems hint_db gl = + let hintlist' = + list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in + Hint_db.add_list hintlist' hint_db + +let make_local_hint_db eapply lems gl = + let sign = pf_hyps gl in + let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in + add_hint_lemmas eapply lems + (Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false)) gl (* Serait-ce possible de compiler d'abord la tactique puis de faire la substitution sans passer par bdize dont l'objectif est de préparer un @@ -671,10 +775,13 @@ let forward_interp_tactic = let set_extern_interp f = forward_interp_tactic := f let conclPattern concl pat tac gl = - let constr_bindings = - try matches pat concl - with PatternMatchingFailure -> error "conclPattern" in - !forward_interp_tactic constr_bindings tac gl + let constr_bindings = + match pat with + | None -> [] + | Some pat -> + try matches pat concl + with PatternMatchingFailure -> error "conclPattern" in + !forward_interp_tactic constr_bindings tac gl (**************************************************************************) (* The Trivial tactic *) @@ -684,6 +791,10 @@ let conclPattern concl pat tac gl = (* Papageno : cette fonction a été pas mal simplifiée depuis que la base de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) +let flags_of_state st = + {auto_unif_flags with + modulo_conv_on_closed_terms = Some st; modulo_delta = st} + let rec trivial_fail_db mod_delta db_list local_db gl = let intro_tac = tclTHEN intro @@ -697,29 +808,12 @@ let rec trivial_fail_db mod_delta db_list local_db gl = (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl and my_find_search_nodelta db_list local_db hdc concl = - let tacl = - if occur_existential concl then - list_map_append (Hint_db.map_all hdc) - (local_db::db_list) - else - list_map_append (Hint_db.map_auto (hdc,concl)) - (local_db::db_list) - in - List.map - (fun {pri=b; pat=p; code=t} -> - (b, - match t with - | Res_pf (term,cl) -> unify_resolve_nodelta (term,cl) - | ERes_pf (_,c) -> (fun gl -> error "eres_pf") - | Give_exact c -> exact_check c - | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN - (unify_resolve_nodelta (term,cl)) - (trivial_fail_db false db_list local_db) - | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> - conclPattern concl (Option.get p) tacast)) - tacl + if occur_existential concl then + List.map (fun hint -> (None,hint)) + (list_map_append (Hint_db.map_all hdc) (local_db::db_list)) + else + List.map (fun hint -> (None,hint)) + (list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)) and my_find_search mod_delta = if mod_delta then my_find_search_delta @@ -727,46 +821,51 @@ and my_find_search mod_delta = and my_find_search_delta db_list local_db hdc concl = let flags = {auto_unif_flags with use_metas_eagerly = true} in - let tacl = if occur_existential concl then list_map_append (fun db -> - let st = {flags with modulo_delta = Hint_db.transparent_state db} in - List.map (fun x -> (st,x)) (Hint_db.map_all hdc db)) + if Hint_db.use_dn db then + let flags = flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db) + else + let flags = {flags with modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> (Some flags,x)) (Hint_db.map_all hdc db)) (local_db::db_list) else list_map_append (fun db -> - let (ids, csts as st) = Hint_db.transparent_state db in - let st, l = - let l = - if (Idpred.is_empty ids && Cpred.is_empty csts) - then Hint_db.map_auto (hdc,concl) db - else Hint_db.map_all hdc db - in {flags with modulo_delta = st}, l - in List.map (fun x -> (st,x)) l) + if Hint_db.use_dn db then + let flags = flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db) + else + let (ids, csts as st) = Hint_db.transparent_state db in + let flags, l = + let l = + if (Idpred.is_empty ids && Cpred.is_empty csts) + then Hint_db.map_auto (hdc,concl) db + else Hint_db.map_all hdc db + in {flags with modulo_delta = st}, l + in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) - in - List.map - (fun (st, {pri=b; pat=p; code=t}) -> - (b, - match t with - | Res_pf (term,cl) -> unify_resolve st (term,cl) - | ERes_pf (_,c) -> (fun gl -> error "eres_pf") - | Give_exact c -> exact_check c - | Res_pf_THEN_trivial_fail (term,cl) -> - tclTHEN - (unify_resolve st (term,cl)) - (trivial_fail_db true db_list local_db) - | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> - conclPattern concl (Option.get p) tacast)) - tacl + +and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) = + match t with + | Res_pf (term,cl) -> unify_resolve_gen flags (term,cl) + | ERes_pf (_,c) -> (fun gl -> error "eres_pf") + | Give_exact c -> exact_check c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN + (unify_resolve_gen flags (term,cl)) + (trivial_fail_db (flags <> None) db_list local_db) + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] + | Extern tacast -> conclPattern concl p tacast and trivial_resolve mod_delta db_list local_db cl = try - let hdconstr = List.hd (head_constr_bound cl []) in - priority - (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl) + let hdconstr,_ = head_constr_bound cl in + List.map (tac_of_hint db_list local_db cl) + (priority + (my_find_search mod_delta db_list local_db + (head_of_constr_reference hdconstr) cl)) with Bound | Not_found -> [] @@ -804,70 +903,82 @@ let h_trivial lems l = let possible_resolve mod_delta db_list local_db cl = try - let hdconstr = List.hd (head_constr_bound cl []) in - List.map snd - (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl) + let hdconstr,_ = head_constr_bound cl in + List.map (tac_of_hint db_list local_db cl) + (my_find_search mod_delta db_list local_db + (head_of_constr_reference hdconstr) cl) with Bound | Not_found -> [] -let decomp_unary_term c gls = - let typc = pf_type_of gls c in - let hd = List.hd (head_constr typc) in - if Hipattern.is_conjunction hd then - simplest_case c gls - else - errorlabstrm "Auto.decomp_unary_term" (str "Not a unary type.") - -let decomp_empty_term c gls = - let typc = pf_type_of gls c in - let (hd,_) = decompose_app typc in - if Hipattern.is_empty_type hd then - simplest_case c gls +let decomp_unary_term_then (id,_,typc) kont1 kont2 gl = + try + let ccl = applist (head_constr typc) in + match Hipattern.match_with_conjunction ccl with + | Some (_,args) -> + tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl + | None -> + kont2 gl + with UserError _ -> kont2 gl + +let decomp_empty_term (id,_,typc) gl = + if Hipattern.is_empty_type typc then + simplest_case (mkVar id) gl else errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.") +let extend_local_db gl decl db = + Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db + +(* Try to decompose hypothesis [decl] into atomic components of a + conjunction with maximum depth [p] (or solve the goal from an + empty type) then call the continuation tactic with hint db extended + with the obtappined not-further-decomposable hypotheses *) + +let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl = + if p = 0 then + kont (extend_local_db gl decl db) gl + else + tclORELSE0 + (decomp_empty_term decl) + (decomp_unary_term_then decl (intros_decomp (p-1) kont [] db) + (kont (extend_local_db gl decl db))) gl + +(* Introduce [n] hypotheses, then decompose then with maximum depth [p] and + call the continuation tactic [kont] with the hint db extended + with the so-obtained not-further-decomposable hypotheses *) + +and intros_decomp p kont decls db n = + if n = 0 then + decomp_and_register_decls p kont decls db + else + tclTHEN intro (tclLAST_DECL (fun d -> + (intros_decomp p kont (d::decls) db (n-1)))) + +(* Decompose hypotheses [hyps] with maximum depth [p] and + call the continuation tactic [kont] with the hint db extended + with the so-obtained not-further-decomposable hypotheses *) + +and decomp_and_register_decls p kont decls = + List.fold_left (decomp_and_register_decl p) kont decls + (* decomp is an natural number giving an indication on decomposition of conjunction in hypotheses, 0 corresponds to no decomposition *) (* n is the max depth of search *) (* local_db contains the local Hypotheses *) -let rec search_gen decomp n mod_delta db_list local_db extra_sign goal = - if n=0 then error "BOUND 2"; - let decomp_tacs = match decomp with - | 0 -> [] - | p -> - (tclTRY_sign decomp_empty_term extra_sign) - :: - (List.map - (fun id -> tclTHENSEQ - [decomp_unary_term (mkVar id); - clear [id]; - search_gen decomp p mod_delta db_list local_db []]) - (pf_ids_of_hyps goal)) - in - let intro_tac = - tclTHEN intro - (fun g' -> - let (hid,_,htyp as d) = pf_last_hyp g' in - let hintl = - try - [make_apply_entry (pf_env g') (project g') - (true,false) None - (mkVar hid, htyp)] - with Failure _ -> [] - in - search_gen decomp n mod_delta db_list (Hint_db.add_list hintl local_db) [d] g') - in - let rec_tacs = - List.map - (fun ntac -> - tclTHEN ntac - (search_gen decomp (n-1) mod_delta db_list local_db empty_named_context)) - (possible_resolve mod_delta db_list local_db (pf_concl goal)) - in - tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal +exception Uplift of tactic list +let rec search_gen p n mod_delta db_list local_db = + let rec search n local_db gl = + if n=0 then error "BOUND 2"; + tclFIRST + (assumption :: + intros_decomp p (search n) [] local_db 1 :: + List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db)) + (possible_resolve mod_delta db_list local_db (pf_concl gl))) gl + in + search n local_db let search = search_gen 0 @@ -883,8 +994,7 @@ let delta_auto mod_delta n lems dbnames gl = error_no_such_hint_database x) ("core"::dbnames) in - let hyps = pf_hyps gl in - tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl + tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl let auto = delta_auto false @@ -896,8 +1006,7 @@ let delta_full_auto mod_delta n lems gl = let dbnames = Hintdbmap.dom !searchtable in let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map (fun x -> searchtable_map x) dbnames in - let hyps = pf_hyps gl in - tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl + tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl let full_auto = delta_full_auto false let new_full_auto = delta_full_auto true @@ -922,14 +1031,15 @@ let h_auto n lems l = (* Depth of search after decomposition of hypothesis, by default one look for an immediate solution *) -(* Papageno : de toute façon un paramète > 1 est traité comme 1 pour - l'instant *) -let default_search_decomp = ref 1 - -let destruct_auto des_opt lems n gl = - let hyps = pf_hyps gl in - search_gen des_opt n false (List.map searchtable_map ["core";"extcore"]) - (make_local_hint_db false lems gl) hyps gl +let default_search_decomp = ref 20 + +let destruct_auto p lems n gl = + decomp_and_register_decls p (fun local_db gl -> + search_gen p n false (List.map searchtable_map ["core";"extcore"]) + (add_hint_lemmas false lems local_db gl) gl) + (pf_hyps gl) + (Hint_db.empty empty_transparent_state false) + gl let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n) @@ -952,7 +1062,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) = let ents = map_succeed (fun f -> f (mkVar id,ty)) - [make_exact_entry None; make_apply_entry env sigma (true,false) None] + [make_exact_entry None; make_apply_entry env sigma (true,true,false) None] in ents @@ -988,25 +1098,23 @@ let compileAutoArg contac = function let compileAutoArgList contac = List.map (compileAutoArg contac) -let rec super_search n db_list local_db argl goal = +let rec super_search n db_list local_db argl gl = if n = 0 then error "BOUND 2"; tclFIRST (assumption :: - (tclTHEN intro + tclTHEN intro (fun g -> let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in super_search n db_list (Hint_db.add_list hintl local_db) - argl g)) + argl g) :: - ((List.map - (fun ntac -> + List.map (fun ntac -> tclTHEN ntac (super_search (n-1) db_list local_db argl)) - (possible_resolve false db_list local_db (pf_concl goal))) + (possible_resolve false db_list local_db (pf_concl gl)) @ - (compileAutoArgList - (super_search (n-1) db_list local_db argl) argl))) goal + compileAutoArgList (super_search (n-1) db_list local_db argl) argl) gl let search_superauto n to_add argl g = let sigma = -- cgit v1.2.3