Cleanup FunSig

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.159"
+let supported_charon_version = "0.1.160"

charon-ml/src/GAst.ml

@@ -30,6 +30,7 @@ type mixed_declaration_group = item_id g_declaration_group [@@deriving show]
 type 'body gfun_decl = {
   def_id : FunDeclId.id;
   item_meta : item_meta;
+  generics : generic_params;
   signature : fun_sig;
   src : item_source;
   is_global_initializer : GlobalDeclId.id option;

charon-ml/src/GAstOfJson.ml

@@ -29,20 +29,31 @@ let rec gfun_decl_of_json
         [
           ("def_id", def_id);
           ("item_meta", item_meta);
+          ("generics", generics);
           ("signature", signature);
           ("src", src);
           ("is_global_initializer", is_global_initializer);
           ("body", body);
         ] ->
         let* def_id = FunDeclId.id_of_json ctx def_id in
         let* item_meta = item_meta_of_json ctx item_meta in
+        let* generics = generic_params_of_json ctx generics in
         let* signature = fun_sig_of_json ctx signature in
         let* src = item_source_of_json ctx src in
         let* is_global_initializer =
           option_of_json global_decl_id_of_json ctx is_global_initializer
         in
         let* body = body_of_json ctx body in
-        Ok { def_id; item_meta; signature; src; is_global_initializer; body }
+        Ok
+          {
+            def_id;
+            item_meta;
+            generics;
+            signature;
+            src;
+            is_global_initializer;
+            body;
+          }
     | _ -> Error "")
 
 (** Deserialize a map from file id to file name.

charon-ml/src/GAstUtils.ml

@@ -1,4 +1,5 @@
 open Types
+open TypesUtils
 open GAst
 
 (** Small utility: list the transitive parents of a region var group. We don't
@@ -41,15 +42,10 @@ let locals_get_input_vars (locals : locals) : local list =
 let fun_body_get_input_vars (fbody : 'body gexpr_body) : local 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]
+(** Get the signature of this function as a bound value, i.e. including its
+    generics parameters. *)
+let bound_fun_sig_of_decl (def : 'a gfun_decl) : bound_fun_sig =
+  { item_binder_params = def.generics; item_binder_value = def.signature }
 
 (** 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

charon-ml/src/LlbcAstUtils.ml

@@ -106,20 +106,37 @@ class ['self] map_crate_with_span =
 
     method visit_fun_decl (_ : (item_id * span) option) (decl : fun_decl) :
         fun_decl =
-      let { def_id; item_meta; signature; src; is_global_initializer; body } =
+      let {
+        def_id;
+        item_meta;
+        generics;
+        signature;
+        src;
+        is_global_initializer;
+        body;
+      } =
         decl
       in
       let decl_span_info = Some (IdFun def_id, item_meta.span) in
       let def_id = self#visit_fun_decl_id decl_span_info def_id in
       let item_meta = self#visit_item_meta decl_span_info item_meta in
+      let generics = self#visit_generic_params decl_span_info generics in
       let signature = self#visit_fun_sig decl_span_info signature in
       let src = self#visit_item_source decl_span_info src in
       let is_global_initializer =
         self#visit_option self#visit_global_decl_id decl_span_info
           is_global_initializer
       in
       let body = self#visit_option self#visit_expr_body decl_span_info body in
-      { def_id; item_meta; signature; src; is_global_initializer; body }
+      {
+        def_id;
+        item_meta;
+        generics;
+        signature;
+        src;
+        is_global_initializer;
+        body;
+      }
 
     method! visit_global_decl (_ : (item_id * span) option) (decl : global_decl)
         =
@@ -293,12 +310,21 @@ class ['self] iter_crate_with_span =
 
     method visit_fun_decl (_ : (item_id * span) option) (decl : fun_decl) : unit
         =
-      let { def_id; item_meta; signature; src; is_global_initializer; body } =
+      let {
+        def_id;
+        item_meta;
+        generics;
+        signature;
+        src;
+        is_global_initializer;
+        body;
+      } =
         decl
       in
       let decl_span_info = Some (IdFun def_id, item_meta.span) in
       self#visit_fun_decl_id decl_span_info def_id;
       self#visit_item_meta decl_span_info item_meta;
+      self#visit_generic_params decl_span_info generics;
       self#visit_fun_sig decl_span_info signature;
       self#visit_item_source decl_span_info src;
       self#visit_option self#visit_global_decl_id decl_span_info

charon-ml/src/NameMatcher.ml

@@ -580,7 +580,7 @@ and match_expr_with_ty (ctx : 'fun_body ctx) (c : match_config) (m : maps)
       let m =
         maps_push_bound_regions_group_if_nonempty m binder.binder_regions
       in
-      let inputs, output = binder.binder_value in
+      let { T.inputs; output; _ } = binder.binder_value in
       (* Match *)
       List.for_all2 (match_expr_with_ty ctx c m) pinputs inputs
       &&
@@ -770,8 +770,7 @@ let match_fn_ptr (ctx : 'fun_body ctx) (c : match_config) (p : pattern)
         | TraitImplItem (_, trait_ref, method_name, _)
           when c.match_with_trait_decl_refs ->
             let subst =
-              Substitute.make_subst_from_generics d.signature.generics
-                func.generics
+              Substitute.make_subst_from_generics d.generics func.generics
             in
             let trait_ref =
               Substitute.trait_decl_ref_substitute subst trait_ref
@@ -1023,7 +1022,7 @@ and ty_to_pattern_aux (ctx : 'fun_body ctx) (c : to_pat_config)
       let m =
         constraints_map_push_regions_map_if_nonempty m binder.binder_regions
       in
-      let inputs, output = binder.binder_value in
+      let { T.inputs; output; _ } = binder.binder_value in
       let inputs = List.map (ty_to_pattern_aux ctx c m) inputs in
       let output =
         if output = TypesUtils.mk_unit_ty then None

charon-ml/src/PrintGAst.ml

@@ -3,6 +3,7 @@
 open Types
 open TypesUtils
 open GAst
+open GAstUtils
 open PrintUtils
 open PrintTypes
 open PrintExpressions
@@ -36,15 +37,16 @@ let assertion_to_string (env : 'a fmt_env) (indent : string) (a : assertion) :
 (** Small helper *)
 let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string)
     (indent_incr : string) (attribute : string option) (name : string option)
-    (args : local list option) (sg : fun_sig) : string =
+    (args : local list option) (sg : bound_fun_sig) : string =
+  let { item_binder_params = generics; item_binder_value = sg; _ } = sg in
   let ty_to_string = ty_to_string env in
 
   (* Unsafe keyword *)
   let unsafe = if sg.is_unsafe then "unsafe " else "" in
 
   (* Generics and predicates *)
   let params, clauses =
-    predicates_and_trait_clauses_to_string env indent indent_incr sg.generics
+    predicates_and_trait_clauses_to_string env indent indent_incr generics
   in
   let params =
     if params = [] then "" else "<" ^ String.concat ", " params ^ ">"
@@ -85,15 +87,15 @@ let fun_sig_with_name_to_string (env : 'a fmt_env) (indent : string)
   ^ clauses
 
 let fun_sig_to_string (env : 'a fmt_env) (indent : string)
-    (indent_incr : string) (sg : fun_sig) : string =
+    (indent_incr : string) (sg : fun_sig item_binder) : string =
   fun_sig_with_name_to_string env indent indent_incr None None None sg
 
 let gfun_decl_to_string (env : 'a fmt_env) (indent : string)
     (indent_incr : string)
     (body_to_string : 'a fmt_env -> string -> string -> 'body -> string)
     (def : 'body gfun_decl) : string =
   (* Locally update the environment *)
-  let env = fmt_env_update_generics_and_preds env def.signature.generics in
+  let env = fmt_env_update_generics_and_preds env def.generics in
 
   let sg = def.signature in
 
@@ -102,6 +104,7 @@ let gfun_decl_to_string (env : 'a fmt_env) (indent : string)
 
   (* We print the declaration differently if it is opaque (no body) or transparent
    * (we have access to a body) *)
+  let sg = bound_fun_sig_of_decl def in
   match def.body with
   | None ->
       fun_sig_with_name_to_string env indent indent_incr (Some "opaque")

charon-ml/src/PrintLlbcAst.ml

@@ -117,9 +117,7 @@ module Ast = struct
     String.concat ";\n"
       (List.map (statement_to_string env indent indent_incr) b.statements)
 
-  let fun_sig_to_string (env : fmt_env) (indent : string) (indent_incr : string)
-      (sg : fun_sig) : string =
-    fun_sig_to_string env indent indent_incr sg
+  let fun_sig_to_string = fun_sig_to_string
 
   let fun_decl_to_string (env : fmt_env) (indent : string)
       (indent_incr : string) (def : fun_decl) : string =

charon-ml/src/PrintTypes.ml

@@ -286,7 +286,7 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string =
       | RShared -> "*const " ^ ty_to_string env rty)
   | TFnPtr binder ->
       let env = fmt_env_push_regions env binder.binder_regions in
-      let inputs, output = binder.binder_value in
+      let { inputs; output; _ } = binder.binder_value in
       let inputs =
         "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> "
       in

charon-ml/src/Substitute.ml

@@ -615,7 +615,7 @@ let lookup_method_sig (crate : 'a gcrate) (trait_id : trait_decl_id)
   (* Substitute the signature to be valid under the binder. *)
   let signature =
     st_substitute_visitor#visit_fun_sig
-      (make_subst_from_generics method_decl.signature.generics
+      (make_subst_from_generics method_decl.generics
          bound_method.binder_value.generics)
       method_decl.signature
   in
@@ -625,39 +625,31 @@ let lookup_method_sig (crate : 'a gcrate) (trait_id : trait_decl_id)
   in
   Some { item_binder_params = trait_params; item_binder_value = bound_sig }
 
-(* Like [lookup_method_sig], but with no binder shenanigans: the returns
-   fun_sig takes as parameters the concatenation of trait generics and method
-   generics. *)
+(* Like [lookup_method_sig], but with no binder shenanigans: the returned
+   binder binds the concatenation of trait generics and method generics. *)
 let lookup_flat_method_sig (crate : 'a gcrate) (trait_id : trait_decl_id)
-    (name : trait_item_name) : fun_sig option =
+    (name : trait_item_name) : bound_fun_sig option =
   let* bound_sig = lookup_method_sig crate trait_id name in
   let bound_sig = fuse_binders st_substitute_visitor#visit_fun_sig bound_sig in
-  let s =
-    { bound_sig.item_binder_value with generics = bound_sig.item_binder_params }
-  in
-  Some s
+  Some bound_sig
 
 (* Lookup the signature of a `Ty::FnDef`. *)
-let lookup_fndef_sig (crate : 'a gcrate) (fn_def : fn_ptr region_binder) :
-    (ty list * ty) region_binder option =
-  match fn_def.binder_value.kind with
+let lookup_fndef_sig (crate : 'a gcrate) (fn_ptr : fn_ptr region_binder) :
+    fun_sig region_binder option =
+  match fn_ptr.binder_value.kind with
   | FunId (FRegular fun_decl_id) ->
       let* fun_decl =
         LlbcAst.FunDeclId.Map.find_opt fun_decl_id crate.fun_decls
       in
       (* Substitute the signature to be valid under the binder. *)
       let fn_sig =
         st_substitute_visitor#visit_fun_sig
-          (make_subst_from_generics fun_decl.signature.generics
-             fn_def.binder_value.generics)
+          (make_subst_from_generics fun_decl.generics
+             fn_ptr.binder_value.generics)
           fun_decl.signature
       in
       (* Rebind everything *)
-      Some
-        {
-          binder_regions = fn_def.binder_regions;
-          binder_value = (fn_sig.inputs, fn_sig.output);
-        }
+      Some { binder_regions = fn_ptr.binder_regions; binder_value = fn_sig }
   | _ -> None
 
 (* Construct a set of generic arguments in the scope of `params` that matches

charon-ml/src/TypesUtils.ml

@@ -15,6 +15,18 @@ end
 module RegionMap = Collections.MakeMap (RegionOrderedType)
 module RegionSet = Collections.MakeSet (RegionOrderedType)
 
+(** 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]
+
+type bound_fun_sig = fun_sig item_binder
+
 let to_name (ls : string list) : name =
   List.map (fun s -> PeIdent (s, Disambiguator.zero)) ls
 

charon-ml/src/generated/Generated_GAst.ml

@@ -95,14 +95,6 @@ and fn_operand =
       (** Regular case: call to a top-level function, trait method, etc. *)
   | FnOpDynamic of operand  (** Use of a function pointer. *)
 
-(** A function signature. *)
-and fun_sig = {
-  is_unsafe : bool;  (** Is the function unsafe or not *)
-  generics : generic_params;
-  inputs : ty list;
-  output : ty;
-}
-
 (** A variable *)
 and local = {
   index : local_id;  (** Unique index identifying the variable *)

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -529,11 +529,7 @@ and closure_info_of_json (ctx : of_json_ctx) (js : json) :
             (region_binder_of_json trait_impl_ref_of_json)
             ctx fn_impl
         in
-        let* signature =
-          region_binder_of_json
-            (pair_of_json (list_of_json ty_of_json) ty_of_json)
-            ctx signature
-        in
+        let* signature = region_binder_of_json fun_sig_of_json ctx signature in
         Ok
           ({ kind; fn_once_impl; fn_mut_impl; fn_impl; signature }
             : closure_info)
@@ -911,17 +907,11 @@ and fun_sig_of_json (ctx : of_json_ctx) (js : json) : (fun_sig, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
-        [
-          ("is_unsafe", is_unsafe);
-          ("generics", generics);
-          ("inputs", inputs);
-          ("output", output);
-        ] ->
+        [ ("is_unsafe", is_unsafe); ("inputs", inputs); ("output", output) ] ->
         let* is_unsafe = bool_of_json ctx is_unsafe in
-        let* generics = generic_params_of_json ctx generics in
         let* inputs = list_of_json ty_of_json ctx inputs in
         let* output = ty_of_json ctx output in
-        Ok ({ is_unsafe; generics; inputs; output } : fun_sig)
+        Ok ({ is_unsafe; inputs; output } : fun_sig)
     | _ -> Error "")
 
 and g_declaration_group_of_json :
@@ -2148,11 +2138,7 @@ and ty_kind_of_json (ctx : of_json_ctx) (js : json) : (ty_kind, string) result =
         let* dyn_trait = dyn_predicate_of_json ctx dyn_trait in
         Ok (TDynTrait dyn_trait)
     | `Assoc [ ("FnPtr", fn_ptr) ] ->
-        let* fn_ptr =
-          region_binder_of_json
-            (pair_of_json (list_of_json ty_of_json) ty_of_json)
-            ctx fn_ptr
-        in
+        let* fn_ptr = region_binder_of_json fun_sig_of_json ctx fn_ptr in
         Ok (TFnPtr fn_ptr)
     | `Assoc [ ("FnDef", fn_def) ] ->
         let* fn_def = region_binder_of_json fn_ptr_of_json ctx fn_def in