diff options
Diffstat (limited to '')
| -rw-r--r-- | src/ExtractToFStar.ml | 7 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 7 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 6 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 1 | ||||
| -rw-r--r-- | src/main.ml | 3 |
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. |