Commit d3ea5de2 authored by Mário Pereira's avatar Mário Pereira
Browse files

Code extraction (wip)

Treatment of top-level constants
parent 87b4ad35
......@@ -356,9 +356,10 @@ module Translate = struct
let p (_, _, is_ghost) = not is_ghost in
List.filter p args
let params args =
let args = filter_params args in
if args = [] then [ML.mk_var_unit ()] else args
let params = function
| [] -> []
| args -> let args = filter_params args in
if args = [] then [ML.mk_var_unit ()] else args
let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body eff =
let i_expr, from_expr, to_expr =
......
......@@ -308,8 +308,7 @@ module Print = struct
(print_lident info) fmt (pv_name pvs)
| Elet (let_def, e) ->
fprintf fmt "@[%a@] in@ %a"
(print_let_def info) let_def
(print_expr info) e;
(print_let_def info) let_def (print_expr info) e;
forget_let_defn let_def
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
......@@ -335,15 +334,14 @@ module Print = struct
| [] -> assert false | [a] -> assign fmt a
| al -> fprintf fmt "@[begin %a end@]" (print_list semi assign) al end
| Eif (e1, e2, {e_node = Eblock []}) ->
fprintf fmt
"@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]"
fprintf fmt "@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]"
(print_expr info) e1 (print_expr info) e2
| Eif (e1, e2, e3) when is_true e2 ->
fprintf fmt
(protect_on paren "@[<hv>%a || %a@]") (print_expr info) e1 (print_expr info) e3
fprintf fmt (protect_on paren "@[<hv>%a || %a@]")
(print_expr info) e1 (print_expr info) e3
| Eif (e1, e2, e3) when is_false e3 ->
fprintf fmt
(protect_on paren "@[<hv>%a && %a@]") (print_expr info) e1 (print_expr info) e2
fprintf fmt (protect_on paren "@[<hv>%a && %a@]")
(print_expr info) e1 (print_expr info) e2
| Eif (e1, e2, e3) ->
fprintf fmt
"@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]"
......
Supports Markdown
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