(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds type 'a glob_extra_genarg_printer = (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds type 'a extra_genarg_printer = (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> 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 | _ -> error "Can declare a pretty-printing rule only for extra argument types." in let f prc prlc prtac x = f prc prlc prtac (out_gen (rawwit wit) x) in let g prc prlc prtac x = g prc prlc prtac (out_gen (glbwit wit) x) in let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule module Make (Ppconstr : Ppconstrsig.Pp) (Taggers : sig val tag_keyword : std_ppcmds -> std_ppcmds val tag_primitive : std_ppcmds -> std_ppcmds val tag_string : std_ppcmds -> std_ppcmds val tag_glob_tactic_expr : glob_tactic_expr -> std_ppcmds -> std_ppcmds val tag_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds val tag_raw_tactic_expr : raw_tactic_expr -> std_ppcmds -> std_ppcmds val tag_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds val tag_tactic_expr : tactic_expr -> std_ppcmds -> std_ppcmds val tag_atomic_tactic_expr : atomic_tactic_expr -> std_ppcmds -> std_ppcmds end) = struct open Taggers let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) let pr_with_occurrences pr (occs,c) = match occs with | AllOccurrences -> pr c | NoOccurrences -> failwith "pr_with_occurrences: no occurrences" | OnlyOccurrences nl -> hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ hov 0 (prlist_with_sep spc (pr_or_var int) nl)) | AllOccurrencesBut nl -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ hov 0 (prlist_with_sep spc (pr_or_var int) nl)) exception ComplexRedFlag let pr_short_red_flag pr r = if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag else if List.is_empty r.rConst then if r.rDelta then mt () else raise ComplexRedFlag else (if r.rDelta then str "-" else mt ()) ++ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") let pr_red_flag pr r = try pr_short_red_flag pr r with complexRedFlags -> (if r.rBeta then pr_arg str "beta" else mt ()) ++ (if r.rIota then pr_arg str "iota" else mt ()) ++ (if r.rZeta then pr_arg str "zeta" else mt ()) ++ (if List.is_empty r.rConst then if r.rDelta then pr_arg str "delta" else mt () else pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) let pr_union pr1 pr2 = function | Inl a -> pr1 a | Inr b -> pr2 b let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function | Red false -> keyword "red" | Hnf -> keyword "hnf" | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o | Cbv f -> if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then keyword "compute" else hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) | Lazy f -> hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) | Cbn f -> hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) | Unfold l -> hov 1 (keyword "unfold" ++ spc() ++ prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l) | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) | Pattern l -> hov 1 (keyword "pattern" ++ pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l) | Red true -> error "Shouldn't be accessible from user." | ExtraRedExpr s -> str s | CbvVm o -> keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o | CbvNative o -> keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> hov 0 (keyword "eval" ++ brk (1,1) ++ pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ keyword "in" ++ spc() ++ prc c) | ConstrContext ((_,id),c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ str "[" ++ prlc c ++ str "]") | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc c) | ConstrTerm c when test c -> h 0 (str "(" ++ prc c ++ str ")") | ConstrTerm c -> prc c let pr_may_eval a = pr_may_eval (fun _ -> false) a let pr_arg pr x = spc () ++ pr x let pr_or_var pr = function | ArgArg x -> pr x | ArgVar (_,s) -> pr_id s let pr_and_short_name pr (c,_) = pr c let pr_or_by_notation f = function | AN v -> f v | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_located pr (loc,x) = pr x let pr_evaluable_reference = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> brk (1,1) ++ keyword "with" ++ brk (1,1) ++ hv 0 (prlist_with_sep spc prc l) | ExplicitBindings l -> brk (1,1) ++ keyword "with" ++ brk (1,1) ++ hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l) | NoBindings -> mt () let pr_bindings_no_with prc prlc = function | ImplicitBindings l -> brk (0,1) ++ prlist_with_sep spc prc l | ExplicitBindings l -> brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | NoBindings -> mt () let pr_clear_flag clear_flag pp x = (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt()) ++ pp x let pr_with_bindings prc prlc (c,bl) = prc c ++ pr_bindings prc prlc bl let pr_with_bindings_arg prc prlc (clear_flag,c) = pr_clear_flag clear_flag (pr_with_bindings prc prlc) c let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (keyword "with" ++ spc () ++ prc c) let pr_message_token prid = function | MsgString s -> tag_string (qs s) | MsgInt n -> int n | MsgIdent id -> prid id let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var (fun s -> tag_string (qs s)) s) 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 | 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] 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 | 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) in hov 0 (list_unpack { list_unpacker } x) | OptArgType _ -> let opt_unpacker wit o = match top o with | None -> mt () | Some x -> pr_top_generic 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 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 -> let r = tacarg_using_rule_token pr_gen (l,al) in pr_gen a :: r | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" let pr_tacarg_using_rule pr_gen l = let l = match l with | (Some 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)) | _ -> tacarg_using_rule_token pr_gen l in pr_sequence (fun x -> x) l let pr_extend_gen pr_gen lev s l = try let tags = List.map genarg_tag l in let (lev',pl) = Hashtbl.find prtac_tab (s,tags) 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 args = match l with | [] -> mt () | _ -> spc() ++ pr_sequence pr_gen l in str "<" ++ name ++ str ">" ++ args let pr_alias_gen 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 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 pr_raw_alias prc prlc prtac prpat = pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) let pr_glob_alias prc prlc prtac prpat = pr_alias_gen (pr_glb_generic prc prlc prtac prpat) let pr_alias prc prlc prtac prpat = pr_alias_gen (pr_top_generic prc prlc prtac prpat) (**********************************************************************) (* The tactic printer *) let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = match ty with Constrexpr.CProdN(_,bll,a) -> let nb = List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in let bll = List.map (fun (x, _, y) -> x, y) bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty let pr_ltac_or_var pr = function | ArgArg x -> pr x | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) let pr_ltac_constant kn = if !Flags.in_debugger then pr_kn kn else try pr_qualid (Nametab.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) str "<" ++ pr_kn kn ++ str ">" let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) let pr_esubst prc l = let pr_qhyp = function (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" | (_,NamedHyp id,c) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" in prlist_with_sep spc pr_qhyp l let pr_bindings_gen for_ex prc prlc = function | ImplicitBindings l -> spc () ++ hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ prlist_with_sep spc prc l) | ExplicitBindings l -> spc () ++ hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ pr_esubst prlc l) | NoBindings -> mt () let pr_bindings prc prlc = pr_bindings_gen false prc prlc let pr_with_bindings prc prlc (c,bl) = hov 1 (prc c ++ pr_bindings prc prlc bl) let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat let pr_with_induction_names prc = function | None, None -> mt () | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat) | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat) | Some eqpat, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat prc ipat ++ spc () ++ pr_eqn_ipat eqpat) let pr_as_intro_pattern prc ipat = spc () ++ hov 1 (keyword "as" ++ spc () ++ Miscprint.pr_intro_pattern prc ipat) let pr_with_inversion_names prc = function | None -> mt () | Some ipat -> pr_as_disjunctive_ipat prc ipat let pr_as_ipat prc = function | None -> mt () | Some ipat -> pr_as_intro_pattern prc ipat let pr_as_name = function | Anonymous -> mt () | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.ghost,id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na let pr_pose prc prlc na c = match na with | Anonymous -> spc() ++ prc c | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c) let pr_assertion prc prdc _prlc ipat c = match ipat with (* Use this "optimisation" or use only the general case ? | IntroIdentifier id -> spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c) *) | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat let pr_assumption prc prdc prlc ipat c = match ipat with (* Use this "optimisation" or use only the general case ?*) (* it seems that this "optimisation" is somehow more natural *) | Some (_,IntroNaming (IntroIdentifier id)) -> spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c) | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat let pr_by_tactic prt = function | TacId [] -> mt () | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs | occs, InHypTypeOnly -> spc () ++ pr_with_occurrences (fun id -> str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")" ) occs | occs, InHypValueOnly -> spc () ++ pr_with_occurrences (fun id -> str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")" ) occs let pr_in pp = spc () ++ hov 0 (keyword "in" ++ pp) let pr_simple_hyp_clause pr_id = function | [] -> mt () | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) 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 let pr_clauses default_is_concl pr_id = function | { onhyps=Some []; concl_occs=occs } when (match default_is_concl with Some true -> true | _ -> false) -> pr_with_occurrences mt (occs,()) | { onhyps=None; concl_occs=AllOccurrences } when (match default_is_concl with Some false -> true | _ -> false) -> mt () | { onhyps=None; concl_occs=NoOccurrences } -> pr_in (str " * |-") | { onhyps=None; concl_occs=occs } -> pr_in (pr_with_occurrences (fun () -> str " *") (occs,())) | { onhyps=Some l; concl_occs=occs } -> let pr_occs = match occs with | NoOccurrences -> mt () | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,()) in pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs) let pr_orient b = if b then mt () else str "<- " let pr_multi = function | Precisely 1 -> mt () | Precisely n -> int n ++ str "!" | UpTo n -> int n ++ str "?" | RepeatStar -> str "?" | RepeatPlus -> str "!" let pr_induction_arg prc prlc = function | ElimOnConstr c -> pr_with_bindings prc prlc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) | ElimOnAnonHyp n -> int n let pr_induction_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" let pr_lazy = function | General -> keyword "multi" | Select -> keyword "lazy" | Once -> mt () let pr_match_pattern pr_pat = function | Term a -> pr_pat a | Subterm (b,None,a) -> (** ppedrot: we don't make difference between [appcontext] and [context] anymore, and the interpretation is governed by a flag instead. *) keyword "context" ++ str" [" ++ pr_pat a ++ str "]" | Subterm (b,Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" let pr_match_hyps pr_pat = function | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp | Def (nal,mv,mp) -> pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv ++ str ":" ++ pr_match_pattern pr_pat mp let pr_match_rule m pr pr_pat = function | Pat ([],mp,t) when m -> pr_match_pattern pr_pat mp ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t (* | Pat (rl,mp,t) -> hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++ (if rl <> [] then spc () else mt ()) ++ hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t)) *) | Pat (rl,mp,t) -> hov 0 ( hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++ (if not (List.is_empty rl) then spc () else mt ()) ++ hov 0 ( str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t let pr_funvar = function | None -> spc () ++ str "_" | Some id -> spc () ++ pr_id id let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.ghost,t))) let pr_let_clauses recflag pr = function | hd::tl -> hv 0 (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding") let pr_seq_body pr tl = hv 0 (str "[ " ++ prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ str " ]") let pr_dispatch pr tl = hv 0 (str "[>" ++ prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ str " ]") let pr_opt_tactic pr = function | TacId [] -> mt () | t -> pr t let pr_tac_extend_gen pr tf tm tl = prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++ pr_opt_tactic pr tm ++ str ".." ++ prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl let pr_then_gen pr tf tm tl = hv 0 (str "[ " ++ pr_tac_extend_gen pr tf tm tl ++ str " ]") let pr_tac_extend pr tf tm tl = hv 0 (str "[>" ++ pr_tac_extend_gen pr tf tm tl ++ str " ]") let pr_hintbases = function | None -> spc () ++ keyword "with" ++ str" *" | Some [] -> mt () | Some l -> spc () ++ hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l) let pr_auto_using prc = function | [] -> mt () | 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) let lseq = 4 let ltactical = 3 let lorelse = 2 let llet = 5 let lfun = 5 let lcomplete = 1 let labstract = 3 let lmatch = 1 let latom = 0 let lcall = 1 let leval = 1 let ltatom = 1 let linfo = 5 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels *) 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; pr_lpattern : 'pat -> std_ppcmds; pr_constant : 'cst -> std_ppcmds; 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_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; } constraint 'a = < term :'trm; utrm :'utrm; dterm :'dtrm; pattern :'pat; constant :'cst; reference :'ref; name :'nam; tacexpr :'tacexpr; level :'lev > let make_pr_tac pr strip_prod_binders tag_atom tag = (* 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 let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in let pr_constrarg c = spc () ++ pr.pr_constr c in let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in let pr_intarg n = spc () ++ int n in (* Some printing combinators *) let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in let extract_binders = function | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) | body -> ([],body) in let pr_binder_fix (nal,t) = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = let rec set_nth_name avoid n = function (nal,ty)::bll -> if n <= List.length nal then match List.chop (n-1) nal with _, (_,Name id) :: _ -> id, (nal,ty)::bll | bef, (loc,Anonymous) :: aft -> let id = next_ident_away (Id.of_string"y") avoid in id, ((bef@(loc,Name id)::aft, ty)::bll) | _ -> assert false else let (id,bll') = set_nth_name avoid (n-List.length nal) bll in (id,(nal,ty)::bll') | [] -> assert false in let (bll,ty) = strip_prod_binders n c in let names = List.fold_left (fun ln (nal,_) -> List.fold_left (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) ln nal) [] bll in let idarg,bll = set_nth_name names n bll in let annot = match names with | [_] -> mt () | _ -> spc() ++ str"{" ++ keyword "struct" ++ spc () ++ pr_id idarg ++ str"}" in hov 1 (str"(" ++ pr_id id ++ prlist pr_binder_fix bll ++ annot ++ str" :" ++ pr_lconstrarg ty ++ str")") in (* spc() ++ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg c) *) let pr_cofix_tac (id,c) = hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in (* Printing tactics as arguments *) 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 ")" ) (* Main tactic printer *) and pr_atom1 a = tag_atom a (match a with (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t | TacIntroPattern (_::_ as p) -> hov 1 (primitive "intros" ++ spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) | TacIntroMove (None,MoveLast) as t -> pr_atom0 t | TacIntroMove (Some id,MoveLast) -> primitive "intro" ++ spc () ++ pr_id id | TacIntroMove (ido,hto) -> hov 1 (primitive "intro" ++ pr_opt pr_id ido ++ Miscprint.pr_move_location pr.pr_name hto) | TacExact c -> hov 1 (primitive "exact" ++ pr_constrarg c) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ primitive (with_evars ev "apply") ++ spc () ++ prlist_with_sep pr_comma pr_with_bindings_arg cb ++ pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp ) | TacElim (ev,cb,cbo) -> hov 1 ( primitive (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++ 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() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l ) | TacAssert (b,Some tac,ipat,c) -> hov 1 ( primitive (if b then "assert" else "enough") ++ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ pr_by_tactic (pr.pr_tactic ltop) tac ) | TacAssert (_,None,ipat,c) -> hov 1 ( primitive "pose proof" ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ) | TacGeneralize l -> hov 1 ( primitive "generalize" ++ spc () ++ prlist_with_sep pr_comma (fun (cl,na) -> 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) -> hov 1 ( (if b then primitive "set" else primitive "remember") ++ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c else pr_pose_as_style pr.pr_constr na c) ++ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ pr_clauses (Some b) pr.pr_name cl) (* | TacInstantiate (n,c,ConclLocation ()) -> hov 1 (str "instantiate" ++ spc() ++ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ pr_lconstrarg c ++ str ")" )) | TacInstantiate (n,c,HypLocation (id,hloc)) -> hov 1 (str "instantiate" ++ spc() ++ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ pr_lconstrarg c ++ str ")" ) ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None))) *) (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> hov 1 ( primitive (with_evars ev (if isrec then "induction" else "destruct")) ++ spc () ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) -> pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++ pr_with_induction_names pr.pr_dconstr ids ++ pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) | TacDoubleInduction (h1,h2) -> hov 1 ( primitive "double induction" ++ pr_arg pr_quantified_hypothesis h1 ++ 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) ++ prlist_with_sep (fun () -> str "," ++ brk (1,1)) (fun (i1,i2) -> pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2) 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 ( pr_red_expr r ++ pr_clauses (Some true) pr.pr_name h ) | TacChange (op,c,h) -> hov 1 ( primitive "change" ++ brk (1,1) ++ ( match op with None -> mt () | Some p -> pr.pr_pattern p ++ spc () ++ keyword "with" ++ spc () ) ++ 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 ( primitive (with_evars ev "rewrite") ++ spc () ++ prlist_with_sep (fun () -> str ","++spc()) (fun (b,m,c) -> pr_orient b ++ pr_multi m ++ pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) l ++ pr_clauses (Some true) pr.pr_name cl ++ ( match by with | Some by -> pr_by_tactic (pr.pr_tactic ltop) by | None -> mt() ) ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( primitive "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ pr_with_inversion_names pr.pr_dconstr ids ++ pr_with_constr pr.pr_constr c ) | TacInversion (NonDepInversion (k,cl,ids),hyp) -> hov 1 ( pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ pr_with_inversion_names pr.pr_dconstr ids ++ pr_simple_hyp_clause pr.pr_name cl ) | TacInversion (InversionUsing (c,cl),hyp) -> hov 1 ( primitive "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ spc () ++ keyword "using" ++ spc () ++ pr.pr_constr c ++ pr_simple_hyp_clause pr.pr_name cl ) ) in let rec pr_tac inherited tac = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with | TacAbstract (t,None) -> keyword "abstract " ++ pr_tac (labstract,L) t, labstract | TacAbstract (t,Some s) -> hov 0 ( keyword "abstract" ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++ keyword "using" ++ spc () ++ pr_id s), labstract | TacLetIn (recflag,llc,u) -> let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( pr_let_clauses recflag (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( pr_lazy lz ++ keyword "match" ++ spc () ++ pr_tac ltop t ++ spc () ++ keyword "with" ++ prlist (fun r -> fnl () ++ str "| " ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r ) lrul ++ fnl() ++ keyword "end"), lmatch | TacMatchGoal (lz,lr,lrul) -> hov 0 ( pr_lazy lz ++ keyword (if lr then "match reverse goal with" else "match goal with") ++ prlist (fun r -> fnl () ++ str "| " ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r ) lrul ++ fnl() ++ keyword "end"), lmatch | TacFun (lvar,body) -> hov 2 ( keyword "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () ++ pr_tac (lfun,E) body), lfun | TacThens (t,tl) -> hov 1 ( pr_tac (lseq,E) t ++ pr_then () ++ spc () ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl), lseq | TacThen (t1,t2) -> hov 1 ( pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++ pr_tac (lseq,L) t2), lseq | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl, lseq | TacExtendTac (tf,t,tr) -> pr_tac_extend (pr_tac ltop) tf t tr , lseq | TacThens3parts (t1,tf,t2,tl) -> hov 1 ( pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++ pr_then_gen (pr_tac ltop) tf t2 tl), lseq | TacTry t -> hov 1 ( keyword "try" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacDo (n,t) -> hov 1 ( str "do" ++ spc () ++ pr_or_var int n ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacTimeout (n,t) -> hov 1 ( keyword "timeout " ++ pr_or_var int n ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacTime (s,t) -> hov 1 ( keyword "time" ++ pr_opt str s ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacRepeat t -> hov 1 ( keyword "repeat" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacProgress t -> hov 1 ( keyword "progress" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacShowHyps t -> hov 1 ( keyword "infoH" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacInfo t -> hov 1 ( keyword "info" ++ spc () ++ pr_tac (ltactical,E) t), linfo | TacOr (t1,t2) -> hov 1 ( pr_tac (lorelse,L) t1 ++ spc () ++ str "+" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), lorelse | TacOnce t -> hov 1 ( keyword "once" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacExactlyOnce t -> hov 1 ( keyword "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacIfThenCatch (t,tt,te) -> hov 1 ( str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), ltactical | TacOrelse (t1,t2) -> hov 1 ( pr_tac (lorelse,L) t1 ++ spc () ++ str "||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), lorelse | TacFail (g,n,l) -> let arg = match n with | ArgArg 0 -> mt () | _ -> pr_arg (pr_or_var int) n in let name = match g with | TacGlobal -> keyword "gfail" | TacLocal -> keyword "fail" in hov 1 ( name ++ arg ++ prlist (pr_arg (pr_message_token pr.pr_name)) l), latom | TacFirst tl -> keyword "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacSolve tl -> keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom | TacArg(_,Tacexp e) -> pr.pr_tactic (latom,E) e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval | TacArg(_,TacFreshId l) -> primitive "fresh" ++ pr_fresh_ids l, latom | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom | TacArg(_,TacCall(loc,f,[])) -> pr.pr_reference f, latom | TacArg(_,TacCall(loc,f,l)) -> pr_with_comments loc (hov 1 ( pr.pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), lcall | TacArg (_,a) -> pr_tacarg a, latom | 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 ) 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 -> keyword "type_term" ++ pr.pr_constr c | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> keyword "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) in pr_tac let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else match ty with Glob_term.GProd(loc,na,Explicit,a,b) -> strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty let raw_printers = (strip_prod_binders_expr) let rec pr_raw_tactic_level n (t:raw_tactic_expr) = 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; pr_lpattern = pr_lconstr_pattern_expr; pr_constant = pr_or_by_notation pr_reference; 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_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; } in make_pr_tac pr raw_printers tag_raw_atomic_tactic_expr tag_raw_tactic_expr n t let pr_raw_tactic = pr_raw_tactic_level ltop let pr_and_constr_expr pr (c,_) = pr c let pr_pat_and_constr_expr pr ((c,_),_) = pr c let rec pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in let rec prtac n (t:glob_tactic_expr) = 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); pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); 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_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 (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)); } in make_pr_tac pr glob_printers tag_glob_atomic_tactic_expr tag_glob_tactic_expr n t in prtac n t let pr_glob_tactic env = pr_glob_tactic_level env ltop let strip_prod_binders_constr n ty = let rec strip_ty acc n ty = if n=0 then (List.rev acc, ty) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> strip_ty (([Loc.ghost,na],a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty let pr_tactic_level env n t = let typed_printers = (strip_prod_binders_constr) in let prtac n (t:tactic_expr) = 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_reference = pr_located pr_ltac_constant; pr_name = pr_id; pr_generic = Genprint.generic_top_print; pr_extend = pr_extend (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (pr_glob_tactic_level env) 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; } in make_pr_tac pr typed_printers tag_atomic_tactic_expr tag_tactic_expr n t in prtac n t let pr_tactic env = pr_tactic_level env ltop end module Tag = struct let keyword = let style = Terminal.make ~bold:true () in Ppstyle.make ~style ["tactic"; "keyword"] let primitive = let style = Terminal.make ~fg_color:`LIGHT_GREEN () in Ppstyle.make ~style ["tactic"; "primitive"] let string = let style = Terminal.make ~fg_color:`LIGHT_RED () in Ppstyle.make ~style ["tactic"; "string"] end include Make (Ppconstr) (struct let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s let do_not_tag _ x = x let tag_keyword = tag Tag.keyword let tag_primitive = tag Tag.primitive let tag_string = tag Tag.string let tag_glob_tactic_expr = do_not_tag let tag_glob_atomic_tactic_expr = do_not_tag let tag_raw_tactic_expr = do_not_tag let tag_raw_atomic_tactic_expr = do_not_tag let tag_tactic_expr = do_not_tag let tag_atomic_tactic_expr = do_not_tag end) (** Registering *) 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_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; 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)))); Genprint.register_print0 Constrarg.wit_clause_dft_concl (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; 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; Genprint.register_print0 Stdarg.wit_pre_ident str str str; Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string 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) module Richpp = struct include Make (Ppconstr.Richpp) (struct open Ppannotation let do_not_tag _ x = x let tag e s = Pp.tag (Pp.Tag.inj e tag) s let tag_keyword = tag AKeyword let tag_primitive = tag AKeyword let tag_string = do_not_tag () let tag_glob_tactic_expr e = tag (AGlobTacticExpr e) let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a) let tag_raw_tactic_expr e = tag (ARawTacticExpr e) let tag_raw_atomic_tactic_expr a = tag (ARawAtomicTacticExpr a) let tag_tactic_expr e = tag (ATacticExpr e) let tag_atomic_tactic_expr a = tag (AAtomicTacticExpr a) end) end