programs: a better pretty-printer, for debugging purposes

parent af319f50
......@@ -737,7 +737,7 @@ testl: bin/whyml.byte
ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
testl-debug: bin/whyml.byte
ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
ocamlrun -bt bin/whyml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
testl-ide: bin/whyide.opt
bin/whyide.opt tests/test-pgm-jcf.mlw
......
......@@ -169,7 +169,7 @@ type label = Term.vsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol option
type ipattern = {
ipat_pat : Term.pattern;
ipat_pat : Term.pattern; (* program variables *)
ipat_node : ipat_node;
}
......@@ -227,7 +227,7 @@ type post = T.post
type rec_variant = pvsymbol * Term.term * Term.lsymbol option
type pattern = {
ppat_pat : Term.pattern;
ppat_pat : Term.pattern; (* logic variables *)
ppat_node : ppat_node;
}
......
......@@ -151,6 +151,7 @@ module rec T : sig
val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_pre : Format.formatter -> pre -> unit
val print_post : Format.formatter -> post -> unit
end = struct
......@@ -371,11 +372,19 @@ end = struct
open Format
open Pretty
let print_post fmt ((_,q), el) =
let print_exn_post fmt (l,(_,q)) =
fprintf fmt "| %a -> {%a}" print_ls l print_fmla q
let print_pre fmt f =
fprintf fmt "@[{ %a }@]" Pretty.print_fmla f
and print_post fmt ((v,q), _) =
fprintf fmt "@[{%a | %a}@]" Pretty.print_vs v Pretty.print_fmla q
let print_post fmt ((v, q), el) =
let print_exn_post fmt (l, (v, q)) =
fprintf fmt "@[<hov 2>| %a %a->@ {%a}@]"
print_ls l (print_option print_vs) v print_fmla q
in
fprintf fmt "{%a} %a" print_fmla q (print_list space print_exn_post) el
fprintf fmt "@[{%a | %a}@ %a@]" print_vs v print_fmla q
(print_list space print_exn_post) el
let rec print_type_v fmt = function
| Tpure ty ->
......
......@@ -111,6 +111,7 @@ module rec T : sig
val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_pre : Format.formatter -> pre -> unit
val print_post : Format.formatter -> post -> unit
end
......
......@@ -1474,15 +1474,16 @@ and fresh_triple gl (_, e, _) =
let rec print_expr fmt e = match e.expr_desc with
| Elogic t ->
print_term fmt t
| Elocal vs ->
fprintf fmt "<local %a>" print_vs vs.pv_vs
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 (_, t) ->
fprintf fmt "@[fun _ ->@ %a@]" print_triple t
| Efun (bl, t) ->
fprintf fmt "@[fun %a ->@ %a@]"
(print_list space print_pv) bl print_triple t
| Elet (v, e1, e2) ->
fprintf fmt "@[let %a = %a in@ %a@]" print_vs v.pv_vs
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) ->
......@@ -1492,20 +1493,42 @@ let rec print_expr fmt e = match e.expr_desc with
| Eany c ->
fprintf fmt "@[[any %a]@]" print_type_c c
| _ ->
fprintf fmt "<other>"
| 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 "@[{%a}@ %a@ {%a}@]" print_pre p print_expr e print_post q
fprintf fmt "@[<hv 0>%a@ %a@ %a@]" T.print_pre p print_expr e T.print_post q
and print_pre fmt _ =
fprintf fmt "<pre>"
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_post fmt _ =
fprintf fmt "<post>"
and print_branch fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pattern p print_expr e
and print_recfun fmt (v, _bl, _, t) =
fprintf fmt "@[rec %a _ = %a@]" print_vs v print_triple t
and print_pattern fmt p =
Pretty.print_pat fmt p.ppat_pat
(* typing declarations (combines the three phases together) *)
......@@ -1602,8 +1625,9 @@ let rec decl ~wp env penv lmod uc = function
Pgm_module.add_logic_pdecl env d uc
| Ptree.Dlet (id, e) ->
let e = type_expr uc e in
Debug.dprintf debug "@[--typing %s-----@\n %a@\n%a@]@."
id.id print_expr e print_type_v e.expr_type_v;
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;
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
......@@ -1617,9 +1641,9 @@ let rec decl ~wp env penv lmod uc = function
let tyv = v.pv_tv in
let loc = loc_of_id v.pv_name in
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; *)
if Debug.test_flag debug then
eprintf "@[--typing %s-----@\n %a@.%a@]@."
id print_recfun d print_type_v tyv;
let ps, uc = add_global loc id tyv uc in
uc, (ps, d)
in
......
......@@ -26,5 +26,3 @@ 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
val print_post : Format.formatter -> Pgm_ttree.post -> unit
......@@ -4,6 +4,17 @@ module P
use import int.Int
use import module stdlib.Ref
use import list.List
use import list.Length
let rec length_ (l : list 'a) variant { length l } =
{}
match l with
| Nil -> 0
| Cons _ r -> 1 + length_ r
end
{ result = length l }
(* parameter b : ref int *)
(* let f () = *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment