programs: pretty-printer moved to new module Pgmpretty_

Makefile.in

@@ -284,8 +284,8 @@ install_no_local::
 
 PGMGENERATED = 
 
-PGM_FILES = pgm_ttree \
-	    pgm_types pgm_module pgm_wp pgm_env pgm_typing pgm_main
+PGM_FILES = pgm_ttree pgm_types pgm_pretty \
+	    pgm_module pgm_wp pgm_env pgm_typing pgm_main
 
 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 

src/programs/pgm_pretty.ml

+
+open Format
+open Why
+open Pp
+open Ident
+open Term
+open Pretty
+open Pgm_types.T
+open Pgm_ttree
+
+(* pretty-printing (for debugging) *)
+
+let rec print_expr fmt e = match e.expr_desc with
+  | Elogic t ->
+      fprintf fmt "@[<hov 2><term: %a>@]" Pretty.print_term t
+  | Elocal v ->
+      fprintf fmt "%a" print_pv v
+  | Eglobal ls ->
+      fprintf fmt "<global %a>" print_ls ls.p_ls
+  | Efun (bl, t) ->
+      fprintf fmt "@[fun %a ->@ %a@]" 
+	(print_list space print_pv) bl print_triple t
+  | Elet (v, e1, e2) ->
+      fprintf fmt "@[<hv 0>@[<hov 2>let %a =@ %a in@]@ %a@]" print_vs v.pv_vs
+	print_expr e1 print_expr e2
+
+  | Eif (e1, e2, e3) ->
+      fprintf fmt "@[if %a@ then@ %a else@ %a@]"
+	print_expr e1 print_expr e2 print_expr e3
+
+  | Eany c ->
+      fprintf fmt "@[[any %a]@]" print_type_c c
+
+  | Elabel (_, _)  ->
+      fprintf fmt "<todo: Elabel>"
+  | Eassert (_, _) ->
+      fprintf fmt "<todo: Eassert>"
+  | Efor (_, _, _, _, _, _) ->
+      fprintf fmt "<todo: Efor>"
+  | Etry (_, _) ->
+      fprintf fmt "<todo: Etry>"
+  | Eraise (_, _)  ->
+      fprintf fmt "<todo: Eraise>"
+  | Ematch (v, cl) ->
+      fprintf fmt "@[<hov 2>match %a with@ %a@]" print_pv v
+	(print_list newline print_branch) cl
+  | Eloop (_, _) ->
+      fprintf fmt "<todo: Eloop>"
+  | Eletrec (_, _)  ->
+      fprintf fmt "<todo: Eletrec>"
+  | Eabsurd ->
+      fprintf fmt "absurd"
+
+and print_pv fmt v =
+  fprintf fmt "<%s : %a/%a>" 
+    v.pv_name.id_string print_ty v.pv_ty print_vs v.pv_vs
+
+and print_triple fmt (p, e, q) =
+  fprintf fmt "@[<hv 0>%a@ %a@ %a@]" print_pre p print_expr e print_post q
+
+and print_recfun fmt (v, bl, _, t) =
+  fprintf fmt "@[<hov 2>rec %a@ %a =@ %a@]" 
+    print_pv v (print_list space print_pv) bl print_triple t
+
+and print_branch fmt (p, e) =
+  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pattern p print_expr e
+
+and print_pattern fmt p = 
+  Pretty.print_pat fmt p.ppat_pat
+

src/programs/pgm_pretty.mli

+
+
+val print_expr : Format.formatter -> Pgm_ttree.expr -> unit
+
+val print_recfun : Format.formatter -> Pgm_ttree.recfun -> unit

src/programs/pgm_typing.ml

@@ -1472,66 +1472,6 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
 and fresh_triple gl (_, e, _) =
   fresh_expr gl ~term:true Sid.empty e
 
-(* pretty-printing (for debugging) *)
-
-let rec print_expr fmt e = match e.expr_desc with
-  | Elogic t ->
-      fprintf fmt "@[<hov 2><term: %a>@]" Pretty.print_term t
-  | Elocal v ->
-      fprintf fmt "%a" print_pv v
-  | Eglobal ls ->
-      fprintf fmt "<global %a>" print_ls ls.p_ls
-  | Efun (bl, t) ->
-      fprintf fmt "@[fun %a ->@ %a@]" 
-	(print_list space print_pv) bl print_triple t
-  | Elet (v, e1, e2) ->
-      fprintf fmt "@[<hv 0>@[<hov 2>let %a =@ %a in@]@ %a@]" print_vs v.pv_vs
-	print_expr e1 print_expr e2
-
-  | Eif (e1, e2, e3) ->
-      fprintf fmt "@[if %a@ then@ %a else@ %a@]"
-	print_expr e1 print_expr e2 print_expr e3
-
-  | Eany c ->
-      fprintf fmt "@[[any %a]@]" print_type_c c
-
-  | Elabel (_, _)  ->
-      fprintf fmt "<todo: Elabel>"
-  | Eassert (_, _) ->
-      fprintf fmt "<todo: Eassert>"
-  | Efor (_, _, _, _, _, _) ->
-      fprintf fmt "<todo: Efor>"
-  | Etry (_, _) ->
-      fprintf fmt "<todo: Etry>"
-  | Eraise (_, _)  ->
-      fprintf fmt "<todo: Eraise>"
-  | Ematch (v, cl) ->
-      fprintf fmt "@[<hov 2>match %a with@ %a@]" print_pv v
-	(print_list newline print_branch) cl
-  | Eloop (_, _) ->
-      fprintf fmt "<todo: Eloop>"
-  | Eletrec (_, _)  ->
-      fprintf fmt "<todo: Eletrec>"
-  | Eabsurd ->
-      fprintf fmt "absurd"
-
-and print_pv fmt v =
-  fprintf fmt "<%s : %a/%a>" 
-    v.pv_name.id_string print_ty v.pv_ty print_vs v.pv_vs
-
-and print_triple fmt (p, e, q) =
-  fprintf fmt "@[<hv 0>%a@ %a@ %a@]" T.print_pre p print_expr e T.print_post q
-
-and print_recfun fmt (v, bl, _, t) =
-  fprintf fmt "@[<hov 2>rec %a@ %a =@ %a@]" 
-    print_pv v (print_list space print_pv) bl print_triple t
-
-and print_branch fmt (p, e) =
-  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pattern p print_expr e
-
-and print_pattern fmt p = 
-  Pretty.print_pat fmt p.ppat_pat
-
 (* typing declarations (combines the three phases together) *)
 
 let create_ienv denv = {
@@ -1629,7 +1569,7 @@ let rec decl ~wp env penv lmod uc = function
       let e = type_expr uc e in
       if Debug.test_flag debug then
 	eprintf "@[--typing %s-----@\n  %a@\n%a@]@."
-	  id.id print_expr e print_type_v e.expr_type_v;
+	  id.id Pgm_pretty.print_expr e print_type_v e.expr_type_v;
       let ls, uc = add_global id.id_loc id.id e.expr_type_v uc in
       let d = Dlet (ls, e) in
       let uc = add_decl d uc in
@@ -1645,7 +1585,7 @@ let rec decl ~wp env penv lmod uc = function
 	let id = v.pv_name.id_string in
 	if Debug.test_flag debug then
           eprintf "@[--typing %s-----@\n  %a@.%a@]@."
-	    id print_recfun d print_type_v tyv;
+	    id Pgm_pretty.print_recfun d print_type_v tyv;
 	let ps, uc = add_global loc id tyv uc in
 	uc, (ps, d)
       in

src/programs/pgm_typing.mli

@@ -25,4 +25,3 @@ val debug : Debug.flag
 val decl : 
   wp:bool -> Env.env -> Pgm_env.t -> Pgm_module.t Pgm_module.Mnm.t -> 
   Pgm_module.uc -> Ptree.program_decl -> Pgm_module.uc
-

src/programs/pgm_wp.ml

@@ -259,13 +259,16 @@ let t_True env =
   t_app (find_ls env "True") [] (ty_app (find_ts env "bool") [])
 
 let rec wp_expr env e q =
-  if Debug.test_flag debug then
-    eprintf "@[wp_expr: q=%a@]@." Pretty.print_fmla (snd (fst q));
   let lab = fresh_label env in
   let q = post_map (old_label env lab) q in
   let f = wp_desc env e q in
   let f = erase_label env lab f in
-  propose_label (label ~loc:e.expr_loc "WP") f
+  let f = propose_label (label ~loc:e.expr_loc "WP") f in
+  if Debug.test_flag debug then
+    eprintf "@[--------@\n@[<hov 2>e = %a@]@\n@[<hov 2>q = %a@]@\n----@]@." 
+      Pgm_pretty.print_expr e
+      Pretty.print_fmla (snd (fst q));
+  f
 
 and wp_desc env e q = match e.expr_desc with
   | Elogic t ->