summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-11-16 10:57:08 +0100
committerSon Ho2023-11-16 10:57:08 +0100
commit0757cdee8c6b8a8020d4b96a44a3017944c9a808 (patch)
tree87888b311cef249f0477be2447f6edfa708c5253 /compiler
parent9ab6a034aaadacac62d241474af3cf28bf6ac928 (diff)
Do more cleanup
Diffstat (limited to 'compiler')
-rw-r--r--compiler/SymbolicToPure.ml25
-rw-r--r--compiler/TypesAnalysis.ml8
2 files changed, 17 insertions, 16 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 4e12d31e..7dad54e1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3,6 +3,9 @@ open LlbcAstUtils
open Pure
open PureUtils
open PrimitiveValues
+open InterpreterUtils
+open FunsAnalysis
+open TypesAnalysis
module T = Types
module Id = Identifiers
module C = Contexts
@@ -10,8 +13,6 @@ module A = LlbcAst
module S = SymbolicAst
module TA = TypesAnalysis
module PP = PrintPure
-module FA = FunsAnalysis
-module IU = InterpreterUtils
(** The local logger *)
let log = Logging.symbolic_to_pure_log
@@ -24,7 +25,7 @@ type type_context = {
This map is empty when we translate the types, then contains all
the translated types when we translate the functions.
*)
- type_infos : TA.type_infos;
+ type_infos : type_infos;
recursive_decls : T.TypeDeclId.Set.t;
}
[@@deriving show]
@@ -47,7 +48,7 @@ type fun_sig_named_outputs = {
type fun_context = {
llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
fun_sigs : fun_sig_named_outputs RegularFunIdNotLoopMap.t; (** *)
- fun_infos : FA.fun_info A.FunDeclId.Map.t;
+ fun_infos : fun_info A.FunDeclId.Map.t;
regions_hierarchies : T.region_groups FunIdMap.t;
}
[@@deriving show]
@@ -513,7 +514,7 @@ let translate_type_id (id : T.type_id) : type_id =
TODO: factor out the various translation functions.
*)
-let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
+let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty =
let translate = translate_fwd_ty type_infos in
match ty with
| T.TAdt (type_id, generics) -> (
@@ -557,15 +558,15 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : T.ty) : ty =
TTraitType (trait_ref, generics, type_name)
| TArrow _ -> raise (Failure "TODO")
-and translate_fwd_generic_args (type_infos : TA.type_infos)
+and translate_fwd_generic_args (type_infos : type_infos)
(generics : T.generic_args) : generic_args =
translate_generic_args (translate_fwd_ty type_infos) generics
-and translate_fwd_trait_ref (type_infos : TA.type_infos) (tr : T.trait_ref) :
+and translate_fwd_trait_ref (type_infos : type_infos) (tr : T.trait_ref) :
trait_ref =
translate_trait_ref (translate_fwd_ty type_infos) tr
-and translate_fwd_trait_instance_id (type_infos : TA.type_infos)
+and translate_fwd_trait_instance_id (type_infos : type_infos)
(id : T.trait_instance_id) : trait_instance_id =
translate_trait_instance_id (translate_fwd_ty type_infos) id
@@ -586,7 +587,7 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
[inside_mut]: are we inside a mutable borrow?
*)
-let rec translate_back_ty (type_infos : TA.type_infos)
+let rec translate_back_ty (type_infos : type_infos)
(keep_region : T.region -> bool) (inside_mut : bool) (ty : T.ty) : ty option
=
let translate = translate_back_ty type_infos keep_region inside_mut in
@@ -791,7 +792,7 @@ let mk_fuel_input_as_list (ctx : bs_ctx) (info : fun_effect_info) :
if function_uses_fuel info then [ mk_fuel_texpression ctx.fuel ] else []
(** Small utility. *)
-let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
+let get_fun_effect_info (fun_infos : fun_info A.FunDeclId.Map.t)
(fun_id : A.fun_id_or_trait_method_ref) (lid : V.LoopId.id option)
(gid : T.RegionGroupId.id option) : fun_effect_info =
match fun_id with
@@ -1783,8 +1784,8 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
^ T.RegionGroupId.to_string rg_id
^ "\n- loop_id: "
^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id
- ^ "\n- eval_ctx:\n" ^ IU.eval_ctx_to_string ectx ^ "\n- abs:\n"
- ^ IU.abs_to_string ectx abs ^ "\n"));
+ ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ectx ^ "\n- abs:\n"
+ ^ abs_to_string ctx abs ^ "\n"));
(* When we end an input abstraction, this input abstraction gets back
* the borrows which it introduced in the context through the input
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 5371a3d7..eb0aeea9 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -1,5 +1,5 @@
open Types
-module A = LlbcAst
+open LlbcAst
type subtype_info = {
under_borrow : bool; (** Are we inside a borrow? *)
@@ -281,7 +281,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
infos
let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
- (infos : type_infos) (decl : A.type_declaration_group) : type_infos =
+ (infos : type_infos) (decl : type_declaration_group) : type_infos =
(* Collect the identifiers used in the declaration group *)
let ids = match decl with NonRecGroup id -> [ id ] | RecGroup ids -> ids in
(* Retrieve the type definitions *)
@@ -289,7 +289,7 @@ let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
(* Initialize the type information for the current definitions *)
let infos =
List.fold_left
- (fun infos def ->
+ (fun infos (def : type_decl) ->
TypeDeclId.Map.add def.def_id (initialize_type_decl_info def) infos)
infos decl_defs
in
@@ -315,7 +315,7 @@ let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
Rk.: pay attention to the difference between type definitions and types!
*)
let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t)
- (decls : A.type_declaration_group list) : type_infos =
+ (decls : type_declaration_group list) : type_infos =
List.fold_left
(fun infos decl -> analyze_type_declaration_group type_decls infos decl)
TypeDeclId.Map.empty decls