summaryrefslogtreecommitdiff
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /parsing/pptactic.ml
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'parsing/pptactic.ml')
-rw-r--r--parsing/pptactic.ml1171
1 files changed, 702 insertions, 469 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 4103ea00..e6c12f4f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -6,69 +6,64 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pptactic.ml,v 1.54.2.5 2005/12/23 22:16:46 herbelin Exp $ *)
+(* $Id: pptactic.ml 8651 2006-03-21 21:54:43Z jforest $ *)
open Pp
open Names
open Nameops
open Util
-open Extend
open Tacexpr
open Rawterm
open Topconstr
open Genarg
open Libnames
open Pattern
+open Ppextend
+open Ppconstr
+open Printer
-let pr_red_expr = Ppconstr.pr_red_expr
-let pr_may_eval = Ppconstr.pr_may_eval
-let pr_sort = Ppconstr.pr_sort
-let pr_global x =
- if Options.do_translate () then (* for pr_gen *)
- Ppconstrnew.pr_global Idset.empty x
- else
- Ppconstr.pr_global Idset.empty x
-let pr_name = Ppconstr.pr_name
-let pr_opt = Ppconstr.pr_opt
-let pr_occurrences = Ppconstr.pr_occurrences
+let pr_global x = Nametab.pr_global_env Idset.empty x
type grammar_terminals = string option list
(* Extensions *)
-let prtac_tab_v7 = Hashtbl.create 17
let prtac_tab = Hashtbl.create 17
-let declare_extra_tactic_pprule for_v8 s (tags,prods) =
- Hashtbl.add prtac_tab_v7 (s,tags) prods;
- if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
+let declare_extra_tactic_pprule (s,tags,prods) =
+ Hashtbl.add prtac_tab (s,tags) prods
-let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab_v7 (s,tags)
+let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags)
type 'a raw_extra_genarg_printer =
- (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (constr_expr -> std_ppcmds) ->
+ (constr_expr -> std_ppcmds) ->
+ (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
type 'a glob_extra_genarg_printer =
- (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (rawconstr_and_expr -> std_ppcmds) ->
+ (rawconstr_and_expr -> std_ppcmds) ->
+ (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
+
type 'a extra_genarg_printer =
- (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (Term.constr -> std_ppcmds) ->
+ (Term.constr -> std_ppcmds) ->
+ (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+ 'a -> std_ppcmds
-let genarg_pprule_v7 = ref Stringmap.empty
let genarg_pprule = ref Stringmap.empty
-let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) =
+let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
let s = match unquote wit with
| ExtraArgType s -> s
| _ -> error
"Can declare a pretty-printing rule only for extra argument types"
in
- let f prc prtac x = f prc prtac (out_gen rawwit x) in
- let g prc prtac x = g prc prtac (out_gen globwit x) in
- let h prc prtac x = h prc prtac (out_gen wit x) in
- genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7;
- if for_v8 then
- genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule
+ let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
+ let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
+ let h prc prlc prtac x = h prc prlc prtac (out_gen wit x) in
+ genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule
let pr_arg pr x = spc () ++ pr x
@@ -84,14 +79,10 @@ let pr_and_short_name pr (c,_) = pr c
let pr_located pr (loc,x) = pr x
-let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp)
-
let pr_evaluable_reference = function
| EvalVarRef id -> pr_id id
| EvalConstRef sp -> pr_global (Libnames.ConstRef sp)
-let pr_inductive ind = pr_global (Libnames.IndRef ind)
-
let pr_quantified_hypothesis = function
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
@@ -108,12 +99,7 @@ let pr_bindings prc prlc = function
prlist_with_sep spc prc l
| ExplicitBindings l ->
brk (1,1) ++ str "with" ++ brk (1,1) ++
- prlist_with_sep spc
- (fun b -> if Options.do_translate () or not !Options.v7 then
- str"(" ++ pr_binding prlc b ++ str")"
- else
- pr_binding prc b)
- l
+ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
| NoBindings -> mt ()
let pr_bindings_no_with prc prlc = function
@@ -122,21 +108,11 @@ let pr_bindings_no_with prc prlc = function
prlist_with_sep spc prc l
| ExplicitBindings l ->
brk (1,1) ++
- prlist_with_sep spc
- (fun b -> if Options.do_translate () or not !Options.v7 then
- str"(" ++ pr_binding prlc b ++ str")"
- else
- pr_binding prc b)
- l
+ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
| NoBindings -> mt ()
let pr_with_bindings prc prlc (c,bl) =
- if Options.do_translate () then
- (* translator calls pr_with_bindings on rawconstr: we cast it! *)
- let bl' = Ppconstrnew.translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
- prc c ++ hv 0 (pr_bindings prc prlc bl')
- else
- prc c ++ hv 0 (pr_bindings prc prlc bl)
+ prc c ++ hv 0 (pr_bindings prc prlc bl)
let pr_with_constr prc = function
| None -> mt ()
@@ -146,109 +122,10 @@ let pr_with_names = function
| None -> mt ()
| Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
-let pr_hyp_location pr_id = function
- | id, _, (InHyp,_) -> spc () ++ pr_id id
- | id, _, (InHypTypeOnly,_) ->
- spc () ++ str "(Type of " ++ pr_id id ++ str ")"
- | id, _, _ -> error "Unsupported hyp location in v7"
-
-let pr_clause pr_id = function
- | [] -> mt ()
- | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
-
-
-let pr_clauses pr_id cls =
- match cls with
- { onhyps = Some l; onconcl = false } ->
- spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
- | { onhyps = Some []; onconcl = true } -> mt()
- | _ -> error "this clause has both hypothesis and conclusion"
-
-let pr_simple_clause pr_id = function
- | [] -> mt ()
- | l -> spc () ++
- hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l)
-
-let pr_clause_pattern pr_id cls =
- pr_opt
- (prlist (fun (id,occs,_) ->
- prlist (pr_arg int) occs ++ spc () ++ pr_id id)) cls.onhyps ++
- if cls.onconcl then
- prlist (pr_arg int) cls.concl_occs ++ spc() ++ str"Goal"
- else mt()
-
-let pr_subterms pr occl =
- hov 0 (pr_occurrences pr occl ++ spc () ++ str "with")
-
-let pr_induction_arg prc = function
- | ElimOnConstr c -> prc c
- | ElimOnIdent (_,id) -> pr_id id
- | ElimOnAnonHyp n -> int n
-
-let pr_induction_kind = function
- | SimpleInversion -> str "Simple Inversion"
- | FullInversion -> str "Inversion"
- | FullInversionClear -> str "Inversion_clear"
-
-let pr_match_pattern pr_pat = function
- | Term a -> pr_pat a
- | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
- | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-
-let pr_match_hyps pr_pat = function
- | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
-
-let pr_match_rule m pr_pat pr = function
- | Pat ([],mp,t) when m ->
- str "[" ++ pr_match_pattern pr_pat mp ++ str "]"
- ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
- | Pat (rl,mp,t) ->
- str "[" ++ prlist_with_sep pr_semicolon
- (pr_match_hyps pr_pat) rl ++ spc () ++
- str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "]" ++
- spc () ++ str "->" ++ brk (1,2) ++ pr t
- | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
-
-let pr_funvar = function
- | None -> spc () ++ str "()"
- | Some id -> spc () ++ pr_id id
-
-let pr_let_clause k pr = function
- | ((_,id),None,t) -> hv 0(str k ++ pr_id id ++ str " =" ++ brk (1,1) ++ pr t)
- | ((_,id),Some c,t) -> str "TODO(LETCLAUSE)"
-
-let pr_let_clauses pr = function
- | hd::tl ->
- hv 0
- (pr_let_clause "Let " pr hd ++
- prlist (fun t -> spc () ++ pr_let_clause "And " pr t) tl)
- | [] -> anomaly "LetIn must declare at least one binding"
-
-let pr_rec_clause pr ((_,id),(l,t)) =
- pr_id id ++ prlist pr_funvar l ++ str "->" ++ spc () ++ pr t
-
-let pr_rec_clauses pr l =
- prlist_with_sep (fun () -> fnl () ++ str "And ") (pr_rec_clause pr) l
-
-let pr_hintbases = function
- | None -> spc () ++ str "with *"
- | Some [] -> mt ()
- | Some l ->
- spc () ++ str "with" ++ hv 0 (prlist (fun s -> spc () ++ str s) l)
-
-let pr_autoarg_adding = function
- | [] -> mt ()
- | l ->
- spc () ++ str "Adding [" ++
- hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
-
-let pr_autoarg_destructing = function
- | true -> spc () ++ str "Destructing"
- | false -> mt ()
-
-let pr_autoarg_usingTDB = function
- | true -> spc () ++ str "Using TDB"
- | false -> mt ()
+let rec pr_message_token prid = function
+ | MsgString s -> qs s
+ | MsgInt n -> int n
+ | MsgIdent id -> prid id
let rec pr_raw_generic prc prlc prtac prref x =
match Genarg.genarg_tag x with
@@ -259,24 +136,20 @@ let rec pr_raw_generic prc prlc prtac prref x =
| PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x)
| IntroPatternArgType -> pr_arg pr_intro_pattern
(out_gen rawwit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen rawwit_ident x))
- | HypArgType -> pr_arg
- (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen rawwit_var x)
+ | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
+ | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x)
| RefArgType -> pr_arg prref (out_gen rawwit_ref x)
| SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc prref)
+ pr_arg (pr_may_eval prc prlc prref)
(out_gen rawwit_constr_may_eval x)
| QuantHypArgType ->
pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr
- (prc,prref)) (out_gen rawwit_red_expr x)
- | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
- | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x))
- | CastedOpenConstrArgType ->
- pr_arg prc (snd (out_gen rawwit_casted_open_constr x))
+ pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
+ | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x)
+ | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
| BindingsArgType ->
@@ -293,10 +166,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
pr_raw_generic prc prlc prtac prref b)
x)
| ExtraArgType s ->
- let tab =
- if Options.do_translate() or not !Options.v7 then !genarg_pprule
- else !genarg_pprule_v7 in
- try pi1 (Stringmap.find s tab) prc prtac x
+ try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
with Not_found -> str " [no printer for " ++ str s ++ str "] "
@@ -309,23 +179,22 @@ let rec pr_glob_generic prc prlc prtac x =
| PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x)
| IntroPatternArgType ->
pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id ((*Constrextern.v7_to_v8_id*) (out_gen globwit_ident x))
- | HypArgType -> pr_arg (pr_located (fun id -> pr_id (Constrextern.v7_to_v8_id id))) (out_gen globwit_var x)
+ | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x)
+ | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x)
| RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x)
| SortArgType -> pr_arg pr_sort (out_gen globwit_sort x)
| ConstrArgType -> pr_arg prc (out_gen globwit_constr x)
| ConstrMayEvalArgType ->
- pr_arg (pr_may_eval prc
+ pr_arg (pr_may_eval prc prlc
(pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x)
| QuantHypArgType ->
pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
| RedExprArgType ->
pr_arg (pr_red_expr
- (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
- | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x)
- | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x))
- | CastedOpenConstrArgType ->
- pr_arg prc (snd (out_gen globwit_casted_open_constr x))
+ (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)))
+ (out_gen globwit_red_expr x)
+ | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x)
+ | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
| BindingsArgType ->
@@ -342,10 +211,7 @@ let rec pr_glob_generic prc prlc prtac x =
pr_glob_generic prc prlc prtac b)
x)
| ExtraArgType s ->
- let tab =
- if Options.do_translate() or not !Options.v7 then !genarg_pprule
- else !genarg_pprule_v7 in
- try pi2 (Stringmap.find s tab) prc prtac x
+ try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
with Not_found -> str " [no printer for " ++ str s ++ str "] "
open Closure
@@ -359,8 +225,8 @@ let rec pr_generic prc prlc prtac x =
| PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x)
| IntroPatternArgType ->
pr_arg pr_intro_pattern (out_gen wit_intro_pattern x)
- | IdentArgType -> pr_arg pr_id (Constrextern.v7_to_v8_id (out_gen wit_ident x))
- | HypArgType -> pr_arg prc (out_gen wit_var x)
+ | IdentArgType -> pr_arg pr_id (out_gen wit_ident x)
+ | VarArgType -> pr_arg pr_id (out_gen wit_var x)
| RefArgType -> pr_arg pr_global (out_gen wit_ref x)
| SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x))
| ConstrArgType -> pr_arg prc (out_gen wit_constr x)
@@ -369,11 +235,10 @@ let rec pr_generic prc prlc prtac x =
| QuantHypArgType ->
pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
| RedExprArgType ->
- pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
- | TacticArgType -> pr_arg prtac (out_gen wit_tactic x)
- | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x))
- | CastedOpenConstrArgType ->
- pr_arg prc (snd (out_gen wit_casted_open_constr x))
+ pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference))
+ (out_gen wit_red_expr x)
+ | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x)
+ | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
| ConstrWithBindingsArgType ->
pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
| BindingsArgType ->
@@ -390,10 +255,7 @@ let rec pr_generic prc prlc prtac x =
pr_generic prc prlc prtac b)
x)
| ExtraArgType s ->
- let tab =
- if Options.do_translate() or not !Options.v7 then !genarg_pprule
- else !genarg_pprule_v7 in
- try pi3 (Stringmap.find s tab) prc prtac x
+ try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
with Not_found -> str " [no printer for " ++ str s ++ str "]"
let rec pr_tacarg_using_rule pr_gen = function
@@ -402,364 +264,735 @@ let rec pr_tacarg_using_rule pr_gen = function
| [], [] -> mt ()
| _ -> failwith "Inconsistent arguments of extended tactic"
-let pr_extend_gen prgen s l =
- let tab =
- if Options.do_translate() or not !Options.v7 then prtac_tab
- else prtac_tab_v7
- in
+let surround p = hov 1 (str"(" ++ p ++ str")")
+
+let pr_extend_gen prgen lev s l =
try
let tags = List.map genarg_tag l in
- (* Hack pour les syntaxes changeant non uniformément en passant a la V8 *)
- let s =
- let n = String.length s in
- if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "v7"
- then String.sub s 0 (n-2) ^ "v8"
- else s in
- let (s,pl) = Hashtbl.find tab (s,tags) in
- str s ++ pr_tacarg_using_rule prgen (pl,l)
+ let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
+ let p = pr_tacarg_using_rule prgen (pl,l) in
+ if lev' > lev then surround p else p
with Not_found ->
str s ++ prlist prgen l ++ str " (* Generic printer *)"
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
+let pr_raw_extend prc prlc prtac =
+ pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
+let pr_glob_extend prc prlc prtac =
+ pr_extend_gen (pr_glob_generic prc prlc prtac)
+let pr_extend prc prlc prtac =
+ pr_extend_gen (pr_generic prc prlc prtac)
+
+(**********************************************************************)
+(* The tactic printer *)
+
+let sep_v = fun _ -> str"," ++ spc()
+
+let strip_prod_binders_expr n ty =
+ let rec strip_ty acc n ty =
+ match ty with
+ Topconstr.CProdN(_,bll,a) ->
+ let nb =
+ List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
+ if nb >= n then (List.rev (bll@acc), a)
+ else strip_ty (bll@acc) (n-nb) a
+ | Topconstr.CArrow(_,a,b) ->
+ if n=1 then
+ (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
+ else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
+ | _ -> 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_arg pr x = spc () ++ pr x
+
+let pr_ltac_constant sp =
+ pr_qualid (Nametab.shortest_qualid_of_tactic sp)
+
+let pr_evaluable_reference_env env = function
+ | EvalVarRef id -> pr_id id
+ | EvalConstRef sp ->
+ Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp)
+
+let pr_inductive env ind =
+ Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind)
+
+let pr_quantified_hypothesis = function
+ | AnonHyp n -> int n
+ | NamedHyp id -> pr_id id
+
+let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
+
+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 prlc prc = function
+ | ImplicitBindings l ->
+ spc () ++
+ hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+ prlist_with_sep spc prc l)
+ | ExplicitBindings l ->
+ spc () ++
+ hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++
+ pr_esubst prlc l)
+ | NoBindings -> mt ()
+
+let pr_bindings prlc prc = pr_bindings_gen false prlc prc
+
+let pr_with_bindings prlc prc (c,bl) =
+ hov 1 (prc c ++ pr_bindings prlc prc bl)
+
+let pr_with_constr prc = function
+ | None -> mt ()
+ | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
+let pr_with_names = function
+ | IntroAnonymous -> mt ()
+ | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+
+let pr_pose prlc prc na c = match na with
+ | Anonymous -> spc() ++ prc c
+ | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+
+let pr_assertion _prlc prc 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_with_names ipat
+
+let pr_assumption prlc prc 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_with_names ipat
+
+let pr_by_tactic prt = function
+ | TacId [] -> mt ()
+ | tac -> spc() ++ str "by " ++ prt tac
+
+let pr_occs pp = function
+ [] -> pp
+ | nl -> hov 1 (pp ++ spc() ++ str"at " ++
+ hov 0 (prlist_with_sep spc int nl))
+
+let pr_hyp_location pr_id = function
+ | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs
+ | id, occs, InHypTypeOnly ->
+ spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs
+ | id, occs, InHypValueOnly ->
+ spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs
+
+let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
+
+let pr_simple_clause pr_id = function
+ | [] -> mt ()
+ | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
+
+let pr_clauses pr_id = function
+ { onhyps=None; onconcl=true; concl_occs=nl } ->
+ pr_in (pr_occs (str " *") nl)
+ | { onhyps=None; onconcl=false } -> pr_in (str " * |-")
+ | { onhyps=Some l; onconcl=true; concl_occs=nl } ->
+ pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l
+ ++ pr_occs (str" |- *") nl)
+ | { onhyps=Some l; onconcl=false } ->
+ pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l)
+
+let pr_clause_pattern pr_id = function
+ | (None, []) -> mt ()
+ | (glopt,l) ->
+ str " in" ++
+ prlist
+ (fun (id,nl) -> prlist (pr_arg int) nl
+ ++ spc () ++ pr_id id) l ++
+ pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
+
+let pr_induction_arg prc = function
+ | ElimOnConstr c -> prc c
+ | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id)
+ | ElimOnAnonHyp n -> int n
+
+let pr_induction_kind = function
+ | SimpleInversion -> str "simple inversion"
+ | FullInversion -> str "inversion"
+ | FullInversionClear -> str "inversion_clear"
+
+let pr_lazy lz = if lz then str "lazy " else mt ()
+
+let pr_match_pattern pr_pat = function
+ | Term a -> pr_pat a
+ | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
+ | Subterm (Some id,a) ->
+ str "context " ++ 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
+
+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) ->
+ prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
+ spc () ++ 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 = function
+ | (id,None,t) ->
+ hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++
+ pr (TacArg t))
+ | (id,Some c,t) ->
+ hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++
+ pr c ++
+ str " :=" ++ brk (1,1) ++ pr (TacArg t))
+
+let pr_let_clauses pr = function
+ | hd::tl ->
+ hv 0
+ (pr_let_clause "let " pr hd ++
+ prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
+ | [] -> anomaly "LetIn must declare at least one binding"
+
+let pr_rec_clause pr (id,(l,t)) =
+ hov 0
+ (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+
+let pr_rec_clauses pr l =
+ prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
+
+let pr_seq_body pr tl =
+ hv 0 (str "[ " ++
+ prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+ str " ]")
+
+let pr_hintbases = function
+ | None -> spc () ++ str "with *"
+ | Some [] -> mt ()
+ | Some l ->
+ spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l)
+
+let pr_auto_using prc = function
+ | [] -> mt ()
+ | l -> spc () ++
+ hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_coma prc l)
+
+let pr_autoarg_adding = function
+ | [] -> mt ()
+ | l ->
+ spc () ++ str "adding [" ++
+ hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
+
+let pr_autoarg_destructing = function
+ | true -> spc () ++ str "destructing"
+ | false -> mt ()
+
+let pr_autoarg_usingTDB = function
+ | true -> spc () ++ str "using tdb"
+ | false -> mt ()
+
+let rec pr_tacarg_using_rule pr_gen = function
+ | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
+ | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al)
+ | [], [] -> mt ()
+ | _ -> failwith "Inconsistent arguments of extended tactic"
+
+let pr_then () = str ";"
-let pr_bindings = pr_bindings pr_constr pr_constr in
-let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in
-let pr_with_bindings = pr_with_bindings pr_constr pr_constr in
-let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in
-let pr_constrarg c = spc () ++ pr_constr c in
+let ltop = (5,E)
+let lseq = 5
+let ltactical = 3
+let lorelse = 2
+let llet = 1
+let lfun = 1
+let lcomplete = 1
+let labstract = 3
+let lmatch = 1
+let latom = 0
+let lcall = 1
+let leval = 1
+let ltatom = 1
+
+let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+
+open Closure
+
+let make_pr_tac
+ (pr_tac_level,pr_constr,pr_lconstr,pr_pat,
+ pr_cst,pr_ind,pr_ref,pr_ident,
+ pr_extend,strip_prod_binders) =
+
+let pr_bindings env =
+ pr_bindings (pr_lconstr env) (pr_constr env) in
+let pr_ex_bindings env =
+ pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
+let pr_with_bindings env =
+ pr_with_bindings (pr_lconstr env) (pr_constr env) in
+let pr_eliminator env cb =
+ str "using" ++ pr_arg (pr_with_bindings env) cb in
+let pr_extend env =
+ pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) in
+let pr_red_expr env =
+ pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) in
+
+let pr_constrarg env c = spc () ++ pr_constr env c in
+let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
let pr_intarg n = spc () ++ int n in
+let pr_binder_fix env (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_lconstr env t in
+ spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+let pr_fix_tac env (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_from (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 =
+ if List.length names = 1 then mt()
+ else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
+ hov 1 (str"(" ++ pr_id id ++
+ prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++
+ pr_lconstrarg env ty ++ str")") in
+(* spc() ++
+ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+ env c)
+*)
+let pr_cofix_tac env (id,c) =
+ hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
+
(* Printing tactics as arguments *)
-let rec pr_atom0 = function
- | TacIntroPattern [] -> str "Intros"
- | TacIntroMove (None,None) -> str "Intro"
- | TacAssumption -> str "Assumption"
- | TacAnyConstructor None -> str "Constructor"
- | TacTrivial (Some []) -> str "Trivial"
- | TacAuto (None,Some []) -> str "Auto"
- | TacAutoTDB None -> str "AutoTDB"
- | TacDestructConcl -> str "DConcl"
- | TacReflexivity -> str "Reflexivity"
- | t -> str "(" ++ pr_atom1 t ++ str ")"
+let rec pr_atom0 env = function
+ | TacIntroPattern [] -> str "intros"
+ | TacIntroMove (None,None) -> str "intro"
+ | TacAssumption -> str "assumption"
+ | TacAnyConstructor None -> str "constructor"
+ | TacTrivial ([],Some []) -> str "trivial"
+ | TacAuto (None,[],Some []) -> str "auto"
+ | TacReflexivity -> str "reflexivity"
+ | t -> str "(" ++ pr_atom1 env t ++ str ")"
(* Main tactic printer *)
-and pr_atom1 = function
- | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac s l
- | TacAlias (_,s,l,_) ->
- pr_extend pr_constr pr_constr pr_tac s (List.map snd l)
+and pr_atom1 env = function
+ | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl
+ | TacSuperAuto _ | TacExtend (_,
+ ("GTauto"|"GIntuition"|"TSimplif"|
+ "LinearIntuition"),_) ->
+ errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
+ | TacExtend (loc,s,l) ->
+ pr_with_comments loc (pr_extend env 1 s l)
+ | TacAlias (loc,s,l,_) ->
+ pr_with_comments loc (pr_extend env 1 s (List.map snd l))
(* Basic tactics *)
- | TacIntroPattern [] as t -> pr_atom0 t
+ | TacIntroPattern [] as t -> pr_atom0 env t
| TacIntroPattern (_::_ as p) ->
- hov 1 (str "Intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
+ hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
| TacIntrosUntil h ->
- hv 1 (str "Intros until" ++ pr_arg pr_quantified_hypothesis h)
- | TacIntroMove (None,None) as t -> pr_atom0 t
- | TacIntroMove (Some id1,None) -> str "Intro " ++ pr_id id1
- | TacIntroMove (ido1,Some (_,id2)) ->
+ hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
+ | TacIntroMove (None,None) as t -> pr_atom0 env t
+ | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1
+ | TacIntroMove (ido1,Some id2) ->
hov 1
- (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
- | TacAssumption as t -> pr_atom0 t
- | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c)
- | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb)
+ (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
+ pr_lident id2)
+ | TacAssumption as t -> pr_atom0 env t
+ | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
+ | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg env c)
+ | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
| TacElim (cb,cbo) ->
- hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++
- pr_opt pr_eliminator cbo)
- | TacElimType c -> hov 1 (str "ElimType" ++ pr_arg pr_constr c)
- | TacCase cb -> hov 1 (str "Case" ++ spc () ++ pr_with_bindings cb)
- | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
- | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n)
+ hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++
+ pr_opt (pr_eliminator env) cbo)
+ | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c)
+ | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb)
+ | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
+ | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
| TacMutualFix (id,n,l) ->
- hov 1 (str "Fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
- hov 0 (str "with" ++ brk (1,1) ++
- prlist_with_sep spc
- (fun (id,n,c) ->
- spc () ++ pr_id id ++ pr_intarg n ++ pr_arg pr_constr c)
- l))
- | TacCofix ido -> hov 1 (str "Cofix" ++ pr_opt pr_id ido)
+ hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
+ str"with " ++ prlist_with_sep spc (pr_fix_tac env) l)
+ | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
| TacMutualCofix (id,l) ->
- hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ spc () ++
- hov 0 (str "with" ++ brk (1,1) ++
- prlist (fun (id,c) -> spc () ++ pr_id id ++ pr_arg pr_constr c)
- l))
- | TacCut c -> hov 1 (str "Cut" ++ pr_arg pr_constr c)
- | TacTrueCut (Anonymous,c) ->
- hov 1 (str "Assert" ++ pr_arg pr_constr c)
- | TacTrueCut (Name id,c) ->
- hov 1 (str "Assert" ++ spc () ++ pr_id id ++ str ":" ++ pr_constr c)
- | TacForward (false,na,c) ->
- hov 1 (str "Assert" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
- | TacForward (true,na,c) ->
- hov 1 (str "Pose" ++ pr_arg pr_name na ++ str ":=" ++ pr_constr c)
+ hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
+ str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
+ | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
+ | TacAssert (Some tac,ipat,c) ->
+ hov 1 (str "assert" ++
+ pr_assumption (pr_lconstr env) (pr_constr env) ipat c ++
+ pr_by_tactic (pr_tac_level env ltop) tac)
+ | TacAssert (None,ipat,c) ->
+ hov 1 (str "pose proof" ++
+ pr_assertion (pr_lconstr env) (pr_constr env) ipat c)
| TacGeneralize l ->
- hov 1 (str "Generalize" ++ spc () ++ prlist_with_sep spc pr_constr l)
+ hov 1 (str "generalize" ++ spc () ++
+ prlist_with_sep spc (pr_constr env) l)
| TacGeneralizeDep c ->
- hov 1 (str "Generalize" ++ spc () ++ str "Dependent" ++ spc () ++
- pr_constr c)
+ hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
+ pr_constrarg env c)
+ | TacLetTac (na,c,cl) when cl = nowhere ->
+ hov 1 (str "pose" ++ pr_pose (pr_lconstr env) (pr_constr env) na c)
| TacLetTac (na,c,cl) ->
- let pcl = match cl with
- {onhyps=None;onconcl=true;concl_occs=[]} -> mt()
- | _ -> pr_clauses pr_ident cl in
- hov 1 (str "LetTac" ++ spc () ++ pr_name na ++ str ":=" ++
- pr_constr c ++ pcl)
- | TacInstantiate (n,c,cls) ->
- hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++
- pr_clauses pr_ident cls)
+ hov 1 (str "set" ++ pr_pose (pr_lconstr env) (pr_constr env) na c ++
+ pr_clauses pr_ident cl)
+(* | TacInstantiate (n,c,ConclLocation ()) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg env c ++ str ")" ))
+ | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg env c ++ str ")" )
+ ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
+*)
(* Derived basic tactics *)
- | TacSimpleInduction (h,_) ->
- hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
- | TacNewInduction (h,e,(ids,_)) ->
- hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
- pr_opt pr_eliminator e ++ pr_with_names ids)
+ | TacSimpleInduction h ->
+ hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
+ | TacNewInduction (h,e,ids) ->
+ hov 1 (str "induction" ++ spc () ++
+ prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++
+ pr_opt (pr_eliminator env) e)
| TacSimpleDestruct h ->
- hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
- | TacNewDestruct (h,e,(ids,_)) ->
- hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
- pr_opt pr_eliminator e ++ pr_with_names ids)
+ hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
+ | TacNewDestruct (h,e,ids) ->
+ hov 1 (str "destruct" ++ spc () ++
+ prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++
+ pr_with_names ids ++
+ pr_opt (pr_eliminator env) e)
| TacDoubleInduction (h1,h2) ->
hov 1
- (str "Double Induction" ++
+ (str "double induction" ++
pr_arg pr_quantified_hypothesis h1 ++
pr_arg pr_quantified_hypothesis h2)
| TacDecomposeAnd c ->
- hov 1 (str "Decompose Record" ++ pr_arg pr_constr c)
+ hov 1 (str "decompose record" ++ pr_constrarg env c)
| TacDecomposeOr c ->
- hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c)
+ hov 1 (str "decompose sum" ++ pr_constrarg env c)
| TacDecompose (l,c) ->
- hov 1 (str "Decompose" ++ spc () ++
- hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
- ++ str "]" ++ pr_arg pr_constr c))
+ hov 1 (str "decompose" ++ spc () ++
+ hov 0 (str "[" ++ prlist_with_sep spc (pr_ind env) l
+ ++ str "]" ++ pr_constrarg env c))
| TacSpecialize (n,c) ->
- hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c)
+ hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++
+ pr_with_bindings env c)
| TacLApply c ->
- hov 1 (str "LApply" ++ pr_constr c)
+ hov 1 (str "lapply" ++ pr_constrarg env c)
(* Automation tactics *)
- | TacTrivial (Some []) as x -> pr_atom0 x
- | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
- | TacAuto (None,Some []) as x -> pr_atom0 x
- | TacAuto (n,db) ->
- hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
- | TacAutoTDB None as x -> pr_atom0 x
- | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
- | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
- | TacDestructHyp (false,(_,id)) -> hov 0 (str "DHyp" ++ spc () ++ pr_id id)
- | TacDestructConcl as x -> pr_atom0 x
- | TacSuperAuto (n,l,b1,b2) ->
- hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++
- pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
+ | TacTrivial ([],Some []) as x -> pr_atom0 env x
+ | TacTrivial (lems,db) ->
+ hov 0 (str "trivial" ++
+ pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
+ | TacAuto (None,[],Some []) as x -> pr_atom0 env x
+ | TacAuto (n,lems,db) ->
+ hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++
+ pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
| TacDAuto (n,p) ->
- hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++
- pr_opt int p)
+ hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p)
(* Context management *)
- | TacClear l ->
- hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
+ | TacClear (keep,l) ->
+ hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
+ prlist_with_sep spc pr_ident l)
| TacClearBody l ->
- hov 1 (str "ClearBody" ++ spc () ++ prlist_with_sep spc pr_ident l)
+ hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
| TacMove (b,id1,id2) ->
(* Rem: only b = true is available for users *)
assert b;
hov 1
- (str "Move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
+ (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
str "after" ++ brk (1,1) ++ pr_ident id2)
| TacRename (id1,id2) ->
hov 1
- (str "Rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
+ (str "rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++
str "into" ++ brk (1,1) ++ pr_ident id2)
(* Constructors *)
- | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l)
- | TacRight l -> hov 1 (str "Right" ++ pr_bindings l)
- | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l)
+ | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l)
+ | TacRight l -> hov 1 (str "right" ++ pr_bindings env l)
+ | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l)
+ | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l)
| TacAnyConstructor (Some t) ->
- hov 1 (str "Constructor" ++ pr_arg pr_tac0 t)
- | TacAnyConstructor None as t -> pr_atom0 t
+ hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t)
+ | TacAnyConstructor None as t -> pr_atom0 env t
| TacConstructor (n,l) ->
- hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
+ hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings env l)
(* Conversion *)
| TacReduce (r,h) ->
- hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clauses pr_ident h)
- | TacChange (occl,c,h) ->
- hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++
- brk (1,1) ++ pr_constr c ++ pr_clauses pr_ident h)
+ hov 1 (pr_red_expr env r ++
+ pr_clauses pr_ident h)
+ | TacChange (occ,c,h) ->
+ hov 1 (str "change" ++ brk (1,1) ++
+ (match occ with
+ None -> mt()
+ | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ")
+ | Some(ocl,c1) ->
+ hov 1 (pr_constr env c1 ++ spc() ++
+ str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++
+ str "with ") ++
+ pr_constr env c ++ pr_clauses pr_ident h)
(* Equivalence relations *)
- | TacReflexivity as x -> pr_atom0 x
- | TacSymmetry cls -> str "Symmetry " ++ pr_clauses pr_ident cls
- | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
+ | TacReflexivity as x -> pr_atom0 env x
+ | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
+ | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c
(* Equality and inversion *)
| TacInversion (DepInversion (k,c,ids),hyp) ->
- hov 1 (str "Dependent " ++ pr_induction_kind k ++
+ hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
- pr_with_names ids ++ pr_with_constr pr_constr c)
+ pr_with_names ids ++ pr_with_constr (pr_constr env) c)
| TacInversion (NonDepInversion (k,cl,ids),hyp) ->
hov 1 (pr_induction_kind k ++ spc () ++
pr_quantified_hypothesis hyp ++
pr_with_names ids ++ pr_simple_clause pr_ident cl)
| TacInversion (InversionUsing (c,cl),hyp) ->
- hov 1 (str "Inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
- str "using" ++ spc () ++ pr_constr c ++
+ hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
+ spc () ++ str "using" ++ spc () ++ pr_constr env c ++
pr_simple_clause pr_ident cl)
-and pr_tactic_seq_body tl =
- hv 0 (str "[ " ++
- prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]")
-
- (* Strictly closed atomic tactic expressions *)
-and pr0 = function
- | TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
- | TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
- | TacId "" -> str "Idtac"
- | TacFail (ArgArg 0,"") -> str "Fail"
- | TacAtom (_,t) -> pr_atom0 t
- | TacArg c -> pr_tacarg c
- | t -> str "(" ++ prtac t ++ str ")"
-
- (* Semi-closed atomic tactic expressions *)
-and pr1 = function
- | TacAtom (_,t) -> pr_atom1 t
- | TacId s -> str "Idtac \"" ++ str s ++ str "\""
- | TacFail (ArgArg 0,s) -> str "Fail \"" ++ str s ++ str "\""
- | TacFail (n,"") -> str "Fail " ++ pr_or_var int n
- | TacFail (n,s) -> str "Fail " ++ pr_or_var int n ++ str " \"" ++ str s ++ str "\""
- | t -> pr0 t
-
- (* Orelse tactic expressions (printed as if parsed associating on the right
- though the semantics is purely associative) *)
-and pr2 = function
- | TacOrelse (t1,t2) ->
- hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2)
- | t -> pr1 t
-
- (* Non closed prefix tactic expressions *)
-and pr3 = function
- | TacTry t -> hov 1 (str "Try" ++ spc () ++ pr3 t)
- | TacDo (n,t) -> hov 1 (str "Do " ++ pr_or_var int n ++ spc () ++ pr3 t)
- | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t)
- | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t)
- | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t)
- | t -> pr2 t
-
-and pr4 = function
- | t -> pr3 t
-
- (* THEN and THENS tactic expressions (printed as if parsed
- associating on the left though the semantics is purely associative) *)
-and pr5 = function
- | TacThens (t,tl) ->
- hov 1 (pr5 t ++ str ";" ++ spc () ++ pr_tactic_seq_body tl)
- | TacThen (t1,t2) ->
- hov 1 (pr5 t1 ++ str ";" ++ spc () ++ pr4 t2)
- | t -> pr4 t
-
- (* Ltac tactic expressions *)
-and pr6 = function
- |(TacAtom _
- | TacThen _
- | TacThens _
- | TacFirst _
- | TacSolve _
- | TacTry _
- | TacOrelse _
- | TacDo _
- | TacRepeat _
- | TacProgress _
- | TacId _
- | TacFail _
- | TacInfo _) as t -> pr5 t
-
- | TacAbstract (t,None) -> str "Abstract " ++ pr6 t
+in
+
+let rec pr_tac env inherited tac =
+ let (strm,prec) = match tac with
+ | TacAbstract (t,None) ->
+ str "abstract " ++ pr_tac env (labstract,L) t, labstract
| TacAbstract (t,Some s) ->
hov 0
- (str "Abstract " ++ pr6 t ++ spc () ++ str "using" ++ spc () ++ pr_id s)
+ (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++
+ str "using " ++ pr_id s),
+ labstract
| TacLetRecIn (l,t) ->
hv 0
- (str "Rec " ++ pr_rec_clauses prtac l ++
- spc () ++ str "In" ++ fnl () ++ prtac t)
+ (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++
+ fnl () ++ pr_tac env (llet,E) t),
+ llet
| TacLetIn (llc,u) ->
v 0
- (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u)
- | TacMatch (t,lrul) ->
- hov 0 (str "Match" ++ spc () ++ pr6 t ++ spc()
- ++ str "With"
+ (hv 0 (pr_let_clauses (pr_tac env ltop) llc
+ ++ str " in") ++
+ fnl () ++ pr_tac env (llet,E) u),
+ llet
+ | TacMatch (lz,t,lrul) ->
+ hov 0 (pr_lazy lz ++ str "match " ++ pr_tac env ltop t ++ str " with"
++ prlist
- (fun r -> fnl () ++ str "|" ++ spc () ++
- pr_match_rule true pr_pat prtac r)
- lrul)
- | TacMatchContext (lr,lrul) ->
- hov 0 (
- str (if lr then "Match Reverse Context With" else "Match Context With")
+ (fun r -> fnl () ++ str "| " ++
+ pr_match_rule true (pr_tac env ltop) pr_pat r)
+ lrul
+ ++ fnl() ++ str "end"),
+ lmatch
+ | TacMatchContext (lz,lr,lrul) ->
+ hov 0 (pr_lazy lz ++
+ str (if lr then "match reverse goal with" else "match goal with")
++ prlist
- (fun r -> fnl () ++ str "|" ++ spc () ++
- pr_match_rule false pr_pat prtac r)
- lrul)
+ (fun r -> fnl () ++ str "| " ++
+ pr_match_rule false (pr_tac env ltop) pr_pat r)
+ lrul
+ ++ fnl() ++ str "end"),
+ lmatch
| TacFun (lvar,body) ->
- hov 0 (str "Fun" ++
- prlist pr_funvar lvar ++ spc () ++ str "->" ++ spc () ++ prtac body)
-
- | TacArg c -> pr_tacarg c
-
-and pr_tacarg0 = function
- | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>")
- | MetaIdArg (_,s) -> str ("$" ^ s)
- | IntroPattern ipat -> pr_intro_pattern ipat
+(* let env = List.fold_right (option_fold_right Idset.add) lvar env in*)
+ hov 2 (str "fun" ++
+ prlist pr_funvar lvar ++ str " =>" ++ spc () ++
+ pr_tac env (lfun,E) body),
+ lfun
+ | TacThens (t,tl) ->
+ hov 1 (pr_tac env (lseq,E) t ++ pr_then () ++ spc () ++
+ pr_seq_body (pr_tac env ltop) tl),
+ lseq
+ | TacThen (t1,t2) ->
+ hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++
+ pr_tac env (lseq,L) t2),
+ lseq
+ | TacTry t ->
+ hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t),
+ ltactical
+ | TacDo (n,t) ->
+ hov 1 (str "do " ++ pr_or_var int n ++ spc () ++
+ pr_tac env (ltactical,E) t),
+ ltactical
+ | TacRepeat t ->
+ hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t),
+ ltactical
+ | TacProgress t ->
+ hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t),
+ ltactical
+ | TacInfo t ->
+ hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t),
+ ltactical
+ | TacOrelse (t1,t2) ->
+ hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
+ pr_tac env (lorelse,E) t2),
+ lorelse
+ | TacFail (n,l) ->
+ str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
+ prlist (pr_arg (pr_message_token pr_ident)) l, latom
+ | TacFirst tl ->
+ str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+ | TacSolve tl ->
+ str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
+ | TacComplete t ->
+ str "complete" ++ spc () ++ pr_tac env (lcomplete,E) t, lcomplete
+ | TacId l ->
+ str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
+ | TacAtom (loc,TacAlias (_,s,l,_)) ->
+ pr_with_comments loc
+ (pr_extend env (level_of inherited) s (List.map snd l)),
+ latom
+ | TacAtom (loc,t) ->
+ pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
+ | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom
+ | TacArg(ConstrMayEval (ConstrTerm c)) ->
+ str "constr:" ++ pr_constr env c, latom
+ | TacArg(ConstrMayEval c) ->
+ pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
+ | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom
+ | TacArg(Integer n) -> int n, latom
+ | TacArg(TacCall(loc,f,l)) ->
+ pr_with_comments loc
+ (hov 1 (pr_ref f ++ spc () ++
+ prlist_with_sep spc (pr_tacarg env) l)),
+ lcall
+ | TacArg a -> pr_tacarg env a, latom
+ in
+ if prec_less prec inherited then strm
+ else str"(" ++ strm ++ str")"
+
+and pr_tacarg env = function
+ | TacDynamic (loc,t) ->
+ pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>"))
+ | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s))
+ | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
| TacVoid -> str "()"
| Reference r -> pr_ref r
- | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c
- | ConstrMayEval c -> pr_may_eval pr_constr pr_cst c
- | Integer n -> int n
- | TacFreshId sopt -> str "FreshId" ++ pr_opt qstring sopt
- | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")"
-
-and pr_tacarg1 = function
- | TacCall (_,f,l) ->
- hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
- | Tacexp t -> pr_tac t
- | t -> pr_tacarg0 t
-
-and pr_tacarg x = pr_tacarg1 x
-
-and prtac x = pr6 x
-
-in (prtac,pr0,pr_match_rule false pr_pat pr_tac)
-
-let pr_raw_extend prc prlc prtac =
- pr_extend_gen (pr_raw_generic prc prlc prtac Ppconstrnew.pr_reference)
-let pr_glob_extend prc prlc prtac =
- pr_extend_gen (pr_glob_generic prc prlc prtac)
-let pr_extend prc prlc prtac =
- pr_extend_gen (pr_generic prc prlc prtac)
+ | ConstrMayEval c ->
+ pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
+ | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt
+ | TacExternal (_,com,req,la) ->
+ str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
+ spc() ++ prlist_with_sep spc (pr_tacarg env) la
+ | (TacCall _|Tacexp _|Integer _) as a ->
+ str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
+
+in (pr_tac, pr_match_rule)
+
+let strip_prod_binders_rawterm n (ty,_) =
+ let rec strip_ty acc n ty =
+ if n=0 then (List.rev acc, (ty,None)) else
+ match ty with
+ Rawterm.RProd(loc,na,a,b) ->
+ strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+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 (([dummy_loc,na],a)::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+let drop_env f _env = f
+
+let rec raw_printers =
+ (pr_raw_tactic_level,
+ drop_env pr_constr_expr,
+ drop_env pr_lconstr_expr,
+ pr_pattern_expr,
+ drop_env pr_reference,
+ drop_env pr_reference,
+ pr_reference,
+ pr_or_metaid pr_lident,
+ pr_raw_extend,
+ strip_prod_binders_expr)
+
+and pr_raw_tactic_level env n (t:raw_tactic_expr) =
+ fst (make_pr_tac raw_printers) env n t
+
+and pr_raw_match_rule env t =
+ snd (make_pr_tac raw_printers) env t
let pr_and_constr_expr pr (c,_) = pr c
let rec glob_printers =
- (pr_glob_tactic,
- pr_glob_tactic0,
- pr_and_constr_expr Printer.pr_rawterm,
- Printer.pr_pattern,
- pr_or_var (pr_and_short_name pr_evaluable_reference),
- pr_or_var pr_inductive,
- pr_or_var (pr_located pr_ltac_constant),
- pr_located pr_id,
- pr_glob_extend)
-
-and pr_glob_tactic (t:glob_tactic_expr) = pi1 (make_pr_tac glob_printers) t
-
-and pr_glob_tactic0 t = pi2 (make_pr_tac glob_printers) t
-
-and pr_glob_match_context t = pi3 (make_pr_tac glob_printers) t
-
-let (pr_tactic,_,_) =
+ (pr_glob_tactic_level,
+ (fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
+ (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
+ (fun c -> pr_constr_pattern_env (Global.env()) c),
+ (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
+ (fun env -> pr_or_var (pr_inductive env)),
+ pr_ltac_or_var (pr_located pr_ltac_constant),
+ pr_lident,
+ pr_glob_extend,
+ strip_prod_binders_rawterm)
+
+and pr_glob_tactic_level env n (t:glob_tactic_expr) =
+ fst (make_pr_tac glob_printers) env n t
+
+and pr_glob_match_rule env t =
+ snd (make_pr_tac glob_printers) env t
+
+let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) =
make_pr_tac
- (pr_glob_tactic,
- pr_glob_tactic0,
- Printer.prterm,
- Printer.pr_pattern,
- pr_evaluable_reference,
+ (pr_glob_tactic_level,
+ pr_constr_env,
+ pr_lconstr_env,
+ pr_constr_pattern,
+ pr_evaluable_reference_env,
pr_inductive,
pr_ltac_constant,
pr_id,
- pr_extend)
+ pr_extend,
+ strip_prod_binders_constr)
+
+let pr_raw_tactic env = pr_raw_tactic_level env ltop
+let pr_glob_tactic env = pr_glob_tactic_level env ltop
+let pr_tactic env = pr_tactic_level env ltop
+
+let _ = Tactic_debug.set_tactic_printer
+ (fun x -> pr_glob_tactic (Global.env()) x)
+
+let _ = Tactic_debug.set_match_pattern_printer
+ (fun env hyp -> pr_match_pattern (pr_constr_pattern_env env) hyp)
+
+let _ = Tactic_debug.set_match_rule_printer
+ (fun rl ->
+ pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl)