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

fix some warnings

Left some unused variables that will be used when TODOs get done.
parent cef08572
No related branches found
No related tags found
No related merge requests found
...@@ -369,10 +369,10 @@ module MLToRust = struct ...@@ -369,10 +369,10 @@ module MLToRust = struct
* It is probably best to leave this and see which tvs actually get used * It is probably best to leave this and see which tvs actually get used
*) *)
let rec discover_lts_tvs_def (d:Rust.def) : Slt.t * Stv.t = let discover_lts_tvs_def (d:Rust.def) : Slt.t * Stv.t =
let tvs_snd_ty (_, t) = discover_lts_tvs_ty t in let tvs_snd_ty (_, t) = discover_lts_tvs_ty t in
(match d with (match d with
| Rust.Dfn (rs, vl, t, e, tvs, lts) -> | Rust.Dfn (_, vl, t, e, tvs, lts) ->
let es = discover_lts_tvs_expr e in let es = discover_lts_tvs_expr e in
let ts = discover_lts_tvs_ty t in let ts = discover_lts_tvs_ty t in
let vs = union_slt_stv_list (List.map tvs_snd_ty vl) in let vs = union_slt_stv_list (List.map tvs_snd_ty vl) in
...@@ -387,13 +387,13 @@ module MLToRust = struct ...@@ -387,13 +387,13 @@ module MLToRust = struct
| Rust.Dstatic _ -> Slt.empty, Stv.empty | Rust.Dstatic _ -> Slt.empty, Stv.empty
(* TODO make sure this is correct *) (* TODO make sure this is correct *)
| Rust.Dtype td -> | Rust.Dtype td ->
(match td.def with (match td.Rust.def with
| None -> Slt.empty, Stv.empty | None -> Slt.empty, Stv.empty
| Some (Dalias t) -> discover_lts_tvs_ty t | Some (Rust.Dalias t) -> discover_lts_tvs_ty t
| Some (Denum vl) -> | Some (Rust.Denum vl) ->
let f (_, tl) = union_slt_stv_list (List.map discover_lts_tvs_ty tl) in let f (_, tl) = union_slt_stv_list (List.map discover_lts_tvs_ty tl) in
union_slt_stv_list (List.map f vl) union_slt_stv_list (List.map f vl)
| Some (Dstruct tl) -> | Some (Rust.Dstruct tl) ->
union_slt_stv_list (List.map tvs_snd_ty tl) union_slt_stv_list (List.map tvs_snd_ty tl)
) )
) )
...@@ -405,7 +405,6 @@ module MLToRust = struct ...@@ -405,7 +405,6 @@ module MLToRust = struct
let e = translate_expr info r.rec_exp in let e = translate_expr info r.rec_exp in
let slt, stv = discover_lts_tvs_def (Rust.Dfn (rs, vars, result_ty, e, r.rec_svar, let slt, stv = discover_lts_tvs_def (Rust.Dfn (rs, vars, result_ty, e, r.rec_svar,
Slt.empty)) in Slt.empty)) in
let slt = Slt.empty in (* TODO discover slt *)
Rust.Dfn (rs, vars, result_ty, e, stv, slt) Rust.Dfn (rs, vars, result_ty, e, stv, slt)
(* (*
...@@ -438,7 +437,7 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) = ...@@ -438,7 +437,7 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
Rust.Denum (List.map translate_cons csl) Rust.Denum (List.map translate_cons csl)
| Drecord fl -> | Drecord fl ->
(* TODO do something with field-wise mutability *) (* TODO do something with field-wise mutability *)
let translate_field (mut, id, t) = let translate_field (_, id, t) =
let t = translate_ty info t in 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 info.box_fields id then box_ty t else t in
(id, t) in (id, t) in
...@@ -447,7 +446,7 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) = ...@@ -447,7 +446,7 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
| Drange _ -> raise (TODO "Drange") (* in ocaml it becomes Z.t *) | Drange _ -> raise (TODO "Drange") (* in ocaml it becomes Z.t *)
| Dfloat _ -> raise (TODO "Dfloat") | Dfloat _ -> raise (TODO "Dfloat")
) )
in { in Rust.{
id=its.its_name; id=its.its_name;
args=Stv.of_list its.its_args; args=Stv.of_list its.its_args;
ltparams=Slt.empty; (* TODO find used lifetimes *) ltparams=Slt.empty; (* TODO find used lifetimes *)
...@@ -541,14 +540,10 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) = ...@@ -541,14 +540,10 @@ let maybe_box (rs: rsymbol) (t: Rust.ty) =
end end
open Format open Format
open Weakhtbl
open Pp open Pp
open Ty
open Printer open Printer
open Expr
open Pmodule open Pmodule
open Ity open Ity
open Pdecl
module Print = struct module Print = struct
open Rust open Rust
...@@ -769,7 +764,7 @@ module Print = struct ...@@ -769,7 +764,7 @@ module Print = struct
let print_constr fmt (id, tl) = let print_constr fmt (id, tl) =
match tl with match tl with
| [] -> fprintf fmt "%a," (print_uident info) id | [] -> fprintf fmt "%a," (print_uident info) id
| l -> | _ ->
fprintf fmt "%a(%a)," (print_uident info) id fprintf fmt "%a(%a)," (print_uident info) id
(print_list comma (print_ty info)) tl in (print_list comma (print_ty info)) tl in
fprintf fmt "@[<hov 2>%senum%a %a {@\n%a@]@\n}@\nuse self::%a::*;" fprintf fmt "@[<hov 2>%senum%a %a {@\n%a@]@\n}@\nuse self::%a::*;"
...@@ -824,11 +819,12 @@ let print_decl = ...@@ -824,11 +819,12 @@ let print_decl =
(* avoid printing the same decl multiple times *) (* avoid printing the same decl multiple times *)
let memo = Hashtbl.create 16 in let memo = Hashtbl.create 16 in
fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d -> fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d ->
ignore old; ignore fname; ignore flat;
let info = { let info = {
syntax = pargs.Pdriver.syntax; syntax = pargs.Pdriver.syntax;
literal = pargs.Pdriver.literal; literal = pargs.Pdriver.literal;
converter = pargs.Pdriver.converter; converter = pargs.Pdriver.converter;
th_known_map = th.th_known; th_known_map = th.Theory.th_known;
mo_known_map = m.mod_known; mo_known_map = m.mod_known;
box_fields = Sid.empty; box_fields = Sid.empty;
box_enum = Rust.Sbe.empty; box_enum = Rust.Sbe.empty;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment