Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.

Re-add, in fact, since it was there in v8.3 but was dead code in v8.4 hence was deleted. It is necessary for printing info traces, however. A lot of the code had changed since v8.3, so adapting the code was non-trivial and some thing may be printed wrong.

It require re-adding a [tacexpr] argument to [gen_tactic_expr]. It had been made obsolete by the deletion of [pr_tactic] in v8.4 (even though printing [glob_tactic_expr] in a [tactic_expr] is only an approximation of the appropriate behaviour).

A new kind of argument, [delayed_constr], has made an appearance between v8.4 and trunk, and it differs from [constr] in the typed level. So it required its own parameter in [gen_tactic_expr]. At this point [delayed_constr] are printed in the globalised level because they are interpreted as closures. Maybe a better approximation is warranted.

Both in the printing of rewrite and induction, I changed a [pr_lconstr] (note the 'l') by a [pr_dconstr]. It is probably not quite correct, and may need fixing (adding a [pr_dlconstr] to [Pptactics] I guess?).

3 files changed, 154 insertions, 44 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index c8c7e28e9..7844f74e2 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -42,11 +42,11 @@ type inversion_kind =
   | FullInversion
   | FullInversionClear
 
-type ('c,'id) inversion_strength =
+type ('c,'d,'id) inversion_strength =
   | NonDepInversion of
-      inversion_kind * 'id list * 'c or_and_intro_pattern_expr located or_var option
+      inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option
   | DepInversion of
-      inversion_kind * 'c option * 'c or_and_intro_pattern_expr located or_var option
+      inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -56,14 +56,14 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
-type ('constr,'id) induction_clause =
-    'constr with_bindings induction_arg *
+type ('dconstr,'id) induction_clause =
+    'dconstr with_bindings induction_arg *
     (intro_pattern_naming_expr located option (* eqn:... *)
-    * 'constr or_and_intro_pattern_expr located or_var option) (* as ... *)
+    * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
-type ('constr,'id) induction_clause_list =
-    ('constr,'id) induction_clause list
+type ('constr,'dconstr,'id) induction_clause_list =
+    ('dconstr,'id) induction_clause list
     * 'constr with_bindings option (* using ... *)
 
 type 'a with_bindings_arg = clear_flag * 'a with_bindings
@@ -121,11 +121,11 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
-  | TacIntroPattern of 'trm intro_pattern_expr located list
+  | TacIntroPattern of 'dtrm intro_pattern_expr located list
   | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      (clear_flag * 'nam * 'trm intro_pattern_expr located option) option
+      (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacFix of Id.t option * int
@@ -133,8 +133,8 @@ type 'a gen_atomic_tactic_expr =
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * 'a gen_tactic_expr option *
-      'trm intro_pattern_expr located option * 'trm
+      bool * 'tacexpr option *
+      'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacGeneralizeDep of 'trm
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
@@ -142,7 +142,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
-      rec_flag * evars_flag * ('trm,'nam) induction_clause_list
+      rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Automation tactics *)
@@ -160,23 +160,32 @@ type 'a gen_atomic_tactic_expr =
 
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
-  | TacChange of 'pat option * 'trm * 'nam clause_expr
+  | TacChange of 'pat option * 'dtrm * 'nam clause_expr
 
   (* Equivalence relations *)
   | TacSymmetry of 'nam clause_expr
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr *
-      'a gen_tactic_expr option
-  | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
+      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (* spiwack: using ['dtrm] here is a small hack, may not be
+         stable by a change in the representation of delayed
+         terms. Because, in fact, it is the whole "with_bindings"
+         which is delayed. But because the "t" level for ['dtrm] is
+         uninterpreted, it works fine here too, and avoid more
+         disruption of this file. *)
+      'tacexpr option
+  | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis
 
 constraint 'a = <
     term:'trm;
+    utrm: 'utrm;
+    dterm: 'dtrm;
     pattern:'pat;
     constant:'cst;
     reference:'ref;
     name:'nam;
+    tacexpr:'tacexpr;
     level:'lev
 >
 
@@ -187,24 +196,24 @@ and 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
-  | UConstr        of 'trm  (* We can reuse ['trm] because terms and untyped terms
-                               only differ at interpretation time (and not at
-                               internalisation), and the output of interpration
-                               is not a variant of [tactic_expr]. *)
+  | UConstr        of 'utrm
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       'a gen_tactic_arg list
   | TacFreshId of string or_var list
-  | Tacexp of 'a gen_tactic_expr
+  | Tacexp of 'tacexpr
   | TacPretype of 'trm
   | TacNumgoals
 
 constraint 'a = <
     term:'trm;
+    utrm: 'utrm;
+    dterm: 'dtrm;
     pattern:'pat;
     constant:'cst;
     reference:'ref;
     name:'nam;
+    tacexpr:'tacexpr;
     level:'lev
 >
 
@@ -273,10 +282,13 @@ and 'a gen_tactic_expr =
 
 constraint 'a = <
     term:'t;
+    utrm: 'utrm;
+    dterm: 'dtrm;
     pattern:'p;
     constant:'c;
     reference:'r;
     name:'n;
+    tacexpr:'tacexpr;
     level:'l
 >
 
@@ -285,16 +297,20 @@ and 'a gen_tactic_fun_ast =
 
 constraint 'a = <
     term:'t;
+    utrm: 'utrm;
+    dterm: 'dtrm;
     pattern:'p;
     constant:'c;
     reference:'r;
     name:'n;
+    tacexpr:'te;
     level:'l
 >
 
 (** Globalized tactics *)
 
 type g_trm = glob_constr_and_expr
+type g_utrm = g_trm
 type g_pat = glob_constr_and_expr * constr_pattern
 type g_cst = evaluable_global_reference and_short_name or_var
 type g_ref = ltac_constant located or_var
@@ -302,14 +318,17 @@ type g_nam  = Id.t located
 
 type g_dispatch =  <
     term:g_trm;
+    utrm:g_utrm;
+    dterm:g_trm;
     pattern:g_pat;
     constant:g_cst;
     reference:g_ref;
     name:g_nam;
+    tacexpr:glob_tactic_expr;
     level:glevel
 >
 
-type glob_tactic_expr =
+and glob_tactic_expr =
     g_dispatch gen_tactic_expr
 
 type glob_atomic_tactic_expr =
@@ -321,6 +340,7 @@ type glob_tactic_arg =
 (** Raw tactics *)
 
 type r_trm = constr_expr
+type r_utrm = r_trm
 type r_pat = constr_pattern_expr
 type r_cst = reference or_by_notation
 type r_ref = reference
@@ -329,22 +349,55 @@ type r_lev = rlevel
 
 type r_dispatch =  <
     term:r_trm;
+    utrm:r_utrm;
+    dterm:r_trm;
     pattern:r_pat;
     constant:r_cst;
     reference:r_ref;
     name:r_nam;
+    tacexpr:raw_tactic_expr;
     level:rlevel
 >
 
+and raw_tactic_expr =
+    r_dispatch gen_tactic_expr
+
 type raw_atomic_tactic_expr =
     r_dispatch gen_atomic_tactic_expr
 
-type raw_tactic_expr =
-    r_dispatch gen_tactic_expr
-
 type raw_tactic_arg =
     r_dispatch gen_tactic_arg
 
+(** Interpreted tactics *)
+
+type t_trm = Term.constr
+type t_utrm = Glob_term.closed_glob_constr
+type t_pat = glob_constr_and_expr * constr_pattern
+type t_cst = evaluable_global_reference and_short_name
+type t_ref = ltac_constant located
+type t_nam  = Id.t
+
+type t_dispatch =  <
+    term:t_trm;
+    utrm:t_utrm;
+    dterm:g_trm;
+    pattern:t_pat;
+    constant:t_cst;
+    reference:t_ref;
+    name:t_nam;
+    tacexpr:glob_tactic_expr;
+    level:tlevel
+>
+
+type tactic_expr =
+    t_dispatch gen_tactic_expr
+
+type atomic_tactic_expr =
+    t_dispatch gen_atomic_tactic_expr
+
+type tactic_arg =
+    t_dispatch gen_tactic_arg
+
 (** Misc *)
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e6fda4b59..cb64c712d 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -321,6 +321,8 @@ let pr_raw_alias prc prlc prtac prpat =
   pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
 let pr_glob_alias prc prlc prtac prpat =
   pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+let pr_alias prc prlc prtac prpat =
+  pr_alias_gen (pr_top_generic prc prlc prtac prpat)
 
 (**********************************************************************)
 (* The tactic printer                                                 *)
@@ -413,21 +415,21 @@ 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 _prlc ipat c = match ipat with
+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 prc ipat
+      spc() ++ prc c ++ pr_as_ipat prdc ipat
 
-let pr_assumption prc prlc ipat c = match ipat with
+let pr_assumption prc prdc prlc ipat c = match ipat with
 (* Use this "optimisation" or use only the general case ?*)
 (* it seems that this "optimisation" is somehow more natural *)
   | Some (_,IntroNaming (IntroIdentifier id)) ->
       spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
   | ipat ->
-      spc() ++ prc c ++ pr_as_ipat prc ipat
+      spc() ++ prc c ++ pr_as_ipat prdc ipat
 
 let pr_by_tactic prt = function
   | TacId [] -> mt ()
@@ -611,9 +613,11 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
     "raw", "glob" and "typed" levels *)
 
 type 'a printer = {
-  pr_tactic : tolerability -> 'a gen_tactic_expr -> std_ppcmds;
+  pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
   pr_constr : 'trm -> std_ppcmds;
+  pr_uconstr: 'utrm -> std_ppcmds;
   pr_lconstr : 'trm -> std_ppcmds;
+  pr_dconstr: 'dtrm -> std_ppcmds;
   pr_pattern : 'pat -> std_ppcmds;
   pr_lpattern : 'pat -> std_ppcmds;
   pr_constant : 'cst -> std_ppcmds;
@@ -626,10 +630,13 @@ type 'a printer = {
 
 constraint 'a = <
     term:'trm;
+    utrm:'utrm;
+    dterm:'dtrm;
     pattern:'pat;
     constant:'cst;
     reference:'ref;
     name:'nam;
+    tacexpr:'tacexpr;
     level:'lev
 >
 
@@ -640,6 +647,7 @@ let make_pr_tac pr
 let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
 let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in
 let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+let pr_with_bindings_arg_full = pr_with_bindings_arg in
 let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
 let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
 
@@ -712,7 +720,7 @@ and pr_atom1 = function
   | TacIntroPattern [] as t -> pr_atom0 t
   | TacIntroPattern (_::_ as p) ->
       hov 1 (str "intros" ++ spc () ++
-             prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_constr) p)
+             prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
   | TacIntroMove (None,MoveLast) as t -> pr_atom0 t
   | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
   | TacIntroMove (ido,hto) ->
@@ -723,7 +731,7 @@ and pr_atom1 = function
       hov 1 ((if a then mt() else str "simple ") ++
              str (with_evars ev "apply") ++ spc () ++
              prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-             pr_in_hyp_as pr.pr_constr pr.pr_name inhyp)
+             pr_in_hyp_as pr.pr_dconstr pr.pr_name inhyp)
   | TacElim (ev,cb,cbo) ->
       hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings_arg cb ++
         pr_opt pr_eliminator cbo)
@@ -739,11 +747,11 @@ and pr_atom1 = function
              str"with " ++ prlist_with_sep spc pr_cofix_tac l)
   | TacAssert (b,Some tac,ipat,c) ->
       hov 1 (str (if b then "assert" else "enough") ++
-             pr_assumption pr.pr_constr pr.pr_lconstr ipat c ++
+             pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
              pr_by_tactic (pr.pr_tactic ltop) tac)
   | TacAssert (_,None,ipat,c) ->
       hov 1 (str "pose proof" ++
-             pr_assertion pr.pr_constr pr.pr_lconstr ipat c)
+             pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
              prlist_with_sep pr_comma (fun (cl,na) ->
@@ -775,8 +783,8 @@ and pr_atom1 = function
       hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
              spc () ++
              prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
-	       pr_clear_flag clear_flag (pr_induction_arg pr.pr_constr pr.pr_lconstr) h ++
-	       pr_with_induction_names pr.pr_constr ids ++
+	       pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+	       pr_with_induction_names pr.pr_dconstr ids ++
 	     pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
              pr_opt pr_eliminator el)
   | TacDoubleInduction (h1,h2) ->
@@ -828,7 +836,7 @@ and pr_atom1 = function
       (match op with
           None -> mt()
         | Some p -> pr.pr_pattern p ++ spc () ++ str "with ") ++
-      pr.pr_constr c ++ pr_clauses (Some true) pr.pr_name h)
+      pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h)
 
   (* Equivalence relations *)
   | TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr.pr_name cls
@@ -839,18 +847,19 @@ and pr_atom1 = function
 	     prlist_with_sep
 	     (fun () -> str ","++spc())
 	     (fun (b,m,c) ->
-		pr_orient b ++ pr_multi m ++ pr_with_bindings_arg c)
+		pr_orient b ++ pr_multi m ++
+                pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
 	     l
 	     ++ pr_clauses (Some true) pr.pr_name cl
 	     ++	(match by with Some by -> pr_by_tactic (pr.pr_tactic ltop) by | None -> mt()))
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-      pr_with_inversion_names pr.pr_constr ids ++ pr_with_constr pr.pr_constr c)
+      pr_with_inversion_names pr.pr_dconstr ids ++ pr_with_constr pr.pr_constr c)
   | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
       hov 1 (pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-      pr_with_inversion_names pr.pr_constr ids ++ pr_simple_hyp_clause pr.pr_name cl)
+      pr_with_inversion_names pr.pr_dconstr ids ++ pr_simple_hyp_clause pr.pr_name cl)
   | TacInversion (InversionUsing (c,cl),hyp) ->
       hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++
       spc () ++ str "using" ++ spc () ++ pr.pr_constr c ++
@@ -992,7 +1001,7 @@ and pr_tacarg = function
   | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s))
   | Reference r -> pr.pr_reference r
   | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
-  | UConstr c -> str"uconstr:" ++ pr.pr_constr c
+  | UConstr c -> str"uconstr:" ++ pr.pr_uconstr c
   | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
   | TacPretype c -> str "type_term" ++ pr.pr_constr c
   | TacNumgoals -> str "numgoals"
@@ -1017,6 +1026,8 @@ let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
   let pr = {
     pr_tactic = pr_raw_tactic_level;
     pr_constr = pr_constr_expr;
+    pr_uconstr = pr_constr_expr;
+    pr_dconstr = pr_constr_expr;
     pr_lconstr = pr_lconstr_expr;
     pr_pattern = pr_constr_pattern_expr;
     pr_lpattern = pr_lconstr_pattern_expr;
@@ -1035,7 +1046,7 @@ 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 =
+let rec pr_glob_tactic_level env n t =
   let glob_printers =
     (strip_prod_binders_glob_constr)
   in
@@ -1043,6 +1054,8 @@ let pr_glob_tactic_level env =
     let pr = {
       pr_tactic = prtac;
       pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
+      pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
+      pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
       pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
       pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
       pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
@@ -1059,10 +1072,52 @@ let pr_glob_tactic_level env =
     } in
     make_pr_tac pr glob_printers n t
   in
-  prtac
+  prtac n t
 
 let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
+
+let strip_prod_binders_constr n ty =
+  let rec strip_ty acc n ty =
+    if n=0 then (List.rev acc, ty) else
+      match Term.kind_of_term ty with
+          Term.Prod(na,a,b) ->
+            strip_ty (([Loc.ghost,na],a)::acc) (n-1) b
+        | _ -> error "Cannot translate fix tactic: not enough products" in
+  strip_ty [] n ty
+
+let pr_tactic_level env n t =
+  let typed_printers =
+    (strip_prod_binders_constr)
+  in
+  let prtac n (t:tactic_expr) =
+    let pr = {
+      pr_tactic = pr_glob_tactic_level env;
+      pr_constr = pr_constr_env env Evd.empty;
+      pr_uconstr = (fun _ -> mt ()); (* arnaud: todo *)
+      pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
+      pr_lconstr = pr_lconstr_env env Evd.empty;
+      pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
+      pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+      pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+      pr_reference = pr_located pr_ltac_constant;
+      pr_name = pr_id;
+      pr_generic = Genprint.generic_top_print;
+      pr_extend = pr_extend
+        (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+        (pr_glob_tactic_level env) pr_constr_pattern;
+      pr_alias = pr_alias
+        (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+        (pr_glob_tactic_level env) pr_constr_pattern;
+    }
+    in
+    make_pr_tac pr typed_printers n t
+  in
+  prtac n t
+
+let pr_tactic env = pr_tactic_level env ltop
+
+
 (** Registering *)
 
 let () =
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 6c2f43cb6..f76e5a3f6 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -105,6 +105,8 @@ val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
 
 val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
+val pr_tactic : env -> tactic_expr -> std_ppcmds
+
 val pr_hintbases : string list option -> std_ppcmds
 
 val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds