|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open Names
open Namegen
open CErrors
open Util
open Constrexpr
open Genarg
open Geninterp
open Stdarg
open Notation_gram
open Tactypes
open Locus
open Decl_kinds
open Genredexpr
open Ppconstr
open Pputils
open Printer
open Genintern
open Tacexpr
open Tacarg
open Tactics
module Tag =
struct
let keyword = "tactic.keyword"
let primitive = "tactic.primitive"
let string = "tactic.string"
end
let tag t s = Pp.tag t 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_atomic_tactic_expr = do_not_tag
let pr_global x = Nametab.pr_global_env Id.Set.empty x
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
| TacNonTerm of ('a * Names.Id.t option) Loc.located
type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
type pp_tactic = {
pptac_level : int;
pptac_prods : grammar_terminals;
}
(* Tactic notations *)
let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
type 'a raw_extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
'a -> Pp.t
type 'a glob_extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
'a -> Pp.t
type 'a extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
'a -> Pp.t
type 'a raw_extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
tolerability -> 'a -> Pp.t
type 'a glob_extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
tolerability -> 'a -> Pp.t
type 'a extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
tolerability -> 'a -> Pp.t
let string_of_genarg_arg (ArgumentType arg) =
let rec aux : type a b c. (a, b, c) genarg_type -> string = function
| ListArg t -> aux t ^ "_list"
| OptArg t -> aux t ^ "_opt"
| PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *)
| ExtraArg s -> ArgT.repr s in
aux arg
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
let has_type (Val.Dyn (tag, _)) t = match Val.eq tag t with
| None -> false
| Some _ -> true
let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t ->
match Val.eq tag t with
| None -> assert false
| Some Refl -> x
let rec pr_value lev v : Pp.t =
if has_type v Val.typ_list then
pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
else if has_type v Val.typ_opt then
pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt)
else if has_type v Val.typ_pair then
let (v1, v2) = unbox v Val.typ_pair in
str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
else
let Val.Dyn (tag, x) = v in
let name = Val.repr tag in
let default = str "<" ++ str name ++ str ">" in
match ArgT.name name with
| None -> default
| Some (ArgT.Any arg) ->
let wit = ExtraArg arg in
match val_tag (Topwit wit) with
| Val.Base t ->
begin match Val.eq t tag with
| None -> default
| Some Refl ->
let open Genprint in
match generic_top_print (in_gen (Topwit wit) x) with
| TopPrinterBasic pr -> pr ()
| TopPrinterNeedsContext pr ->
let env = Global.env() in
pr env (Evd.from_env env)
| TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
let env = Global.env() in
printer env (Evd.from_env env) default_ensure_surrounded
end
| _ -> default
let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c
let pr_red_expr env sigma pr c = Ppred.pr_red_expr_env env sigma pr keyword c
let pr_may_eval env sigma test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->
hov 0
(keyword "eval" ++ brk (1,1) ++
pr_red_expr env sigma (prc,prlc,pr2,pr3) r ++ spc () ++
keyword "in" ++ spc() ++ prc env sigma c)
| ConstrContext ({CAst.v=id},c) ->
hov 0
(keyword "context" ++ spc () ++ pr_id id ++ spc () ++
str "[ " ++ prlc env sigma c ++ str " ]")
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
h 0 (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c
let pr_may_eval env sigma a =
pr_may_eval env sigma (fun _ -> false) a
let pr_arg pr x = spc () ++ pr x
let pr_and_short_name pr (c,_) = pr c
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_clear_flag clear_flag pp x =
match clear_flag with
| Some false -> surround (pp x)
| Some true -> str ">" ++ pp x
| None -> pp x
let pr_with_bindings prc prlc (c,bl) =
prc c ++ Miscprint.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 tacarg_using_rule_token pr_gen = function
| [] -> []
| TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l
| TacNonTerm (_, ((symb, arg), _)) :: l ->
pr_gen symb arg :: tacarg_using_rule_token pr_gen l
let pr_tacarg_using_rule pr_gen l =
let l = match l with
| TacTerm s :: l ->
(* 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
| _ -> tacarg_using_rule_token pr_gen l
in
pr_sequence (fun x -> x) l
let pr_extend_gen pr_gen _ { mltac_name = s; mltac_index = i } l =
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
in
str "<" ++ name ++ str ">" ++ args
let rec pr_user_symbol = function
| Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list"
| Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list"
| Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list"
| Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list"
| Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt"
| Extend.Uentry tag ->
let ArgT.Any tag = tag in
ArgT.repr tag
| Extend.Uentryl (_, lvl) -> "tactic" ^ string_of_int lvl
let pr_alias_key key =
try
let prods = (KNmap.find key !prnotation_tab).pptac_prods in
let pr = function
| TacTerm s -> primitive s
| TacNonTerm (_, (symb, _)) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
in
pr_sequence pr prods
with Not_found ->
(* FIXME: This key, moreover printed with a low-level printer,
has no meaning user-side *)
KerName.print key
let pr_alias_gen pr_gen lev key l =
try
let pp = KNmap.find key !prnotation_tab in
let rec pack prods args = match prods, args with
| [], [] -> []
| TacTerm s :: prods, args -> TacTerm s :: pack prods args
| TacNonTerm (_, (_, None)) :: prods, args -> pack prods args
| TacNonTerm (loc, (symb, (Some _ as ido))) :: prods, arg :: args ->
TacNonTerm (loc, ((symb, arg), ido)) :: pack prods args
| _ -> raise Not_found
in
let prods = pack pp.pptac_prods l in
let p = pr_tacarg_using_rule pr_gen prods in
if pp.pptac_level > lev then surround p else p
with Not_found ->
let pr _ = str "_" in
KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg))
let is_genarg tag wit =
let ArgT.Any tag = tag in
argument_type_eq (ArgumentType (ExtraArg tag)) wit
let get_list : type l. l generic_argument -> l generic_argument list option =
function (GenArg (wit, arg)) -> match wit with
| Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg)
| Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg)
| _ -> None
let get_opt : type l. l generic_argument -> l generic_argument option option =
function (GenArg (wit, arg)) -> match wit with
| Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg)
| Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
| _ -> None
let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t =
fun prtac symb arg -> match symb with
| Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
| Extend.Ulist1 s | Extend.Ulist0 s ->
begin match get_list arg with
| None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
| Some l -> pr_sequence (pr_any_arg prtac s) l
end
| Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
begin match get_list arg with
| None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
| Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
end
| Extend.Uopt s ->
begin match get_opt arg with
| None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
| Some l -> pr_opt (pr_any_arg prtac s) l
end
| Extend.Uentry _ | Extend.Uentryl _ ->
str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
let pr_targ prtac symb arg = match symb with
| Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
prtac (1, Any) arg
| Extend.Uentryl (_, l) -> prtac (l, Any) arg
| _ ->
match arg with
| TacGeneric arg ->
let pr l arg = prtac l (TacGeneric arg) in
pr_any_arg pr symb arg
| _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
let pr_raw_extend_rec prtac =
pr_extend_gen (pr_farg prtac)
let pr_glob_extend_rec prtac =
pr_extend_gen (pr_farg prtac)
let pr_raw_alias prtac lev key args =
pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args
let pr_glob_alias prtac lev key args =
pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args
(**********************************************************************)
(* The tactic printer *)
let strip_prod_binders_expr n ty =
let rec strip_ty acc n ty =
match ty.CAst.v with
Constrexpr.CProdN(bll,a) ->
let bll = List.map (function
| CLocalAssum (nal,_,t) -> nal,t
| _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in
let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in
if nb >= n then (List.rev (bll@acc)), a
else strip_ty (bll@acc) (n-nb) a
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_ltac_or_var pr = function
| ArgArg x -> pr x
| ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id)
let pr_ltac_constant kn =
if !Flags.in_debugger then KerName.print kn
else try
pr_qualid (Tacenv.shortest_qualid_of_tactic kn)
with Not_found -> (* local tactic not accessible anymore *)
str "<" ++ KerName.print 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_as_disjunctive_ipat prc ipatl =
keyword "as" ++ spc () ++
pr_or_var (fun {CAst.loc;v=p} -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
let pr_eqn_ipat {CAst.v=ipat} = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
let pr_with_induction_names prc = function
| None, None -> mt ()
| Some eqpat, None -> hov 1 (pr_eqn_ipat eqpat)
| None, Some ipat -> hov 1 (pr_as_disjunctive_ipat prc ipat)
| Some eqpat, Some ipat ->
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 (CAst.make 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 {CAst.v=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
| Some tac -> keyword "by" ++ spc () ++ prt tac
| None -> mt()
let pr_hyp_location pr_id = function
| occs, InHyp -> pr_with_occurrences pr_id occs
| occs, InHypTypeOnly ->
pr_with_occurrences (fun id ->
str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
) occs
| occs, InHypValueOnly ->
pr_with_occurrences (fun id ->
str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
) occs
let pr_in pp = 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 (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
let pr_in_clause pr_id = function
| { onhyps=None; concl_occs=NoOccurrences } ->
(str "* |-")
| { onhyps=None; concl_occs=occs } ->
(pr_with_occurrences (fun () -> str "*") (occs,()))
| { onhyps=Some l; concl_occs=NoOccurrences } ->
prlist_with_sep (fun () -> str ", ") (pr_hyp_location pr_id) l
| { onhyps=Some l; concl_occs=occs } ->
let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
(prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
(* Some true = default is concl; Some false = default is all; None = no default *)
let pr_clauses has_default pr_id = function
| { onhyps=Some []; concl_occs=occs }
when (match has_default with Some true -> true | _ -> false) ->
pr_with_occurrences mt (occs,())
| { onhyps=None; concl_occs=AllOccurrences }
when (match has_default 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",")
(fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs)
let pr_orient b = if b then mt () else str "<- "
let pr_multi = let open Equality in function
| Precisely 1 -> mt ()
| Precisely n -> int n ++ str "!"
| UpTo n -> int n ++ str "?"
| RepeatStar -> str "?"
| RepeatPlus -> str "!"
let pr_core_destruction_arg prc prlc = function
| ElimOnConstr c -> pr_with_bindings prc prlc c
| ElimOnIdent {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id)
| ElimOnAnonHyp n -> int n
let pr_destruction_arg prc prlc (clear_flag,h) =
pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
let pr_inversion_kind = let open Inv in function
| SimpleInversion -> primitive "simple inversion"
| FullInversion -> primitive "inversion"
| FullInversionClear -> primitive "inversion_clear"
let pr_range_selector (i, j) =
if Int.equal i j then int i
else int i ++ str "-" ++ int j
let pr_goal_selector toplevel = let open Goal_select in function
| SelectAlreadyFocused -> str "!:"
| SelectNth i -> int i ++ str ":"
| SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
| SelectId id -> str "[" ++ Id.print id ++ str "]:"
| SelectAll -> assert toplevel; str "all:"
let pr_goal_selector ~toplevel s =
(if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s
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 (None,a) ->
keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
| Subterm (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 n = spc () ++ Name.print n
let pr_let_clause k pr_gen pr_arg (na,(bl,t)) =
let pr = function
| TacGeneric arg ->
let name = string_of_genarg_arg (genarg_tag arg) in
if name = "unit" || name = "int" then
(* Hard-wired parsing rules *)
pr_gen arg
else
str name ++ str ":" ++ surround (pr_gen arg)
| _ -> pr_arg (TacArg (CAst.make t)) in
hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
str " :=" ++ brk (1,1) ++ pr t)
let pr_let_clauses recflag pr_gen pr = function
| hd::tl ->
hv 0
(pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++
prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen 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 -> keyword "with" ++ str" *"
| Some [] -> mt ()
| Some l -> hov 2 (keyword "with" ++ prlist (fun s -> spc () ++ str s) l)
let pr_auto_using prc = function
| [] -> mt ()
| l -> hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
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 -> Pp.t;
pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t;
pr_pattern : Environ.env -> Evd.evar_map -> 'pat -> Pp.t;
pr_lpattern : Environ.env -> Evd.evar_map -> 'pat -> Pp.t;
pr_constant : 'cst -> Pp.t;
pr_reference : 'ref -> Pp.t;
pr_name : 'nam -> Pp.t;
pr_generic : Environ.env -> Evd.evar_map -> 'lev generic_argument -> Pp.t;
pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t;
pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t;
}
constraint 'a = <
term :'trm;
dterm :'dtrm;
pattern :'pat;
constant :'cst;
reference :'ref;
name :'nam;
tacexpr :'tacexpr;
level :'lev
>
let pr_atom env sigma pr strip_prod_binders tag_atom =
let pr_with_bindings = pr_with_bindings (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in
let pr_with_bindings_arg_full = pr_with_bindings_arg in
let pr_with_bindings_arg = pr_with_bindings_arg (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in
let pr_red_expr = pr_red_expr env sigma (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
let _pr_constrarg c = spc () ++ pr.pr_constr env sigma c in
let pr_lconstrarg c = spc () ++ pr.pr_lconstr env sigma 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 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 env sigma 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
_, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll
| bef, {CAst.loc;v=Anonymous} :: aft ->
let id = next_ident_away (Id.of_string"y") avoid in
id, ((bef@(CAst.make ?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 { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln)
ln nal)
Id.Set.empty bll in
let idarg,bll = set_nth_name names n bll in
let annot =
if Int.equal (Id.Set.cardinal names) 1 then
mt ()
else
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 (false,[]) -> primitive "intros"
| TacIntroPattern (true,[]) -> primitive "eintros"
| 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 (ev,(_::_ as p)) ->
hov 1 (primitive (if ev then "eintros" else "intros") ++
(match p with
| [{CAst.v=IntroForthcoming false}] -> mt ()
| _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern @@ pr.pr_dconstr env sigma) p))
| 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_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) 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)
| 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)
| TacMutualCofix (id,l) ->
hov 1 (
primitive "cofix" ++ spc () ++ pr_id id ++ spc()
++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
)
| TacAssert (ev,b,Some tac,ipat,c) ->
hov 1 (
primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++
pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
)
| TacAssert (ev,_,None,ipat,c) ->
hov 1 (
primitive (if ev then "epose proof" else "pose proof")
++ pr_assertion (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c
)
| TacGeneralize l ->
hov 1 (
primitive "generalize" ++ spc ()
++ prlist_with_sep pr_comma (fun (cl,na) ->
pr_with_occurrences (pr.pr_constr env sigma) cl ++ pr_as_name na)
l
)
| TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c)
| TacLetTac (ev,na,c,cl,b,e) ->
hov 1 (
primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
(if b then pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c
else pr_pose_as_style (pr.pr_constr env sigma) na c) ++
pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
pr_non_empty_arg (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 (h,ids,cl) ->
pr_destruction_arg (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) h ++
pr_non_empty_arg (pr_with_induction_names (pr.pr_dconstr env sigma)) ids ++
pr_opt (pr_clauses None pr.pr_name) cl) l ++
pr_opt pr_eliminator el
)
(* Conversion *)
| TacReduce (r,h) ->
hov 1 (
pr_red_expr r
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
| TacChange (check,op,c,h) ->
let name = if check then "change_no_check" else "change" in
hov 1 (
primitive name ++ brk (1,1)
++ (
match op with
None ->
mt ()
| Some p ->
pr.pr_pattern env sigma p ++ spc ()
++ keyword "with" ++ spc ()
) ++ pr.pr_dconstr env sigma c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
(* Equality and inversion *)
| TacRewrite (ev,l,cl,tac) ->
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 env sigma) (pr.pr_dconstr env sigma) c)
l
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
)
| TacInversion (DepInversion (k,c,ids),hyp) ->
hov 1 (
primitive "dependent " ++ pr_inversion_kind k ++ spc ()
++ pr_quantified_hypothesis hyp
++ pr_with_inversion_names (pr.pr_dconstr env sigma) ids
++ pr_with_constr (pr.pr_constr env sigma) c
)
| TacInversion (NonDepInversion (k,cl,ids),hyp) ->
hov 1 (
pr_inversion_kind k ++ spc ()
++ pr_quantified_hypothesis hyp
++ pr_non_empty_arg (pr_with_inversion_names @@ pr.pr_dconstr env sigma) ids
++ pr_non_empty_arg (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 env sigma c
++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
)
)
in
pr_atom1
let make_pr_tac env sigma pr strip_prod_binders tag_atom tag =
let extract_binders = function
| Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
| body -> ([],body) 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.pr_generic env sigma) (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 env sigma) 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 env sigma) 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
| TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom { CAst.loc; v=t } ->
pr_with_comments ?loc (hov 1 (pr_atom env sigma pr strip_prod_binders tag_atom t)), ltatom
| TacArg { CAst.v=Tacexp e } ->
pr_tac inherited e, latom
| TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } ->
keyword "constr:" ++ pr.pr_constr env sigma c, latom
| TacArg { CAst.v=ConstrMayEval c } ->
pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
| TacArg { CAst.v=TacFreshId l } ->
primitive "fresh" ++ pr_fresh_ids l, latom
| TacArg { CAst.v=TacGeneric arg } ->
pr.pr_generic env sigma arg, latom
| TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
pr.pr_reference f, latom
| TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
pr_with_comments ?loc (hov 1 (
pr.pr_reference f ++ spc ()
++ prlist_with_sep spc pr_tacarg l)),
lcall
| TacArg { CAst.v=a } ->
pr_tacarg a, latom
| TacML { CAst.loc; v=(s,l) } ->
pr_with_comments ?loc (pr.pr_extend 1 s l), lcall
| TacAlias { CAst.loc; v=(kn,l) } ->
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
| Reference r ->
pr.pr_reference r
| ConstrMayEval c ->
pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
| TacFreshId l ->
keyword "fresh" ++ pr_fresh_ids l
| TacPretype c ->
keyword "type_term" ++ pr.pr_constr env sigma c
| TacNumgoals ->
keyword "numgoals"
| (TacCall _|Tacexp _ | TacGeneric _) as a ->
hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (CAst.make 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 DAst.get ty with
Glob_term.GProd(na,Explicit,a,b) ->
strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
| _ -> user_err Pp.(str "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 env sigma n (t:raw_tactic_expr) =
let pr = {
pr_tactic = pr_raw_tactic_level env sigma;
pr_constr = 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_qualid;
pr_reference = pr_qualid;
pr_name = pr_lident;
pr_generic = Pputils.pr_raw_generic;
pr_extend = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma;
pr_alias = pr_raw_alias @@ pr_raw_tactic_level env sigma;
} in
make_pr_tac env sigma
pr raw_printers
tag_raw_atomic_tactic_expr tag_raw_tactic_expr
n t
let pr_raw_tactic env sigma = pr_raw_tactic_level env sigma ltop
let pr_and_constr_expr pr (c,_) = pr c
let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c
let 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 = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
pr_lpattern = (fun env sigma -> 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 = Pputils.pr_glb_generic;
pr_extend = pr_glob_extend_rec prtac;
pr_alias = pr_glob_alias prtac;
} in
make_pr_tac env (Evd.from_env env)
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 ty = EConstr.Unsafe.to_constr ty in
let rec strip_ty acc n ty =
if n=0 then (List.rev acc, EConstr.of_constr ty) else
match Constr.kind ty with
| Constr.Prod(na,a,b) ->
strip_ty (([CAst.make na.Context.binder_name],EConstr.of_constr a)::acc) (n-1) b
| _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_atomic_tactic_level env sigma t =
let prtac (t:atomic_tactic_expr) =
let pr = {
pr_tactic = (fun _ _ -> str "");
pr_constr = pr_econstr_env;
pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
pr_lconstr = pr_leconstr_env;
pr_pattern = pr_constr_pattern_env;
pr_lpattern = pr_lconstr_pattern_env;
pr_constant = pr_evaluable_reference_env env;
pr_reference = pr_located pr_ltac_constant;
pr_name = pr_id;
(* Those are not used by the atomic printer *)
pr_generic = (fun _ -> assert false);
pr_extend = (fun _ _ _ -> assert false);
pr_alias = (fun _ _ _ -> assert false);
}
in
pr_atom env sigma pr strip_prod_binders_constr tag_atomic_tactic_expr t
in
prtac t
let pr_raw_generic = Pputils.pr_raw_generic
let pr_glb_generic = Pputils.pr_glb_generic
let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma
let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env)
let pr_alias pr lev key args =
pr_alias_gen (fun _ arg -> pr arg) lev key args
let pr_extend pr lev ml args =
pr_extend_gen pr lev ml args
let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c
let declare_extra_genarg_pprule wit
(f : 'a raw_extra_genarg_printer)
(g : 'b glob_extra_genarg_printer)
(h : 'c extra_genarg_printer) =
begin match wit with
| ExtraArg _ -> ()
| _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let f x =
Genprint.PrinterBasic (fun env sigma ->
f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
let g x =
Genprint.PrinterBasic (fun env sigma ->
g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
(fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
(fun env sigma -> pr_glob_tactic_level env) x)
in
let h x =
Genprint.TopPrinterNeedsContext (fun env sigma ->
h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "") x)
in
Genprint.register_print0 wit f g h
let declare_extra_genarg_pprule_with_level wit
(f : 'a raw_extra_genarg_printer_with_level)
(g : 'b glob_extra_genarg_printer_with_level)
(h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded =
begin match wit with
| ExtraArg s -> ()
| _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let open Genprint in
let f x =
PrinterNeedsLevel {
default_already_surrounded = default_surrounded;
default_ensure_surrounded = default_non_surrounded;
printer = (fun env sigma n ->
f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in
let g x =
PrinterNeedsLevel {
default_already_surrounded = default_surrounded;
default_ensure_surrounded = default_non_surrounded;
printer = (fun env sigma n ->
g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
(fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
(fun env sigma -> pr_glob_tactic_level env) n x) }
in
let h x =
TopPrinterNeedsContextAndLevel {
default_already_surrounded = default_surrounded;
default_ensure_surrounded = default_non_surrounded;
printer = (fun env sigma n ->
h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "") n x) }
in
Genprint.register_print0 wit f g h
let declare_extra_vernac_genarg_pprule wit f =
let f x = Genprint.PrinterBasic (fun env sigma -> f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
Genprint.register_vernac_print0 wit f
(** Registering *)
let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma ->
let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in
Miscprint.pr_intro_pattern print_constr p)
let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma ->
pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env,
pr_evaluable_reference_env env, pr_constr_pattern_env) r)
let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
let sigma, bl = bl env sigma in
Miscprint.pr_bindings
(pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
let sigma, bl = bl env sigma in
pr_with_bindings
(pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl)
let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma ->
let sigma, c = match c with
| clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c)
| clear_flag,ElimOnAnonHyp n as x -> sigma, x
| clear_flag,ElimOnIdent id as x -> sigma, x in
pr_destruction_arg
(pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
let make_constr_printer f c =
Genprint.TopPrinterNeedsContextAndLevel {
Genprint.default_already_surrounded = Ppconstr.ltop;
Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
Genprint.printer = (fun env sigma n -> f env sigma n c)}
let lift f a = Genprint.PrinterBasic (fun env sigma -> f a)
let lift_env f a = Genprint.PrinterBasic (fun env sigma -> f env sigma a)
let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a)
let register_basic_print0 wit f g h =
Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
let pr_glob_constr_pptac env sigma c =
pr_glob_constr_env env c
let pr_lglob_constr_pptac env sigma c =
pr_lglob_constr_env env c
let pr_raw_intro_pattern =
lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)
let pr_glob_intro_pattern =
lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c))
let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
let open Genprint in
register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
register_basic_print0 wit_ref
pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
register_basic_print0 wit_var pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env;
Genprint.register_print0
wit_clause_dft_concl
(lift (pr_clauses (Some true) pr_lident))
(lift (pr_clauses (Some true) pr_lident))
(fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c))
;
Genprint.register_print0
wit_constr
(lift_env Ppconstr.pr_lconstr_expr)
(lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
wit_uconstr
(lift_env Ppconstr.pr_constr_expr)
(lift_env (fun env sigma (c,_) -> pr_glob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_closed_glob_n_env)
;
Genprint.register_print0
wit_open_constr
(lift_env Ppconstr.pr_constr_expr)
(lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
wit_red_expr
(lift_env (fun env sigma -> pr_red_expr env sigma (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
(lift_env (fun env sigma -> pr_red_expr env sigma
((fun env sigma -> pr_and_constr_expr @@ pr_glob_constr_pptac env sigma),
(fun env sigma -> pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma),
pr_or_var (pr_and_short_name pr_evaluable_reference),
(fun env sigma -> pr_pat_and_constr_expr @@ pr_glob_constr_pptac env sigma))))
pr_red_expr_env
;
register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
register_print0 wit_bindings
(lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_constr_expr env sigma)
(pr_lconstr_expr env sigma)))
(lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_bindings_env
;
register_print0 wit_constr_with_bindings
(lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
(lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
(pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_with_bindings_env
;
register_print0 wit_open_constr_with_bindings
(lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
(lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
(pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_with_bindings_env
;
register_print0 Tacarg.wit_destruction_arg
(lift_env (fun env sigma -> pr_destruction_arg (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
(lift_env (fun env sigma -> pr_destruction_arg (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
(pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_destruction_arg_env
;
register_basic_print0 Stdarg.wit_int int int int;
register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool;
register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit;
register_basic_print0 Stdarg.wit_pre_ident str str str;
register_basic_print0 Stdarg.wit_string qstring qstring qstring
let () =
let printer env sigma _ _ prtac = prtac env sigma in
declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
ltop (0,E)
let () =
let pr_unit _env _sigma _ _ _ _ () = str "()" in
let printer env sigma _ _ prtac = prtac env sigma in
declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit
ltop (0,E)
¤ Dauer der Verarbeitung: 0.87 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
