From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- parsing/egrammar.ml | 9 +++++---- parsing/egrammar.mli | 5 +++-- parsing/g_constrnew.ml4 | 6 ++++-- parsing/g_ltacnew.ml4 | 20 +++++++++++++------- parsing/g_tactic.ml4 | 6 +++--- parsing/g_tacticnew.ml4 | 6 +++--- parsing/pcoq.ml4 | 5 +++-- parsing/pcoq.mli | 5 +++-- parsing/pptactic.ml | 10 +++++++--- parsing/pptactic.mli | 4 +++- parsing/prettyp.ml | 10 ++++++---- parsing/q_coqast.ml4 | 4 ++-- 12 files changed, 55 insertions(+), 35 deletions(-) (limited to 'parsing') diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 7a151c1a..09889d40 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml,v 1.48.2.3 2004/11/26 19:37:59 herbelin Exp $ *) +(* $Id: egrammar.ml,v 1.48.2.4 2005/12/23 22:16:46 herbelin Exp $ *) open Pp open Util @@ -30,12 +30,13 @@ type all_grammar_command = | TacticGrammar of (string * (string * grammar_production list) * (Names.dir_path * Tacexpr.raw_tactic_expr)) - list + list * (string * Genarg.argument_type list * + (string * Pptactic.grammar_terminals)) list let subst_all_grammar_command subst = function | Notation _ -> anomaly "Notation not in GRAMMAR summary" | Grammar gc -> Grammar (subst_grammar_command subst gc) - | TacticGrammar g -> TacticGrammar g (* TODO ... *) + | TacticGrammar (g,p) -> TacticGrammar (g,p) (* TODO ... *) let (grammar_state : all_grammar_command list ref) = ref [] @@ -419,7 +420,7 @@ let extend_grammar gram = (match gram with | Notation (_,a) -> extend_constr_notation a | Grammar g -> extend_grammar_rules g - | TacticGrammar l -> add_tactic_entries l); + | TacticGrammar (l,_) -> add_tactic_entries l); grammar_state := gram :: !grammar_state let reset_extend_grammars_v8 () = diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 0009b4b6..ade91453 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: egrammar.mli,v 1.14.2.5 2004/11/27 09:25:44 herbelin Exp $ i*) +(*i $Id: egrammar.mli,v 1.14.2.6 2005/12/23 22:16:46 herbelin Exp $ i*) (*i*) open Util @@ -28,7 +28,8 @@ type all_grammar_command = | TacticGrammar of (string * (string * grammar_production list) * (Names.dir_path * Tacexpr.raw_tactic_expr)) - list + list * (string * Genarg.argument_type list * + (string * Pptactic.grammar_terminals)) list val extend_grammar : all_grammar_command -> unit diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index adc26532..fe579e98 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constrnew.ml4,v 1.41.2.2 2004/11/17 12:48:35 herbelin Exp $ *) +(* $Id: g_constrnew.ml4,v 1.41.2.4 2005/09/21 14:47:33 herbelin Exp $ *) open Pcoq open Constr @@ -285,7 +285,9 @@ GEXTEND Gram [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] ; pattern: - [ "10" LEFTA + [ "200" RIGHTA [ ] + | "99" RIGHTA [ ] + | "10" LEFTA [ p = pattern ; lp = LIST1 (pattern LEVEL "0") -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 9c8d1675..7492ac8c 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltacnew.ml4,v 1.22.2.2 2004/07/16 19:30:38 herbelin Exp $ *) +(* $Id: g_ltacnew.ml4,v 1.22.2.3 2005/06/21 15:31:12 herbelin Exp $ *) open Pp open Util @@ -43,7 +43,7 @@ let tactic_expr = Gram.Entry.create "tactic:tactic_expr" if not !Options.v7 then GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_expr tactic_arg; + GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval; tactic_expr: [ "5" LEFTA @@ -108,14 +108,20 @@ GEXTEND Gram | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; may_eval_arg: + [ [ c = constr_eval -> ConstrMayEval c + | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ] + ; + constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrMayEval (ConstrEval (rtc,c)) + ConstrEval (rtc,c) | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrMayEval (ConstrContext (id,c)) + ConstrContext (id,c) | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrMayEval (ConstrTypeOf c) - | IDENT "fresh"; s = OPT STRING -> - TacFreshId s ] ] + ConstrTypeOf c ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> c + | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a1559572..fd64defc 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_tactic.ml4,v 1.83.2.4 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: g_tactic.ml4,v 1.83.2.5 2005/05/15 12:47:04 herbelin Exp $ *) open Pp open Ast @@ -306,14 +306,14 @@ GEXTEND Gram (* Automation tactic *) | IDENT "Trivial"; db = hintbases -> TacTrivial db - | IDENT "Auto"; n = OPT natural; db = hintbases -> TacAuto (n, db) + | IDENT "Auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db) | IDENT "AutoTDB"; n = OPT natural -> TacAutoTDB n | IDENT "CDHyp"; id = identref -> TacDestructHyp (true,id) | IDENT "DHyp"; id = identref -> TacDestructHyp (false,id) | IDENT "DConcl" -> TacDestructConcl | IDENT "SuperAuto"; l = autoargs -> TacSuperAuto l - | IDENT "Auto"; n = OPT natural; IDENT "Decomp"; p = OPT natural -> + | IDENT "Auto"; n = OPT int_or_var; IDENT "Decomp"; p = OPT natural -> TacDAuto (n, p) (* Context management *) diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 643be98d..5ffd2fd7 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_tacticnew.ml4,v 1.35.2.6 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: g_tacticnew.ml4,v 1.35.2.7 2005/05/15 12:47:05 herbelin Exp $ *) open Pp open Ast @@ -340,7 +340,7 @@ GEXTEND Gram (* Automation tactic *) | IDENT "trivial"; db = hintbases -> TacTrivial db - | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db) + | IDENT "auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db) (* Obsolete since V8.0 | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n @@ -349,7 +349,7 @@ GEXTEND Gram | IDENT "dconcl" -> TacDestructConcl | IDENT "superauto"; l = autoargs -> TacSuperAuto l *) - | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural -> + | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural -> TacDAuto (n, p) (* Context management *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index b5ab2387..a8922536 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.ml4,v 1.80.2.3 2005/01/15 14:56:53 herbelin Exp $ i*) +(*i $Id: pcoq.ml4,v 1.80.2.4 2005/06/21 15:31:12 herbelin Exp $ i*) open Pp open Util @@ -379,7 +379,8 @@ module Tactic = make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" let bindings = make_gen_entry utactic rawwit_bindings "bindings" - let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg" +(*v7*) let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg" +(*v8*) let constr_may_eval = make_gen_entry utactic rawwit_constr_may_eval "constr_may_eval" let quantified_hypothesis = make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis" let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 361137f4..15a2c2cc 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli,v 1.63.2.2 2005/01/15 14:56:53 herbelin Exp $ i*) +(*i $Id: pcoq.mli,v 1.63.2.3 2005/06/21 15:31:12 herbelin Exp $ i*) open Util open Names @@ -160,7 +160,8 @@ module Tactic : val castedopenconstr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e - val constrarg : (constr_expr,reference) may_eval Gram.Entry.e +(*v7*) val constrarg : (constr_expr,reference) may_eval Gram.Entry.e +(*v8*) val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1d7a9428..4103ea00 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml,v 1.54.2.3 2005/01/15 14:56:53 herbelin Exp $ *) +(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *) open Pp open Names @@ -42,6 +42,8 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) = Hashtbl.add prtac_tab_v7 (s,tags) prods; if for_v8 then Hashtbl.add prtac_tab (s,tags) prods +let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags) + type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -536,7 +538,8 @@ and pr_atom1 = function | TacTrivial (Some []) as x -> pr_atom0 x | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db) | TacAuto (None,Some []) as x -> pr_atom0 x - | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db) + | TacAuto (n,db) -> + hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db) | TacAutoTDB None as x -> pr_atom0 x | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n) | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id) @@ -546,7 +549,8 @@ and pr_atom1 = function hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2) | TacDAuto (n,p) -> - hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p) + hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ + pr_opt int p) (* Context management *) | TacClear l -> diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index b9cf7401..5c3035ba 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pptactic.mli,v 1.9.2.2 2005/01/21 17:19:37 herbelin Exp $ i*) +(*i $Id: pptactic.mli,v 1.9.2.3 2005/12/23 22:16:46 herbelin Exp $ i*) open Pp open Genarg @@ -46,6 +46,8 @@ type grammar_terminals = string option list val declare_extra_tactic_pprule : bool -> string -> argument_type list * (string * grammar_terminals) -> unit +val exists_extra_tactic_pprule : string -> argument_type list -> bool + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 169eff94..1505745c 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: prettyp.ml,v 1.50.2.1 2004/07/16 19:30:40 herbelin Exp $ *) +(* $Id: prettyp.ml,v 1.50.2.2 2005/11/21 09:16:28 herbelin Exp $ *) open Pp open Util @@ -180,8 +180,10 @@ let print_located_qualid ref = let (loc,qid) = qualid_of_reference ref in let module N = Nametab in let expand = function - | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref - | SyntacticDef kn -> Syntactic kn, N.shortest_qualid_of_syndef kn in + | TrueGlobal ref -> + Term ref, N.shortest_qualid_of_global Idset.empty ref + | SyntacticDef kn -> + Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in match List.map expand (N.extended_locate_all qid) with | [] -> let (dir,id) = repr_qualid qid in @@ -329,7 +331,7 @@ let print_constant_with_infos sp = let print_inductive sp = (print_mutual sp) let print_syntactic_def sep kn = - let qid = Nametab.shortest_qualid_of_syndef kn in + let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in let c = Syntax_def.search_syntactic_definition dummy_loc kn in (str (if !Options.v7 then "Syntactic Definition " else "Notation ") ++ pr_qualid qid ++ str sep ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a278e3d5..e8e1830a 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_coqast.ml4,v 1.47.2.5 2005/01/15 14:56:54 herbelin Exp $ *) +(* $Id: q_coqast.ml4,v 1.47.2.6 2005/05/15 12:47:05 herbelin Exp $ *) open Util open Names @@ -454,7 +454,7 @@ let rec mlexpr_of_atomic_tactic = function (* Automation tactics *) | Tacexpr.TacAuto (n,l) -> - let n = mlexpr_of_option mlexpr_of_int n in + let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in <:expr< Tacexpr.TacAuto $n$ $l$ >> (* -- cgit v1.2.3