diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 24 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 54 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 17 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.mli | 8 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 5 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 | ||||
| -rw-r--r-- | tactics/auto.ml | 21 |
9 files changed, 104 insertions, 37 deletions
@@ -32,6 +32,10 @@ Tactics - Tactic "exists" and "eexists" supports iteration using comma-separated arguments. - Tactic "gappa" has been removed from the Dp plugin. +- Tactic "firstorder" now supports the combination of its "using" and + "with" options. +- An inductive type as argument of the "using" option of "auto/eauto/firstorder" + is interpreted as using the collection of its constructors. Tactic Language @@ -45,6 +49,8 @@ Vernacular commands - New support for local binders in the syntax of Record/Structure fields. - Most commands referring to constant (e.g. Print or About) now support referring to the constant by a notation string. +- Added "Reserved Infix" as a specific shortcut of the corresponding + "Reserved Notation". Tools diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index abc294e8b..6dbdaedd4 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3115,10 +3115,16 @@ hints of the database named {\tt core}. Uses all existing hint databases, minus the special database {\tt v62}. See Section~\ref{Hints-databases} -\item \texttt{auto using $lemma_1, \ldots, lemma_n$} +\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$} - Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be combined - with the \texttt{with \ident} option). + Uses \nterm{lemma}$_1$, \ldots, \nterm{lemma}$_n$ in addition to + hints (can be combined with the \texttt{with \ident} option). If + $lemma_i$ is an inductive type, it is the collection of its + constructors which is added as hints. + +\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$ with \ident$_1$ \dots\ \ident$_n$} + + This combines the effects of the {\tt using} and {\tt with} options. \item {\tt trivial}\tacindex{trivial} @@ -3300,11 +3306,17 @@ instead may reason about any first-order class inductive definition. Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search environment. - \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ } + \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ } \tacindex{firstorder using} - Adds lemmas in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$ - to the proof-search environment. + Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$ + to the proof-search environment. If {\qualid}$_i$ refers to an inductive + type, it is the collection of its constructors which is added as hints. + +\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} + + This combines the effects of the {\tt using} and {\tt with} options. + \end{Variants} Proof-search is bounded by a depth parameter which can be set by typing the diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 272737cc6..2a5dc64bc 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -833,6 +833,10 @@ GEXTEND Gram pil = LIST1 production_item; ":="; t = Tactic.tactic -> VernacTacticNotation (n,pil,t) + | IDENT "Reserved"; IDENT "Infix"; s = ne_string; + l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> + VernacSyntaxExtension (use_locality (),("_ '"^s^"' _",l)) + | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; s = ne_string; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 96c5bcae4..8302da5c1 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -58,12 +58,7 @@ let default_solver=(Tacinterp.interp <:tactic<auto with *>>) let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") -type external_env= - Ids of global_reference list - | Bases of Auto.hint_db_name list - | Void - -let gen_ground_tac flag taco ext gl= +let gen_ground_tac flag taco ids bases gl= let backup= !qflag in try qflag:=flag; @@ -71,11 +66,9 @@ let gen_ground_tac flag taco ext gl= match taco with Some tac-> tac | None-> default_solver in - let startseq= - match ext with - Void -> (fun gl -> empty_seq !ground_depth) - | Ids l-> create_with_ref_list l !ground_depth - | Bases l-> create_with_auto_hints l !ground_depth in + let startseq gl= + let seq=empty_seq !ground_depth in + extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in let result=ground_tac solver startseq gl in qflag:=backup;result with e ->qflag:=backup;raise e @@ -96,18 +89,45 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) +open Genarg +open Ppconstr +open Printer +let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_coma pr_reference +let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_coma (pr_or_var (pr_located pr_global)) +let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_coma pr_global + +ARGUMENT EXTEND firstorder_using + TYPED AS reference_list + PRINTED BY pr_firstorder_using_typed + RAW_TYPED AS reference_list + RAW_PRINTED BY pr_firstorder_using_raw + GLOB_TYPED AS reference_list + GLOB_PRINTED BY pr_firstorder_using_glob +| [ "using" reference(a) ] -> [ [a] ] +| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] +| [ "using" reference(a) reference(b) reference_list(l) ] -> [ + Flags.if_verbose + Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); + a::b::l + ] +| [ ] -> [ [] ] +END + TACTIC EXTEND firstorder - [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ] + [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) l [] ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ] + [ gen_ground_tac true (Option.map eval_tactic t) [] l ] +| [ "firstorder" tactic_opt(t) firstorder_using(l) + "with" ne_preident_list(l') ] -> + [ gen_ground_tac true (Option.map eval_tactic t) l l' ] | [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) Void ] + [ gen_ground_tac true (Option.map eval_tactic t) [] [] ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (Option.map eval_tactic t) Void ] + [ gen_ground_tac false (Option.map eval_tactic t) [] [] ] END @@ -119,7 +139,7 @@ let default_declarative_automation gls = (Some (tclTHEN default_solver (Cctac.congruence_tac !congruence_depth []))) - Void) gls + [] []) gls diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index fd5972fb7..98b178bde 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -253,17 +253,26 @@ let empty_seq depth= history=History.empty; depth=depth} -let create_with_ref_list l depth gl= +let expand_constructor_hints = + list_map_append (function + | IndRef ind -> + list_tabulate (fun i -> ConstructRef (ind,i+1)) + (Inductiveops.nconstructors ind) + | gr -> + [gr]) + +let extend_with_ref_list l seq gl= + let l = expand_constructor_hints l in let f gr seq= let c=constr_of_global gr in let typ=(pf_type_of gl c) in add_formula Hyp gr typ seq gl in - List.fold_right f l (empty_seq depth) + List.fold_right f l seq open Auto -let create_with_auto_hints l depth gl= - let seqref=ref (empty_seq depth) in +let extend_with_auto_hints l seq gl= + let seqref=ref seq in let f p_a_t = match p_a_t.code with Res_pf (c,_) | Give_exact c diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 51db9de16..206de27ed 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -57,10 +57,10 @@ val take_formula : t -> Formula.t * t val empty_seq : int -> t -val create_with_ref_list : global_reference list -> - int -> Proof_type.goal sigma -> t +val extend_with_ref_list : global_reference list -> + t -> Proof_type.goal sigma -> t -val create_with_auto_hints : Auto.hint_db_name list -> - int -> Proof_type.goal sigma -> t +val extend_with_auto_hints : Auto.hint_db_name list -> + t -> Proof_type.goal sigma -> t val print_cmap: global_reference list CM.t -> unit diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3150ed63b..727fd6f85 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -71,7 +71,6 @@ let substnl_ind_type l n = map_inductive_type (substnl l n) let mkAppliedInd (IndType ((ind,params), realargs)) = applist (mkInd ind,params@realargs) - (* Does not consider imbricated or mutually recursive types *) let mis_is_recursive_subset listind rarg = let rec one_is_rec rvec = @@ -125,6 +124,10 @@ let get_full_arity_sign env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_arity_ctxt +let nconstructors ind = + let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in + Array.length mip.mind_consnames + (* Length of arity (w/o local defs) *) let inductive_nargs env ind = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cc1bb7f41..cea769955 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -58,6 +58,8 @@ val mis_nf_constructor_type : val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array +val nconstructors : inductive -> int + (* Return the lengths of parameters signature and real arguments signature *) val inductive_nargs : env -> inductive -> int * int diff --git a/tactics/auto.ml b/tactics/auto.ml index 394626f24..547ad2a77 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -14,6 +14,7 @@ open Names open Nameops open Term open Termops +open Inductiveops open Sign open Environ open Inductive @@ -547,10 +548,9 @@ let interp_hints h = HintsTransparencyEntry (List.map fr lhints, b) | HintsConstructors lqid -> let constr_hints_of_ind qid = - let isp = global_inductive qid in - let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in - list_tabulate (fun i -> None, true, mkConstruct (isp,i+1)) - (Array.length consnames) in + let ind = global_inductive qid in + list_tabulate (fun i -> None, true, mkConstruct (ind,i+1)) + (nconstructors ind) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in @@ -727,10 +727,21 @@ let unify_resolve_gen = function | None -> unify_resolve_nodelta | Some flags -> unify_resolve flags +(* Util *) + +let expand_constructor_hints lems = + list_map_append (fun lem -> + match kind_of_term lem with + | Ind ind -> + list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind) + | _ -> + [lem]) lems + (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) let add_hint_lemmas eapply lems hint_db gl = + let lems = expand_constructor_hints lems in let hintlist' = list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in Hint_db.add_list hintlist' hint_db @@ -926,7 +937,7 @@ let extend_local_db 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 *) + with the obtained not-further-decomposable hypotheses *) let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl = if p = 0 then |