summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-03 20:13:06 +0100
committerSon Ho2022-02-03 20:13:06 +0100
commitbef57f9d4921e5e8021c086923628b16f5ea18ea (patch)
treeb8ac532543979e31a52319a592068924931604b4
parent53b2695d426b1b04d5527a42b9d79a186a24e65b (diff)
Cleanup a bit
-rw-r--r--src/ExtractToFStar.ml7
-rw-r--r--src/PureMicroPasses.ml7
-rw-r--r--src/PureToExtract.ml6
-rw-r--r--src/SymbolicAst.ml1
-rw-r--r--src/main.ml3
5 files changed, 10 insertions, 14 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index f457dcca..2994d95f 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -324,7 +324,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) :
extraction_ctx =
(* Compute and register the type def name *)
- let ctx, def_name = ctx_add_type_def def ctx in
+ let ctx = ctx_add_type_def def ctx in
(* Compute and register:
* - the variant names, if this is an enumeration
* - the field names, if this is a structure
@@ -597,12 +597,13 @@ let extract_adt_g_value
* We could update the code to print something of the form:
* `{ field0=...; ...; fieldn=...; }` in case of structures.
*)
- let adt_ident =
+ let cons =
match variant_id with
| Some vid -> ctx_get_variant adt_id vid ctx
| None -> ctx_get_struct adt_id ctx
in
if inside && field_values <> [] then F.pp_print_string fmt "(";
+ F.pp_print_string fmt cons;
let ctx =
Collections.List.fold_left_link
(fun () -> F.pp_print_space fmt ())
@@ -875,7 +876,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
let def_name = ctx_get_local_function def.def_id def.back_id ctx in
(* Add the type parameters - note that we need those bindings only for the
* body translation (they are not top-level) *)
- let ctx, type_params = ctx_add_type_params def.signature.type_params ctx in
+ let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 7e74835a..66442ec7 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -1,6 +1,5 @@
(** The following module defines micro-passes which operate on the pure AST *)
-open Errors
open Pure
open PureUtils
open TranslateCore
@@ -605,7 +604,9 @@ let filter_unused (filter_monadic_calls : bool) (ctx : trans_ctx)
(* Return *)
{ def with body; inputs_lvs }
-(** Add unit arguments for functions with no arguments, and change their return type. *)
+(** Add unit arguments for functions with no arguments, and change their return type.
+ TODO: filter the backward functions with no outputs.
+ *)
let to_monadic (def : fun_def) : fun_def =
(* Update the body *)
let obj =
@@ -677,7 +678,7 @@ let unit_vars_to_unit (def : fun_def) : fun_def =
{ def with body; inputs_lvs }
(** Unfold the monadic let-bindings to explicit matches. *)
-let unfold_monadic_let_bindings (ctx : trans_ctx) (def : fun_def) : fun_def =
+let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def =
(* It is a very simple map *)
let obj =
object (self)
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 47097d7d..bd69837a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -4,7 +4,6 @@
backends we target.
*)
-open Errors
open Pure
open TranslateCore
module C = Contexts
@@ -386,11 +385,10 @@ let ctx_add_type_def_struct (def : type_def) (ctx : extraction_ctx) :
let ctx = ctx_add (StructId (AdtId def.def_id)) cons_name ctx in
(ctx, cons_name)
-let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) :
- extraction_ctx * string =
+let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) : extraction_ctx =
let def_name = ctx.fmt.type_name def.name in
let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
- (ctx, def_name)
+ ctx
let ctx_add_field (def : type_def) (field_id : FieldId.id) (field : field)
(ctx : extraction_ctx) : extraction_ctx * string =
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 4eca712a..aad5de15 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -3,7 +3,6 @@
the symbolic execution: we later apply transformations to generate the
pure AST that we export. *)
-open Identifiers
module T = Types
module V = Values
module E = Expressions
diff --git a/src/main.ml b/src/main.ml
index c52b7bd3..842f06a4 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -6,9 +6,6 @@ module A = CfimAst
module I = Interpreter
module EL = Easy_logging.Logging
module TA = TypesAnalysis
-open PureToExtract
-open ExtractAst
-open ExtractToFStar
(* This is necessary to have a backtrace when raising exceptions - for some
* reason, the -g option doesn't work.