diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 447 |
1 files changed, 192 insertions, 255 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b8ad996aa3..982c18ec61 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,11 +26,11 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } (* ML Extensions *) @@ -61,14 +61,14 @@ type 'a glob_extra_genarg_printer = type 'a extra_genarg_printer = (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds let genarg_pprule = ref String.Map.empty let declare_extra_genarg_pprule wit f g h = - let s = match unquote (topwit wit) with - | ExtraArgType s -> s + let s = match wit with + | ExtraArg s -> ArgT.repr s | _ -> error "Can declare a pretty-printing rule only for extra argument types." in @@ -106,6 +106,8 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) + let pr_value _ _ = str "(* FIXME *)" + let pr_with_occurrences pr (occs,c) = match occs with | AllOccurrences -> @@ -265,149 +267,89 @@ module Make let with_evars ev s = if ev then "e" ^ s else s - let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) - | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) - | 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 - pr_sequence map (raw l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match raw o with + let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = in_gen (rawwit wit1) p in - let q = in_gen (rawwit wit2) q in - pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q] + | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_raw_print x - - - let rec pr_glb_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) - | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) - | ConstrMayEvalArgType -> - 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 - pr_sequence map (glb l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match glb o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]) + | ExtraArg s -> + try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x) + with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x) + + + let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = glb o in - let p = in_gen (glbwit wit1) p in - let q = in_gen (glbwit wit2) q in - pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q] - in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_glb_print x - - let rec pr_top_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) - | VarArgType -> pr_id (out_gen (topwit wit_var) x) - | 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 - pr_sequence map (top l) + | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match top o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) + with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) + + let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) + | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = top o in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q] - in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_top_print x + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (topwit wit1) p in + let q = in_gen (topwit wit2) q in + let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) + with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) let rec tacarg_using_rule_token pr_gen = function - | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | None :: l, a :: al -> + | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) + | Egramml.GramNonTerminal _ :: l, a :: al -> let r = tacarg_using_rule_token pr_gen (l,al) in pr_gen a :: r | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" + type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg + + let filter_arg = function + | Egramml.GramTerminal _ -> None + | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t) + let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Some s :: l, al) -> + | (Egramml.GramTerminal s :: l, al) -> (** First terminal token should be considered as the name of the tactic, so we tag it differently than the other terminal tokens. *) primitive s :: (tacarg_using_rule_token pr_gen (l, al)) @@ -415,13 +357,14 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = + let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = try 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 + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ @@ -433,28 +376,35 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_gen pr_gen lev key l = + let pr_alias_gen check pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab 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 + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - let pr_raw_extend prc prlc prtac prpat = - pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference) - let pr_glob_extend prc prlc prtac prpat = - pr_extend_gen (pr_glb_generic prc prlc prtac prpat) - let pr_extend prc prlc prtac prpat = - pr_extend_gen (pr_top_generic prc prlc prtac prpat) + let check_type t arg = match t, arg with + | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg) + | _ -> false + + let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false + + let pr_raw_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) + let pr_glob_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) + let pr_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) + pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen (pr_glb_generic prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) let pr_alias prc prlc prtac prpat = - pr_alias_gen (pr_top_generic prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) (**********************************************************************) (* The tactic printer *) @@ -586,8 +536,7 @@ module Make let pr_in_hyp_as prc pr_id = function | None -> mt () - | Some (clear,id,ipat) -> - pr_in (spc () ++ pr_clear_flag clear pr_id id) ++ pr_as_ipat prc ipat + | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat let pr_clauses default_is_concl pr_id = function | { onhyps=Some []; concl_occs=occs } @@ -722,11 +671,6 @@ module Make | l -> spc () ++ hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) - let string_of_debug = function - | Off -> "" - | Debug -> "debug " - | Info -> "info_" - let pr_then () = str ";" let ltop = (5,E) @@ -752,7 +696,6 @@ module Make type 'a printer = { pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; pr_constr : 'trm -> std_ppcmds; - pr_uconstr : 'utrm -> std_ppcmds; pr_lconstr : 'trm -> std_ppcmds; pr_dconstr : 'dtrm -> std_ppcmds; pr_pattern : 'pat -> std_ppcmds; @@ -761,13 +704,12 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> 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; + pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds; + pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds; } constraint 'a = < term :'trm; - utrm :'utrm; dterm :'dtrm; pattern :'pat; constant :'cst; @@ -781,7 +723,6 @@ module Make (* some shortcuts *) let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in let pr_with_bindings_arg_full = pr_with_bindings_arg in let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in @@ -849,9 +790,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial" - | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto" - | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -886,13 +824,10 @@ module Make ++ pr_opt pr_eliminator cbo) | TacCase (ev,cb) -> hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) - | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) - | TacCofix ido -> - hov 1 (primitive "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> hov 1 ( primitive "cofix" ++ spc () ++ pr_id id ++ spc() @@ -916,11 +851,6 @@ module Make pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) | TacLetTac (na,c,cl,b,e) -> @@ -959,43 +889,7 @@ module Make ++ pr_arg pr_quantified_hypothesis h2 ) - (* Automation tactics *) - | TacTrivial (_,[],Some []) as x -> - pr_atom0 x - | TacTrivial (d,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "trivial" - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - | TacAuto (_,None,[],Some []) as x -> - pr_atom0 x - | TacAuto (d,n,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "auto" - ++ pr_opt (pr_or_var int) n - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - (* Context management *) - | TacClear (true,[]) as t -> - pr_atom0 t - | TacClear (keep,l) -> - hov 1 ( - primitive "clear" ++ spc () - ++ (if keep then str "- " else mt ()) - ++ prlist_with_sep spc pr.pr_name l - ) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) - | TacMove (id1,id2) -> - hov 1 ( - primitive "move" - ++ brk (1,1) ++ pr.pr_name id1 - ++ Miscprint.pr_move_location pr.pr_name id2 - ) | TacRename l -> hov 1 ( primitive "rename" ++ brk (1,1) @@ -1006,13 +900,6 @@ module Make l ) - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( @@ -1032,10 +919,6 @@ module Make ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h ) - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> hov 1 ( @@ -1257,26 +1140,17 @@ module Make | TacML (loc,s,l) -> pr_with_comments loc (pr.pr_extend 1 s l), lcall | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom + pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm 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) -> - pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s) | Reference r -> pr.pr_reference r | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c - | UConstr c -> - keyword "uconstr:" ++ pr.pr_uconstr c | TacFreshId l -> keyword "fresh" ++ pr_fresh_ids l | TacPretype c -> @@ -1304,7 +1178,6 @@ module Make let pr = { pr_tactic = pr_raw_tactic_level; pr_constr = pr_constr_expr; - pr_uconstr = pr_constr_expr; pr_dconstr = pr_constr_expr; pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; @@ -1313,7 +1186,7 @@ module Make pr_reference = pr_reference; pr_name = pr_lident; pr_generic = Genprint.generic_raw_print; - pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; } in make_pr_tac @@ -1327,7 +1200,7 @@ module Make let pr_pat_and_constr_expr pr ((c,_),_) = pr c - let rec pr_glob_tactic_level env n t = + let pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in @@ -1335,7 +1208,6 @@ module Make let pr = { pr_tactic = prtac; pr_constr = pr_and_constr_expr (pr_glob_constr_env env); - pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); @@ -1344,7 +1216,7 @@ module Make pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Genprint.generic_glb_print; - pr_extend = pr_glob_extend + pr_extend = pr_glob_extend_rec (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); pr_alias = pr_glob_alias @@ -1377,21 +1249,20 @@ module Make let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; - 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; - pr_extend = pr_extend + pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + pr_value pr_constr_pattern; pr_alias = pr_alias (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - (pr_glob_tactic_level env) pr_constr_pattern; + pr_value pr_constr_pattern; } in make_pr_tac @@ -1401,6 +1272,39 @@ module Make in prtac n t + let pr_raw_generic env = pr_raw_generic_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference + + let pr_glb_generic env = pr_glb_generic_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let pr_top_generic env = pr_top_generic_rec + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + pr_value pr_constr_pattern + + let pr_raw_extend env = pr_raw_extend_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr + + let pr_glob_extend env = pr_glob_extend_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let check_val_type t arg = + let AnyArg t = t in +(* let t = Genarg.val_tag (Obj.magic t) in *) +(* let Val.Dyn (t', _) = arg in *) +(* match Genarg.Val.eq t t' with *) +(* | None -> false *) +(* | Some _ -> true *) + true (** FIXME *) + + let pr_alias pr lev key args = + pr_alias_gen check_val_type pr lev key args + + let pr_extend pr lev ml args = + pr_extend_gen check_val_type pr lev ml args + let pr_tactic env = pr_tactic_level env ltop end @@ -1437,17 +1341,26 @@ 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 let pr_string s = str "\"" ++ str s ++ str "\"" in + Genprint.register_print0 Constrarg.wit_int_or_var + (pr_or_var int) (pr_or_var int) int; Genprint.register_print0 Constrarg.wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; + Genprint.register_print0 Constrarg.wit_ident + pr_id pr_id pr_id; + Genprint.register_print0 Constrarg.wit_var + (pr_located pr_id) (pr_located pr_id) pr_id; Genprint.register_print0 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) @@ -1457,11 +1370,41 @@ let () = Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 + Constrarg.wit_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + Genprint.register_print0 + Constrarg.wit_open_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + 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 it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); + Genprint.register_print0 Constrarg.wit_constr_may_eval + (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) + (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) + (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr)) + pr_constr; + 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 it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed 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; @@ -1472,16 +1415,10 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer -let _ = Hook.set Tactic_debug.tactic_printer - (fun x -> pr_glob_tactic (Global.env()) x) - -let _ = Hook.set Tactic_debug.match_pattern_printer - (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) - -let _ = Hook.set Tactic_debug.match_rule_printer - (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) - (fun (_,p) -> pr_constr_pattern p) rl) +let () = + let pr_unit _ _ _ () = str "()" in + let printer _ _ prtac = prtac (0, E) in + declare_extra_genarg_pprule wit_ltac printer printer pr_unit module Richpp = struct |