diff options
Diffstat (limited to 'compiler/SymbolicToPure.ml')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 75 |
1 files changed, 54 insertions, 21 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 922f0375..58fb6d04 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -474,10 +474,9 @@ let rec translate_sty (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_sgeneric_args (generics : T.generic_args) : generic_args = @@ -497,11 +496,10 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause = let translate_strait_type_constraint (ttc : T.trait_type_constraint) : trait_type_constraint = - let { T.trait_ref; generics; type_name; ty } = ttc in + let { T.trait_ref; type_name; ty } = ttc in let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in let ty = translate_sty ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let translate_predicates (preds : T.predicates) : predicates = let trait_type_constraints = @@ -638,10 +636,9 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_fwd_generic_args (type_infos : type_infos) @@ -737,16 +734,14 @@ let rec translate_back_ty (type_infos : type_infos) | TRawPtr _ -> (* TODO: not sure what to do here *) None - | TTraitType (trait_ref, generics, type_name) -> - assert (generics.regions = []); + | TTraitType (trait_ref, type_name) -> assert ( AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); if inside_mut then - (* Translate the trait ref and the generics as "forward" generics - + (* Translate the trait ref as a "forward" trait ref - 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 (TTraitType (trait_ref, generics, type_name)) + Some (TTraitType (trait_ref, type_name)) else None | TArrow _ -> raise (Failure "TODO") @@ -1895,7 +1890,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = | Panic -> translate_panic ctx | FunCall (call, e) -> translate_function_call call e ctx | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx - | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx + | EvalGlobal (gid, generics, sv, e) -> + translate_global_eval gid generics sv e ctx | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx | IntroSymbolic (ectx, p, sv, v, e) -> @@ -2667,11 +2663,12 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) (* Create the let-binding *) mk_let effect_info.can_fail output call next_e) -and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value) - (e : S.expression) (ctx : bs_ctx) : texpression = +and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args) + (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression = let ctx, var = fresh_var_for_symbolic_value sval ctx in let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in - let global_expr = { id = Global gid; generics = empty_generic_args } in + let generics = ctx_translate_fwd_generic_args ctx generics in + let global_expr = { id = Global gid; generics } in (* We use translate_fwd_ty to translate the global type *) let ty = ctx_translate_fwd_ty ctx decl.ty in let gval = { e = Qualif global_expr; ty } in @@ -2956,11 +2953,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) in { e = StructUpdate su; ty = var.ty } | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } - | VaTraitConstValue (trait_ref, generics, const_name) -> + | VaTraitConstValue (trait_ref, const_name) -> let type_infos = ctx.type_ctx.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 - let qualif_id = TraitConst (trait_ref, generics, const_name) in + let qualif_id = TraitConst (trait_ref, const_name) in let qualif = { id = qualif_id; generics = empty_generic_args } in { e = Qualif qualif; ty = var.ty } in @@ -3844,3 +3840,40 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) required_methods; provided_methods; } + +let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : + global_decl = + let { + A.meta; + def_id; + is_local; + name = llbc_name; + generics = llbc_generics; + preds; + ty; + kind; + body = body_id; + } = + decl + 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 ty = translate_fwd_ty ctx.type_ctx.type_infos ty in + { + meta; + def_id; + is_local; + llbc_name; + name; + llbc_generics; + generics; + preds; + ty; + kind; + body_id; + } |