Commit ec869ddc authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: distinguish "let" and "let rec" in pretty-printing

parent 2fceb267
......@@ -276,9 +276,9 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt (protect_on (pri > 0) "@[<hov 2>let %a =@ %a@ in@]@\n%a")
print_lv lv (print_lexpr 4) e1 print_expr e2;
forget_lv lv
| Erec ({ rec_defn = rdl }, e) ->
| Erec ({ rec_defn = rdl; rec_letrec = lr }, e) ->
fprintf fmt (protect_on (pri > 0) "%a@ in@\n%a")
(print_list_next newline print_rec) rdl print_expr e;
(print_list_next newline (print_rec lr)) rdl print_expr e;
let forget_rd rd = forget_ps rd.fun_ps in
List.iter forget_rd rdl
| Eif (e0,e1,e2) ->
......@@ -323,10 +323,10 @@ and print_xbranch fmt (xs, pv, e) =
fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" print_xs xs print_pv pv print_expr e;
forget_pv pv
and print_rec fst fmt { fun_ps = ps ; fun_lambda = lam } =
and print_rec lr fst fmt { fun_ps = ps ; fun_lambda = lam } =
let print_arg fmt pv = fprintf fmt "@[(%a)@]" print_pvty pv in
fprintf fmt "@[<hov 2>%s (%a)@ %a =@\n{ %a }@\n%a%a@\n{ %a }@]"
(if fst then "let rec" else "with")
(if fst then if lr > 0 then "let rec" else "let" else "with")
print_psty ps
(print_list space print_arg) lam.l_args
print_term lam.l_pre
......@@ -401,8 +401,8 @@ let print_let_decl fmt { let_sym = lv ; let_expr = e } =
(* FIXME: don't forget global regions *)
forget_tvs_regs ()
let print_rec_decl fst fmt rd =
print_rec fst fmt rd;
let print_rec_decl lr fst fmt rd =
print_rec lr fst fmt rd;
forget_tvs_regs ()
let print_exn_decl fmt xs =
......@@ -416,15 +416,10 @@ let print_pdecl fmt d = match d.pd_node with
| PDdata tl -> print_list_next newline print_data_decl fmt tl
| PDval vd -> print_val_decl fmt vd
| PDlet ld -> print_let_decl fmt ld
| PDrec rdl -> print_list_next newline print_rec_decl fmt rdl.rec_defn
| PDrec { rec_defn = rdl; rec_letrec = lr } ->
print_list_next newline (print_rec_decl lr) fmt rdl
| PDexn xs -> print_exn_decl fmt xs
let print_next_data_decl = print_data_decl false
let print_data_decl = print_data_decl true
let print_next_rec_decl = print_rec_decl false
let print_rec_decl = print_rec_decl true
(* Print exceptions *)
let () = Exn_printer.register
......
......@@ -53,9 +53,5 @@ val print_ppat : formatter -> ppattern -> unit (* program patterns *)
val print_expr : formatter -> expr -> unit (* expression *)
val print_ty_decl : formatter -> itysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
val print_next_data_decl : formatter -> data_decl -> unit
val print_pdecl : formatter -> pdecl -> unit
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