Merge pull request #512 from Nadrieril/properly-bind-methods

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.59"
+let supported_charon_version = "0.1.60"

charon-ml/src/GAstUtils.ml

@@ -41,6 +41,68 @@ let locals_get_input_vars (locals : locals) : var list =
 let fun_body_get_input_vars (fbody : 'body gexpr_body) : var list =
   locals_get_input_vars fbody.locals
 
+(** Like `binder` but for the free variables bound by the generics of an item.
+    This is not present in the charon ast but returned by helpers so we don't
+    forget to substitute. Use `Substitute.apply_args_to_item_binder` to get the
+    correctly-substituted inner value. *)
+type 'a item_binder = {
+  item_binder_params : generic_params;
+  item_binder_value : 'a;
+}
+[@@deriving show, ord]
+
+(** Lookup a method in this trait decl. The two levels of binders in the output
+    reflect that there are two binding levels: the trait generics and the method
+    generics. *)
+let lookup_trait_decl_method (tdecl : trait_decl) (name : trait_item_name) :
+    fun_decl_ref binder item_binder option =
+  Option.map
+    (fun (_, bound_fn) ->
+      { item_binder_params = tdecl.generics; item_binder_value = bound_fn })
+    (List.find_opt
+       (fun (s, _) -> s = name)
+       (tdecl.required_methods @ tdecl.provided_methods))
+
+(** Lookup a method in this trait decl. The two levels of binders in the output
+    reflect that there are two binding levels: the trait generics and the method
+    generics. *)
+let lookup_trait_decl_provided_method (tdecl : trait_decl)
+    (name : trait_item_name) : fun_decl_ref binder item_binder option =
+  Option.map
+    (fun (_, bound_fn) ->
+      { item_binder_params = tdecl.generics; item_binder_value = bound_fn })
+    (List.find_opt (fun (s, _) -> s = name) tdecl.provided_methods)
+
+(** Lookup a method in this trait decl. The two levels of binders in the output
+    reflect that there are two binding levels: the trait generics and the method
+    generics. *)
+let lookup_trait_decl_required_method (tdecl : trait_decl)
+    (name : trait_item_name) : fun_decl_ref binder item_binder option =
+  Option.map
+    (fun (_, bound_fn) ->
+      { item_binder_params = tdecl.generics; item_binder_value = bound_fn })
+    (List.find_opt (fun (s, _) -> s = name) tdecl.required_methods)
+
+(** Lookup a method in this trait impl. The two levels of binders in the output
+    reflect that there are two binding levels: the impl generics and the method
+    generics. *)
+let lookup_trait_impl_provided_method (timpl : trait_impl)
+    (name : trait_item_name) : fun_decl_ref binder item_binder option =
+  Option.map
+    (fun (_, bound_fn) ->
+      { item_binder_params = timpl.generics; item_binder_value = bound_fn })
+    (List.find_opt (fun (s, _) -> s = name) timpl.provided_methods)
+
+(** Lookup a method in this trait impl. The two levels of binders in the output
+    reflect that there are two binding levels: the impl generics and the method
+    generics. *)
+let lookup_trait_impl_required_method (timpl : trait_impl)
+    (name : trait_item_name) : fun_decl_ref binder item_binder option =
+  Option.map
+    (fun (_, bound_fn) ->
+      { item_binder_params = timpl.generics; item_binder_value = bound_fn })
+    (List.find_opt (fun (s, _) -> s = name) timpl.required_methods)
+
 let g_declaration_group_to_list (g : 'a g_declaration_group) : 'a list =
   match g with
   | RecGroup ids -> ids

charon-ml/src/NameMatcher.ml

@@ -729,7 +729,7 @@ let match_fn_ptr (ctx : ctx) (c : match_config) (p : pattern) (func : E.fn_ptr)
             then
               let subst =
                 Substitute.make_subst_from_generics d.signature.generics
-                  func.generics Self
+                  func.generics
               in
               let trait_ref =
                 Substitute.trait_decl_ref_substitute subst trait_ref

charon-ml/src/PrintGAst.ml

@@ -179,13 +179,17 @@ let trait_decl_to_string (env : 'a fmt_env) (indent : string)
     let required_methods =
       List.map
         (fun (name, f) ->
-          indent1 ^ "fn " ^ name ^ " : " ^ fun_decl_id_to_string env f ^ "\n")
+          indent1 ^ "fn " ^ name ^ " : "
+          ^ fun_decl_id_to_string env f.binder_value.fun_id
+          ^ "\n")
         def.required_methods
     in
     let provided_methods =
       List.map
         (fun (name, f) ->
-          indent1 ^ "fn " ^ name ^ " : " ^ fun_decl_id_to_string env f ^ "\n")
+          indent1 ^ "fn " ^ name ^ " : "
+          ^ fun_decl_id_to_string env f.binder_value.fun_id
+          ^ "\n")
         def.provided_methods
     in
     let items =
@@ -249,7 +253,9 @@ let trait_impl_to_string (env : 'a fmt_env) (indent : string)
         def.types
     in
     let env_method (name, f) =
-      indent1 ^ "fn " ^ name ^ " : " ^ fun_decl_id_to_string env f ^ "\n"
+      indent1 ^ "fn " ^ name ^ " : "
+      ^ fun_decl_id_to_string env f.binder_value.fun_id
+      ^ "\n"
     in
     let required_methods = List.map env_method def.required_methods in
     let provided_methods = List.map env_method def.provided_methods in

charon-ml/src/Substitute.ml

@@ -4,6 +4,7 @@
 
 open Types
 open TypesUtils
+open GAstUtils
 open Expressions
 open LlbcAst
 
@@ -44,6 +45,7 @@ let empty_subst : subst =
     tr_self = Self;
   }
 
+(** The do-nothing substitution when used with `subst_free_vars` *)
 let empty_bound_sb_subst : single_binder_subst =
   {
     r_sb_subst = compose empty_subst.r_subst zero_db_var;
@@ -53,6 +55,7 @@ let empty_bound_sb_subst : single_binder_subst =
     tr_sb_self = empty_subst.tr_self;
   }
 
+(** The do-nothing substitution when used with `subst_at_binder_zero` *)
 let empty_free_sb_subst : single_binder_subst =
   let free x = Free x in
   {
@@ -64,7 +67,7 @@ let empty_free_sb_subst : single_binder_subst =
   }
 
 let error_sb_subst : single_binder_subst =
-  let error _ = failwith "Unexpected bound Cariable" in
+  let error _ = failwith "Unexpected bound variable" in
   {
     r_sb_subst = compose empty_subst.r_subst error;
     ty_sb_subst = compose empty_subst.ty_subst error;
@@ -116,25 +119,53 @@ let subst_remove_binder_zero (subst : single_binder_subst) : subst =
     tr_self = subst.tr_sb_self;
   }
 
+(** Visitor that shifts all bound variables by the given delta *)
+let st_shift_visitor =
+  object (self)
+    inherit [_] map_statement
+    method! visit_de_bruijn_id delta dbid = dbid + delta
+  end
+
+(* Shift the the substitution under one binder. *)
+let shift_subst (subst : subst) : subst =
+  (* We decrement the input because the variables we encounter will be bound
+     deeper. We shift the output so that it's valid at the new depth we're
+     substituting it into. *)
+  {
+    r_subst =
+      compose
+        (st_shift_visitor#visit_region 1)
+        (compose subst.r_subst decr_db_var);
+    ty_subst =
+      compose (st_shift_visitor#visit_ty 1) (compose subst.ty_subst decr_db_var);
+    cg_subst =
+      compose
+        (st_shift_visitor#visit_const_generic 1)
+        (compose subst.cg_subst decr_db_var);
+    tr_subst =
+      compose
+        (st_shift_visitor#visit_trait_instance_id 1)
+        (compose subst.tr_subst decr_db_var);
+    tr_self = subst.tr_self;
+  }
+
+(** Visitor that applies the given substitution *)
 let st_substitute_visitor =
   object (self)
     inherit [_] map_statement
 
+    method! visit_binder visit_value (subst : subst) x =
+      (* Note that we don't visit the bound variables. *)
+      let { binder_params; binder_value } = x in
+      (* Crucial: we shift the substitution to be valid under this binder. *)
+      let binder_value = visit_value (shift_subst subst) binder_value in
+      { binder_params; binder_value }
+
     method! visit_region_binder visit_value (subst : subst) x =
-      (* Shift the indices of the substitution under one binder level. *)
-      let shift_subst (subst : subst) : subst =
-        {
-          r_subst = compose subst.r_subst decr_db_var;
-          ty_subst = compose subst.ty_subst decr_db_var;
-          cg_subst = compose subst.cg_subst decr_db_var;
-          tr_subst = compose subst.tr_subst decr_db_var;
-          tr_self = subst.tr_self;
-        }
-      in
-      let subst = shift_subst subst in
-      (* Note that we ignore the bound regions variables *)
+      (* Note that we don't visit the bound variables. *)
       let { binder_regions; binder_value } = x in
-      let binder_value = visit_value subst binder_value in
+      (* Crucial: we shift the substitution to be valid under this binder. *)
+      let binder_value = visit_value (shift_subst subst) binder_value in
       { binder_regions; binder_value }
 
     method! visit_RVar (subst : subst) var = subst.r_subst var
@@ -291,8 +322,8 @@ let make_trait_subst_from_clauses (clauses : trait_clause list)
     (List.map (fun (x : trait_clause) -> x.clause_id) clauses)
     (List.map (fun (x : trait_ref) -> x.trait_id) trs)
 
-let make_subst_from_generics (params : generic_params) (args : generic_args)
-    (tr_sb_self : trait_instance_id) : subst =
+let make_sb_subst_from_generics (params : generic_params) (args : generic_args)
+    : single_binder_subst =
   let r_sb_subst = make_region_subst_from_vars params.regions args.regions in
   let ty_sb_subst = make_type_subst_from_vars params.types args.types in
   let cg_sb_subst =
@@ -301,14 +332,16 @@ let make_subst_from_generics (params : generic_params) (args : generic_args)
   let tr_sb_subst =
     make_trait_subst_from_clauses params.trait_clauses args.trait_refs
   in
-  subst_free_vars
-    { r_sb_subst; ty_sb_subst; cg_sb_subst; tr_sb_subst; tr_sb_self }
+  { r_sb_subst; ty_sb_subst; cg_sb_subst; tr_sb_subst; tr_sb_self = Self }
+
+let make_subst_from_generics (params : generic_params) (args : generic_args) :
+    subst =
+  subst_free_vars (make_sb_subst_from_generics params args)
 
 let make_subst_from_generics_erase_regions (params : generic_params)
-    (generics : generic_args) (tr_self : trait_instance_id) =
+    (generics : generic_args) : subst =
   let generics = generic_args_erase_regions generics in
-  let tr_self = trait_instance_id_erase_regions tr_self in
-  let subst = make_subst_from_generics params generics tr_self in
+  let subst = make_subst_from_generics params generics in
   { subst with r_subst = (fun _ -> RErased) }
 
 (** Instantiate the type variables in an ADT definition, and return, for
@@ -319,9 +352,7 @@ let make_subst_from_generics_erase_regions (params : generic_params)
 *)
 let type_decl_get_instantiated_variants_fields_types (def : type_decl)
     (generics : generic_args) : (VariantId.id option * ty list) list =
-  (* There shouldn't be any reference to Self *)
-  let tr_self = UnknownTrait __FUNCTION__ in
-  let subst = make_subst_from_generics def.generics generics tr_self in
+  let subst = make_subst_from_generics def.generics generics in
   let (variants_fields : (VariantId.id option * field list) list) =
     match def.kind with
     | Enum variants ->
@@ -349,9 +380,7 @@ let type_decl_get_instantiated_field_types (def : type_decl)
   (* For now, check that there are no clauses - otherwise we might need
      to normalize the types *)
   assert (def.generics.trait_clauses = []);
-  (* There shouldn't be any reference to Self *)
-  let tr_self = UnknownTrait __FUNCTION__ in
-  let subst = make_subst_from_generics def.generics generics tr_self in
+  let subst = make_subst_from_generics def.generics generics in
   let fields = type_decl_get_fields def opt_variant_id in
   List.map (fun f -> ty_substitute subst f.field_ty) fields
 
@@ -411,5 +440,73 @@ let statement_substitute_ids (ty_subst : TypeVarId.id -> TypeVarId.id)
       method! visit_const_generic_var_id _ id = cg_subst id
     end
   in
-
   visitor#visit_ty () ty
+
+(** Remove this binder by substituting the provided arguments for each bound
+    variable. The `substitutor` argument must be the appropriate
+    `st_substitute_visitor` method. *)
+let apply_args_to_binder (args : generic_args) (substitutor : subst -> 'a -> 'a)
+    (binder : 'a binder) : 'a =
+  substitutor
+    (subst_remove_binder_zero
+       (make_sb_subst_from_generics binder.binder_params args))
+    binder.binder_value
+
+(** Remove this binder by substituting the provided arguments for each bound
+    variable. The `substitutor` argument must be the appropriate
+    `st_substitute_visitor` method. *)
+let apply_args_to_item_binder (args : generic_args)
+    (substitutor : subst -> 'a -> 'a) (binder : 'a item_binder) : 'a =
+  substitutor
+    (subst_free_vars
+       (make_sb_subst_from_generics binder.item_binder_params args))
+    binder.item_binder_value
+
+(** Helper *)
+let instantiate_method item_generics method_generics
+    (bound_fn : fun_decl_ref binder item_binder) : fun_decl_ref =
+  apply_args_to_binder method_generics st_substitute_visitor#visit_fun_decl_ref
+    (apply_args_to_item_binder item_generics
+       (st_substitute_visitor#visit_binder
+          st_substitute_visitor#visit_fun_decl_ref)
+       bound_fn)
+
+(** Like lookup_trait_decl_provided_method, but also correctly substitutes the generics. *)
+let lookup_and_subst_trait_decl_method (tdecl : trait_decl)
+    (name : trait_item_name) decl_generics method_generics : fun_decl_ref option
+    =
+  Option.map
+    (instantiate_method decl_generics method_generics)
+    (lookup_trait_decl_method tdecl name)
+
+(** Like lookup_trait_decl_provided_method, but also correctly substitutes the generics. *)
+let lookup_and_subst_trait_decl_provided_method (tdecl : trait_decl)
+    (name : trait_item_name) decl_generics method_generics : fun_decl_ref option
+    =
+  Option.map
+    (instantiate_method decl_generics method_generics)
+    (lookup_trait_decl_provided_method tdecl name)
+
+(** Like lookup_trait_decl_required_method, but also correctly substitutes the generics. *)
+let lookup_and_subst_trait_decl_required_method (tdecl : trait_decl)
+    (name : trait_item_name) decl_generics method_generics : fun_decl_ref option
+    =
+  Option.map
+    (instantiate_method decl_generics method_generics)
+    (lookup_trait_decl_required_method tdecl name)
+
+(** Like lookup_trait_impl_provided_method, but also correctly substitutes the generics. *)
+let lookup_and_subst_trait_impl_provided_method (timpl : trait_impl)
+    (name : trait_item_name) impl_generics method_generics : fun_decl_ref option
+    =
+  Option.map
+    (instantiate_method impl_generics method_generics)
+    (lookup_trait_impl_provided_method timpl name)
+
+(** Like lookup_trait_impl_required_method, but also correctly substitutes the generics. *)
+let lookup_and_subst_trait_impl_required_method (timpl : trait_impl)
+    (name : trait_item_name) impl_generics method_generics : fun_decl_ref option
+    =
+  Option.map
+    (instantiate_method impl_generics method_generics)
+    (lookup_trait_impl_required_method timpl name)

charon-ml/src/TypesUtils.ml

@@ -147,20 +147,6 @@ let empty_generic_params : generic_params =
     trait_type_constraints = [];
   }
 
-let merge_generic_args (g1 : generic_args) (g2 : generic_args) : generic_args =
-  let { regions = r1; types = tys1; const_generics = cgs1; trait_refs = tr1 } =
-    g1
-  in
-  let { regions = r2; types = tys2; const_generics = cgs2; trait_refs = tr2 } =
-    g2
-  in
-  {
-    regions = r1 @ r2;
-    types = tys1 @ tys2;
-    const_generics = cgs1 @ cgs2;
-    trait_refs = tr1 @ tr2;
-  }
-
 let generic_args_of_params span (generics : generic_params) : generic_args =
   let regions =
     List.map (fun (v : region_var) -> RVar (Free v.index)) generics.regions