diff options
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r-- | tactics/auto.ml | 312 |
1 files changed, 201 insertions, 111 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 3cd1591d..2a5bb95c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 9154 2006-09-20 17:18:18Z corbinea $ *) +(* $Id: auto.ml 11094 2008-06-10 19:35:23Z herbelin $ *) open Pp open Util @@ -93,8 +93,8 @@ let empty_se = ([],[],Btermdn.create ()) let add_tac t (l,l',dn) = match t.pat with - None -> (insert t l, l', dn) - | Some pat -> (l, insert t l', Btermdn.add dn (pat,t)) + None -> if not (List.mem t l) then (insert t l, l', dn) else (l, l', dn) + | Some pat -> if not (List.mem t l') then (l, insert t l', Btermdn.add dn (pat,t)) else (l, l', dn) let lookup_tacs (hdc,c) (l,l',dn) = @@ -137,14 +137,16 @@ end module Hintdbmap = Gmap -type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t +type hint_db = Names.transparent_state * Hint_db.t -type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref +type frozen_hint_db_table = (string,hint_db) Hintdbmap.t + +type hint_db_table = (string,hint_db) Hintdbmap.t ref type hint_db_name = string let searchtable = (ref Hintdbmap.empty : hint_db_table) - + let searchtable_map name = Hintdbmap.find name !searchtable let searchtable_add (name,db) = @@ -182,23 +184,20 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable" -let make_exact_entry (c,cty) = +let make_exact_entry pri (c,cty) = let cty = strip_outer_cast cty in match kind_of_term cty with | Prod (_,_,_) -> failwith "make_exact_entry" | _ -> (head_of_constr_reference (List.hd (head_constr cty)), - { pri=0; pat=None; code=Give_exact c }) + { pri=(match pri with Some pri -> pri | None -> 0); pat=None; code=Give_exact c }) -let dummy_goal = - {it={evar_hyps=empty_named_context_val; - evar_concl=mkProp; - evar_body=Evar_empty; - evar_extra=None}; - sigma=Evd.empty} +let dummy_goal = + {it = make_evar empty_named_context_val mkProp; + sigma = empty} -let make_apply_entry env sigma (eapply,verbose) (c,cty) = +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 | Prod _ -> @@ -207,45 +206,47 @@ let make_apply_entry env sigma (eapply,verbose) (c,cty) = let pat = Pattern.pattern_of_constr c' in let hd = (try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry") in - let nmiss = List.length (clenv_missing ce) - in - if eapply & (nmiss <> 0) then begin - if verbose then + let nmiss = List.length (clenv_missing ce) in + if nmiss = 0 then + (hd, + { pri = (match pri with None -> nb_hyp cty | Some p -> p); + pat = Some pat; + code = Res_pf(c,{ce with env=empty_env}) }) + else begin + if not eapply then failwith "make_apply_entry"; + if verbose then warn (str "the hint: eapply " ++ pr_lconstr c ++ - str " will only be used by eauto"); + str " will only be used by eauto"); (hd, - { pri = nb_hyp cty + nmiss; - pat = Some pat; - code = ERes_pf(c,{ce with templenv=empty_env}) }) - end else - (hd, - { pri = nb_hyp cty; - pat = Some pat; - code = Res_pf(c,{ce with templenv=empty_env}) }) + { 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" -(* eap is (e,v) with e=true if eapply and v=true if verbose +(* flags is (e,v) with e=true if eapply and v=true if verbose c is a constr cty is the type of constr *) -let make_resolves env sigma eap c = +let make_resolves env sigma flags pri c = let cty = type_of env sigma c in let ents = map_succeed (fun f -> f (c,cty)) - [make_exact_entry; make_apply_entry env sigma (eap,Options.is_verbose())] + [make_exact_entry pri; make_apply_entry env sigma flags pri] in if ents = [] then errorlabstrm "Hint" - (pr_lconstr c ++ spc() ++ str"cannot be used as a hint"); + (pr_lconstr c ++ spc() ++ + (if fst 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) - (mkVar hname, htyp)] + [make_apply_entry env sigma (true, false) None + (mkVar hname, htyp)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp" @@ -270,7 +271,7 @@ let make_trivial env sigma c = let ce = mk_clenv_from dummy_goal (c,t) in (hd, { pri=1; pat = Some (Pattern.pattern_of_constr (clenv_type ce)); - code=Res_pf_THEN_trivial_fail(c,{ce with templenv=empty_env}) }) + code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) open Vernacexpr @@ -278,18 +279,32 @@ open Vernacexpr (* declaration of the AUTOHINT library object *) (**************************************************************************) +let add_hint_list hintlist (st,db) = + let db' = Hint_db.add_list hintlist db in + let st' = + List.fold_left + (fun (ids, csts as st) (_, hint) -> + match hint.code with + | Unfold_nth egr -> + (match egr with + | EvalVarRef id -> (Idpred.add id ids, csts) + | EvalConstRef cst -> (ids, Cpred.add cst csts)) + | _ -> st) + st hintlist + in (st', db') + (* If the database does not exist, it is created *) (* TODO: should a warning be printed in this case ?? *) let add_hint dbname hintlist = try let db = searchtable_map dbname in - let db' = Hint_db.add_list hintlist db in + let db' = add_hint_list hintlist db in searchtable_add (dbname,db') with Not_found -> - let db = Hint_db.add_list hintlist Hint_db.empty in + let db = add_hint_list hintlist (empty_transparent_state, Hint_db.empty) in searchtable_add (dbname,db) -let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist +let cache_autohint (_,(local,name,hints)) = add_hint name hints let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for auto") @@ -300,7 +315,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = let trans_clenv clenv = Clenv.subst_clenv subst clenv in let trans_data data code = { data with - pat = option_smartmap (subst_pattern subst) data.pat ; + pat = Option.smartmap (subst_pattern subst) data.pat ; code = code ; } in @@ -367,7 +382,8 @@ let add_resolves env sigma clist local dbnames = Lib.add_anonymous_leaf (inAutoHint (local,dbname, - List.flatten (List.map (make_resolves env sigma true) clist)))) + List.flatten (List.map (fun (x, y) -> + make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))) dbnames @@ -411,29 +427,30 @@ 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 f lhints) local dbnames + add_resolves env sigma (List.map (fun (pri, x) -> pri, f x) lhints) local dbnames | HintsImmediate lhints -> add_trivials env sigma (List.map f lhints) local dbnames | HintsUnfold lhints -> - let f qid = - let r = Nametab.global qid in - let r' = match r with + 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 r ++ spc () ++ + (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference") in - (r,r') in + if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> let add_one qid = let env = Global.env() and sigma = Evd.empty in - let isp = global_inductive qid in + let isp = inductive_of_reference qid in let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in let lcons = list_tabulate - (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in + (fun i -> None, 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) -> @@ -476,7 +493,7 @@ let fmt_hint_list_for_head c = let dbs = Hintdbmap.to_list !searchtable in let valid_dbs = map_succeed - (fun (name,db) -> (name,db,Hint_db.map_all c db)) + (fun (name,(_,db)) -> (name,db,Hint_db.map_all c db)) dbs in if valid_dbs = [] then @@ -502,11 +519,11 @@ let fmt_hint_term cl = let valid_dbs = if occur_existential cl then map_succeed - (fun (name, db) -> (name, db, Hint_db.map_all hd db)) + (fun (name, (_, db)) -> (name, db, Hint_db.map_all hd db)) dbs else map_succeed - (fun (name, db) -> + (fun (name, (_, db)) -> (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) dbs in @@ -527,7 +544,10 @@ let print_applicable_hint () = print_hint_term (pf_concl gl) (* displays the whole hint database db *) -let print_hint_db db = +let print_hint_db ((ids, csts),db) = + msg (hov 0 + (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++ + str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); Hint_db.iter (fun head hintlist -> msg (hov 0 @@ -559,22 +579,38 @@ let print_searchtable () = let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l) +(* tell auto not to reuse already instantiated metas in unification (for + compatibility, since otherwise, apply succeeds oftener) *) + +open Unification + +let auto_unif_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; + use_metas_eagerly = false; + modulo_delta = empty_transparent_state; +} (* Try unification with the precompiled clause, then use registered Apply *) -let unify_resolve (c,clenv) gls = +let unify_resolve_nodelta (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver false clenv' gls in + let _ = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gls in h_simplest_apply c gls +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 + + (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) -let make_local_hint_db lems g = +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 true) lems in - Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty) + let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in + (empty_transparent_state, Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty)) (* 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 @@ -607,47 +643,90 @@ 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 rec trivial_fail_db db_list local_db gl = +let rec trivial_fail_db mod_delta db_list local_db gl = let intro_tac = tclTHEN intro (fun g'-> let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') + in trivial_fail_db mod_delta db_list (add_hint_list hintl local_db) g') in tclFIRST (assumption::intro_tac:: (List.map tclCOMPLETE - (trivial_resolve db_list local_db (pf_concl gl)))) gl + (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl -and my_find_search db_list local_db hdc concl = +and my_find_search_nodelta db_list local_db hdc concl = let tacl = if occur_existential concl then - list_map_append (fun db -> Hint_db.map_all hdc db) (local_db::db_list) - else - list_map_append (fun db -> Hint_db.map_auto (hdc,concl) db) + list_map_append + (fun (st, db) -> (Hint_db.map_all hdc db)) + (local_db::db_list) + else + list_map_append (fun (_, db) -> + Hint_db.map_auto (hdc,concl) db) (local_db::db_list) in - List.map - (fun {pri=b; pat=p; code=t} -> - (b, + List.map + (fun {pri=b; pat=p; code=t} -> + (b, match t with - | Res_pf (term,cl) -> unify_resolve (term,cl) + | 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 (term,cl)) - (trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + (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 (out_some p) tacast)) + conclPattern concl (Option.get p) tacast)) tacl -and trivial_resolve db_list local_db cl = +and my_find_search mod_delta = + if mod_delta then my_find_search_delta + else my_find_search_nodelta + +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 (st, db) -> + let st = {flags with modulo_delta = st} in + List.map (fun x -> (st,x)) (Hint_db.map_all hdc db)) + (local_db::db_list) + else + list_map_append (fun ((ids, csts as st), db) -> + 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) + (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 trivial_resolve mod_delta db_list local_db cl = try let hdconstr = List.hd (head_constr_bound cl []) in priority - (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) + (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl) with Bound | Not_found -> [] @@ -661,30 +740,33 @@ let trivial lems dbnames gl = error ("trivial: "^x^": No such Hint database")) ("core"::dbnames) in - tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl + tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl let full_trivial 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 - tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl + tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl let gen_trivial lems = function | None -> full_trivial lems | Some l -> trivial lems l +let inj_open c = (Evd.empty,c) + let h_trivial lems l = - Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l) + Refiner.abstract_tactic (TacTrivial (List.map inj_open lems,l)) + (gen_trivial lems l) (**************************************************************************) (* The classical Auto tactic *) (**************************************************************************) -let possible_resolve db_list local_db cl = +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 db_list local_db (head_of_constr_reference hdconstr) cl) + (my_find_search mod_delta db_list local_db (head_of_constr_reference hdconstr) cl) with Bound | Not_found -> [] @@ -710,7 +792,7 @@ let decomp_empty_term c gls = (* n is the max depth of search *) (* local_db contains the local Hypotheses *) -let rec search_gen decomp n db_list local_db extra_sign goal = +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 -> [] @@ -721,7 +803,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = (fun id -> tclTHENSEQ [decomp_unary_term (mkVar id); clear [id]; - search_gen decomp p db_list local_db []]) + search_gen decomp p mod_delta db_list local_db []]) (pf_ids_of_hyps goal)) in let intro_tac = @@ -731,18 +813,18 @@ let rec search_gen decomp n db_list local_db extra_sign goal = let hintl = try [make_apply_entry (pf_env g') (project g') - (true,false) + (true,false) None (mkVar hid, htyp)] with Failure _ -> [] in - search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d] g') + search_gen decomp n mod_delta db_list (add_hint_list hintl local_db) [d] g') in let rec_tacs = List.map (fun ntac -> tclTHEN ntac - (search_gen decomp (n-1) db_list local_db empty_named_context)) - (possible_resolve db_list local_db (pf_concl goal)) + (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 @@ -751,7 +833,7 @@ let search = search_gen 0 let default_search_depth = ref 5 -let auto n lems dbnames gl = +let delta_auto mod_delta n lems dbnames gl = let db_list = List.map (fun x -> @@ -762,17 +844,24 @@ let auto n lems dbnames gl = ("core"::dbnames) in let hyps = pf_hyps gl in - tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl + tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl + +let auto = delta_auto false + +let new_auto = delta_auto true let default_auto = auto !default_search_depth [] [] -let full_auto n lems gl = +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 db_list (make_local_hint_db lems gl) hyps) gl - + tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl + +let full_auto = delta_full_auto false +let new_full_auto = delta_full_auto true + let default_full_auto gl = full_auto !default_search_depth [] gl let gen_auto n lems dbnames = @@ -781,10 +870,11 @@ let gen_auto n lems dbnames = | None -> full_auto n lems | Some l -> auto n lems l -let inj_or_var = option_map (fun n -> ArgArg n) +let inj_or_var = Option.map (fun n -> ArgArg n) let h_auto n lems l = - Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l) + Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l)) + (gen_auto n lems l) (**************************************************************************) (* The "destructing Auto" from Eduardo *) @@ -796,23 +886,23 @@ let h_auto n lems l = l'instant *) let default_search_decomp = ref 1 -let destruct_auto des_opt n gl = +let destruct_auto des_opt lems n gl = let hyps = pf_hyps gl in - search_gen des_opt n [searchtable_map "core"] - (make_local_hint_db [] gl) hyps gl + search_gen des_opt n false (List.map searchtable_map ["core";"extcore"]) + (make_local_hint_db false lems gl) hyps gl -let dautomatic des_opt n = tclTRY (destruct_auto des_opt n) +let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n) -let default_dauto = dautomatic !default_search_decomp !default_search_depth +let dauto (n,p) lems = + let p = match p with Some p -> p | None -> !default_search_decomp in + let n = match n with Some n -> n | None -> !default_search_depth in + dautomatic p lems n -let dauto = function - | None, None -> default_dauto - | Some n, None -> dautomatic !default_search_decomp n - | Some n, Some p -> dautomatic p n - | None, Some p -> dautomatic p !default_search_depth +let default_dauto = dauto (None,None) [] -let h_dauto (n,p) = - Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p)) +let h_dauto (n,p) lems = + Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map inj_open lems)) + (dauto (n,p) lems) (***************************************) (*** A new formulation of Auto *********) @@ -822,7 +912,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) = let ents = map_succeed (fun f -> f (mkVar id,ty)) - [make_exact_entry; make_apply_entry env sigma (true,false)] + [make_exact_entry None; make_apply_entry env sigma (true,false) None] in ents @@ -866,14 +956,14 @@ let rec super_search n db_list local_db argl goal = (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) + super_search n db_list (add_hint_list hintl local_db) argl g)) :: ((List.map (fun ntac -> tclTHEN ntac (super_search (n-1) db_list local_db argl)) - (possible_resolve db_list local_db (pf_concl goal))) + (possible_resolve false db_list local_db (pf_concl goal))) @ (compileAutoArgList (super_search (n-1) db_list local_db argl) argl))) goal @@ -884,7 +974,7 @@ let search_superauto n to_add argl g = (fun (id,c) -> add_named_decl (id, None, pf_type_of g c)) to_add empty_named_context in let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in - let db = Hint_db.add_list db0 (make_local_hint_db [] g) in + let db = add_hint_list db0 (make_local_hint_db false [] g) in super_search n [Hintdbmap.find "core" !searchtable] db argl g let superauto n to_add argl = @@ -892,8 +982,8 @@ let superauto n to_add argl = let default_superauto g = superauto !default_search_depth [] [] g -let interp_to_add gl locqid = - let r = Nametab.global locqid in +let interp_to_add gl r = + let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in let id = id_of_global r in (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r) |