diff options
| -rw-r--r-- | src/CfimOfJson.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 23 | ||||
| -rw-r--r-- | src/Substitute.ml | 27 | ||||
| -rw-r--r-- | src/Values.ml | 2 |
4 files changed, 49 insertions, 7 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index dfa7527e..b693a4db 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -180,8 +180,8 @@ let var_of_json (js : json) : (var, string) result = | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] -> let* index = VarId.id_of_json index in let* name = string_option_of_json name in - let* ty = ety_of_json ty in - Ok { index; name; ty } + let* var_ty = ety_of_json ty in + Ok { index; name; var_ty } | _ -> Error "") let big_int_of_json (js : json) : (big_int, string) result = diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 74cbe70d..77af0b54 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1933,4 +1933,27 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : (C.eval_ctx * statement_eval_res) eval_result = + (* There are two cases * + - this is a local function, in which case we execute its body + - this is a non-local function, in which case there is a special treatment + *) + match call.func with + | A.Local fid -> + eval_local_function_call fid call.region_params call.type_params call.args + call.dest + | A.Assumed fid -> + eval_assumed_function_call fid call.region_params call.type_params + call.args call.dest + +and eval_local_function_call (fid : A.FunDefId.id) + (region_params : T.erased_region list) (type_params : T.ety list) + (args : E.operand list) (dest : E.place) : + (C.eval_ctx * statement_eval_res) eval_result = + (* Retrieve the (correctly instantiated) body *) + raise Unimplemented + +and eval_assumed_function_call (fid : A.assumed_fun_id) + (region_params : T.erased_region list) (type_params : T.ety list) + (args : E.operand list) (dest : E.place) : + (C.eval_ctx * statement_eval_res) eval_result = raise Unimplemented diff --git a/src/Substitute.ml b/src/Substitute.ml index 917275af..5cd62c0c 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -4,13 +4,14 @@ module T = Types module V = Values +module A = CfimAst module C = Contexts (** Substitute types variables and regions in a type *) -let rec ty_subst (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty) - (ty : 'r1 T.ty) : 'r2 T.ty = +let rec ty_substitute (rsubst : 'r1 -> 'r2) + (tsubst : T.TypeVarId.id -> 'r2 T.ty) (ty : 'r1 T.ty) : 'r2 T.ty = let open T in - let subst = ty_subst rsubst tsubst in + let subst = ty_substitute rsubst tsubst in (* helper *) match ty with | Adt (def_id, regions, tys) -> @@ -34,7 +35,7 @@ let rec ty_subst (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty) let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety) (ty : T.rty) : T.ety = let rsubst (r : T.RegionVarId.id T.region) : T.erased_region = T.Erased in - ty_subst rsubst tsubst ty + ty_substitute rsubst tsubst ty (** Create a type substitution from a list of type variable ids and a list of types (with which to substitute the type variable ids *) @@ -90,3 +91,21 @@ let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx) (types : T.ety list) : T.ety T.FieldId.vector = let def = C.ctx_lookup_type_def ctx def_id in type_def_get_instantiated_field_type def opt_variant_id types + +(** Apply a type substitution to an expression *) +let rec expression_substitute (tsubst : T.TypeVarId.id -> T.ety) + (e : A.expression) : A.expression = + raise Errors.Unimplemented + +(** Apply a type substitution to a function body. Return the local variables + and the body. *) +let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety) + (def : A.fun_def) : V.var V.VarId.vector * A.expression = + let rsubst r = r in + let locals = + V.VarId.map + (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty }) + def.A.locals + in + let body = expression_substitute tsubst def.body in + (locals, body) diff --git a/src/Values.ml b/src/Values.ml index 5c31feef..2c80cfe9 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -14,7 +14,7 @@ module RegionId = IdGen () type var = { index : VarId.id; (** Unique variable identifier *) name : string option; - ty : ety; + var_ty : ety; (** The variable type - erased type, because variables are not used ** in function signatures *) } |