diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 73 | ||||
| -rw-r--r-- | printing/pptactic.mli | 2 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 6 | ||||
| -rw-r--r-- | printing/printmod.ml | 1 |
4 files changed, 37 insertions, 45 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index bc559460e0..dfb8837eca 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -34,13 +34,14 @@ type pp_tactic = { } (* ML Extensions *) -let prtac_tab = Hashtbl.create 17 +let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t = + Hashtbl.create 17 (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods + Hashtbl.add prtac_tab key pt let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -274,15 +275,7 @@ module Make | ConstrMayEvalArgType -> pr_may_eval prc prlc (pr_or_by_notation prref) prpat (out_gen (rawwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) - (out_gen (rawwit wit_red_expr) x) | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -319,17 +312,7 @@ module Make pr_may_eval prc prlc (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat (out_gen (glbwit wit_constr_may_eval) x) - | QuantHypArgType -> - pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr - (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) - (out_gen (glbwit wit_red_expr) x) | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -362,16 +345,7 @@ module Make | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) - (out_gen (topwit wit_red_expr) x) | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in - pr_with_bindings prc prlc (c,b) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -414,14 +388,18 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev s l = + let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = try - let tags = List.map genarg_tag l in - let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in + let pp_rules = Hashtbl.find prtac_tab s in + let pp = pp_rules.(i) in + let (lev', pl) = pp.pptac_prods in let p = pr_tacarg_using_rule pr_gen (pl,l) in if lev' > lev then surround p else p with Not_found -> - let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let name = + str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ + str "@" ++ int i + in let args = match l with | [] -> mt () | _ -> spc() ++ pr_sequence pr_gen l @@ -755,7 +733,7 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds; + pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds; pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; } @@ -1258,9 +1236,6 @@ module Make else str"(" ++ strm ++ str")" and pr_tacarg = function - | TacDynamic (loc,t) -> - pr_with_comments loc - (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>") | MetaIdArg (loc,true,s) -> pr_with_comments loc (str "$" ++ str s) | MetaIdArg (loc,false,s) -> @@ -1374,9 +1349,9 @@ module Make pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; - pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); - pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); - pr_constant = pr_and_short_name (pr_evaluable_reference_env env); + pr_pattern = pr_constr_pattern_env env Evd.empty; + pr_lpattern = pr_lconstr_pattern_env env Evd.empty; + pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; pr_generic = Genprint.generic_top_print; @@ -1431,6 +1406,9 @@ end) (** Registering *) +let run_delayed c = + Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1441,7 +1419,7 @@ let () = Constrarg.wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty)))); + (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c)))); Genprint.register_print0 Constrarg.wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1456,6 +1434,19 @@ let () = (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + Genprint.register_print0 Constrarg.wit_red_expr + (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern)); + Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + Genprint.register_print0 Constrarg.wit_bindings + (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it); + Genprint.register_print0 Constrarg.wit_constr_with_bindings + (pr_with_bindings pr_constr_expr pr_lconstr_expr) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun { Evd.it = it } -> pr_with_bindings pr_constr pr_lconstr it); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; diff --git a/printing/pptactic.mli b/printing/pptactic.mli index fa91aefcf3..30b9483db7 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -48,7 +48,7 @@ type pp_tactic = { pptac_prods : int * grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 166a6675c1..1631bda377 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -59,19 +59,19 @@ module type Pp = sig (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> int -> - ml_tactic_name -> raw_generic_argument list -> std_ppcmds + ml_tactic_entry -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - ml_tactic_name -> glob_generic_argument list -> std_ppcmds + ml_tactic_entry -> glob_generic_argument list -> std_ppcmds val pr_extend : (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (constr_pattern -> std_ppcmds) -> int -> - ml_tactic_name -> typed_generic_argument list -> std_ppcmds + ml_tactic_entry -> typed_generic_argument list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds diff --git a/printing/printmod.ml b/printing/printmod.ml index 1d275c1aa6..d6f847cc71 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,6 +65,7 @@ let get_new_id locals id = (** Inductive declarations *) +open Context open Termops open Reduction |