summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/InterpreterStatements.ml75
1 files changed, 67 insertions, 8 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index d67d57db..2a5c8952 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1188,8 +1188,64 @@ and eval_transparent_function_call_concrete (config : C.config)
and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
: st_cm_fun =
fun cf ctx ->
- (* Instantiate the signature and introduce fresh abstractions and region ids while doing so *)
- let func, def, self_trait_ref, inst_sg =
+ (* Instantiate the signature and introduce fresh abstractions and region ids while doing so.
+
+ We perform some manipulations when instantiating the signature.
+ In particular, we have a special treatment of trait method calls when
+ the trait ref is a known impl.
+
+ For instance:
+ {[
+ trait HasValue {
+ fn has_value(&self) -> bool;
+ }
+
+ impl<T> HasValue for Option<T> {
+ fn has_value(&self) {
+ match self {
+ None => false,
+ Some(_) => true,
+ }
+ }
+ }
+
+ fn option_has_value<T>(x: &Option<T>) -> bool {
+ x.has_value()
+ }
+ ]}
+
+ The generated code looks like this:
+ {[
+ structure HasValue (T : Type) = {
+ has_value : T -> result bool
+ }
+
+ let OptionHasValueImpl.has_value (T : Type) (self : T) : result bool =
+ match self with
+ | None => false
+ | Some _ => true
+
+ let OptionHasValueInstance (T : Type) : HasValue (Option T) = {
+ has_value = OptionHasValueInstance.has_value
+ }
+ ]}
+
+ In [option_has_value], we don't want to refer to the [has_value] method
+ of the instance of [HasValue] for [Option<T>]. We want to refer directly
+ to the function which implements [has_value] for [Option<T>].
+ That is, instead of generating this:
+ {[
+ let option_has_value (T : Type) (x : Option T) : result bool =
+ (OptionHasValueInstance T).has_value x
+ ]}
+
+ We want to generate this:
+ {[
+ let option_has_value (T : Type) (x : Option T) : result bool =
+ OptionHasValueImpl.has_value T x
+ ]}
+ *)
+ let func, generics, def, self_trait_ref, inst_sg =
match call.func with
| A.FunId (A.Regular fid) ->
let def = C.ctx_lookup_fun_decl ctx fid in
@@ -1197,7 +1253,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
let inst_sg =
instantiate_fun_sig ctx call.generics tr_self def.A.signature
in
- (call.func, def, None, inst_sg)
+ (call.func, call.generics, def, None, inst_sg)
| A.FunId (A.Assumed _) ->
(* Unreachable: must be a transparent function *)
raise (Failure "Unreachable")
@@ -1242,9 +1298,12 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
in
(* Also update the function identifier: we want to forget
the fact that we called a trait method, and treat it as
- a regular function acll. *)
+ a regular function call to the top-level function
+ which implements the method. In order to do this properly,
+ we also need to update the generics.
+ *)
let func = A.FunId (A.Regular id) in
- (func, method_def, None, inst_sg)
+ (func, generics, method_def, None, inst_sg)
| None ->
(* If not found, lookup the methods provided by the trait *declaration*
(remember: for now, we forbid overriding provided methods) *)
@@ -1299,7 +1358,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
(* We directly call the function, pretending it is not a trait method call *)
(* TODO: we need to add the self trait ref *)
let func = A.FunId (A.Regular method_def.def_id) in
- (func, method_def, Some trait_ref, inst_sg))
+ (func, generics, method_def, Some trait_ref, inst_sg))
| _ ->
(* We are using a local clause - we lookup the trait decl *)
let trait_decl =
@@ -1328,13 +1387,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
let inst_sg =
instantiate_fun_sig ctx generics tr_self method_def.A.signature
in
- (call.func, method_def, None, inst_sg))
+ (call.func, generics, method_def, None, inst_sg))
in
(* Sanity check *)
assert (List.length call.args = List.length def.A.signature.inputs);
(* Evaluate the function call *)
eval_function_call_symbolic_from_inst_sig config func inst_sg self_trait_ref
- call.generics call.args call.dest cf ctx
+ generics call.args call.dest cf ctx
(** Evaluate a function call in symbolic mode by using the function signature.