Merge pull request #517 from Nadrieril/partially-generic-ml-visitors

charon-ml/src/BigInt.ml

@@ -0,0 +1,24 @@
+(** We use big integers to store the integer values (this way we don't have
+    to think about the bounds, nor architecture issues - Rust allows to
+    manipulate 128-bit integers for instance).
+ *)
+type big_int = (Z.t[@opaque])
+[@@deriving
+  visitors { name = "iter_big_int"; variety = "iter" },
+    visitors { name = "map_big_int"; variety = "map" },
+    visitors { name = "reduce_big_int"; variety = "reduce" },
+    visitors { name = "mapreduce_big_int"; variety = "mapreduce" }]
+
+let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
+  match json with
+  | `Int i -> Ok (Z.of_int i)
+  | `Intlit is -> Ok (Z.of_string is)
+  | _ -> Error "not an integer or an integer literal"
+
+let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
+
+let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
+  Format.pp_print_string fmt (Z.to_string bi)
+
+let compare_big_int (bi0 : big_int) (bi1 : big_int) : int = Z.compare bi0 bi1
+let show_big_int (bi : big_int) : string = Z.to_string bi

charon-ml/src/Substitute.ml

@@ -234,11 +234,16 @@ let predicates_substitute (subst : subst) (p : generic_params) : generic_params
     trait_clauses = List.map (visitor#visit_trait_clause subst) trait_clauses;
     regions_outlive =
       List.map
-        (visitor#visit_region_binder visitor#visit_region_outlives subst)
+        (visitor#visit_region_binder
+           (visitor#visit_outlives_pred visitor#visit_region
+              visitor#visit_region)
+           subst)
         regions_outlive;
     types_outlive =
       List.map
-        (visitor#visit_region_binder visitor#visit_type_outlives subst)
+        (visitor#visit_region_binder
+           (visitor#visit_outlives_pred visitor#visit_ty visitor#visit_region)
+           subst)
         types_outlive;
     trait_type_constraints =
       List.map

charon-ml/src/Types.ml

@@ -46,3 +46,6 @@ type ety = ty
 
 (** Type with non-erased regions (this only has an informative purpose) *)
 and rty = ty [@@deriving show, ord]
+
+and region_outlives = (region, region) outlives_pred
+and type_outlives = (ty, region) outlives_pred

charon-ml/src/generated/Generated_Expressions.ml

@@ -15,25 +15,6 @@ module VarId = IdGen ()
 module GlobalDeclId = Types.GlobalDeclId
 module FunDeclId = Types.FunDeclId
 
-type var_id = VarId.id [@@deriving show, ord]
-
-(* Ancestors for the rvalue visitors *)
-class ['self] iter_rvalue_base =
-  object (self : 'self)
-    inherit [_] iter_type_decl
-    method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
-    method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
-    method visit_field_id : 'env -> field_id -> unit = fun _ _ -> ()
-  end
-
-class ['self] map_rvalue_base =
-  object (self : 'self)
-    inherit [_] map_type_decl
-    method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x
-    method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
-    method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
-  end
-
 type place = { kind : place_kind; ty : ty }
 
 and place_kind =
@@ -390,20 +371,24 @@ and aggregate_kind =
       (** Aggregated values for closures group the function id together with its
           state.
        *)
+
+and var_id = (VarId.id[@opaque])
 [@@deriving
   show,
     ord,
     visitors
       {
         name = "iter_rvalue";
+        monomorphic = [ "env" ];
         variety = "iter";
-        ancestors = [ "iter_rvalue_base" ];
+        ancestors = [ "iter_type_decl" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       },
     visitors
       {
         name = "map_rvalue";
+        monomorphic = [ "env" ];
         variety = "map";
-        ancestors = [ "map_rvalue_base" ];
+        ancestors = [ "map_type_decl" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       }]

charon-ml/src/generated/Generated_GAst.ml

@@ -24,7 +24,7 @@ type fun_id = Expressions.fun_id [@@deriving show, ord]
 type fun_id_or_trait_method_ref = Expressions.fun_id_or_trait_method_ref
 [@@deriving show, ord]
 
-type fun_decl_id = FunDeclId.id [@@deriving show, ord]
+type fun_decl_id = Types.fun_decl_id [@@deriving show, ord]
 
 (** A variable *)
 type var = {
@@ -158,13 +158,15 @@ and fun_sig = {
     visitors
       {
         name = "iter_fun_sig";
+        monomorphic = [ "env" ];
         variety = "iter";
         ancestors = [ "iter_rvalue" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       },
     visitors
       {
         name = "map_fun_sig";
+        monomorphic = [ "env" ];
         variety = "map";
         ancestors = [ "map_rvalue" ];
         nude = true (* Don't inherit VisitorsRuntime *);
@@ -189,13 +191,15 @@ type global_decl = {
     visitors
       {
         name = "iter_global_decl";
+        monomorphic = [ "env" ];
         variety = "iter";
         ancestors = [ "iter_fun_sig" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       },
     visitors
       {
         name = "map_global_decl";
+        monomorphic = [ "env" ];
         variety = "map";
         ancestors = [ "map_fun_sig" ];
         nude = true (* Don't inherit VisitorsRuntime *);
@@ -277,13 +281,15 @@ type trait_decl = {
     visitors
       {
         name = "iter_trait_decl";
+        monomorphic = [ "env" ];
         variety = "iter";
         ancestors = [ "iter_global_decl" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       },
     visitors
       {
         name = "map_trait_decl";
+        monomorphic = [ "env" ];
         variety = "map";
         ancestors = [ "map_global_decl" ];
         nude = true (* Don't inherit VisitorsRuntime *);
@@ -334,13 +340,15 @@ type trait_impl = {
     visitors
       {
         name = "iter_trait_impl";
+        monomorphic = [ "env" ];
         variety = "iter";
         ancestors = [ "iter_trait_decl" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       },
     visitors
       {
         name = "map_trait_impl";
+        monomorphic = [ "env" ];
         variety = "map";
         ancestors = [ "map_trait_decl" ];
         nude = true (* Don't inherit VisitorsRuntime *);

charon-ml/src/generated/Generated_LlbcAst.ml

@@ -76,13 +76,15 @@ and switch =
     visitors
       {
         name = "iter_statement";
+        monomorphic = [ "env" ];
         variety = "iter";
         ancestors = [ "iter_trait_impl" ];
         nude = true (* Don't inherit VisitorsRuntime *);
       },
     visitors
       {
         name = "map_statement";
+        monomorphic = [ "env" ];
         variety = "map";
         ancestors = [ "map_trait_impl" ];
         nude = true (* Don't inherit VisitorsRuntime *);