summaryrefslogtreecommitdiff
path: root/compiler/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicToPure.ml')
-rw-r--r--compiler/SymbolicToPure.ml622
1 files changed, 342 insertions, 280 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2ce8c706..4df3ee73 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2,18 +2,18 @@ open Utils
open LlbcAstUtils
open Pure
open PureUtils
-module Id = Identifiers
+open InterpreterUtils
+open FunsAnalysis
+open TypesAnalysis
+module T = Types
+module V = Values
module C = Contexts
module A = LlbcAst
module S = SymbolicAst
-module TA = TypesAnalysis
-module L = Logging
module PP = PrintPure
-module FA = FunsAnalysis
-module IU = InterpreterUtils
(** The local logger *)
-let log = L.symbolic_to_pure_log
+let log = Logging.symbolic_to_pure_log
type type_context = {
llbc_type_decls : T.type_decl TypeDeclId.Map.t;
@@ -23,7 +23,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]
@@ -46,7 +46,8 @@ 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]
@@ -207,116 +208,96 @@ type bs_ctx = {
[@@deriving show]
(* TODO: move *)
-let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
- Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
- ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx ctx.fun_decl
-
-let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
- let rvar_to_string = Print.Types.region_var_id_to_string in
- let r_to_string = Print.Types.region_id_to_string in
- let type_var_id_to_string = Print.Types.type_var_id_to_string in
- let var_id_to_string = Print.Expressions.var_id_to_string in
- let ast_fmt = bs_ctx_to_ast_formatter ctx in
+let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
+ let type_decls = ctx.type_context.llbc_type_decls in
+ let fun_decls = ctx.fun_context.llbc_fun_decls in
+ let global_decls = ctx.global_context.llbc_global_decls in
+ let trait_decls = ctx.trait_decls_ctx in
+ let trait_impls = ctx.trait_impls_ctx in
+ let generics = ctx.fun_decl.signature.generics in
+ let preds = ctx.fun_decl.signature.preds in
{
- Print.Values.rvar_to_string;
- r_to_string;
- type_var_id_to_string;
- type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
- const_generic_var_id_to_string = ast_fmt.const_generic_var_id_to_string;
- global_decl_id_to_string = ast_fmt.global_decl_id_to_string;
- adt_variant_to_string = ast_fmt.adt_variant_to_string;
- var_id_to_string;
- adt_field_names = ast_fmt.adt_field_names;
- trait_decl_id_to_string = ast_fmt.trait_decl_id_to_string;
- trait_impl_id_to_string = ast_fmt.trait_impl_id_to_string;
- trait_clause_id_to_string = ast_fmt.trait_clause_id_to_string;
+ type_decls;
+ fun_decls;
+ global_decls;
+ trait_decls;
+ trait_impls;
+ generics;
+ preds;
+ locals = [];
}
-let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
- let generics = ctx.fun_decl.signature.generics in
+let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
let type_decls = ctx.type_context.llbc_type_decls in
let fun_decls = ctx.fun_context.llbc_fun_decls in
let global_decls = ctx.global_context.llbc_global_decls in
- PrintPure.mk_ast_formatter type_decls fun_decls global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx generics.types
- generics.const_generics
+ let trait_decls = ctx.trait_decls_ctx in
+ let trait_impls = ctx.trait_impls_ctx in
+ let generics = ctx.sg.generics in
+ {
+ type_decls;
+ fun_decls;
+ global_decls;
+ trait_decls;
+ trait_impls;
+ generics;
+ locals = [];
+ }
-let ctx_egeneric_args_to_string (ctx : bs_ctx) (args : T.egeneric_args) : string
- =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- let fmt = Print.PC.ctx_to_etype_formatter fmt in
- Print.PT.egeneric_args_to_string fmt args
+let ctx_generic_args_to_string (ctx : bs_ctx) (args : T.generic_args) : string =
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Types.generic_args_to_string env args
+
+let name_to_string (ctx : bs_ctx) =
+ Print.Types.name_to_string (bs_ctx_to_fmt_env ctx)
let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- let fmt = Print.PC.ctx_to_rtype_formatter fmt in
- Print.PV.symbolic_value_to_string fmt sv
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Values.symbolic_value_to_string env sv
let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- Print.PV.typed_value_to_string fmt v
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Values.typed_value_to_string env v
-let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
- let fmt = bs_ctx_to_pp_ast_formatter ctx in
- let fmt = PrintPure.ast_to_type_formatter fmt in
- PrintPure.ty_to_string fmt false ty
+let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.ty_to_string env false ty
-let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string =
- let fmt = bs_ctx_to_ctx_formatter ctx in
- let fmt = Print.PC.ctx_to_rtype_formatter fmt in
- Print.PT.rty_to_string fmt ty
+let ty_to_string (ctx : bs_ctx) (ty : T.ty) : string =
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Types.ty_to_string env ty
-let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
- let type_decls = ctx.type_context.llbc_type_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
- let fmt =
- PrintPure.mk_type_formatter type_decls global_decls ctx.trait_decls_ctx
- ctx.trait_impls_ctx def.generics.types def.generics.const_generics
- in
- PrintPure.type_decl_to_string fmt def
+let type_decl_to_string (ctx : bs_ctx) (def : T.type_decl) : string =
+ let env = bs_ctx_to_fmt_env ctx in
+ Print.Types.type_decl_to_string env def
+
+let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.type_decl_to_string env def
let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
- let fmt = bs_ctx_to_pp_ast_formatter ctx in
- PrintPure.texpression_to_string fmt false "" " " e
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.texpression_to_string env false "" " " e
let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
- let type_params = sg.generics.types in
- let cg_params = sg.generics.const_generics in
- let type_decls = ctx.type_context.llbc_type_decls in
- let fun_decls = ctx.fun_context.llbc_fun_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
- let fmt =
- PrintPure.mk_ast_formatter type_decls fun_decls global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
- in
- PrintPure.fun_sig_to_string fmt sg
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.fun_sig_to_string env sg
let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
- let generics = def.signature.generics in
- let type_params = generics.types in
- let cg_params = generics.const_generics in
- let type_decls = ctx.type_context.llbc_type_decls in
- let fun_decls = ctx.fun_context.llbc_fun_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
- let fmt =
- PrintPure.mk_ast_formatter type_decls fun_decls global_decls
- ctx.trait_decls_ctx ctx.trait_impls_ctx type_params cg_params
- in
- PrintPure.fun_decl_to_string fmt def
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.fun_decl_to_string env def
let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
- let fmt = bs_ctx_to_pp_ast_formatter ctx in
- PrintPure.typed_pattern_to_string fmt p
+ let env = bs_ctx_to_pure_fmt_env ctx in
+ PrintPure.typed_pattern_to_string env p
(* TODO: move *)
let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
- let fmt = bs_ctx_to_ast_formatter ctx in
- let fmt = Print.Contexts.ast_to_value_formatter fmt in
+ let env = bs_ctx_to_fmt_env ctx in
let verbose = false in
let indent = "" in
let indent_incr = " " in
- Print.Values.abs_to_string fmt verbose indent indent_incr abs
+ Print.Values.abs_to_string env verbose indent indent_incr abs
let get_instantiated_fun_sig (fun_id : A.fun_id)
(back_id : T.RegionGroupId.id option) (generics : generic_args)
@@ -343,13 +324,13 @@ let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
(* TODO: move *)
let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
(back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
- let id = (E.Regular def_id, back_id) in
+ let id = (E.FRegular def_id, back_id) in
(RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg
(* Some generic translation functions (we need to translate different "flavours"
- of types: sty, forward types, backward types, etc.) *)
-let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
- (generics : 'r T.generic_args) : generic_args =
+ of types: forward types, backward types, etc.) *)
+let rec translate_generic_args (translate_ty : T.ty -> ty)
+ (generics : T.generic_args) : generic_args =
(* We ignore the regions: if they didn't cause trouble for the symbolic execution,
then everything's fine *)
let types = List.map translate_ty generics.types in
@@ -359,7 +340,7 @@ let rec translate_generic_args (translate_ty : 'r T.ty -> ty)
in
{ types; const_generics; trait_refs }
-and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
+and translate_trait_ref (translate_ty : T.ty -> ty) (tr : T.trait_ref) :
trait_ref =
let trait_id = translate_trait_instance_id translate_ty tr.trait_id in
let generics = translate_generic_args translate_ty tr.generics in
@@ -368,13 +349,13 @@ and translate_trait_ref (translate_ty : 'r T.ty -> ty) (tr : 'r T.trait_ref) :
in
{ trait_id; generics; trait_decl_ref }
-and translate_trait_decl_ref (translate_ty : 'r T.ty -> ty)
- (tr : 'r T.trait_decl_ref) : trait_decl_ref =
+and translate_trait_decl_ref (translate_ty : T.ty -> ty) (tr : T.trait_decl_ref)
+ : trait_decl_ref =
let decl_generics = translate_generic_args translate_ty tr.decl_generics in
{ trait_decl_id = tr.trait_decl_id; decl_generics }
-and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
- (id : 'r T.trait_instance_id) : trait_instance_id =
+and translate_trait_instance_id (translate_ty : T.ty -> ty)
+ (id : T.trait_instance_id) : trait_instance_id =
let translate_trait_instance_id = translate_trait_instance_id translate_ty in
match id with
| T.Self -> Self
@@ -393,19 +374,20 @@ and translate_trait_instance_id (translate_ty : 'r T.ty -> ty)
| FnPointer _ -> raise (Failure "TODO")
| UnknownTrait s -> raise (Failure ("Unknown trait found: " ^ s))
-let rec translate_sty (ty : T.sty) : ty =
+(** Translate a signature type - TODO: factor out the different translation functions *)
+let rec translate_sty (ty : T.ty) : ty =
let translate = translate_sty in
match ty with
- | T.Adt (type_id, generics) -> (
+ | T.TAdt (type_id, generics) -> (
let generics = translate_sgeneric_args generics in
match type_id with
- | T.AdtId adt_id -> Adt (AdtId adt_id, generics)
- | T.Tuple ->
+ | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
+ | T.TTuple ->
assert (generics.const_generics = []);
mk_simpl_tuple_ty generics.types
- | T.Assumed aty -> (
+ | T.TAssumed aty -> (
match aty with
- | T.Box -> (
+ | T.TBox -> (
(* Eliminate the boxes *)
match generics.types with
| [ ty ] -> ty
@@ -414,40 +396,40 @@ let rec translate_sty (ty : T.sty) : ty =
(Failure
"Box/vec/option type with incorrect number of arguments")
)
- | T.Array -> Adt (Assumed Array, generics)
- | T.Slice -> Adt (Assumed Slice, generics)
- | T.Str -> Adt (Assumed Str, generics)))
- | TypeVar vid -> TypeVar vid
- | Literal ty -> Literal ty
- | Never -> raise (Failure "Unreachable")
- | Ref (_, rty, _) -> translate rty
- | RawPtr (ty, rkind) ->
- let mut = match rkind with Mut -> Mut | Shared -> Const in
+ | T.TArray -> TAdt (TAssumed TArray, generics)
+ | T.TSlice -> TAdt (TAssumed TSlice, generics)
+ | T.TStr -> TAdt (TAssumed TStr, generics)))
+ | TVar vid -> TVar vid
+ | TLiteral ty -> TLiteral ty
+ | TNever -> raise (Failure "Unreachable")
+ | TRef (_, rty, _) -> translate rty
+ | TRawPtr (ty, rkind) ->
+ let mut = match rkind with RMut -> Mut | RShared -> Const in
let ty = translate ty in
let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
- Adt (Assumed (RawPtr mut), generics)
- | TraitType (trait_ref, generics, type_name) ->
+ TAdt (TAssumed (TRawPtr mut), generics)
+ | TTraitType (trait_ref, generics, type_name) ->
let trait_ref = translate_strait_ref trait_ref in
let generics = translate_sgeneric_args generics in
- TraitType (trait_ref, generics, type_name)
- | Arrow _ -> raise (Failure "TODO")
+ TTraitType (trait_ref, generics, type_name)
+ | TArrow _ -> raise (Failure "TODO")
-and translate_sgeneric_args (generics : T.sgeneric_args) : generic_args =
+and translate_sgeneric_args (generics : T.generic_args) : generic_args =
translate_generic_args translate_sty generics
-and translate_strait_ref (tr : T.strait_ref) : trait_ref =
+and translate_strait_ref (tr : T.trait_ref) : trait_ref =
translate_trait_ref translate_sty tr
-and translate_strait_instance_id (id : T.strait_instance_id) : trait_instance_id
+and translate_strait_instance_id (id : T.trait_instance_id) : trait_instance_id
=
translate_trait_instance_id translate_sty id
let translate_trait_clause (clause : T.trait_clause) : trait_clause =
- let { T.clause_id; meta = _; trait_id; generics } = clause in
- let generics = translate_sgeneric_args generics in
+ let { T.clause_id; meta = _; trait_id; clause_generics } = clause in
+ let generics = translate_sgeneric_args clause_generics in
{ clause_id; trait_id; generics }
-let translate_strait_type_constraint (ttc : T.strait_type_constraint) :
+let translate_strait_type_constraint (ttc : T.trait_type_constraint) :
trait_type_constraint =
let { T.trait_ref; generics; type_name; ty } = ttc in
let trait_ref = translate_strait_ref trait_ref in
@@ -482,21 +464,30 @@ let translate_variant (v : T.variant) : variant =
let translate_variants (vl : T.variant list) : variant list =
List.map translate_variant vl
-(** Translate a type def kind to IM *)
+(** Translate a type def kind from LLBC *)
let translate_type_decl_kind (kind : T.type_decl_kind) : type_decl_kind =
match kind with
| T.Struct fields -> Struct (translate_fields fields)
| T.Enum variants -> Enum (translate_variants variants)
| T.Opaque -> Opaque
-(** Translate a type definition from IM
+(** Translate a type definition from LLBC
- TODO: this is not symbolic to pure but IM to pure. Still, I don't see the
- point of moving this definition for now.
+ Remark: this is not symbolic to pure but LLBC to pure. Still,
+ I don't see the point of moving this definition for now.
*)
-let translate_type_decl (def : T.type_decl) : type_decl =
+let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
+ type_decl =
+ log#ldebug
+ (lazy
+ (let ctx = Print.Contexts.decls_ctx_to_fmt_env ctx in
+ "translate_type_decl:\n\n"
+ ^ Print.Types.type_decl_to_string ctx def
+ ^ "\n"));
+ let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
let def_id = def.T.def_id in
- let name = def.name in
+ let llbc_name = def.name in
+ let name = Print.Types.name_to_string env def.name in
let { T.regions; types; const_generics; trait_clauses } = def.generics in
(* Can't translate types with regions for now *)
assert (regions = []);
@@ -504,43 +495,60 @@ let translate_type_decl (def : T.type_decl) : type_decl =
let generics = { types; const_generics; trait_clauses } in
let kind = translate_type_decl_kind def.T.kind in
let preds = translate_predicates def.preds in
- { def_id; name; generics; kind; preds }
+ let is_local = def.is_local in
+ let meta = def.meta in
+ {
+ def_id;
+ is_local;
+ llbc_name;
+ name;
+ meta;
+ generics;
+ llbc_generics = def.generics;
+ kind;
+ preds;
+ }
let translate_type_id (id : T.type_id) : type_id =
match id with
- | AdtId adt_id -> AdtId adt_id
- | T.Assumed aty ->
+ | TAdtId adt_id -> TAdtId adt_id
+ | TAssumed aty ->
let aty =
match aty with
- | T.Array -> Array
- | T.Slice -> Slice
- | T.Str -> Str
- | T.Box ->
+ | T.TArray -> TArray
+ | T.TSlice -> TSlice
+ | T.TStr -> TStr
+ | T.TBox ->
(* Boxes have to be eliminated: this type id shouldn't
be translated *)
raise (Failure "Unreachable")
in
- Assumed aty
- | T.Tuple -> Tuple
+ TAssumed aty
+ | TTuple -> TTuple
(** Translate a type, seen as an input/output of a forward function
- (preserve all borrows, etc.)
+ (preserve all borrows, etc.).
+
+ Remark: it doesn't matter whether the types has regions or erased regions
+ (both cases happen, actually).
+
+ TODO: factor out the various translation functions.
*)
-let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r 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.Adt (type_id, generics) -> (
+ | T.TAdt (type_id, generics) -> (
let t_generics = translate_fwd_generic_args type_infos generics in
(* Eliminate boxes and simplify tuples *)
match type_id with
- | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
+ | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
let type_id = translate_type_id type_id in
- Adt (type_id, t_generics)
- | Tuple ->
+ TAdt (type_id, t_generics)
+ | TTuple ->
(* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
identity *)
mk_simpl_tuple_ty t_generics.types
- | T.Assumed T.Box -> (
+ | TAssumed TBox -> (
(* We eliminate boxes *)
(* No general parametricity for now *)
assert (
@@ -555,41 +563,41 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
(Failure
"Unreachable: box/vec/option receives exactly one type \
parameter")))
- | TypeVar vid -> TypeVar vid
- | Never -> raise (Failure "Unreachable")
- | Literal lty -> Literal lty
- | Ref (_, rty, _) -> translate rty
- | RawPtr (ty, rkind) ->
- let mut = match rkind with Mut -> Mut | Shared -> Const in
+ | TVar vid -> TVar vid
+ | TNever -> raise (Failure "Unreachable")
+ | TLiteral lty -> TLiteral lty
+ | TRef (_, rty, _) -> translate rty
+ | TRawPtr (ty, rkind) ->
+ let mut = match rkind with RMut -> Mut | RShared -> Const in
let ty = translate ty in
let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in
- Adt (Assumed (RawPtr mut), generics)
- | TraitType (trait_ref, generics, type_name) ->
+ TAdt (TAssumed (TRawPtr mut), generics)
+ | TTraitType (trait_ref, generics, type_name) ->
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
let generics = translate_fwd_generic_args type_infos generics in
- TraitType (trait_ref, generics, type_name)
- | Arrow _ -> raise (Failure "TODO")
+ TTraitType (trait_ref, generics, type_name)
+ | TArrow _ -> raise (Failure "TODO")
-and translate_fwd_generic_args (type_infos : TA.type_infos)
- (generics : 'r T.generic_args) : generic_args =
+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 : 'r 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)
- (id : 'r T.trait_instance_id) : trait_instance_id =
+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
(** Simply calls [translate_fwd_ty] *)
-let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : 'r T.ty) : ty =
+let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
let type_infos = ctx.type_context.type_infos in
translate_fwd_ty type_infos ty
(** Simply calls [translate_fwd_generic_args] *)
-let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
- : generic_args =
+let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
+ generic_args =
let type_infos = ctx.type_context.type_infos in
translate_fwd_generic_args type_infos generics
@@ -599,21 +607,22 @@ let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : 'r T.generic_args)
[inside_mut]: are we inside a mutable borrow?
*)
-let rec translate_back_ty (type_infos : TA.type_infos)
- (keep_region : 'r -> bool) (inside_mut : bool) (ty : 'r T.ty) : ty option =
+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
(* A small helper for "leave" types *)
let wrap ty = if inside_mut then Some ty else None in
match ty with
- | T.Adt (type_id, generics) -> (
+ | T.TAdt (type_id, generics) -> (
match type_id with
- | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
+ | TAdtId _ | TAssumed (TArray | TSlice | TStr) ->
let type_id = translate_type_id type_id in
if inside_mut then
(* We do not want to filter anything, so we translate the generics
as "forward" types *)
let generics = translate_fwd_generic_args type_infos generics in
- Some (Adt (type_id, generics))
+ Some (TAdt (type_id, generics))
else
(* If not inside a mutable reference: check if at least one
of the generics contains a mutable reference (i.e., is not
@@ -624,9 +633,9 @@ let rec translate_back_ty (type_infos : TA.type_infos)
let types = List.filter_map translate generics.types in
if types <> [] then
let generics = translate_fwd_generic_args type_infos generics in
- Some (Adt (type_id, generics))
+ Some (TAdt (type_id, generics))
else None
- | Assumed T.Box -> (
+ | TAssumed TBox -> (
(* Don't accept ADTs (which are not tuples) with borrows for now *)
assert (not (TypesUtils.ty_has_borrows type_infos ty));
(* Eliminate the box *)
@@ -636,7 +645,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
raise
(Failure "Unreachable: boxes receive exactly one type parameter")
)
- | T.Tuple -> (
+ | TTuple -> (
(* Tuples can contain borrows (which we eliminate) *)
let tys_t = List.filter_map translate generics.types in
match tys_t with
@@ -645,35 +654,35 @@ let rec translate_back_ty (type_infos : TA.type_infos)
(* Note that if there is exactly one type, [mk_simpl_tuple_ty]
* is the identity *)
Some (mk_simpl_tuple_ty tys_t)))
- | TypeVar vid -> wrap (TypeVar vid)
- | Never -> raise (Failure "Unreachable")
- | Literal lty -> wrap (Literal lty)
- | Ref (r, rty, rkind) -> (
+ | TVar vid -> wrap (TVar vid)
+ | TNever -> raise (Failure "Unreachable")
+ | TLiteral lty -> wrap (TLiteral lty)
+ | TRef (r, rty, rkind) -> (
match rkind with
- | T.Shared ->
+ | RShared ->
(* Ignore shared references, unless we are below a mutable borrow *)
if inside_mut then translate rty else None
- | T.Mut ->
+ | RMut ->
(* Dive in, remembering the fact that we are inside a mutable borrow *)
let inside_mut = true in
if keep_region r then
translate_back_ty type_infos keep_region inside_mut rty
else None)
- | RawPtr _ ->
+ | TRawPtr _ ->
(* TODO: not sure what to do here *)
None
- | TraitType (trait_ref, generics, type_name) ->
+ | TTraitType (trait_ref, generics, type_name) ->
assert (generics.regions = []);
(* Translate the trait ref and the generics as "forward" generics -
we do not want to filter any type *)
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
let generics = translate_fwd_generic_args type_infos generics in
- Some (TraitType (trait_ref, generics, type_name))
- | Arrow _ -> raise (Failure "TODO")
+ Some (TTraitType (trait_ref, generics, type_name))
+ | TArrow _ -> raise (Failure "TODO")
(** Simply calls [translate_back_ty] *)
let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
- (inside_mut : bool) (ty : 'r T.ty) : ty option =
+ (inside_mut : bool) (ty : T.ty) : ty option =
let type_infos = ctx.type_context.type_infos in
translate_back_ty type_infos keep_region inside_mut ty
@@ -682,7 +691,7 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
T.ConstGenericVarId.Map.of_list
(List.map
(fun (cg : T.const_generic_var) ->
- (cg.index, ctx_translate_fwd_ty ctx (T.Literal cg.ty)))
+ (cg.index, ctx_translate_fwd_ty ctx (T.TLiteral cg.ty)))
ctx.sg.generics.const_generics)
in
let env = VarId.Map.empty in
@@ -803,11 +812,11 @@ 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
- | TraitMethod (_, _, fid) | FunId (Regular fid) ->
+ | TraitMethod (_, _, fid) | FunId (FRegular fid) ->
let info = A.FunDeclId.Map.find fid fun_infos in
let stateful_group = info.stateful in
let stateful =
@@ -820,7 +829,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
can_diverge = info.can_diverge;
is_rec = info.is_rec || Option.is_some lid;
}
- | FunId (Assumed aid) ->
+ | FunId (FAssumed aid) ->
assert (lid = None);
{
can_fail = Assumed.assumed_fun_can_fail aid;
@@ -844,11 +853,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
let fun_infos = decls_ctx.fun_ctx.fun_infos in
let type_infos = decls_ctx.type_ctx.type_infos in
(* Retrieve the list of parent backward functions *)
+ let regions_hierarchy =
+ FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
+ in
let gid, parents =
match bid with
| None -> (None, T.RegionGroupId.Set.empty)
| Some bid ->
- let parents = list_ancestor_region_groups sg bid in
+ let parents = list_ancestor_region_groups regions_hierarchy bid in
(Some bid, parents)
in
(* Is the function stateful, and can it fail? *)
@@ -861,21 +873,21 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
(* Create the context *)
let ctx =
let region_groups =
- List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy
+ List.map (fun (g : T.region_group) -> g.id) regions_hierarchy
in
let ctx =
InterpreterUtils.initialize_eval_context decls_ctx region_groups
sg.generics.types sg.generics.const_generics
in
(* Compute the normalization map for the *sty* types and add it to the context *)
- AssociatedTypes.ctx_add_norm_trait_stypes_from_preds ctx
+ AssociatedTypes.ctx_add_norm_trait_types_from_preds ctx
sg.preds.trait_type_constraints
in
(* Normalize the signature *)
let sg =
let ({ A.inputs; output; _ } : A.fun_sig) = sg in
- let norm = AssociatedTypes.ctx_normalize_sty ctx in
+ let norm = AssociatedTypes.ctx_normalize_ty ctx in
let inputs = List.map norm inputs in
let output = norm output in
{ sg with A.inputs; output }
@@ -893,14 +905,14 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
* so just check that there aren't parent regions *)
assert (T.RegionGroupId.Set.is_empty parents);
(* Small helper to translate types for backward functions *)
- let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.sty -> ty option
- =
- let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
- let regions = T.RegionVarId.Set.of_list rg.regions in
+ let translate_back_ty_for_gid (gid : T.RegionGroupId.id) : T.ty -> ty option =
+ let rg = T.RegionGroupId.nth regions_hierarchy gid in
+ let regions = T.RegionId.Set.of_list rg.regions in
let keep_region r =
match r with
- | T.Static -> raise Unimplemented
- | T.Var r -> T.RegionVarId.Set.mem r regions
+ | T.RStatic -> raise Unimplemented
+ | T.RErased -> raise (Failure "Unexpected erased region")
+ | T.RVar r -> T.RegionId.Set.mem r regions
in
let inside_mut = false in
translate_back_ty type_infos keep_region inside_mut
@@ -1026,8 +1038,18 @@ let translate_fun_sig (decls_ctx : C.decls_ctx) (fun_id : A.fun_id)
effect_info;
}
in
- let preds = translate_predicates sg.A.preds in
- let sg = { generics; preds; inputs; output; doutputs; info } in
+ let preds = translate_predicates sg.preds in
+ let sg =
+ {
+ generics;
+ llbc_generics = sg.generics;
+ preds;
+ inputs;
+ output;
+ doutputs;
+ info;
+ }
+ in
{ sg; output_names }
let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
@@ -1042,7 +1064,7 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
(* Return *)
(ctx, state_pat)
-let fresh_var_llbc_ty (basename : string option) (ty : 'r T.ty) (ctx : bs_ctx) :
+let fresh_var_llbc_ty (basename : string option) (ty : T.ty) (ctx : bs_ctx) :
bs_ctx * var =
(* Generate the fresh variable *)
let id, var_counter = VarId.fresh ctx.var_counter in
@@ -1106,7 +1128,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
(** Peel boxes as long as the value is of the form [Box<T>] *)
let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
match (v.value, v.ty) with
- | V.Adt av, T.Adt (T.Assumed T.Box, _) -> (
+ | V.VAdt av, T.TAdt (T.TAssumed T.TBox, _) -> (
match av.field_values with
| [ bv ] -> unbox_typed_value bv
| _ -> raise (Failure "Unreachable"))
@@ -1145,13 +1167,13 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
(* Translate the value *)
let value =
match v.value with
- | V.Literal cv -> { e = Const cv; ty }
- | Adt av -> (
+ | VLiteral cv -> { e = Const cv; ty }
+ | VAdt av -> (
let variant_id = av.variant_id in
let field_values = List.map translate av.field_values in
(* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
match v.ty with
- | T.Adt (T.Tuple, _) ->
+ | TAdt (TTuple, _) ->
assert (variant_id = None);
mk_simpl_tuple_texpression field_values
| _ ->
@@ -1169,27 +1191,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
let cons = { e = cons_e; ty = cons_ty } in
(* Apply the constructor *)
mk_apps cons field_values)
- | Bottom -> raise (Failure "Unreachable")
- | Loan lc -> (
+ | VBottom -> raise (Failure "Unreachable")
+ | VLoan lc -> (
match lc with
- | SharedLoan (_, v) -> translate v
- | MutLoan _ -> raise (Failure "Unreachable"))
- | Borrow bc -> (
+ | VSharedLoan (_, v) -> translate v
+ | VMutLoan _ -> raise (Failure "Unreachable"))
+ | VBorrow bc -> (
match bc with
- | V.SharedBorrow bid ->
+ | VSharedBorrow bid ->
(* Lookup the shared value in the context, and continue *)
let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
translate sv
- | V.ReservedMutBorrow bid ->
+ | VReservedMutBorrow bid ->
(* Same as for shared borrows. However, note that we use reserved borrows
* only in *meta-data*: a value *actually used* in the translation can't come
* from an unpromoted reserved borrow *)
let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
translate sv
- | V.MutBorrow (_, v) ->
+ | VMutBorrow (_, v) ->
(* Borrows are the identity in the extraction *)
translate v)
- | Symbolic sv -> symbolic_value_to_texpression ctx sv
+ | VSymbolic sv -> symbolic_value_to_texpression ctx sv
in
(* Debugging *)
log#ldebug
@@ -1229,10 +1251,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
(* For now, only tuples can contain borrows *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
+ | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
assert (field_values = []);
None
- | T.Tuple ->
+ | TTuple ->
(* Return *)
if field_values = [] then None
else
@@ -1374,10 +1396,10 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
* vector value upon visiting the "abstraction borrow" node *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
+ | TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
assert (field_values = []);
(ctx, None)
- | T.Tuple ->
+ | TTuple ->
(* Return *)
let variant_id = adt_v.variant_id in
assert (variant_id = None);
@@ -1488,11 +1510,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
(call_info.forward, abs_ancestors)
(** Add meta-information to an expression *)
-let mk_meta_symbolic_assignments (vars : var list) (values : texpression list)
+let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
(e : texpression) : texpression =
let var_values = List.combine vars values in
List.fold_right
- (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+ (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e)
var_values e
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1508,7 +1530,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
| Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
| IntroSymbolic (ectx, p, sv, v, e) ->
translate_intro_symbolic ectx p sv v e ctx
- | Meta (meta, e) -> translate_meta meta e ctx
+ | Meta (meta, e) -> translate_emeta meta e ctx
| ForwardEnd (ectx, loop_input_values, e, back_e) ->
translate_forward_end ectx loop_input_values e back_e ctx
| Loop loop -> translate_loop loop ctx
@@ -1645,7 +1667,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
log#ldebug
(lazy
("translate_function_call:\n"
- ^ ctx_egeneric_args_to_string ctx call.generics));
+ ^ ctx_generic_args_to_string ctx call.generics));
(* Translate the function call *)
let generics = ctx_translate_fwd_generic_args ctx call.generics in
let args =
@@ -1787,13 +1809,13 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
log#ldebug
(lazy
("translate_end_abstraction_synth_input:" ^ "\n- function: "
- ^ Print.name_to_string ctx.fun_decl.name
+ ^ name_to_string ctx ctx.fun_decl.name
^ "\n- rg_id: "
^ 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
@@ -1845,11 +1867,12 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
("translate_end_abstraction_synth_input:"
^ "\n\n- given back variables types:\n"
^ Print.list_to_string
- (fun (v : var) -> ty_to_string ctx v.ty)
+ (fun (v : var) -> pure_ty_to_string ctx v.ty)
given_back_variables
^ "\n\n- consumed values:\n"
^ Print.list_to_string
- (fun e -> texpression_to_string ctx e ^ " : " ^ ty_to_string ctx e.ty)
+ (fun e ->
+ texpression_to_string ctx e ^ " : " ^ pure_ty_to_string ctx e.ty)
consumed_values
^ "\n"));
@@ -1948,7 +1971,8 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
^ "\n- inst_sg.inputs ("
^ string_of_int (List.length inst_sg.inputs)
^ "): "
- ^ String.concat ", " (List.map (ty_to_string ctx) inst_sg.inputs)));
+ ^ String.concat ", "
+ (List.map (pure_ty_to_string ctx) inst_sg.inputs)));
List.iter
(fun (x, ty) -> assert ((x : texpression).ty = ty))
(List.combine inputs inst_sg.inputs);
@@ -2070,8 +2094,9 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
log#ldebug
(lazy
("\n- given_back ty: "
- ^ ty_to_string ctx given_back.ty
- ^ "\n- sig input ty: " ^ ty_to_string ctx input.ty));
+ ^ pure_ty_to_string ctx given_back.ty
+ ^ "\n- sig input ty: "
+ ^ pure_ty_to_string ctx input.ty));
assert (given_back.ty = input.ty))
given_back_inputs;
(* Translate the next expression *)
@@ -2098,7 +2123,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
(* Actually the same case as [SynthInput] *)
translate_end_abstraction_synth_input ectx abs e ctx rg_id
| V.LoopCall ->
- let fun_id = E.Regular ctx.fun_decl.A.def_id in
+ let fun_id = E.FRegular ctx.fun_decl.def_id in
let effect_info =
get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
(Some vloop_id) (Some rg_id)
@@ -2202,7 +2227,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
var_values
in
let vars, values = List.split var_values in
- mk_meta_symbolic_assignments vars values next_e
+ mk_emeta_symbolic_assignments vars values next_e
else next_e
in
@@ -2229,7 +2254,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
let func =
{ id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args }
in
- let func_ty = mk_arrow (Literal Bool) mk_unit_ty in
+ let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in
let func = { e = Qualif func; ty = func_ty } in
let assertion = mk_apps func args in
mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
@@ -2325,12 +2350,12 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
(* We don't need to update the context: we don't introduce any
* new values/variables *)
let branch = translate_expression branch_e ctx in
- let pat = mk_typed_pattern_from_literal (PV.Scalar v) in
+ let pat = mk_typed_pattern_from_literal (VScalar v) in
{ pat; branch }
in
let branches = List.map translate_branch branches in
let otherwise = translate_expression otherwise ctx in
- let pat_ty = Literal (Integer int_ty) in
+ let pat_ty = TLiteral (TInteger int_ty) in
let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in
let otherwise : match_branch =
{ pat = otherwise_pat; branch = otherwise }
@@ -2379,7 +2404,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
let branch = translate_expression branch ctx in
match type_id with
- | T.AdtId adt_id ->
+ | TAdtId adt_id ->
(* Detect if this is an enumeration or not *)
let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
let is_enum = TypesUtils.type_decl_is_enum tdef in
@@ -2426,14 +2451,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
let field_proj = gen_field_proj fid var in
mk_let monadic (mk_typed_pattern_from_var var None) field_proj e)
id_var_pairs branch
- | T.Tuple ->
+ | TTuple ->
let vars = List.map (fun x -> mk_typed_pattern_from_var x None) vars in
let monadic = false in
mk_let monadic
(mk_simpl_tuple_pattern vars)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
- | T.Assumed T.Box ->
+ | TAssumed TBox ->
(* There should be exactly one variable *)
let var =
match vars with [ v ] -> v | _ -> raise (Failure "Unreachable")
@@ -2445,7 +2470,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
(mk_typed_pattern_from_var var None)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
- | T.Assumed (T.Array | T.Slice | T.Str) ->
+ | TAssumed (TArray | TSlice | TStr) ->
(* We can't expand those values: we can access the fields only
* through the functions provided by the API (note that we don't
* know how to expand values like vectors or arrays, because they have a variable number
@@ -2469,19 +2494,19 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
*)
let v =
match v with
- | SingleValue v -> typed_value_to_texpression ctx ectx v
- | Array values ->
+ | VaSingleValue v -> typed_value_to_texpression ctx ectx v
+ | VaArray values ->
(* We use a struct update to encode the array aggregate, in order
to preserve the structure and allow generating code of the shape
`[x0, ...., xn]` *)
let values = List.map (typed_value_to_texpression ctx ectx) values in
let values = FieldId.mapi (fun fid v -> (fid, v)) values in
let su : struct_update =
- { struct_id = Assumed Array; init = None; updates = values }
+ { struct_id = TAssumed TArray; init = None; updates = values }
in
{ e = StructUpdate su; ty = var.ty }
- | ConstGenericValue cg_id -> { e = CVar cg_id; ty = var.ty }
- | TraitConstValue (trait_ref, generics, const_name) ->
+ | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
+ | VaTraitConstValue (trait_ref, generics, const_name) ->
let type_infos = ctx.type_context.type_infos in
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
let generics = translate_fwd_generic_args type_infos generics in
@@ -2558,7 +2583,7 @@ and translate_forward_end (ectx : C.eval_ctx)
let org_args = args in
(* Lookup the effect info for the loop function *)
- let fid = E.Regular ctx.fun_decl.A.def_id in
+ let fid = E.FRegular ctx.fun_decl.def_id in
let effect_info =
get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
in
@@ -2633,7 +2658,7 @@ and translate_forward_end (ectx : C.eval_ctx)
We then remove all the meta information from the body *before* calling
{!PureMicroPasses.decompose_loops}.
*)
- mk_meta_symbolic_assignments loop_info.input_vars org_args e
+ mk_emeta_symbolic_assignments loop_info.input_vars org_args e
and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
@@ -2661,7 +2686,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
^ T.RegionGroupId.Map.show
(fun (rids, tys) ->
"(" ^ T.RegionId.Set.show rids ^ ", "
- ^ Print.list_to_string (rty_to_string ctx) tys
+ ^ Print.list_to_string (ty_to_string ctx) tys
^ ")")
loop.rg_to_given_back_tys
^ "\n"));
@@ -2728,12 +2753,10 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
call to the loop forward function) *)
let generics =
let { types; const_generics; trait_clauses } = ctx.sg.generics in
- let types =
- List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) types
- in
+ let types = List.map (fun (ty : T.type_var) -> TVar ty.T.index) types in
let const_generics =
List.map
- (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
+ (fun (cg : T.const_generic_var) -> T.CgVar cg.T.index)
const_generics
in
let trait_refs =
@@ -2793,6 +2816,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
{
fun_end;
loop_id;
+ meta = loop.meta;
fuel0 = ctx.fuel0;
fuel = ctx.fuel;
input_state;
@@ -2808,7 +2832,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let ty = fun_end.ty in
{ e = loop; ty }
-and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) :
texpression =
let next_e = translate_expression e ctx in
let meta =
@@ -2909,24 +2933,28 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
log#ldebug
(lazy
("SymbolicToPure.translate_fun_decl: "
- ^ Print.fun_name_to_string def.A.name
+ ^ name_to_string ctx def.name
^ " ("
^ Print.option_to_string T.RegionGroupId.to_string bid
^ ")\n"));
(* Translate the declaration *)
- let def_id = def.A.def_id in
- let basename = def.name in
+ let def_id = def.def_id in
+ let llbc_name = def.name in
+ let name = name_to_string ctx llbc_name in
(* Retrieve the signature *)
let signature = ctx.sg in
+ let regions_hierarchy =
+ FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies
+ in
(* Translate the body, if there is *)
let body =
match body with
| None -> None
| Some body ->
let effect_info =
- get_fun_effect_info ctx.fun_context.fun_infos (FunId (Regular def_id))
- None bid
+ get_fun_effect_info ctx.fun_context.fun_infos
+ (FunId (FRegular def_id)) None bid
in
let body = translate_expression body ctx in
(* Add a match over the fuel, if necessary *)
@@ -2960,7 +2988,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
| None -> []
| Some back_id ->
let parents_ids =
- list_ordered_ancestor_region_groups def.signature back_id
+ list_ordered_ancestor_region_groups regions_hierarchy back_id
in
let backward_ids = List.append parents_ids [ back_id ] in
List.concat
@@ -2987,7 +3015,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
log#ldebug
(lazy
("SymbolicToPure.translate_fun_decl: "
- ^ Print.fun_name_to_string def.A.name
+ ^ name_to_string ctx def.name
^ " ("
^ Print.option_to_string T.RegionGroupId.to_string bid
^ ")" ^ "\n- forward_inputs: "
@@ -2999,8 +3027,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
^ "\n- back_state: "
^ String.concat ", " (List.map show_var back_state)
^ "\n- signature.inputs: "
- ^ String.concat ", " (List.map (ty_to_string ctx) signature.inputs)
- ));
+ ^ String.concat ", "
+ (List.map (pure_ty_to_string ctx) signature.inputs)));
(* TODO: we need to normalize the types *)
if !Config.type_check_pure_code then
assert (
@@ -3018,14 +3046,17 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
let loop_id = None in
(* Assemble the declaration *)
- let def =
+ let def : fun_decl =
{
def_id;
+ is_local = def.is_local;
+ meta = def.meta;
kind = def.kind;
num_loops;
loop_id;
back_id = bid;
- basename;
+ llbc_name;
+ name;
signature;
is_global_decl_body = def.is_global_decl_body;
body;
@@ -3039,8 +3070,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(* return *)
def
-let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
- List.map translate_type_decl type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
+ List.map (translate_type_decl ctx)
+ (TypeDeclId.Map.values ctx.type_ctx.type_decls)
(** Translates function signatures.
@@ -3064,19 +3096,23 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
let translate_one (fun_id : A.fun_id) (input_names : string option list)
(sg : A.fun_sig) : (regular_fun_id_not_loop * fun_sig_named_outputs) list
=
+ (* Retrieve the regions hierarchy *)
+ let regions_hierarchy =
+ FunIdMap.find fun_id decls_ctx.fun_ctx.regions_hierarchies
+ in
(* The forward function *)
let fwd_sg = translate_fun_sig decls_ctx fun_id sg input_names None in
let fwd_id = (fun_id, None) in
(* The backward functions *)
let back_sgs =
List.map
- (fun (rg : T.region_var_group) ->
+ (fun (rg : T.region_group) ->
let tsg =
translate_fun_sig decls_ctx fun_id sg input_names (Some rg.id)
in
let id = (fun_id, Some rg.id) in
(id, tsg))
- sg.regions_hierarchy
+ regions_hierarchy
in
(* Return *)
(fwd_id, fwd_sg) :: back_sgs
@@ -3089,14 +3125,16 @@ let translate_fun_signatures (decls_ctx : C.decls_ctx)
(fun m (id, sg) -> RegularFunIdNotLoopMap.add id sg m)
RegularFunIdNotLoopMap.empty translated
-let translate_trait_decl (type_infos : TA.type_infos)
- (trait_decl : A.trait_decl) : trait_decl =
+let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
+ : trait_decl =
let {
def_id;
- name;
- generics;
+ is_local;
+ name = llbc_name;
+ meta;
+ generics = llbc_generics;
preds;
- parent_clauses;
+ parent_clauses = llbc_parent_clauses;
consts;
types;
required_methods;
@@ -3104,9 +3142,15 @@ let translate_trait_decl (type_infos : TA.type_infos)
} : A.trait_decl =
trait_decl
in
- let generics = translate_generic_params generics in
+ let type_infos = ctx.type_ctx.type_infos in
+ let name =
+ Print.Types.name_to_string
+ (Print.Contexts.decls_ctx_to_fmt_env ctx)
+ llbc_name
+ in
+ let generics = translate_generic_params llbc_generics in
let preds = translate_predicates preds in
- let parent_clauses = List.map translate_trait_clause parent_clauses in
+ let parent_clauses = List.map translate_trait_clause llbc_parent_clauses in
let consts =
List.map
(fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3122,23 +3166,30 @@ let translate_trait_decl (type_infos : TA.type_infos)
in
{
def_id;
+ is_local;
+ llbc_name;
name;
+ meta;
generics;
+ llbc_generics;
preds;
parent_clauses;
+ llbc_parent_clauses;
consts;
types;
required_methods;
provided_methods;
}
-let translate_trait_impl (type_infos : TA.type_infos)
- (trait_impl : A.trait_impl) : trait_impl =
+let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
+ : trait_impl =
let {
A.def_id;
- name;
- impl_trait;
- generics;
+ is_local;
+ name = llbc_name;
+ meta;
+ impl_trait = llbc_impl_trait;
+ generics = llbc_generics;
preds;
parent_trait_refs;
consts;
@@ -3148,10 +3199,16 @@ let translate_trait_impl (type_infos : TA.type_infos)
} =
trait_impl
in
+ let type_infos = ctx.type_ctx.type_infos in
let impl_trait =
- translate_trait_decl_ref (translate_fwd_ty type_infos) impl_trait
+ translate_trait_decl_ref (translate_fwd_ty type_infos) llbc_impl_trait
+ in
+ let name =
+ Print.Types.name_to_string
+ (Print.Contexts.decls_ctx_to_fmt_env ctx)
+ llbc_name
in
- let generics = translate_generic_params generics in
+ let generics = translate_generic_params llbc_generics in
let preds = translate_predicates preds in
let parent_trait_refs = List.map translate_strait_ref parent_trait_refs in
let consts =
@@ -3169,9 +3226,14 @@ let translate_trait_impl (type_infos : TA.type_infos)
in
{
def_id;
+ is_local;
+ llbc_name;
name;
+ meta;
impl_trait;
+ llbc_impl_trait;
generics;
+ llbc_generics;
preds;
parent_trait_refs;
consts;