Commit 8eab207e authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

[Raise] expressions compiled and printed
parent 9e91b944
......@@ -73,8 +73,14 @@ module ref.Ref
syntax val (:=) "Pervasives.(:=) %1 %2"
end
(* FIXME: once we extract ref.Refint, this module
will no longer be useful in the driver *)
module ref.Refint
syntax val incr "%1 := Z.succ (Pervasives.(!) %1)"
syntax val decr "%1 := Z.pred (Pervasives.(!) %1)"
syntax val (+=) "%1 := Z.add (Pervasives.(!) %1) %2"
syntax val (-=) "%1 := Z.sub (Pervasives.(!) %1) %2"
syntax val ( *= ) "%1 := Z.mul (Pervasives.(!) %1) %2"
end
module null.Null
......
......@@ -100,9 +100,6 @@ module ML = struct
type binop = Band | Bor | Beq
type exn =
| Xident of ident
type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
type expr = {
......@@ -128,8 +125,8 @@ module ML = struct
| Eblock of expr list
| Ewhile of expr * expr
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
| Eraise of exn * expr option
| Etry of expr * (exn * pvsymbol option * expr) list
| Eraise of xsymbol * expr option
| Etry of expr * (xsymbol * pvsymbol list * expr) list
| Eabsurd
and let_def =
......@@ -176,8 +173,8 @@ module ML = struct
let tunit = Ttuple []
let ity_int = I ity_int
let ity_unit = I ity_unit
let ity_int = I ity_int
let ity_unit = I ity_unit
let enope = Eblock []
......@@ -498,6 +495,7 @@ module Translate = struct
ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
| Eexec ({c_node = Cany}, _) ->
raise ExtractionAny
(* ML.mk_unit *)
| Eabsurd ->
ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
| Ecase (e1, _) when e_ghost e1 ->
......@@ -520,27 +518,26 @@ module Translate = struct
| Efor (pv1, (pv2, To, pv3), _, efor) ->
let efor = expr info efor in
mk_for_to info pv1 pv2 pv3 efor eff
(* let direction = for_direction direction in *)
(* ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, efor)) (ML.I e.e_ity) eff *)
| Efor (pv1, (pv2, DownTo, pv3), _, efor) ->
let efor = expr info efor in
mk_for_downto info pv1 pv2 pv3 efor eff
| Eghost _ ->
(* ML.mk_unit; *)
assert false
| Eghost _ -> assert false
| Eassign al ->
ML.mk_expr (ML.Eassign al) (ML.I e.e_ity) eff
| Epure _ -> assert false (*TODO*)
| Etry _ -> assert false (*TODO*)
| Etry (etry, pvl_e_map) ->
let etry = expr info etry in
let bl =
let bl_map = Mxs.bindings pvl_e_map in
List.map (fun (xs, (pvl, e)) -> xs, pvl, expr info e) bl_map in
ML.mk_expr (ML.Etry (etry, bl)) (ML.I e.e_ity) eff
| Eraise (xs, ex) ->
let ex =
let open ML in
match expr info ex with
| {e_node = Eblock []} -> None
| {ML.e_node = ML.Eblock []} -> None
| e -> Some e
in
let exn = ML.Xident xs.xs_name in
ML.mk_expr (ML.Eraise (exn, ex)) (ML.I e.e_ity) eff
ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff
| Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _) ->
assert false (*TODO*)
| Eexec ({c_node=Cpur (_, _); _ }, _) ->
......@@ -591,7 +588,8 @@ module Translate = struct
| PDlet (LDsym (rs, _)) when rs_ghost rs ->
[]
| PDlet (LDsym (rs, {c_node = Cany})) ->
raise (ExtractionVal rs)
[]
(* raise (ExtractionVal rs) *)
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
let args = params cty.cty_args in
[ML.Dlet (ML.Lsym (rs, args, expr info e))]
......
......@@ -292,7 +292,7 @@ module Print = struct
print_list_next newline print_one fmt rdef;
List.iter (fun fd -> Hrs.remove ht_rs fd.rec_rsym) rdef
and print_enode info fmt = function
and print_enode ?(paren=false) info fmt = function
| Econst c ->
let n = Number.compute_int c in
fprintf fmt "(Z.of_string \"%s\")" (BigInt.to_string n)
......@@ -346,11 +346,11 @@ module Print = struct
| Ewhile (e1, e2) ->
fprintf fmt "@[<hov 2>while %a do@ %a@ done@]"
(print_expr info) e1 (print_expr info) e2
| Eraise (Xident id, None) -> (* FIXME : check exceptions in driver *)
fprintf fmt "raise %a" (print_uident info) id
| Eraise (Xident id, Some e) ->
fprintf fmt "(raise %a %a)"
(print_uident info) id (print_expr info) e
| Eraise (xs, None) -> (* FIXME : check exceptions in driver *)
fprintf fmt (protect_on paren "raise %a") (print_uident info) xs.xs_name
| Eraise (xs, Some e) ->
fprintf fmt (protect_on paren "raise (%a %a)")
(print_uident info) xs.xs_name (print_expr ~paren:true info) e
| Etuple _ -> (* TODO *) assert false
| Efor (pv1, pv2, direction, pv3, e) ->
let print_for_direction fmt = function
......@@ -358,12 +358,13 @@ module Print = struct
| DownTo -> fprintf fmt "downto"
in
fprintf fmt "@[<hov 2>for %a = %a %a %a do@ @[%a@]@ done@]"
(print_lident info) (pv_name pv1)
(print_lident info) (pv_name pv2)
(print_lident info) (pv_name pv1) (print_lident info) (pv_name pv2)
print_for_direction direction
(print_lident info) (pv_name pv3)
(print_expr info) e
| Etry _ -> (* TODO *) assert false
(print_lident info) (pv_name pv3) (print_expr info) e
| Etry (e, bl) ->
fprintf fmt
"@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
(print_expr info) e (print_list newline (print_xbranch info)) bl
| Enot _ -> (* TODO *) assert false
| Ebinop _ -> (* TODO *) assert false
| Ecast _ -> (* TODO *) assert false
......@@ -372,8 +373,14 @@ module Print = struct
fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]"
(print_pat info) p (print_expr info) e
and print_expr info fmt e =
print_enode info fmt e.e_node
and print_xbranch info fmt (xs, pvl, e) =
let print_var fmt pv =
print_lident info fmt (pv_name pv) in
fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) (xs.xs_name)
(print_list nothing print_var) pvl (print_expr info) e
and print_expr ?(paren=false) info fmt e =
print_enode ~paren info fmt e.e_node
let print_type_decl info fmt its =
let print_constr fmt (id, cs_args) =
......
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