Skip to content
Snippets Groups Projects
Commit 21889381 authored by nilfit's avatar nilfit
Browse files

add box matching in patterns 

uses some unstable syntax
parent 18255260
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/mlw/rust_printer.ml
+ 171
− 36
View file @ 21889381
......@@ -39,6 +39,7 @@ module Rust = struct
| Por of pat * pat (* p1 | p2 *)
| Pat of vsymbol * pat (* vs @ pat *)
(* TODO test @ in more situations *)
| Pbox of pat (* the `box` keyword (unstable) *)
type var = ident * ty (* ref? mut? *)
......@@ -121,8 +122,6 @@ type info = {
converter : Printer.syntax_map;
th_known_map : Decl.known_map;
mo_known_map : Pdecl.known_map;
mutable box_fields : Sid.t;
mutable box_enum : Rust.Sbe.t;
}
module MLToRust = struct
......@@ -133,16 +132,36 @@ module MLToRust = struct
module Slt = Rust.Slt
module Sbe = Rust.Sbe
type box_info = {
mutable box_fields : Sid.t;
mutable box_enum : Sbe.t;
}
let boxes = { box_fields = Sid.empty; box_enum = Sbe.empty }
(* TODO make sure we don't extract any ghosts *)
let id_is_func = id_equal ts_func.ts_name
let is_id_func = id_equal ts_func.ts_name
(* TODO should have a mask here, right now we might bring some ghosts along *)
let rec mlty_of_ity (ity:Ity.ity) : ty =
let rec loop t = match t.ity_node with
| Ityvar tvs -> Tvar tvs
| Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
Ttuple (List.map loop itl)
| Ityapp ({its_ts = ts}, itl, _) ->
Tapp (ts.ts_name, List.map loop itl)
| Ityreg {reg_its = its; reg_args = args} ->
let args = List.map loop args in
Tapp (its.its_ts.ts_name, args) in
loop ity
let rec translate_ty info (t:ty) : Rust.ty =
match t with
| Tvar tvs -> Rust.Tvar tvs
| Ttuple tl -> Rust.Ttuple (List.map (translate_ty info) tl)
(* function *)
| Tapp (ts, tl) when id_is_func ts ->
| Tapp (ts, tl) when is_id_func ts ->
let args_and_res = function_sig info t in
let args, res = Lists.chop_last args_and_res in
Rust.Tfn(args, res)
......@@ -156,16 +175,26 @@ module MLToRust = struct
and function_sig info (t:ty) : Rust.ty list =
match t with
| Tapp (ts, tl) when id_is_func ts ->
| Tapp (ts, tl) when is_id_func ts ->
(match tl with
| [ta; tb] -> translate_ty info ta :: function_sig info tb
| _ -> assert false)
| _ -> [translate_ty info t]
(* let translate_ity info ity = translate_ty info (mlty_of_ity ity) *)
let translate_var (info:info) ((id, ty, _ghost):var) : Rust.var =
(id, translate_ty info ty)
let translate_vars info = List.map (translate_var info)
let get_its_defn info rs =
match Mid.find_opt rs.rs_name info.mo_known_map with
| Some {pd_node = PDtype itdl} ->
let eq_rs {itd_constructors=rsl} =
List.exists (rs_equal rs) (*fun {rs_name} -> id_equal id rs_name*) rsl in
List.find eq_rs itdl
| _ -> raise (TODO "no PDtype")
let get_record info rs =
match Mid.find_opt rs.rs_name info.mo_known_map with
| Some {pd_node = PDtype itdl} ->
......@@ -175,23 +204,116 @@ module MLToRust = struct
List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
| _ -> []
(* TODO delete this *)
(*
let s_ty t =
match (t : ty) with
| Mltree.Tvar _ -> "tv"
| Mltree.Tapp (id, _) -> Printf.sprintf "app(%s)" id.id_string
| Mltree.Ttuple _ -> "tup"
let p_ty t = Printf.printf "%s\n" (s_ty t)
let p_tyl tl =
raise (TODO "p_tyl")
(* List.iter p_ty tl *)
let id_of_ty = function
| Tapp (id, _) -> id
| _ -> raise (TODO "id_of_ty not Tapp")
(* really just needs to raise a better exception *)
*)
(* TODO can't take a Mltree.ty here, since we only have ity on the calling
* side, unless we also translate from Ty.ty to Mltree.ty (using
* Compile.Translate.type_) or from Ity.ity to Mltree.ty (using
* Compile.Translate.mlty_of_ity). They are both private..
* Might be better to just take the ity here and
* deal with it once *)
(*
let rec translate_pat (info:info) (p:pat) (t:ty) : Rust.pat =
let translate_pats = List.map2 (translate_pat info) in
match p, t with
| Pwild, _ -> Rust.Pwild
| Pvar vs, _ -> Rust.Pvar (vs, false) (* TODO needs to be mutable sometimes *)
| Papp (lsym, pl), Tapp (id, tl) ->
(* TODO boxcheck the id (up one level), map2 on pl tl*)
(*
let maybe_box (p: Rust.pat) (t:ty) =
if Sid.contains boxes.box_fields (id_of_ty t) then Rust.Pbox p else p in
*)
(* TODO *)
let id_of_corety {ty_node} =
match ty_node with
| Tyapp (ts, _) -> ts.ts_name
| _ -> raise (TODO "corety not app") in
let patty = (id_of_corety (Opt.get_exn (TODO "pat_ty") lsym.ls_value)) in
let debugs = Printf.sprintf "{LISTLEN %s %d %d, %s}\n" (id_of_ty t).id_string
(List.length pl) (List.length lsym.ls_args) patty.id_string in
(* p_tyl tl; *)
let subpats = [Rust.Pwild] in
(* let subpats = translate_pats pl tl in *)
(* TODO list lengths don't match *)
(* let subpats = List.map2 maybe_box subpats tl in *)
(* TODO box correctly for driver syntax as well *)
(match query_syntax info.syntax lsym.ls_name with
| Some s -> Rust.Pde_syn (s, subpats)
| None ->
let rs = restore_rs lsym in
let itd = get_its_defn info rs in
let pjl = itd.itd_fields in
(* let debugs = Printf.sprintf "{%s, pjllen %d}" debugs (List.length pjl) in *)
Rust.Pde_syn (debugs, [
match pjl with
| [] -> Rust.Pde_enum (lsym, subpats)
| pjl -> Rust.Pde_str (rs, pjl, subpats)
])
)
| Ptuple pl, Ttuple tl ->
Rust.Pde_syn ("PTUP %1", [
Rust.Ptuple (translate_pats pl tl)
])
(* TODO t should be a Ttuple(tl) and we should map2 (??) pl tl *)
| Por (p1, p2), _ -> Rust.Por (translate_pat info p1 t, translate_pat info p2 t)
| Pas (p, vs), _ -> Rust.Pat (vs, translate_pat info p t)
(* TODO pattern bindings are not allowed after @: l @ (a, b) *)
| _, _ -> raise (TODO "pattern doesn't match type")
*)
let rec translate_pat (info:info) (p:pat) : Rust.pat =
let translate_pats = List.map (translate_pat info) in
match p with
| Pwild -> Rust.Pwild
| Pvar vs -> Rust.Pvar (vs, false) (* TODO needs to be mutable sometimes *)
| Papp (lsym, pl) ->
let rs = restore_rs lsym in
let itd = get_its_defn info rs in
let pjl = itd.itd_fields in
let subpats = translate_pats pl in
let subpats =
(match pjl with
| [] -> (* enum *)
let maybe_box i p =
if Sbe.contains boxes.box_enum (rs.rs_name, i)
then Rust.Pbox p else p in
List.mapi maybe_box subpats
| pjl -> (* struct *)
let maybe_box rs p =
Printf.printf "<box? %s>\n" rs.rs_name.id_string;
Printf.printf "<card %d>" (Sid.cardinal boxes.box_fields);
if Sid.contains boxes.box_fields rs.rs_name
then Rust.Pbox p else p in
List.map2 maybe_box pjl subpats) in
(match query_syntax info.syntax lsym.ls_name with
| Some s -> Rust.Pde_syn (s, translate_pats pl)
| Some s -> Rust.Pde_syn (s, subpats)
| None ->
let rs = restore_rs lsym in
let pjl = get_record info rs in
match pjl with
| [] -> Rust.Pde_enum (lsym, translate_pats pl)
| pjl -> Rust.Pde_str (rs, pjl, translate_pats pl))
(* TODO find the type we are matching against so we can print the
* pattern correctly: S {_, a} instead of {_, a} *)
| Ptuple pl -> Rust.Ptuple (translate_pats pl)
(match pjl with
| [] -> Rust.Pde_enum (lsym, subpats)
| pjl -> Rust.Pde_str (rs, pjl, subpats)
)
)
| Ptuple pl ->
Rust.Pde_syn ("PTUP %1", [
Rust.Ptuple (translate_pats pl)
])
| Por (p1, p2) -> Rust.Por (translate_pat info p1, translate_pat info p2)
| Pas (p, vs) -> Rust.Pat (vs, translate_pat info p)
(* TODO pattern bindings are not allowed after @: l @ (a, b) *)
......@@ -208,6 +330,21 @@ module MLToRust = struct
let box_expr (e:Rust.expr) = Rust.Esyntax ("Box::new(%1)", [e])
let rec translate_expr (info:info) (e:expr) : Rust.expr =
let expr_ty exp =
match exp.e_ity with
| I ity ->
mlty_of_ity ity
(* TODO what happens when the expr has a ghost value? *)
(* Compile.Translate.mlty_of_ity MaskVisible ity *) (* it is not public *)
(*
(match ity.ity_node with
(* TODO what to do with args and regs? *)
| Ityreg {reg_its = ts; reg_args = tl; reg_regs = rl}
| Ityapp (ts, tl, rl) -> ts.its_ts
| Ityvar _ -> raise (TODO "expr with ityvar"))
*)
| C {cty_result = ity; cty_mask = mask} -> raise (TODO "expr cty") in
(* let final_e = *)
Rust.clean_expr (match e.e_node with
| Econst c ->
let n = Number.compute_int_constant c in
......@@ -243,7 +380,7 @@ module MLToRust = struct
| [] -> raise (TODO "Constructor (el)")
| rsl ->
let maybe_box (rs: rsymbol) (e: Rust.expr) =
if Sid.contains info.box_fields rs.rs_name then box_expr e
if Sid.contains boxes.box_fields rs.rs_name then box_expr e
else e in
let el = List.map2 maybe_box rsl el in
Rust.Estruct (rs, rsl, el)
......@@ -269,11 +406,12 @@ module MLToRust = struct
raise (TODO "Eassign")
| Ematch (e1, [(p, e2)], []) ->
(* TODO is this always irrefutable? *)
(* Rust.Elet (translate_pat info p (expr_ty e1), translate_expr info e1, *)
Rust.Elet (translate_pat info p, translate_expr info e1,
translate_expr info e2)
| Ematch (e, bl, []) ->
(* no exception branches -> normal Ematch *)
Rust.Ematch (translate_expr info e, List.map (translate_branch info) bl)
Rust.Ematch (translate_expr info e, List.map (translate_branch info (expr_ty e)) bl)
| Ematch (e, bl, xl) -> raise (TODO "Ematch+exn")
(* TODO in general: wrap exn branches in Error patterns and normal
* branches in Oks? *)
......@@ -299,8 +437,15 @@ module MLToRust = struct
| Eabsurd -> Rust.Eunreachable
| Mltree.Ehole -> raise (TODO "Ehole")
| _ -> raise (TODO "expr"))
(*
in
let ty_s = s_ty (expr_ty e) in
let syn = Printf.sprintf "<%s %%1>" ty_s in
Rust.Esyntax (syn, [final_e])
*)
and translate_branch info ((p, e):reg_branch) : Rust.branch =
and translate_branch info ty ((p, e):reg_branch) : Rust.branch =
(* (translate_pat info p ty, translate_expr info e) *)
(translate_pat info p, translate_expr info e)
let union_stv_list sl = List.fold_left Stv.union Stv.empty sl
......@@ -396,15 +541,6 @@ module MLToRust = struct
Slt.empty)) in
Rust.Dfn (rs, vars, result_ty, e, stv, slt)
(*
let maybe_box (rs: rsymbol) (t: Rust.ty) =
(* lookup rs fields like in isconstructor *)
if Sid.contains info.box_fields rs.rs_name
(* || Sbe.contains info.box_enums rs.rs_name *) (* TODO per-field tests *)
then box_ty t else t in
let tl = List.map2 maybe_box rsl tl in
*)
let box_ty (t:Rust.ty) = Rust.Tsyn ("Box<%1>", [t])
let translate_its info (its:its_defn) : Rust.t_defn =
......@@ -417,7 +553,7 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
(* constructor argument *)
let translate_cons_arg id_cons i t =
let t = translate_ty info t in
if Sbe.contains info.box_enum (id_cons, i)
if Sbe.contains boxes.box_enum (id_cons, i)
then box_ty t else t in
(* constructor *)
let translate_cons (id, tl) =
......@@ -427,8 +563,9 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
| Drecord fl ->
(* TODO do something with field-wise mutability *)
let translate_field (_, id, t) =
Printf.printf "<boxf? %s>\n" id.id_string;
let t = translate_ty info t in
let t = if Sid.contains info.box_fields id then box_ty t else t in
let t = if Sid.contains boxes.box_fields id then box_ty t else t in
(id, t) in
Rust.Dstruct (List.map translate_field fl)
| Dalias t -> Rust.Dalias (translate_ty info t)
......@@ -502,7 +639,6 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
) in
union_res (List.map box itl)
let translate_decl (info:info) (d:decl) : Rust.def list =
match d with
| Dlet (Lsym (rs, ty, vars, e)) ->
......@@ -518,10 +654,9 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
(* top level (static) variables *)
(* TODO find mlw that leads to this case *)
| Dtype itsl ->
let bf, be = box_typedefs itsl info.box_fields info.box_enum in
(* mutate info *)
info.box_fields <- bf;
info.box_enum <- be;
let bf, be = box_typedefs itsl boxes.box_fields boxes.box_enum in
boxes.box_fields <- bf;
boxes.box_enum <- be;
List.map (fun its -> Rust.Dtype (translate_its info its)) itsl
| Dlet _ -> raise (TODO "Dlet")
| Dexn (_, _) ->raise (TODO "Dexn")
......@@ -582,6 +717,7 @@ module Print = struct
List.iter forget_pat pl
| Por (p1, p2) -> forget_pat p1; forget_pat p2
| Pat (_, p) -> forget_pat p
| Pbox p -> forget_pat p
let print_qident ~sanitizer (info:info) fmt id =
(* TODO: support modules *)
......@@ -675,6 +811,7 @@ module Print = struct
fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2
| Pat ({vs_name=id}, p) ->
fprintf fmt "%a @@ %a" (print_lident info) id (print_pat info) p
| Pbox p -> fprintf fmt "box %a" (print_pat info) p
let pv_name (pv:pvsymbol) : ident = pv.pv_vs.vs_name
let print_pv info fmt pv = print_lident info fmt (pv_name pv)
......@@ -815,8 +952,6 @@ let print_decl =
converter = pargs.Pdriver.converter;
th_known_map = th.Theory.th_known;
mo_known_map = m.mod_known;
box_fields = Sid.empty;
box_enum = Rust.Sbe.empty;
} in
if not (Hashtbl.mem memo d) then begin Hashtbl.add memo d ();
Print.print_decl info fmt d;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment