diff options
| -rw-r--r-- | parsing/pptactic.ml | 42 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 8 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 40 |
3 files changed, 40 insertions, 50 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1e839fcc62..d24de56750 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -28,29 +28,16 @@ let pr_name = Ppconstr.pr_name let pr_opt = Ppconstr.pr_opt let pr_occurrences = Ppconstr.pr_occurrences +type grammar_terminals = string option list + (* Extensions *) let prtac_tab_v7 = Hashtbl.create 17 let prtac_tab = Hashtbl.create 17 -(* We need system F typing strength *) -type ('a,'b) gen_gram_prod_builder = - ('a,'b) generic_argument list -> - string * Egrammar.grammar_tactic_production list -let inst1 (f:('a,'b) gen_gram_prod_builder) = - (Obj.magic f : (constr_expr,raw_tactic_expr) gen_gram_prod_builder) -let inst2 (f:('a,'b) gen_gram_prod_builder) = - (Obj.magic f : (rawconstr * constr_expr option,glob_tactic_expr) gen_gram_prod_builder) -let inst3 (f:('a,'b) gen_gram_prod_builder) = - (Obj.magic f : (Term.constr,glob_tactic_expr) gen_gram_prod_builder) - -let declare_extra_tactic_pprule for_v8 s f = - let f = inst1 f in - let g = inst2 f in - let h = inst3 f in - Hashtbl.add prtac_tab_v7 s (f,g,h); - if for_v8 then Hashtbl.add prtac_tab s (f,g,h) - -let p = prtac_tab +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 + type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -357,20 +344,19 @@ let rec pr_generic prc prlc prtac x = with Not_found -> str " [no printer for " ++ str s ++ str "]" let rec pr_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> - spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> - pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) + | Some s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) + | None :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" -let pr_extend_gen proj prgen s l = +let pr_extend_gen prgen s l = let tab = if Options.do_translate() or not !Options.v7 then prtac_tab else prtac_tab_v7 in try - let (s,pl) = proj (Hashtbl.find tab s) l in + let tags = List.map genarg_tag l in + let (s,pl) = Hashtbl.find tab (s,tags) in str s ++ pr_tacarg_using_rule prgen (pl,l) with Not_found -> str s ++ prlist prgen l ++ str " (* Generic printer *)" @@ -666,11 +652,11 @@ and prtac x = pr6 x in (prtac,pr0,pr_match_rule false pr_pat pr_tac) let pr_raw_extend prc prlc prtac = - pr_extend_gen pi1 (pr_raw_generic prc prlc prtac pr_reference) + pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference) let pr_glob_extend prc prlc prtac = - pr_extend_gen pi2 (pr_glob_generic prc prlc prtac) + pr_extend_gen (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = - pr_extend_gen pi3 (pr_generic prc prlc prtac) + pr_extend_gen (pr_generic prc prlc prtac) let pr_and_constr_expr pr (c,_) = pr c diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 5d5f62f389..729947bb8e 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -40,13 +40,11 @@ val declare_extra_genarg_pprule : ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit -type ('a,'b) gen_gram_prod_builder = - ('a,'b) generic_argument list -> - string * Egrammar.grammar_tactic_production list +type grammar_terminals = string option list (* if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : - bool -> string -> ('a,'b) gen_gram_prod_builder -> unit +val declare_extra_tactic_pprule : bool -> string -> + argument_type list * (string * grammar_terminals) -> unit val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 218a9e0db3..7c6194871b 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -102,22 +102,31 @@ let mlexpr_of_grammar_production = function | TacNonTerm (loc,nt,g,sopt) -> <:expr< Egrammar.TacNonTerm $default_loc$ ($g$,$mlexpr_of_argtype loc nt$) $mlexpr_of_option mlexpr_of_string sopt$ >> +let mlexpr_terminals_of_grammar_production = function + | TacTerm s -> <:expr< Some $mlexpr_of_string s$ >> + | TacNonTerm (loc,nt,g,sopt) -> <:expr< None >> + let mlexpr_of_semi_clause = mlexpr_of_pair mlexpr_of_string (mlexpr_of_list mlexpr_of_grammar_production) let mlexpr_of_clause = mlexpr_of_list (fun (a,b,c) -> mlexpr_of_semi_clause (a,b)) +let rec make_tags loc = function + | [] -> <:expr< [] >> + | TacNonTerm(loc',t,_,Some p)::l -> + let l = make_tags loc l in + let loc = join_loc loc' loc in + let t = mlexpr_of_argtype loc' t in + <:expr< [ $t$ :: $l$ ] >> + | _::l -> make_tags loc l -let add_printing_clause (s,pt,e) l = - let p = make_patt pt in - let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, w, mlexpr_of_semi_clause (s,pt))::l +let make_one_printing_rule (s,pt,e) = + let loc = MLast.loc_of_expr e in + let prods = mlexpr_of_list mlexpr_terminals_of_grammar_production pt in + <:expr< ($make_tags loc pt$, ($str:s$, $prods$)) >> -let make_printing_rule l = - let default = - (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in - List.fold_right add_printing_clause l [default] +let make_printing_rule = mlexpr_of_list make_one_printing_rule let new_tac_ext (s,cl) = (String.lowercase s, List.map @@ -129,7 +138,7 @@ let new_tac_ext (s,cl) = cl) let declare_tactic_v7 loc s cl = - let pl = make_printing_rule cl in + let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in let hide_tac (_,p,e) = (* reste a definir les fonctions cachees avec des noms frais *) @@ -147,17 +156,16 @@ let declare_tactic_v7 loc s cl = declare open Pcoq; Egrammar.extend_tactic_grammar $se$ $gl$; - let pp = fun [ $list:pl$ ] in - Pptactic.declare_extra_tactic_pprule False $se$ pp; + List.iter (Pptactic.declare_extra_tactic_pprule False $se$) $pp$; end >> let declare_tactic loc s cl = let (s',cl') = new_tac_ext (s,cl) in - let pl' = make_printing_rule cl' in + let pp' = make_printing_rule cl' in let gl' = mlexpr_of_clause cl' in let se' = mlexpr_of_string s' in - let pl = make_printing_rule cl in + let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in let hide_tac (_,p,e) = (* reste a definir les fonctions cachees avec des noms frais *) @@ -181,10 +189,8 @@ let declare_tactic loc s cl = with e -> Pp.pp (Cerrors.explain_exn e); if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$ else Egrammar.extend_tactic_grammar $se'$ $gl'$; - let pp' = fun [ $list:pl'$ ] in - Pptactic.declare_extra_tactic_pprule True $se'$ pp'; - let pp = fun [ $list:pl$ ] in - Pptactic.declare_extra_tactic_pprule False $se'$ pp; + List.iter (Pptactic.declare_extra_tactic_pprule True $se'$) $pp'$; + List.iter (Pptactic.declare_extra_tactic_pprule False $se'$) $pp$; end >> |