Merge pull request #376 from Nadrieril/poly-clauses

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.42"
+let supported_charon_version = "0.1.43"

charon-ml/src/GAstOfJson.ml

@@ -770,10 +770,6 @@ and global_decl_id_of_json (js : json) : (global_decl_id, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with x -> GlobalDeclId.id_of_json x | _ -> Error "")
 
-and unsolved_trait_id_of_json (js : json) : (unsolved_trait_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with x -> UnsolvedTraitId.id_of_json x | _ -> Error "")
-
 and type_var_of_json (js : json) : (type_var, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -830,10 +826,12 @@ and trait_instance_id_of_json (js : json) : (trait_instance_id, string) result =
         Ok (ParentClause (x_0, x_1, x_2))
     | `String "SelfId" -> Ok Self
     | `Assoc [ ("BuiltinOrAuto", builtin_or_auto) ] ->
-        let* builtin_or_auto = trait_decl_ref_of_json builtin_or_auto in
+        let* builtin_or_auto =
+          region_binder_of_json trait_decl_ref_of_json builtin_or_auto
+        in
         Ok (BuiltinOrAuto builtin_or_auto)
     | `Assoc [ ("Dyn", dyn) ] ->
-        let* dyn = trait_decl_ref_of_json dyn in
+        let* dyn = region_binder_of_json trait_decl_ref_of_json dyn in
         Ok (Dyn dyn)
     | `Assoc [ ("Unknown", unknown) ] ->
         let* unknown = string_of_json unknown in
@@ -845,7 +843,9 @@ and trait_ref_of_json (js : json) : (trait_ref, string) result =
     (match js with
     | `Assoc [ ("kind", kind); ("trait_decl_ref", trait_decl_ref) ] ->
         let* trait_id = trait_instance_id_of_json kind in
-        let* trait_decl_ref = trait_decl_ref_of_json trait_decl_ref in
+        let* trait_decl_ref =
+          region_binder_of_json trait_decl_ref_of_json trait_decl_ref
+        in
         Ok ({ trait_id; trait_decl_ref } : trait_ref)
     | _ -> Error "")
 
@@ -909,6 +909,22 @@ and generic_args_of_json (js : json) : (generic_args, string) result =
         Ok ({ regions; types; const_generics; trait_refs } : generic_args)
     | _ -> Error "")
 
+and region_binder_of_json :
+      'a0.
+      (json -> ('a0, string) result) ->
+      json ->
+      ('a0 region_binder, string) result =
+ fun arg0_of_json js ->
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("regions", regions); ("skip_binder", skip_binder) ] ->
+        let* binder_regions =
+          vector_of_json region_id_of_json region_var_of_json regions
+        in
+        let* binder_value = arg0_of_json skip_binder in
+        Ok ({ binder_regions; binder_value } : _ region_binder)
+    | _ -> Error "")
+
 and generic_params_of_json (id_to_file : id_to_file_map) (js : json) :
     (generic_params, string) result =
   combine_error_msgs js __FUNCTION__
@@ -940,16 +956,20 @@ and generic_params_of_json (id_to_file : id_to_file_map) (js : json) :
         in
         let* regions_outlive =
           list_of_json
-            (outlives_pred_of_json region_of_json region_of_json)
+            (region_binder_of_json
+               (outlives_pred_of_json region_of_json region_of_json))
             regions_outlive
         in
         let* types_outlive =
           list_of_json
-            (outlives_pred_of_json ty_of_json region_of_json)
+            (region_binder_of_json
+               (outlives_pred_of_json ty_of_json region_of_json))
             types_outlive
         in
         let* trait_type_constraints =
-          list_of_json trait_type_constraint_of_json trait_type_constraints
+          list_of_json
+            (region_binder_of_json trait_type_constraint_of_json)
+            trait_type_constraints
         in
         Ok
           ({
@@ -994,7 +1014,7 @@ and trait_clause_of_json (id_to_file : id_to_file_map) (js : json) :
         ] ->
         let* clause_id = trait_clause_id_of_json clause_id in
         let* span = option_of_json (span_of_json id_to_file) span in
-        let* trait = trait_decl_ref_of_json trait in
+        let* trait = region_binder_of_json trait_decl_ref_of_json trait in
         Ok ({ clause_id; span; trait } : trait_clause)
     | _ -> Error "")
 

charon-ml/src/NameMatcher.ml

@@ -295,6 +295,12 @@ let maps_push_bound_regions_group (m : maps) : maps =
   in
   { m with rmap }
 
+(** Push a group of bound regions if the group is non-empty - TODO: make this
+    more precise *)
+let maps_push_bound_regions_group_if_nonempty (m : maps) (regions : 'a list) :
+    maps =
+  match regions with [] -> m | _ -> maps_push_bound_regions_group m
+
 (** Update a map and check that there are no incompatible
     constraints at the same time. *)
 let update_map (find_opt : 'a -> 'm -> 'b option) (add : 'a -> 'b -> 'm -> 'm)
@@ -500,10 +506,10 @@ and match_expr_with_ty (ctx : ctx) (c : match_config) (m : maps) (pty : expr)
       && match_ref_kind prk rk
   | EVar v, _ -> opt_update_tmap c m v ty
   | EComp pid, TTraitType (trait_ref, type_name) ->
-      match_trait_type ctx c pid trait_ref type_name
-  | EArrow (pinputs, pout), TArrow (_, inputs, out) -> (
-      (* Push a region group in the map *)
-      let m = maps_push_bound_regions_group m in
+      match_trait_type ctx c m pid trait_ref type_name
+  | EArrow (pinputs, pout), TArrow (regions, inputs, out) -> (
+      (* Push a region group in the map, if necessary - TODO: make this more precise *)
+      let m = maps_push_bound_regions_group_if_nonempty m regions in
       (* Match *)
       List.for_all2 (match_expr_with_ty ctx c m) pinputs inputs
       &&
@@ -530,24 +536,30 @@ and match_expr_with_trait_impl_id (ctx : ctx) (c : match_config) (ptr : expr)
         impl.impl_trait.decl_generics
   | EPrimAdt _ | ERef _ | EVar _ | EArrow _ | ERawPtr _ -> false
 
-and match_trait_ref (ctx : ctx) (c : match_config) (pid : pattern)
+and match_trait_ref (ctx : ctx) (c : match_config) (m : maps) (pid : pattern)
     (tr : T.trait_ref) : bool =
   (* Lookup the trait declaration *)
   let d =
-    T.TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id ctx.trait_decls
+    T.TraitDeclId.Map.find tr.trait_decl_ref.binder_value.trait_decl_id
+      ctx.trait_decls
+  in
+  (* Push a region group in the map, if necessary - TODO: make this more precise *)
+  let m =
+    maps_push_bound_regions_group_if_nonempty m tr.trait_decl_ref.binder_regions
   in
   (* Match the trait decl ref *)
-  match_name_with_generics ctx c pid d.item_meta.name
-    tr.trait_decl_ref.decl_generics
+  match_name_with_generics ctx c ~m pid d.item_meta.name
+    tr.trait_decl_ref.binder_value.decl_generics
 
-and match_trait_ref_item (ctx : ctx) (c : match_config) (pid : pattern)
-    (tr : T.trait_ref) (item_name : string) (generics : T.generic_args) : bool =
+and match_trait_ref_item (ctx : ctx) (c : match_config) (m : maps)
+    (pid : pattern) (tr : T.trait_ref) (item_name : string)
+    (generics : T.generic_args) : bool =
   if c.match_with_trait_decl_refs then
     (* We match the trait decl ref *)
     (* We split the pattern between the trait decl ref and the associated item name *)
     let pid, pitem_name = Collections.List.pop_last pid in
     (* Match the trait ref *)
-    match_trait_ref ctx c pid tr
+    match_trait_ref ctx c m pid tr
     &&
     (* Match the item name *)
     match pitem_name with
@@ -557,9 +569,9 @@ and match_trait_ref_item (ctx : ctx) (c : match_config) (pid : pattern)
     | _ -> false
   else raise (Failure "Unimplemented")
 
-and match_trait_type (ctx : ctx) (c : match_config) (pid : pattern)
+and match_trait_type (ctx : ctx) (c : match_config) (m : maps) (pid : pattern)
     (tr : T.trait_ref) (type_name : string) : bool =
-  match_trait_ref_item ctx c pid tr type_name TypesUtils.empty_generic_args
+  match_trait_ref_item ctx c m pid tr type_name TypesUtils.empty_generic_args
 
 and match_generic_args (ctx : ctx) (c : match_config) (m : maps)
     (pgenerics : generic_args) (generics : T.generic_args) : bool =
@@ -662,7 +674,8 @@ let match_fn_ptr (ctx : ctx) (c : match_config) (p : pattern) (func : E.fn_ptr)
       let d = A.FunDeclId.Map.find fid ctx.fun_decls in
       match_name_with_generics ctx c p d.item_meta.name func.generics
   | TraitMethod (tr, method_name, _) ->
-      match_trait_ref_item ctx c p tr method_name func.generics
+      match_trait_ref_item ctx c (mk_empty_maps ()) p tr method_name
+        func.generics
 
 let mk_name_with_generics_matcher (ctx : ctx) (c : match_config) (pat : string)
     : T.name -> T.generic_args -> bool =
@@ -773,6 +786,12 @@ let constraints_map_push_regions_map (m : constraints)
   let rmap = constraints_map_compute_regions_map regions in
   { m with rmap = rmap :: m.rmap }
 
+(** Push a regions map to the constraints map, if the group of regions
+    is non-empty - TODO: do something more precise *)
+let constraints_map_push_regions_map_if_nonempty (m : constraints)
+    (regions : T.region_var list) : constraints =
+  match regions with [] -> m | _ -> constraints_map_push_regions_map m regions
+
 type to_pat_config = {
   tgt : target_kind;
   use_trait_decl_refs : bool;  (** See {!match_with_trait_decl_refs} *)
@@ -868,7 +887,8 @@ and ty_to_pattern_aux (ctx : ctx) (c : to_pat_config) (m : constraints)
       in
       EComp name
   | TArrow (regions, inputs, out) ->
-      let m = constraints_map_push_regions_map m regions in
+      (* Push a regions map if necessary - TODO: make this more precise *)
+      let m = constraints_map_push_regions_map_if_nonempty m regions in
       let inputs = List.map (ty_to_pattern_aux ctx c m) inputs in
       let out =
         if out = TypesUtils.mk_unit_ty then None
@@ -886,9 +906,17 @@ and trait_ref_item_with_generics_to_pattern (ctx : ctx) (c : to_pat_config)
   if c.use_trait_decl_refs then
     let trait_decl_ref = trait_ref.trait_decl_ref in
     let d =
-      T.TraitDeclId.Map.find trait_decl_ref.trait_decl_id ctx.trait_decls
+      T.TraitDeclId.Map.find trait_decl_ref.binder_value.trait_decl_id
+        ctx.trait_decls
+    in
+    (* Push a regions map if necessary - TODO: make this more precise *)
+    let m =
+      constraints_map_push_regions_map_if_nonempty m
+        trait_decl_ref.binder_regions
+    in
+    let g =
+      generic_args_to_pattern ctx c m trait_decl_ref.binder_value.decl_generics
     in
-    let g = generic_args_to_pattern ctx c m trait_decl_ref.decl_generics in
     let name =
       name_with_generic_args_to_pattern_aux ctx c d.item_meta.name (Some g)
     in

charon-ml/src/PrintTypes.ml

@@ -95,6 +95,17 @@ let region_to_string (env : ('a, 'b) fmt_env) (r : region) : string =
 
 let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id
 
+let region_binder_to_string (value_to_string : ('a, 'b) fmt_env -> 'c -> string)
+    (env : ('a, 'b) fmt_env) (rb : 'c region_binder) : string =
+  let env = fmt_env_push_regions env rb.binder_regions in
+  let value = value_to_string env rb.binder_value in
+  match rb.binder_regions with
+  | [] -> value
+  | _ ->
+      "for <"
+      ^ String.concat "," (List.map region_var_to_string rb.binder_regions)
+      ^ "> " ^ value
+
 let rec type_id_to_string (env : ('a, 'b) fmt_env) (id : type_id) : string =
   match id with
   | TAdtId id -> type_decl_id_to_string env id
@@ -231,7 +242,8 @@ and trait_instance_id_to_string (env : ('a, 'b) fmt_env)
       let impl = trait_impl_id_to_string env id in
       let generics = generic_args_to_string env generics in
       impl ^ generics
-  | BuiltinOrAuto trait -> trait_decl_ref_to_string env trait
+  | BuiltinOrAuto trait ->
+      region_binder_to_string trait_decl_ref_to_string env trait
   | Clause id -> trait_clause_id_to_string env id
   | ParentClause (inst_id, _decl_id, clause_id) ->
       let inst_id = trait_instance_id_to_string env inst_id in
@@ -244,7 +256,7 @@ and trait_instance_id_to_string (env : ('a, 'b) fmt_env)
       ^ generic_args_to_string env generics
       ^ ")"
   | Dyn trait ->
-      let trait = trait_decl_ref_to_string env trait in
+      let trait = region_binder_to_string trait_decl_ref_to_string env trait in
       "dyn(" ^ trait ^ ")"
   | Unsolved (decl_id, generics) ->
       "unsolved("
@@ -302,7 +314,9 @@ and raw_attribute_to_string (attr : raw_attribute) : string =
 let trait_clause_to_string (env : ('a, 'b) fmt_env) (clause : trait_clause) :
     string =
   let clause_id = trait_clause_id_to_string env clause.clause_id in
-  let trait = trait_decl_ref_to_string env clause.trait in
+  let trait =
+    region_binder_to_string trait_decl_ref_to_string env clause.trait
+  in
   "[" ^ clause_id ^ "]: " ^ trait
 
 let generic_params_to_strings (env : ('a, 'b) fmt_env)
@@ -363,18 +377,24 @@ let predicates_and_trait_clauses_to_string (env : ('a, 'b) fmt_env)
   let params, trait_clauses = generic_params_to_strings env generics in
   let region_to_string = region_to_string env in
   let regions_outlive =
+    let outlive_to_string _ (x, y) =
+      region_to_string x ^ " : " ^ region_to_string y
+    in
     List.map
-      (fun (x, y) -> region_to_string x ^ " : " ^ region_to_string y)
+      (region_binder_to_string outlive_to_string env)
       generics.regions_outlive
   in
   let types_outlive =
+    let outlive_to_string _ (x, y) =
+      ty_to_string env x ^ " : " ^ region_to_string y
+    in
     List.map
-      (fun (x, y) -> ty_to_string env x ^ " : " ^ region_to_string y)
+      (region_binder_to_string outlive_to_string env)
       generics.types_outlive
   in
   let trait_type_constraints =
     List.map
-      (trait_type_constraint_to_string env)
+      (region_binder_to_string trait_type_constraint_to_string env)
       generics.trait_type_constraints
   in
   (* Split between the inherited clauses and the local clauses *)

charon-ml/src/Substitute.ml

@@ -48,6 +48,20 @@ let st_substitute_visitor (subst : subst) =
       let output = self#visit_ty subst output in
       TArrow (regions, inputs, output)
 
+    (** We need to properly handle the DeBruijn indices *)
+    method! visit_region_binder visit_value subst x =
+      (* Decrement the DeBruijn indices before calling the substitution *)
+      let r_subst r =
+        match r with
+        | RBVar (db, rid) -> subst.r_subst (RBVar (db - 1, rid))
+        | _ -> subst.r_subst r
+      in
+      let subst = { subst with r_subst } in
+      (* Note that we ignore the bound regions variables *)
+      let { binder_regions; binder_value } = x in
+      let binder_value = visit_value subst binder_value in
+      { binder_regions; binder_value }
+
     method! visit_TVar (subst : subst) id = subst.ty_subst id
     method! visit_CgVar _ id = subst.cg_subst id
     method! visit_Clause (subst : subst) id = subst.tr_subst id
@@ -111,11 +125,16 @@ let predicates_substitute (subst : subst) (p : generic_params) : generic_params
     const_generics;
     trait_clauses = List.map (visitor#visit_trait_clause subst) trait_clauses;
     regions_outlive =
-      List.map (visitor#visit_region_outlives subst) regions_outlive;
-    types_outlive = List.map (visitor#visit_type_outlives subst) types_outlive;
+      List.map
+        (visitor#visit_region_binder visitor#visit_region_outlives subst)
+        regions_outlive;
+    types_outlive =
+      List.map
+        (visitor#visit_region_binder visitor#visit_type_outlives subst)
+        types_outlive;
     trait_type_constraints =
       List.map
-        (visitor#visit_trait_type_constraint subst)
+        (visitor#visit_region_binder visitor#visit_trait_type_constraint subst)
         trait_type_constraints;
   }