Commit 1c97f58f authored by Mário Pereira's avatar Mário Pereira

OCaml extraction: fixed problem with let-in expressions inside constructors arguments

This closes issue #122
parent acef5992
......@@ -89,5 +89,5 @@ depend: .depend
clean:
rm -f $(BD)/*.o $(BD)/*.cmi $(BD)/*.cmx
rm -f $(BD)/*__*.ml
rm -f $(BD)*.ml
rm -f *~ *.o *.cmi *.cmx build/prover
......@@ -266,7 +266,7 @@ module Translate = struct
| Elet (LDvar (pv, e1), e2)
when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
if eff_pure e1.e_effect then expr info svar mask e2
else let e1 = expr info svar MaskGhost e1 in
else let e1 = ML.e_ignore (expr info svar MaskGhost e1) in
ML.e_seq e1 (expr info svar mask e2) (ML.I e.e_ity) mask eff lbl
| Elet (LDvar (pv, e1), e2) ->
Debug.dprintf debug_compile "compiling local definition of %s@."
......
......@@ -309,8 +309,10 @@ let e_app rs pvl =
let e_fun args e = mk_expr (Efun (args, e))
let e_ignore e =
if is_unit e.e_ity then e
else mk_expr (Eignore e) ity_unit MaskVisible e.e_effect e.e_label
(* TODO : avoid ignore around a unit type expresson *)
(* if is_unit e.e_ity then begin Format.eprintf "hit!@."; e end
* else *)
mk_expr (Eignore e) ity_unit MaskVisible e.e_effect e.e_label
let e_if e1 e2 e3 =
mk_expr (Eif (e1, e2, e3)) e2.e_ity
......
......@@ -352,12 +352,11 @@ module Print = struct
(print_expr ~paren:true info) t
| [], tl ->
fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
(print_list comma (print_expr info)) tl
| pjl, tl ->
let equal fmt () = fprintf fmt " = " in
fprintf fmt "@[<hov 2>{ @[%a@] }@]"
(print_list2 semi equal (print_rs info) (print_expr info))
(pjl, tl) end
(print_list comma (print_expr ~paren:true info)) tl
| pjl, tl -> let equal fmt () = fprintf fmt " =@ " in
fprintf fmt "@[<hov 2>{ %a }@]"
(print_list2 semi equal (print_rs info)
(print_expr ~paren:true info)) (pjl, tl) end
| _, None, [] ->
(print_lident info) fmt rs.rs_name
| _, _, tl ->
......@@ -586,7 +585,7 @@ module Print = struct
| l -> fprintf fmt "@[<hov 4>| %a of %a@]" (print_uident info) id
(print_list star (print_ty ~paren:false info)) l in
let print_field fmt (is_mutable, id, ty) =
fprintf fmt "%s%a: %a;" (if is_mutable then "mutable " else "")
fprintf fmt "%s%a: @[%a@];" (if is_mutable then "mutable " else "")
(print_lident info) id (print_ty ~paren:false info) ty in
let print_def fmt = function
| None ->
......
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