diff options
Diffstat (limited to '')
| -rw-r--r-- | src/CfimAst.ml | 11 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 12 | ||||
| -rw-r--r-- | src/Substitute.ml | 4 | ||||
| -rw-r--r-- | src/Values.ml | 12 |
6 files changed, 23 insertions, 24 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 9acf40ff..0e36f6df 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -5,6 +5,17 @@ open Expressions module FunDefId = IdGen () +type var = { + index : VarId.id; (** Unique variable identifier *) + name : string option; + var_ty : ety; + (** The variable type - erased type, because variables are not used + ** in function signatures - TODO: useless? TODO: binder type for + function definitions *) +} +[@@deriving show] +(** A variable, as used in a function definition *) + type assumed_fun_id = BoxNew | BoxDeref | BoxDerefMut | BoxFree [@@deriving show] diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 383b8410..f16ae601 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -172,14 +172,14 @@ let type_def_of_json (js : json) : (T.type_def, string) result = Ok { T.def_id; name; region_params; type_params; kind } | _ -> Error "") -let var_of_json (js : json) : (V.var, string) result = +let var_of_json (js : json) : (A.var, string) result = combine_error_msgs js "var_of_json" (match js with | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] -> let* index = V.VarId.id_of_json index in let* name = string_option_of_json name in let* var_ty = ety_of_json ty in - Ok { V.index; name; var_ty } + Ok { A.index; name; var_ty } | _ -> Error "") let big_int_of_json (js : json) : (V.big_int, string) result = diff --git a/src/Interpreter.ml b/src/Interpreter.ml index b936fa70..21124c48 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -48,9 +48,9 @@ let mk_typed_value (ty : T.ety) (value : V.value) : V.typed_value = { V.value; ty } (* TODO: move *) -let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : V.var +let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var = - { V.index; name; var_ty } + { A.index; name; var_ty } (** Small helper *) let mk_place_from_var_id (var_id : V.VarId.id) : E.place = diff --git a/src/Print.ml b/src/Print.ml index dc559dc3..9c1aaa94 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -176,9 +176,6 @@ module Values = struct let var_id_to_string (id : V.VarId.id) : string = "var@" ^ V.VarId.to_string id - let var_to_string (v : V.var) : string = - match v.name with None -> var_id_to_string v.index | Some name -> name - let big_int_to_string (bi : V.big_int) : string = Z.to_string bi let scalar_value_to_string (sv : V.scalar_value) : string = @@ -765,6 +762,9 @@ module CfimAst = struct ^ statement_to_string fmt (indent ^ indent_incr) indent_incr loop_st ^ "\n" ^ indent ^ "}" + let var_to_string (v : A.var) : string = + match v.name with None -> PV.var_id_to_string v.index | Some name -> name + let fun_def_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (def : A.fun_def) : string = let rty_fmt = ast_to_rtype_formatter fmt in @@ -793,7 +793,7 @@ module CfimAst = struct let args = List.combine inputs sg.inputs in let args = List.map - (fun (var, rty) -> PV.var_to_string var ^ " : " ^ rty_to_string rty) + (fun (var, rty) -> var_to_string var ^ " : " ^ rty_to_string rty) args in let args = String.concat ", " args in @@ -808,7 +808,7 @@ module CfimAst = struct let locals = List.map (fun var -> - indent ^ indent_incr ^ PV.var_to_string var ^ " : " + indent ^ indent_incr ^ var_to_string var ^ " : " ^ ety_to_string var.var_ty ^ ";") def.locals in @@ -860,7 +860,7 @@ module Module = struct in let var_id_to_string vid = let var = V.VarId.nth def.locals vid in - PV.var_to_string var + PA.var_to_string var in let adt_variant_to_string = PC.type_ctx_to_adt_variant_to_string_fun type_context diff --git a/src/Substitute.ml b/src/Substitute.ml index 9099155f..3a2358f8 100644 --- a/src/Substitute.ml +++ b/src/Substitute.ml @@ -193,11 +193,11 @@ and switch_targets_substitute (tsubst : T.TypeVarId.id -> T.ety) (** 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 list * A.statement = + (def : A.fun_def) : A.var list * A.statement = let rsubst r = r in let locals = List.map - (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty }) + (fun v -> { v with A.var_ty = ty_substitute rsubst tsubst v.A.var_ty }) def.A.locals in let body = statement_substitute tsubst def.body in diff --git a/src/Values.ml b/src/Values.ml index 57a0aeb0..cb8a1200 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -17,18 +17,6 @@ module AbstractionId = IdGen () module RegionId = IdGen () -(* TODO: move? *) -type var = { - index : VarId.id; (** Unique variable identifier *) - name : string option; - var_ty : ety; - (** The variable type - erased type, because variables are not used - ** in function signatures - TODO: useless? TODO: binder type for - function definitions *) -} -[@@deriving show] -(** A variable, as used in a type definition *) - (** A variable *) type big_int = Z.t |