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

propagate lifetimes up to where they need to be declared 

no lifetimes are generated yet
parent 6df5e58f
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/mlw/rust_printer.ml
+ 93
− 215
View file @ 11a70056
......@@ -6,10 +6,12 @@ open Term
open Pdecl
module Rust = struct
module Slt = Sid (* set of lifetimes *)
type ty =
| Tvar of tvsymbol
| Ttuple of ty list
| Tapp of string option * ident * ty list
| Tapp of string option * ident * ty list * Slt.t (* lifetimes last *)
| Tfn of ty list * ty (* arg types, result type*)
(* | Tstruct *)
(* | Tsyntax *)
......@@ -26,11 +28,6 @@ module Rust = struct
| Por of pat * pat (* p1 | p2 *)
| Pat of vsymbol * pat (* vs @ pat *)
(* TODO test @ in more situations *)
(*
Message::Hello { id: id_variable @ 3...7 } => {
println!("Found an id in range: {}", id_variable)
}
*)
type var = ident * ty (* ref? mut? *)
......@@ -45,7 +42,7 @@ module Rust = struct
| Eif of expr * expr * expr
| Eclosure of var list * expr
| Ewhile of expr * expr
| Eabsurd
| Eunreachable
and branch = pat * expr
......@@ -60,23 +57,25 @@ module Rust = struct
}
* It is not needed to translate Mltree.
*)
(* TODO introduce tuple structs and make enum a list of typedefs *)
| Dstruct of (ident * ty) list
type t_defn = {
id: ident;
args: Stv.t;
args: Stv.t; (* util/extset of type variables *)
ltparams: Slt.t; (* lifetime parameters *)
priv: bool;
def: typedef option;
}
type def =
| Dfn of rsymbol * var list * ty * expr * Stv.t
| Dfn of rsymbol * var list * ty * expr * Stv.t * Slt.t
| Dstatic of pvsymbol * expr
| Dtype of t_defn
let rec clean_expr (e:expr) : expr =
match e with
| Econst _ | Evar _ | Eabsurd -> e
| Econst _ | Evar _ | Eunreachable -> e
| Eblock el ->
(match List.map clean_expr el with
| [Eblock el'] -> clean_expr (Eblock el')
......@@ -104,6 +103,8 @@ module MLToRust = struct
open Printer
exception TODO of string
module Slt = Rust.Slt
(* TODO make sure we don't extract any ghosts *)
let rec translate_ty info (t:ty) : Rust.ty =
......@@ -119,7 +120,7 @@ module MLToRust = struct
let args_and_res = function_sig info t in
let args, res = Lists.chop_last args_and_res in
Rust.Tfn(args, res)
| _ -> Rust.Tapp (syn, ts, List.map (translate_ty info) tl)
| _ -> Rust.Tapp (syn, ts, List.map (translate_ty info) tl, Slt.empty)
and function_sig info (t:ty) : Rust.ty list =
match t with
......@@ -210,7 +211,7 @@ module MLToRust = struct
| Mltree.Eexn (_, _, _) -> raise (TODO "Eexn")
| Mltree.Eignore _ -> raise (TODO "Eignore")
| Mltree.Eany _ -> raise (TODO "Eany")
| Eabsurd -> Rust.Eabsurd
| Eabsurd -> Rust.Eunreachable
| Mltree.Ehole -> raise (TODO "Ehole")
| _ -> raise (TODO "expr"))
......@@ -218,19 +219,29 @@ module MLToRust = struct
(translate_pat info p, translate_expr info e)
let union_stv_list sl = List.fold_left Stv.union Stv.empty sl
let union_slt_list sl = List.fold_left Slt.union Slt.empty sl
let union_slt_stv_list sl =
let (l, t) = List.split sl in union_slt_list l, union_stv_list t
let rec discover_tvs_ty (t:Rust.ty) : Stv.t =
let rec discover_lts_tvs_ty (t:Rust.ty) : Slt.t * Stv.t =
let map_and_union tl = union_slt_stv_list
(List.map discover_lts_tvs_ty tl) in
match t with
| Rust.Tvar tv -> Stv.singleton tv
| Rust.Ttuple tl | Rust.Tapp (_, _, tl) ->
union_stv_list (List.map discover_tvs_ty tl)
| Rust.Tvar tv -> (Slt.empty, Stv.singleton tv)
| Rust.Ttuple tl ->
map_and_union tl
| Rust.Tapp (_, _, tl, lts) ->
let slt, stv = map_and_union tl in
(Slt.union lts slt, stv)
| Rust.Tfn (tl, t) ->
union_stv_list (discover_tvs_ty t :: (List.map discover_tvs_ty tl))
map_and_union (t::tl)
let rec discover_tvs_expr (e:Rust.expr) : Stv.t =
let map_and_union el = union_stv_list (List.map discover_tvs_expr el) in
let rec discover_lts_tvs_expr (e:Rust.expr) : Slt.t * Stv.t =
let map_and_union el = union_slt_stv_list
(List.map discover_lts_tvs_expr el) in
(* let map_and_union el = union_stv_list (List.map discover_lts_tvs_expr el) in *)
(match e with
| Rust.Econst _ | Rust.Evar _ | Rust.Eabsurd -> Stv.empty
| Rust.Econst _ | Rust.Evar _ | Rust.Eunreachable -> Slt.empty, Stv.empty
| Rust.Ecall (_, _, el) | Rust.Eblock el -> map_and_union el
| Rust.Elet (_, e1, e2) -> map_and_union [e1;e2]
| Rust.Ematch (e, bl) ->
......@@ -239,8 +250,10 @@ module MLToRust = struct
| Rust.Eif (a, b, c) -> map_and_union [a;b;c]
| Rust.Ewhile (t, b) -> map_and_union [t;b]
| Rust.Eclosure (vl, e) ->
let v_stv = union_stv_list (List.map (fun (_, t) -> discover_tvs_ty t) vl) in
Stv.union (discover_tvs_expr e) v_stv
(* let v_stv = union_stv_list (List.map (fun (_, t) -> discover_lts_tvs_ty t) vl) in *)
let sl = List.map (fun (_, t) -> discover_lts_tvs_ty t) vl in
let s = discover_lts_tvs_expr e in
union_slt_stv_list (s::sl)
)
(* TODO in which places in the expr do we have to look?
* e_ity can have tvs
......@@ -253,26 +266,32 @@ module MLToRust = struct
* It is probably best to leave this and see which tvs actually get used
*)
let rec discover_tvs_def (d:Rust.def) : Stv.t =
let tvs_snd_ty (_, t) = discover_tvs_ty t in
let rec discover_lts_tvs_def (d:Rust.def) : Slt.t * Stv.t =
let tvs_snd_ty (_, t) = discover_lts_tvs_ty t in
(match d with
| Rust.Dfn (rs, vl, t, e, tvs) ->
let e_stv = discover_tvs_expr e in
let t_stv = discover_tvs_ty t in
| Rust.Dfn (rs, vl, t, e, tvs, lts) ->
let es = discover_lts_tvs_expr e in
let ts = discover_lts_tvs_ty t in
let vs = union_slt_stv_list (List.map tvs_snd_ty vl) in
union_slt_stv_list [es; ts; vs; (lts, tvs)]
(*
let e_stv = discover_lts_tvs_expr e in
let t_stv = discover_lts_tvs_ty t in
let v_stv = List.fold_left Stv.union Stv.empty
(List.map tvs_snd_ty vl) in
union_stv_list [e_stv; t_stv; v_stv; tvs]
| Rust.Dstatic _ -> Stv.empty
*)
| Rust.Dstatic _ -> Slt.empty, Stv.empty
(* TODO make sure this is correct *)
| Rust.Dtype td ->
(match td.def with
| None -> Stv.empty
| Some (Dalias t) -> discover_tvs_ty t
| None -> Slt.empty, Stv.empty
| Some (Dalias t) -> discover_lts_tvs_ty t
| Some (Denum vl) ->
let tvs (_, tl) = union_stv_list (List.map discover_tvs_ty tl) in
union_stv_list (List.map tvs vl)
let f (_, tl) = union_slt_stv_list (List.map discover_lts_tvs_ty tl) in
union_slt_stv_list (List.map f vl)
| Some (Dstruct tl) ->
union_stv_list (List.map tvs_snd_ty tl)
union_slt_stv_list (List.map tvs_snd_ty tl)
)
)
......@@ -281,9 +300,10 @@ module MLToRust = struct
let vars = translate_vars info r.rec_args in
let result_ty = translate_ty info r.rec_res in
let e = translate_expr info r.rec_exp in
(* util/extset of type variables *)
let stv = discover_tvs_def (Rust.Dfn (rs, vars, result_ty, e, r.rec_svar)) in
Rust.Dfn (rs, vars, result_ty, e, stv)
let slt, stv = discover_lts_tvs_def (Rust.Dfn (rs, vars, result_ty, e, r.rec_svar,
Slt.empty)) in
let slt = Slt.empty in (* TODO discover slt *)
Rust.Dfn (rs, vars, result_ty, e, stv, slt)
let translate_its info (its:its_defn) : Rust.t_defn =
(* TODO recursive data types using references (need lifetimes) *)
......@@ -304,6 +324,7 @@ module MLToRust = struct
in {
id=its.its_name;
args=Stv.of_list its.its_args;
ltparams=Slt.empty; (* TODO find used lifetimes *)
priv=its.its_private;
def=def
}
......@@ -314,8 +335,9 @@ module MLToRust = struct
let er = translate_expr info e in
let tr = translate_ty info ty in
let vr = translate_vars info vars in
let stv = discover_tvs_def (Rust.Dfn (rs, vr, tr, er, Stv.empty)) in
[Rust.Dfn (rs, vr, tr, er, stv)]
let slt, stv = discover_lts_tvs_def (Rust.Dfn (rs, vr, tr, er,
Stv.empty, Slt.empty)) in
[Rust.Dfn (rs, vr, tr, er, stv, slt)]
| Dlet (Lrec rdefs) -> List.map (translate_rdef info) rdefs
| Dlet (Lvar (pv, e)) -> [Rust.Dstatic (pv, translate_expr info e)]
(* top level (static) variables *)
......@@ -365,13 +387,13 @@ module Print = struct
(* iprinter: local names
* aprinter: generic types
* sprinter: static *)
let iprinter, aprinter, sprinter =
* lprinter: lifetime variables *)
let iprinter, aprinter, lprinter =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer rust_keywords ~sanitizer:isanitize,
create_ident_printer rust_keywords ~sanitizer:lsanitize,
create_ident_printer rust_keywords ~sanitizer:isanitize
create_ident_printer rust_keywords ~sanitizer:isanitize,
create_ident_printer rust_keywords ~sanitizer:lsanitize
let forget_id id = forget_id iprinter id
let forget_var (id, _) = forget_id id
......@@ -402,14 +424,30 @@ module Print = struct
let print_rs info fmt rs =
print_lident info fmt rs.rs_name
(* TODO make sure tvs are declared before use *)
let print_list2_append_delim fmt ~start ~stop ~sep print1 print2 (l1, l2) =
match (l1, l2) with
| [], [] -> ()
| [], _ -> start fmt (); print_list sep print2 fmt l2; stop fmt ()
| _, [] -> start fmt (); print_list sep print1 fmt l1; stop fmt ()
| _ ->
start fmt (); print_list sep print1 fmt l1; sep fmt ();
print_list sep print2 fmt l2; stop fmt ()
let print_tv fmt tv = fprintf fmt "%s" (id_unique
~sanitizer:String.capitalize_ascii aprinter tv.tv_name)
(* TODO remove *)
let print_stv fmt (stv:Stv.t) =
(print_list_delim ~start:lchevron ~stop:rchevron ~sep: comma print_tv) fmt
(Stv.elements stv)
let print_lifetime fmt lt =
fprintf fmt "%s" (id_unique ~sanitizer:String.lowercase_ascii lprinter lt)
let print_slt_stv fmt ((slt:Slt.t), (stv:Stv.t)) =
print_list2_append_delim fmt ~start:lchevron ~stop:rchevron ~sep:comma
print_lifetime print_tv (Slt.elements slt, Stv.elements stv)
let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
match l1, l2 with
| [x1], [x2] ->
......@@ -422,11 +460,13 @@ module Print = struct
let rec print_ty info fmt ty =
match ty with
| Tvar tv -> print_tv fmt tv
| Tapp (s_opt, ts, tl) ->
| Tapp (s_opt, ts, tl, lts) ->
begin match s_opt with
| Some s -> fprintf fmt "%a" (syntax_arguments s (print_ty info)) tl
| None ->
(* print_slt_stv fmt (lts, (Stv.of_list tl)) *) (* tl is ty not tvsymbol *)
match tl with
(* TODO make a function that print_slt_ty handles <> *)
| [] -> (print_uident info) fmt ts
| tl ->
fprintf fmt "%a<%a>" (print_uident info) ts
......@@ -506,8 +546,7 @@ module Print = struct
(print_list comma (print_arg info)) args
(print_expr info) e;
forget_vars args
| Eabsurd -> fprintf fmt "panic!(\"absurd\")"
| Eunreachable -> fprintf fmt "unreachable!()"
and print_branch info fmt (p, e) =
fprintf fmt "@[<hov 2>| %a =>@ {@\n%a@]@\n}"
......@@ -526,23 +565,24 @@ module Print = struct
fprintf fmt "%a(%a)," (print_uident info) id
(print_list comma (print_ty info)) tl in
fprintf fmt "@[<hov 2>%senum%a %a {@\n%a@]@\n}@\nuse self::%a::*;"
pub print_stv td.args (print_uident info) td.id (print_list newline
print_constr) csl (print_uident info) td.id
pub print_slt_stv (td.ltparams, td.args) (print_uident info) td.id
(print_list newline print_constr) csl (print_uident info) td.id
| Some (Dstruct fl) ->
let print_field fmt (id, ty) =
fprintf fmt "pub %a: %a," (print_lident info) id (print_ty info) ty in
fprintf fmt "@[<hov 2>%sstruct%a %a {@\n%a@]@\n}" pub print_stv td.args
(print_uident info) td.id (print_list newline print_field) fl
fprintf fmt "@[<hov 2>%sstruct%a %a {@\n%a@]@\n}" pub print_slt_stv
(td.ltparams, td.args) (print_uident info) td.id (print_list newline
print_field) fl
| Some (Dalias t) ->
fprintf fmt "%stype%a %a = %a;" pub print_stv td.args
fprintf fmt "%stype%a %a = %a;" pub print_slt_stv (td.ltparams, td.args)
(print_uident info) td.id (print_ty info) t
let print_def info fmt (d:def) =
match d with
| Dfn (rs, args, res_ty, e, tvs) ->
| Dfn (rs, args, res_ty, e, tvs, lts) ->
fprintf fmt "pub fn %a%a(@[%a@])@ ->@ %a@ @[<hov 2>{@\n%a@]@\n}@\n"
(print_lident info) rs.rs_name
print_stv tvs
print_slt_stv (lts, tvs)
(print_list comma (print_arg info)) args
(print_ty info) res_ty (print_expr info) e;
forget_vars args
......@@ -561,136 +601,6 @@ end
(* used to deal with recursive functions *)
let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
let print_ident fmt id = fprintf fmt "%s" (id_unique printer id)
(* TODO make sure tvs are declared before use *)
let print_tv fmt tv = fprintf fmt "%s" (id_unique printer tv.tv_name)
let rec print_ty info fmt ty =
match ty with
| Tvar tv -> print_tv fmt tv
| Tapp (ts, tl) ->
begin match query_syntax info.syntax ts with
| Some s -> fprintf fmt "%a" (syntax_arguments s (print_ty info)) tl
| None -> print_todo fmt "type_no_syntax"
end
| Ttuple _ -> print_todo fmt "Ttuple"
let print_vs_arg info fmt (id, ty, is_ghost) =
fprintf fmt "%a:@ %a" print_ident id (print_ty info) ty
let get_record info rs =
match Mid.find_opt rs.rs_name info.mo_known_map with
| Some {pd_node = PDtype itdl} ->
let eq_rs {itd_constructors} =
List.exists (rs_equal rs) itd_constructors in
let itd = List.find eq_rs itdl in
List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
| _ -> []
let print_constant fmt c = print_todo fmt "constant"
let pv_name pv = pv.pv_vs.vs_name
let print_pv fmt pv = print_ident fmt (pv_name pv)
let rec print_apply_args info fmt = function
| expr :: exprl, pv :: pvl ->
(*
if is_optional ~attrs:(pv_name pv).id_attrs then
begin match expr.e_node with
| Eapp (rs, _)
when query_syntax info.info_syn rs.rs_name = Some "None" -> ()
| _ -> fprintf fmt "?%s:%a" (pv_name pv).id_string
(print_expr ~paren:true info) expr end
else if is_named ~attrs:(pv_name pv).id_attrs then
fprintf fmt "~%s:%a" (pv_name pv).id_string
(print_expr ~paren:true info) expr
else *)fprintf fmt "%a" (print_expr ~paren:true info) expr;
if exprl <> [] then fprintf fmt ",@ ";
print_apply_args info fmt (exprl, pvl)
| expr :: exprl, [] ->
fprintf fmt "%a" (print_expr ~paren:true info) expr;
print_apply_args info fmt (exprl, [])
| [], _ -> ()
and print_apply info rs fmt pvl =
let isfield =
match rs.rs_field with
| None -> false
| Some _ -> true in
let isconstructor () =
match Mid.find_opt rs.rs_name info.mo_known_map with
| Some {pd_node = PDtype its} ->
let is_constructor its =
List.exists (rs_equal rs) its.itd_constructors in
List.exists is_constructor its
| _ -> false in
match query_syntax info.converter rs.rs_name,
query_syntax info.syntax rs.rs_name, pvl with
| Some s, _, [{e_node = Econst _}] ->
(* print_todo fmt "Some s, _, [{...}]" *)
syntax_arguments s print_constant fmt pvl
| _, Some s, _ (* when is_local_id info rs.rs_name *)->
(* print_todo fmt "_, Some s, _" *)
syntax_arguments s (print_expr ~paren:true info) fmt pvl;
| _, None, tl when is_rs_tuple rs ->
print_todo fmt "_, None, [t1]"
(*
fprintf fmt "@[(%a)@]"
(print_list comma (print_expr info)) tl
*)
| _, None, [t1] when isfield ->
print_todo fmt "_, None, [t1]"
(* fprintf fmt "%a.%a" (print_expr info) t1 print_ident rs.rs_name *)
| _, None, tl when isconstructor () ->
let pjl = get_record info rs in
print_todo fmt "_, None, tl";
begin match pjl, tl with
| [], [] ->
print_todo fmt "[],[]"
(* print_ident fmt rs.rs_name *)
| [], [t] ->
print_todo fmt "[],[t]"
(*
fprintf fmt "@[<hov 2>%a %a@]" print_ident rs.rs_name
(print_expr ~paren:true info) t
*)
| [], tl ->
print_todo fmt "[],tl"
(*
fprintf fmt "@[<hov 2>%a (%a)@]" print_ident rs.rs_name
(print_list comma (print_expr ~paren:true info)) tl
*)
| pjl, tl ->
print_todo fmt "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
*)
end
| _, None, [] ->
print_todo fmt "_, None, []"
(* print_ident fmt rs.rs_name *)
| _, _, tl ->
(* print_todo fmt "_,_,tl" *)
fprintf fmt "@[<hov 2>%a(%a)@]"
print_ident rs.rs_name
(print_apply_args info) (tl, rs.rs_cty.cty_args)
and print_expr ?(paren=false) info fmt e = match e.e_node with
| Econst c ->
let n = Number.compute_int_constant c in
let n = BigInt.to_string n in
let id = match e.e_ity with
| I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
| _ -> assert false in
(match query_syntax info.literal id with
| Some s -> syntax_arguments s print_constant fmt [e]
| None -> fprintf fmt "%s" n) (* TODO big int *)
(* | None -> fprintf fmt (protect_on paren "Z.of_string \"%s\"") n) *)
| Evar pvs -> print_pv fmt pvs
| Eapp (rs, []) when rs_equal rs rs_true -> fprintf fmt "true"
| Eapp (rs, []) when rs_equal rs rs_false -> fprintf fmt "false"
| Eapp (rs, pvl) ->
......@@ -700,38 +610,6 @@ end
| _ ->
fprintf fmt (protect_on false "%a")
(print_apply info (Hrs.find_def ht_rs rs rs)) pvl end
| Efun (_, _) -> print_todo fmt "fun"
| Elet (_, _) -> print_todo fmt "let"
| Eif (_, _, _) -> print_todo fmt "if"
| Eassign _ -> print_todo fmt "assign"
| Ematch (_, _, _) -> print_todo fmt "match"
| Eblock _ -> print_todo fmt "block"
| Ewhile (_, _) -> print_todo fmt "while"
| Efor (_, _, _, _, _) -> print_todo fmt "for"
| Eraise (_, _) -> print_todo fmt "raise"
| Eexn (_, _, _) -> print_todo fmt "exn"
| Eignore _ -> print_todo fmt "ignore"
| Eany _ -> print_todo fmt "any"
| Eabsurd -> print_todo fmt "absurd"
| Ehole -> print_todo fmt "hole"
let print_let_def info fmt ldef =
match ldef with
| Lvar (_) -> print_todo fmt "var"
| Lsym (rs, res_ty, args, e) ->
fprintf fmt "pub fn %a(@[%a@])@ ->@ %a@ @[<hov>{@;<1 2>@[<hov>%a@]}@]"
print_ident rs.rs_name
(print_list comma (print_vs_arg info)) args
(print_ty info) res_ty (print_expr info) e;
forget_vars args
| Lany (_) -> print_todo fmt "any"
| Lrec (_) -> print_todo fmt "rec"
let print_decl info fmt = function
| Dlet ldef ->
print_let_def info fmt ldef
| _ -> print_todo fmt "decl cases"
end
*)
let print_decl =
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment