Ity, Expr: pretty-printing

src/mlw/expr.ml

@@ -1029,14 +1029,18 @@ and print_enode pri fmt e = match e.e_node with
   | Esym s -> print_ps fmt s
   | Efun e1 ->
       let c = cty_of_expr e in
-      if c.cty_args = [] then
-        fprintf fmt "@[<hov 2>abstract%a@\n%a@]@\nend"
-          print_cty_head c print_expr e1
-      else
-        fprintf fmt "@[<hov 2>fun %a ->@\n%a@]"
-          print_cty_head c print_expr e1
-  | Eany ->
-      fprintf fmt "@[<hov 2>any %a@]" print_cty (cty_of_expr e)
+      fprintf fmt "@[<hov 2>fun%a ->@\n%a@]"
+        (print_spec c.cty_args c.cty_pre c.cty_post c.cty_xpost
+          Spv.empty eff_empty) None print_expr e1
+  | Eany -> fprintf fmt "@[<hov 2>any%a@]" print_cty (cty_of_expr e)
+  | Eapp ({e_node = Efun e; e_vty = VtyC ({cty_args = []} as c)},[],_) ->
+      fprintf fmt "@[<hov 2>abstract%a@\n%a@]@\nend"
+        (print_spec [] c.cty_pre c.cty_post c.cty_xpost
+          Spv.empty eff_empty) None print_expr e
+  | Eapp ({e_node = Eany; e_vty = VtyC ({cty_args = []} as c)},[],_) ->
+      fprintf fmt "@[<hov 2>any %a%a@]" print_ity c.cty_result
+        (print_spec [] c.cty_pre c.cty_post c.cty_xpost
+          c.cty_reads c.cty_effect) None
   | Eapp (e,[],_) -> print_lexpr pri fmt e
   | Eapp ({e_node = Esym s},vl,_) when is_ps_tuple s ->
       fprintf fmt "(%a)" (Pp.print_list Pp.comma print_pv) vl
@@ -1135,7 +1139,7 @@ and print_let_defn fmt = function
         print_pv v print_id_labels v.pv_vs.vs_name
         (print_lexpr 0 (*4*)) e
   | {let_sym = ValS s; let_expr = {e_node = Efun e} as e0} ->
-      fprintf fmt "@[<hov 2>let %a@ %a =@\n%a@]"
+      fprintf fmt "@[<hov 2>let %a%a =@\n%a@]"
         print_ps_head s
         print_cty (cty_of_expr e0)
         (print_lexpr 0 (*4*)) e
@@ -1150,13 +1154,30 @@ and print_rec_defn fmt {rec_defn = fdl} =
 and print_rec_fun fst fmt fd =
   let e = match fd.fun_expr.e_node with
     | Efun e -> e | _ -> assert false in
-  fprintf fmt "@[<hov 2>%s %a@ %a%a =@\n%a@]"
+  fprintf fmt "@[<hov 2>%s %a%a%a =@\n%a@]"
     (if fst then "let rec" else "with")
     print_ps_head fd.fun_sym
     print_cty (cty_of_expr fd.fun_expr)
     print_variant fd.fun_varl
     (print_lexpr 0 (*4*)) e
 
+let print_val_decl fmt = function
+  | ValV v ->
+      fprintf fmt "@[<hov 2>val %s%a%a :@ %a@]"
+        (if v.pv_ghost then "ghost " else "")
+        print_pv v print_id_labels v.pv_vs.vs_name
+        print_ity v.pv_ity
+  | ValS ({ps_logic = PLpv v; ps_cty = c} as s) ->
+      fprintf fmt "@[<hov 2>val %a%a@]" print_ps_head s
+        (print_spec c.cty_args c.cty_pre (List.tl c.cty_post) c.cty_xpost
+          (Spv.remove v c.cty_reads) c.cty_effect) (Some c.cty_result)
+  | ValS ({ps_logic = PLls _; ps_cty = c} as s) ->
+      fprintf fmt "@[<hov 2>val %a%a@]" print_ps_head s
+        (print_spec c.cty_args c.cty_pre (List.tl c.cty_post) c.cty_xpost
+          c.cty_reads c.cty_effect) (Some c.cty_result)
+  | ValS s ->
+      fprintf fmt "@[<hov 2>val %a%a@]" print_ps_head s print_cty s.ps_cty
+
 (* exception handling *)
 
 let () = Exn_printer.register (fun fmt e -> match e with

src/mlw/expr.mli

@@ -255,12 +255,11 @@ val e_func_app_l : expr -> expr list -> expr
 
 (** {2 Pretty-printing} *)
 
-open Format
-
 val forget_ps  : psymbol -> unit (* flush id_unique for a program symbol *)
 
-val print_ps   : formatter -> psymbol -> unit     (* program symbol *)
-val print_expr : formatter -> expr -> unit        (* expression *)
+val print_ps   : Format.formatter -> psymbol -> unit  (* program symbol *)
+val print_expr : Format.formatter -> expr -> unit     (* expression *)
 
-val print_let_defn : formatter -> let_defn -> unit
-val print_rec_defn : formatter -> rec_defn -> unit
+val print_val_decl : Format.formatter -> val_decl -> unit
+val print_let_defn : Format.formatter -> let_defn -> unit
+val print_rec_defn : Format.formatter -> rec_defn -> unit

src/mlw/ity.ml

@@ -1058,7 +1058,7 @@ exception FoundPrefix of pvsymbol list
 
 let unknown = create_pvsymbol (id_fresh "?") ity_unit
 
-let print_cty_spec fmt c =
+let print_spec args pre post xpost rds eff fmt ity =
   let dot fmt () = pp_print_char fmt '.' in
   let print_pfx reg fmt pfx = fprintf fmt "@[%a:@,%a@]"
     (Pp.print_list dot print_pv) pfx print_reg reg in
@@ -1073,64 +1073,53 @@ let print_cty_spec fmt c =
         raise (FoundPrefix (unknown::pfx))
     | _ -> () in
   let find_prefix reg = try
-    List.iter (fun v -> find_prefix [v] reg v.pv_ity) c.cty_args;
-    Spv.iter (fun v -> find_prefix [v] reg v.pv_ity) c.cty_reads;
-    assert false (* cannot have an effect on an unknown region *)
-    with FoundPrefix pfx -> List.rev pfx in
-  let print_reads fmt pvl = if pvl <> [] then
-    fprintf fmt "@\nreads {%a}" (Pp.print_list Pp.comma print_pv) pvl in
-  let print_writes fmt c = if not (Mreg.is_empty c.cty_effect.eff_writes) then
-    let print_wr fmt (reg,fds) =
-      let pfx = find_prefix reg in
-      let print_fld fmt {pv_vs = {vs_name = id}} =
-        fprintf fmt "(%a).%s" (print_pfx reg) pfx id.id_string in
-      if Spv.is_empty fds then print_pfx reg fmt pfx else
-        Pp.print_list Pp.comma print_fld fmt (Spv.elements fds) in
-    fprintf fmt "@\nwrites {%a}" (Pp.print_list Pp.comma print_wr)
-      (Mreg.bindings c.cty_effect.eff_writes) in
-  let print_resets fmt c = if not (Mreg.is_empty c.cty_effect.eff_resets) then
-    let print_rs fmt (reg,cvr) =
-      let print_cvr fmt reg = print_pfx reg fmt (find_prefix reg) in
-      if Sreg.is_empty cvr then print_pfx reg fmt (find_prefix reg) else
-        fprintf fmt "%a@ (under %a)" (print_pfx reg) (find_prefix reg)
-          (Pp.print_list Pp.comma print_cvr) (Sreg.elements cvr) in
-    fprintf fmt "@\nresets {%a}" (Pp.print_list Pp.comma print_rs)
-      (Mreg.bindings c.cty_effect.eff_resets) in
-  let print_pre fmt p =
-    fprintf fmt "@\nrequires { @[%a@] }" print_term p in
+    List.iter (fun v -> find_prefix [v] reg v.pv_ity) args;
+    Spv.iter (fun v -> find_prefix [v] reg v.pv_ity) rds;
+    [unknown] with FoundPrefix pfx -> List.rev pfx in
+  let print_write fmt (reg,fds) =
+    let pfx = find_prefix reg in
+    let print_fld fmt {pv_vs = {vs_name = id}} =
+      fprintf fmt "(%a).%s" (print_pfx reg) pfx id.id_string in
+    if Spv.is_empty fds then print_pfx reg fmt pfx else
+      Pp.print_list Pp.comma print_fld fmt (Spv.elements fds) in
+  let print_raise fmt (reg,cvr) =
+    let print_cvr fmt reg = print_pfx reg fmt (find_prefix reg) in
+    if Sreg.is_empty cvr then print_pfx reg fmt (find_prefix reg) else
+      fprintf fmt "%a@ (under %a)" (print_pfx reg) (find_prefix reg)
+        (Pp.print_list Pp.comma print_cvr) (Sreg.elements cvr) in
+  let print_result fmt ity = fprintf fmt " :@ %a" print_ity ity in
+  let print_pre fmt p = fprintf fmt "@\nrequires { @[%a@] }" print_term p in
   let print_post fmt q =
     let v, q = open_post q in
     fprintf str_formatter "%a" print_vs v;
     let n = flush_str_formatter () in
-    begin if n = "result" || t_v_occurs v q = 0 then
+    if n = "result" || t_v_occurs v q = 0 then
       fprintf fmt "@\nensures  { @[%a@] }" print_term q else
-      fprintf fmt "@\nreturns  { %s ->@ @[%a@] }" n print_term q
-    end;
+      fprintf fmt "@\nreturns  { %s ->@ @[%a@] }" n print_term q;
     forget_var v in
   let print_xpost xs fmt q =
     let v, q = open_post q in
-    begin if ty_equal v.vs_ty ty_unit && t_v_occurs v q = 0 then
-      fprintf fmt "@\nraises   { %a ->@ @[%a@] }"
-        print_xs xs print_term q else
-      fprintf fmt "@\nraises   { %a %a ->@ @[%a@] }"
-        print_xs xs print_vs v print_term q
-    end;
+    fprintf fmt "@\nraises   { %a%a ->@ @[%a@] }" print_xs xs
+      (fun fmt v -> if not (ty_equal v.vs_ty ty_unit && t_v_occurs v q = 0)
+        then fprintf fmt " %a" print_vs v) v print_term q;
     forget_var v in
   let print_xpost fmt (xs,ql) =
     Pp.print_list Pp.nothing (print_xpost xs) fmt ql in
-  fprintf fmt "%a%a%a%a%a%a" print_reads (Spv.elements c.cty_reads)
-    print_writes c print_resets c
-    (Pp.print_list Pp.nothing print_pre) c.cty_pre
-    (Pp.print_list Pp.nothing print_post) c.cty_post
-    (Pp.print_list Pp.nothing print_xpost) (Mexn.bindings c.cty_xpost)
-
-let print_cty fmt c = fprintf fmt "%a :@ %a%a"
-  (Pp.print_list Pp.space print_pvty) c.cty_args
-  print_ity c.cty_result print_cty_spec c
-
-let print_cty_head fmt c = fprintf fmt "%a%a"
-  (Pp.print_list Pp.space print_pvty) c.cty_args
-  print_cty_spec c
+  Pp.print_list_pre Pp.space print_pvty fmt args;
+  Pp.print_option print_result fmt ity;
+  if eff.eff_diverg then pp_print_string fmt " diverges";
+  if not (Spv.is_empty rds) then fprintf fmt "@\nreads  { %a }"
+    (Pp.print_list Pp.comma print_pv) (Spv.elements rds);
+  if not (Mreg.is_empty eff.eff_writes) then fprintf fmt "@\nwrites { %a }"
+    (Pp.print_list Pp.comma print_write) (Mreg.bindings eff.eff_writes);
+  if not (Mreg.is_empty eff.eff_resets) then fprintf fmt "@\nresets { %a }"
+    (Pp.print_list Pp.comma print_raise) (Mreg.bindings eff.eff_resets);
+  Pp.print_list Pp.nothing print_pre fmt pre;
+  Pp.print_list Pp.nothing print_post fmt post;
+  Pp.print_list Pp.nothing print_xpost fmt (Mexn.bindings xpost)
+
+let print_cty fmt c = print_spec c.cty_args c.cty_pre c.cty_post
+  c.cty_xpost c.cty_reads c.cty_effect fmt (Some c.cty_result)
 
 (** exception handling *)
 

src/mlw/ity.mli

@@ -350,18 +350,18 @@ val cty_add_post : cty -> post list -> cty
 
 (** {2 Pretty-printing} *)
 
-open Format
-
 val forget_reg : region -> unit   (* flush id_unique for a region *)
 val forget_pv  : pvsymbol -> unit (* flush for a program variable *)
 
-val print_its : formatter -> itysymbol -> unit    (* type symbol *)
-val print_reg : formatter -> region -> unit       (* region *)
-val print_ity : formatter -> ity -> unit          (* individual type *)
-val print_ity_full : formatter -> ity -> unit     (* type with regions *)
+val print_its : Format.formatter -> itysymbol -> unit (* type symbol *)
+val print_reg : Format.formatter -> region -> unit    (* region *)
+val print_ity : Format.formatter -> ity -> unit       (* individual type *)
+val print_ity_full : Format.formatter -> ity -> unit  (* type with regions *)
+
+val print_xs   : Format.formatter -> xsymbol -> unit  (* exception symbol *)
+val print_pv   : Format.formatter -> pvsymbol -> unit (* program variable *)
+val print_pvty : Format.formatter -> pvsymbol -> unit (* pvsymbol : type *)
+val print_cty  : Format.formatter -> cty -> unit      (* computation type *)
 
-val print_xs   : formatter -> xsymbol -> unit     (* exception symbol *)
-val print_pv   : formatter -> pvsymbol -> unit    (* program variable *)
-val print_pvty : formatter -> pvsymbol -> unit    (* pvsymbol : type *)
-val print_cty  : formatter -> cty -> unit         (* computation type *)
-val print_cty_head : formatter -> cty -> unit     (* args and spec only *)
+val print_spec : pvsymbol list -> pre list -> post list -> post list Mexn.t ->
+  Spv.t -> effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)