diff options
| -rw-r--r-- | grammar/argextend.ml4 | 33 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 53 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 3 |
4 files changed, 53 insertions, 38 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 82bc09519..f26a66a12 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -64,6 +64,27 @@ let rec make_prod = function let make_rule loc (prods,act) = <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> +let is_ident x = function +| <:expr< $lid:s$ >> -> CString.equal s x +| _ -> false + +let make_extend loc s cl wit = match cl with +| [[ExtNonTerminal (_, Uentry e, id)], act] when is_ident id act -> + (** Special handling of identity arguments by not redeclaring an entry *) + <:str_item< + value $lid:s$ = + let () = Pcoq.register_grammar $wit$ $lid:e$ in + $lid:e$ + >> +| _ -> + let se = mlexpr_of_string s in + let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in + <:str_item< + value $lid:s$ = + let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + $lid:s$ >> + let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let rawtyp, rawpr, globtyp, globpr = match typ with | `Uniform typ -> @@ -129,8 +150,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$) = @@ -139,10 +158,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>; + make_extend loc s cl wit; <:str_item< do { - Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$; Egramcoq.create_ltac_quotation $se$ @@ -153,8 +170,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in - let rawwit = <:expr< Genarg.rawwit $wit$ >> in - let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in let pr_rules = match pr with | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in @@ -162,10 +177,8 @@ let declare_vernac_argument loc s pr cl = [ <:str_item< value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; - <:str_item< - value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>; + make_extend loc s cl wit; <:str_item< do { - Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule $wit$ $pr_rules$ (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8c85d0162..a18dfa509 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -85,7 +85,7 @@ let make_fun_clauses loc s l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (nt, g, id) -> - let base s = <:expr< Pcoq.genarg_grammar $mk_extraarg loc s$ >> in + let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ $mlexpr_of_prod_entry_key base g$ >> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 05fd9f9d8..b769a3cbc 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -229,23 +229,24 @@ let get_typed_entry e = let new_entry etyp u s = let utab = get_utable u in let uname = Entry.univ_name u in - let entry = Entry.create u s in + let _ = Entry.create u s in let ename = uname ^ ":" ^ s in let e = Gram.entry_create ename in - Hashtbl.add utab s (TypedEntry (etyp, e)); (entry, e) + Hashtbl.add utab s (TypedEntry (etyp, e)); e -let make_gen_entry u rawwit s = snd (new_entry rawwit u s) +let make_gen_entry u rawwit s = new_entry rawwit u s module GrammarObj = struct - type ('r, _, _) obj = 'r Entry.t + type ('r, _, _) obj = 'r Gram.entry let name = "grammar" let default _ = None end module Grammar = Register(GrammarObj) -let genarg_grammar wit = Grammar.obj wit +let register_grammar = Grammar.register0 +let genarg_grammar = Grammar.obj let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = let utab = get_utable u in @@ -253,9 +254,9 @@ let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a let u = Entry.univ_name u in failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists"); else - let (entry, e) = new_entry etyp u s in + let e = new_entry etyp u s in let Rawwit t = etyp in - let () = Grammar.register0 t entry in + let () = Grammar.register0 t e in e (* Initial grammar entries *) @@ -863,24 +864,24 @@ let () = let open Constrarg in (* Grammar.register0 wit_unit; *) (* Grammar.register0 wit_bool; *) - Grammar.register0 wit_int (name_of_entry Prim.integer); - Grammar.register0 wit_string (name_of_entry Prim.string); - Grammar.register0 wit_pre_ident (name_of_entry Prim.preident); - Grammar.register0 wit_int_or_var (name_of_entry Tactic.int_or_var); - Grammar.register0 wit_intro_pattern (name_of_entry Tactic.simple_intropattern); - Grammar.register0 wit_ident (name_of_entry Prim.ident); - Grammar.register0 wit_var (name_of_entry Prim.var); - Grammar.register0 wit_ref (name_of_entry Prim.reference); - Grammar.register0 wit_quant_hyp (name_of_entry Tactic.quantified_hypothesis); - Grammar.register0 wit_sort (name_of_entry Constr.sort); - Grammar.register0 wit_constr (name_of_entry Constr.constr); - Grammar.register0 wit_constr_may_eval (name_of_entry Tactic.constr_may_eval); - Grammar.register0 wit_uconstr (name_of_entry Tactic.uconstr); - Grammar.register0 wit_open_constr (name_of_entry Tactic.open_constr); - Grammar.register0 wit_constr_with_bindings (name_of_entry Tactic.constr_with_bindings); - Grammar.register0 wit_bindings (name_of_entry Tactic.bindings); + Grammar.register0 wit_int (Prim.integer); + Grammar.register0 wit_string (Prim.string); + Grammar.register0 wit_pre_ident (Prim.preident); + Grammar.register0 wit_int_or_var (Tactic.int_or_var); + Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern); + Grammar.register0 wit_ident (Prim.ident); + Grammar.register0 wit_var (Prim.var); + Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis); + Grammar.register0 wit_sort (Constr.sort); + Grammar.register0 wit_constr (Constr.constr); + Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval); + Grammar.register0 wit_uconstr (Tactic.uconstr); + Grammar.register0 wit_open_constr (Tactic.open_constr); + Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings); + Grammar.register0 wit_bindings (Tactic.bindings); (* Grammar.register0 wit_hyp_location_flag; *) - Grammar.register0 wit_red_expr (name_of_entry Tactic.red_expr); - Grammar.register0 wit_tactic (name_of_entry Tactic.tactic); - Grammar.register0 wit_clause_dft_concl (name_of_entry Tactic.clause_dft_concl); + Grammar.register0 wit_red_expr (Tactic.red_expr); + Grammar.register0 wit_tactic (Tactic.tactic); + Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index b1353ef8a..64f6f720c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -160,7 +160,8 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t +val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit +val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry val get_entry : gram_universe -> string -> typed_entry |