app_node, stack, state printers

7 files changed, 43 insertions, 8 deletions

diff --git a/dev/base_include b/dev/base_include
index 06a62abce..62574a593 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -42,6 +42,7 @@
 #install_printer  (* Cpred.t *) pp_cpred;;
 #install_printer ppzipper;;
 #install_printer ppstack;;
+#install_printer (* Reductionops.Stack.t *) pp_stack_t;;
 #install_printer ppatom;;
 #install_printer ppwhd;;
 #install_printer ppvblock;;
diff --git a/dev/db b/dev/db
index 7d738cd10..ca37bd0a3 100644
--- a/dev/db
+++ b/dev/db
@@ -28,6 +28,7 @@ install_printer Top_printers.ppconstraints
 install_printer Top_printers.pptype
 install_printer Top_printers.ppj
 install_printer Top_printers.ppenv
+install_printer Top_printers.pp_stack_t
 
 install_printer Top_printers.ppmetas
 install_printer Top_printers.ppevm
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 9f39496de..82155a305 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -116,6 +116,7 @@ let prdelta s = pp (Mod_subst.debug_pr_delta s)
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
+let pp_stack_t n = pp (Reductionops.Stack.pr Termops.print_constr n)
 
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 32c57694b..a9ab64190 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,6 +29,9 @@ exception Elimconst
 
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 module Stack = struct
+  let pr_app_node pr node =
+    let open Pp in surround (prlist_with_sep pr_comma pr node)
+
   type 'a member =
   | App of 'a list
   | Case of case_info * 'a * 'a array * ('a * 'a list) option
@@ -37,6 +40,24 @@ module Stack = struct
   | Update of 'a
   and 'a t = 'a member list
 
+  let rec pr_member pr_c member =
+    let open Pp in
+    let pr_c x = hov 1 (pr_c x) in
+    match member with
+    | App app -> str "ZApp" ++ pr_app_node pr_c app
+    | Case (_,_,br,cst) ->
+       str "ZCase(" ++
+	 prvect_with_sep (pr_bar) pr_c br
+       ++ str ")"
+    | Fix (f,args,cst) ->
+       str "ZFix(" ++ Termops.pr_fix Termops.print_constr f
+       ++ pr_comma () ++ pr pr_c args ++ str ")"
+    | Shift i -> str "ZShift(" ++ int i ++ str ")"
+    | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")"
+  and pr pr_c l =
+    let open Pp in
+    prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
+
   let compare_shape stk1 stk2 =
     let rec compare_rec bal stk1 stk2 =
       match (stk1,stk2) with
@@ -194,6 +215,10 @@ type  contextual_state_reduction_function =
 type  state_reduction_function =  contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
+let pr_state (tm,sk) =
+  let open Pp in
+  h 0 (Termops.print_constr tm ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr sk)
+
 (*************************************)
 (*** Reduction Functions Operators ***)
 (*************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7b9eb68d5..6c5d9e485 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -29,6 +29,8 @@ module Stack : sig
   | Update of 'a
   and 'a t = 'a member list
 
+  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+
   val empty : 'a t
   val compare_shape : 'a t -> 'a t -> bool
   (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
@@ -77,6 +79,8 @@ type contextual_state_reduction_function =
 type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
+val pr_state : state -> Pp.std_ppcmds
+
 (** {6 Machinery about a stack of unfolded constant }
 
     cst applied to params must convertible to term of the state applied to args
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 8d2234022..781bd599c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -35,6 +35,15 @@ let pr_name = function
 
 let pr_con sp = str(string_of_con sp)
 
+let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
+  let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
+  hov 1
+      (str"fix " ++ int i ++ spc() ++  str"{" ++
+         v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
+           pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+	   cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+         str"}")
+
 let rec pr_constr c = match kind_of_term c with
   | Rel n -> str "#"++int n
   | Meta n -> str "Meta(" ++ int n ++ str ")"
@@ -71,14 +80,7 @@ let rec pr_constr c = match kind_of_term c with
              pr_constr c ++ str"of") ++ cut() ++
        prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
       cut() ++ str"end")
-  | Fix ((t,i),(lna,tl,bl)) ->
-      let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
-      hov 1
-        (str"fix " ++ int i ++ spc() ++  str"{" ++
-         v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
-           pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
-           cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
-         str"}")
+  | Fix f -> pr_fix pr_constr f
   | CoFix(i,(lna,tl,bl)) ->
       let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
       hov 1
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 1aa7d9e9e..d9213fc13 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -29,6 +29,7 @@ val refresh_universes_strict : types -> types
 (** printers *)
 val print_sort : sorts -> std_ppcmds
 val pr_sort_family : sorts_family -> std_ppcmds
+val pr_fix : (constr -> std_ppcmds) -> fixpoint -> std_ppcmds
 
 (** debug printer: do not use to display terms to the casual user... *)
 val set_print_constr : (env -> constr -> std_ppcmds) -> unit