extraction: for loops are kept in intermediate ASTs

parent b8fb2e85
......@@ -323,9 +323,9 @@ end
module mach.int.Refint63
syntax val incr "incr %1"
syntax val decr "decr %1"
syntax val (+=) "%1 := !%1 + %2" (*"(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"*)
syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
syntax val (+=) "%1 := !%1 + %2"
syntax val (-=) "%1 := !%1 - %2"
syntax val ( *= ) "%1 := !%1 * %2"
end
module mach.int.MinMax63
syntax val min "Pervasives.min %1 %2"
......
......@@ -177,7 +177,6 @@ module ML = struct
let tunit = Ttuple []
let ity_int = I Ity.ity_int
let ity_unit = I Ity.ity_unit
let is_unit = function
......@@ -224,6 +223,9 @@ module ML = struct
let e_while e1 e2 =
mk_expr (Mltree.Ewhile (e1, e2)) ity_unit
let e_for pv1 pv2 dir pv3 e1 =
mk_expr (Mltree.Efor (pv1, pv2, dir, pv3, e1)) ity_unit
let e_match e bl =
mk_expr (Mltree.Ematch (e, bl))
......@@ -338,14 +340,16 @@ module Translate = struct
Mltree.Tapp (its.its_ts.ts_name, args) in
loop t
let ty_int = mlty_of_ity MaskVisible ity_int
let pvty pv =
if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
else let (vs, vs_ty) = vsty pv.pv_vs in
ML.mk_var vs vs_ty false
(* let for_direction = function *)
(* | To -> Mltree.To *)
(* | DownTo -> Mltree.DownTo *)
let for_direction = function
| To -> Mltree.To
| DownTo -> Mltree.DownTo
let isconstructor info rs =
match Mid.find_opt rs.rs_name info.Mltree.from_km with
......@@ -426,59 +430,6 @@ module Translate = struct
ML.mk_expr (Mltree.Evar pv) (Mltree.I pv.pv_ity) eff_empty Slab.empty in
filter_params_cty pv_not_ghost def pvl cty_args
let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body_expr eff =
let i_expr, from_expr, to_expr =
let int_ity = ML.ity_int in let eff_e = eff_empty in
ML.mk_expr (Mltree.Evar i_pv) int_ity eff_e Slab.empty,
ML.mk_expr (Mltree.Evar from_pv) int_ity eff_e Slab.empty,
ML.mk_expr (Mltree.Evar to_pv) int_ity eff_e Slab.empty in
let for_rs =
let for_id = id_fresh "for_loop_to" in
let for_cty = create_cty [i_pv] [] [] Mxs.empty Mpv.empty eff ity_unit in
create_rsymbol for_id for_cty in
let for_expr =
let test =
ML.mk_expr (Mltree.Eapp (op_b_rs, [i_expr; to_expr]))
(Mltree.I ity_bool) eff_empty Slab.empty in
let next_expr =
let one_const = Number.int_const_of_int 1 in
let one_expr =
ML.mk_expr (Mltree.Econst one_const) ML.ity_int
eff_empty Slab.empty in
let i_op_one = Mltree.Eapp (op_a_rs, [i_expr; one_expr]) in
ML.mk_expr i_op_one ML.ity_int eff_empty Slab.empty in
let rec_call =
ML.mk_expr (Mltree.Eapp (for_rs, [next_expr])) ML.ity_unit
eff Slab.empty in
let seq_expr =
ML.e_seq body_expr rec_call ML.ity_unit eff Slab.empty in
ML.mk_expr (Mltree.Eif (test, seq_expr, ML.e_unit)) ML.ity_unit
eff Slab.empty in
let ty_int = mlty_of_ity MaskVisible ity_int in
let for_call_expr = let for_call = Mltree.Eapp (for_rs, [from_expr]) in
ML.mk_expr for_call ML.ity_unit eff Slab.empty in
let pv_name pv = pv.pv_vs.vs_name in
let args = [ pv_name i_pv, ty_int, false ] in
let for_rec_def = {
Mltree.rec_sym = for_rs; Mltree.rec_args = args;
Mltree.rec_rsym = for_rs; Mltree.rec_exp = for_expr;
Mltree.rec_res = ML.tunit; Mltree.rec_svar = Stv.empty;
} in
let for_let = Mltree.Elet (Mltree.Lrec [for_rec_def], for_call_expr) in
ML.mk_expr for_let ML.ity_unit eff
let mk_for_downto info i_pv from_pv to_pv body eff =
let ge_rs, minus_rs =
let ns = (Opt.get info.Mltree.from_mod).mod_export in
ns_find_rs ns ["Int"; "infix >="], ns_find_rs ns ["Int"; "infix -"] in
mk_for ge_rs minus_rs i_pv from_pv to_pv body eff
let mk_for_to info i_pv from_pv to_pv body eff =
let le_rs, plus_rs =
let ns = (Opt.get info.Mltree.from_mod).mod_export in
ns_find_rs ns ["Int"; "infix <="], ns_find_rs ns ["Int"; "infix +"] in
mk_for le_rs plus_rs i_pv from_pv to_pv body eff
(* build the set of type variables from functions arguments *)
let rec add_tvar acc = function
| Mltree.Tvar tv -> Stv.add tv acc
......@@ -607,12 +558,10 @@ module Translate = struct
ML.e_if e1 e2 e3 eff lbl
| Ewhile (e1, _, _, e2) ->
ML.e_while (expr info svar e1) (expr info svar e2) eff lbl
| Efor (pv1, (pv2, To, pv3), _, _, efor) ->
let efor = expr info svar efor in
mk_for_to info pv1 pv2 pv3 efor eff lbl
| Efor (pv1, (pv2, DownTo, pv3), _, _, efor) ->
| Efor (pv1, (pv2, dir, pv3), _, _, efor) ->
let dir = for_direction dir in
let efor = expr info svar efor in
mk_for_downto info pv1 pv2 pv3 efor eff lbl
ML.e_for pv1 pv2 dir pv3 efor eff lbl
| Eghost _ -> assert false
| Eassign al ->
ML.e_assign al (Mltree.I e.e_ity) eff lbl
......@@ -684,7 +633,10 @@ module Translate = struct
| Alias t, _, _ ->
ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
(Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
| Range _, _, _ -> assert false (* TODO *)
| Range _, [], [] ->
assert (args = []); (* a range type is not polymorphic *)
ML.mk_its_defn id [] is_private (Some (Mltree.Dalias ty_int))
| Range _, _, _ -> assert false (* a range type has no field/constr. *)
| Float _, _, _ -> assert false (* TODO *)
end
......@@ -914,9 +866,7 @@ module Transform = struct
mk (Ewhile (e1, e2)), Spv.union s1 s2
| Efor (x, pv1, dir, pv2, e) ->
let e, spv = expr info subst e in
let e = mk (Efor (x, pv1, dir, pv2, e)) in
(* be careful when pv1 and pv2 are in subst *)
mk_let subst pv1 (mk_let subst pv2 e), spv
mk (Efor (x, pv1, dir, pv2, e)), spv
| Eraise (exn, None) -> mk (Eraise (exn, None)), Spv.empty
| Eraise (exn, Some e) ->
let e, spv = expr info subst e in
......@@ -933,10 +883,10 @@ module Transform = struct
let e, spv = expr info subst e in
mk (Eignore e), spv
and mk_let subst pv e =
try let e1 = Mpv.find pv subst in
{ e with e_node = Elet (Lvar (pv, e1), e) }
with Not_found -> e
(* and mk_let subst pv e = *)
(* try let e1 = Mpv.find pv subst in *)
(* { e with e_node = Elet (Lvar (pv, e1), e) } *)
(* with Not_found -> e *)
and branch info subst (pat, e) =
let e, spv = expr info subst e in (pat, e), spv
......
......@@ -263,6 +263,7 @@ module Print = struct
(** Expressions *)
let pv_name pv = pv.pv_vs.vs_name
let print_pv info fmt pv = print_lident info fmt (pv_name pv)
let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
......@@ -289,6 +290,10 @@ module Print = struct
else fprintf fmt "%s" s
| _ -> assert false end
let print_for_direction fmt = function
| To -> fprintf fmt "to"
| DownTo -> fprintf fmt "downto"
let rec print_apply_args info fmt = function
| expr :: exprl, pv :: pvl ->
if is_optional ~labels:(pv_name pv).id_label then
......@@ -420,7 +425,7 @@ module Print = struct
| _ -> assert false in
(match query_syntax info.info_literal id with
| Some s -> syntax_arguments s print_constant fmt [e]
| None -> fprintf fmt "(Z.of_string \"%s\")" n)
| None -> fprintf fmt (protect_on paren "Z.of_string \"%s\"") n)
| Evar pvs ->
(print_lident info) fmt (pv_name pvs)
| Elet (let_def, e) ->
......@@ -492,16 +497,25 @@ module Print = struct
(print_expr info) e1 (print_expr info) e2
| Eraise (xs, e_opt) ->
print_raise ~paren info xs fmt e_opt
(* | Etuple _ -> (\* TODO *\) assert false *)
| Efor (pv1, pv2, direction, pv3, e) ->
let print_for_direction fmt = function
| To -> fprintf fmt "to"
| DownTo -> fprintf fmt "downto"
in
| Efor (pv1, pv2, dir, pv3, e) ->
let for_id = id_register (id_fresh "for_loop_to") in
let cmp, op = match dir with
| To -> "Z.leq", "Z.succ"
| DownTo -> "Z.geq", "Z.pred" in
fprintf fmt (protect_on paren
"@[<hov 2>let rec %a %a =@ if %s %a %a then \
begin@ %a; %a (%s %a) end@ in@ %a %a@]")
(* let rec *) (print_lident info) for_id (print_pv info) pv1
(* if *) cmp (print_pv info) pv1 (print_pv info) pv3
(* then *) (print_expr info) e (print_lident info) for_id
op (print_pv info) pv1
(* in *) (print_lident info) for_id (print_pv info) pv2
(*
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_for_direction direction (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"
......
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