Automatically include needed children when generating ml type decls

charon-ml/src/PrintExpressions.ml

@@ -9,12 +9,6 @@ open PrintTypes
 let fun_decl_id_to_string = PrintTypes.fun_decl_id_to_string
 let var_id_to_pretty_string (id : var_id) : string = "v@" ^ VarId.to_string id
 
-let variant_id_to_pretty_string (id : variant_id) : string =
-  "Variant@" ^ VariantId.to_string id
-
-let field_id_to_pretty_string (id : field_id) : string =
-  "Field@" ^ FieldId.to_string id
-
 let var_to_string (v : var) : string =
   match v.name with
   | None -> var_id_to_pretty_string v.index
@@ -28,21 +22,6 @@ let var_id_to_string (env : 'a fmt_env) (id : VarId.id) : string =
       | None -> var_id_to_pretty_string id
       | Some name -> name ^ "^" ^ VarId.to_string id)
 
-let adt_variant_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id)
-    (variant_id : VariantId.id) : string =
-  match TypeDeclId.Map.find_opt def_id env.crate.type_decls with
-  | None ->
-      type_decl_id_to_pretty_string def_id
-      ^ "::"
-      ^ variant_id_to_pretty_string variant_id
-  | Some def -> begin
-      match def.kind with
-      | Enum variants ->
-          let variant = VariantId.nth variants variant_id in
-          name_to_string env def.item_meta.name ^ "::" ^ variant.variant_name
-      | _ -> raise (Failure "Unreachable")
-    end
-
 let projection_elem_to_string (env : 'a fmt_env) (sub : string)
     (pe : projection_elem) : string =
   match pe with

charon-ml/src/PrintTypes.ml

@@ -82,6 +82,12 @@ let trait_decl_id_to_pretty_string (id : trait_decl_id) : string =
 let trait_impl_id_to_pretty_string (id : trait_impl_id) : string =
   "TraitImpl@" ^ TraitImplId.to_string id
 
+let variant_id_to_pretty_string (id : variant_id) : string =
+  "Variant@" ^ VariantId.to_string id
+
+let field_id_to_pretty_string (id : field_id) : string =
+  "Field@" ^ FieldId.to_string id
+
 let lookup_var_in_env (env : 'a fmt_env)
     (find_in : generic_params -> 'id -> 'b option) (var : 'id de_bruijn_var) :
     'b option =
@@ -475,6 +481,21 @@ let type_decl_to_string (env : 'a fmt_env) (def : type_decl) : string =
   | Opaque -> "opaque type " ^ name ^ params ^ clauses
   | TError err -> "error(\"" ^ err ^ "\")"
 
+let adt_variant_to_string (env : 'a fmt_env) (def_id : TypeDeclId.id)
+    (variant_id : VariantId.id) : string =
+  match TypeDeclId.Map.find_opt def_id env.crate.type_decls with
+  | None ->
+      type_decl_id_to_pretty_string def_id
+      ^ "::"
+      ^ variant_id_to_pretty_string variant_id
+  | Some def -> begin
+      match def.kind with
+      | Enum variants ->
+          let variant = VariantId.nth variants variant_id in
+          name_to_string env def.item_meta.name ^ "::" ^ variant.variant_name
+      | _ -> raise (Failure "Unreachable")
+    end
+
 let adt_field_names (env : 'a fmt_env) (def_id : TypeDeclId.id)
     (opt_variant_id : VariantId.id option) : string list option =
   match TypeDeclId.Map.find_opt def_id env.crate.type_decls with

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

@@ -372,9 +372,6 @@ and aggregate_kind =
           state.
        *)
 
-and variant_id = (VariantId.id[@opaque])
-and field_id = (FieldId.id[@opaque])
-
 and var_id = (VarId.id[@opaque])
 [@@deriving
   show,

charon-ml/src/generated/Generated_Types.ml

@@ -564,9 +564,6 @@ and trait_clause = {
 (** .0 outlives .1 *)
 and ('a0, 'a1) outlives_pred = 'a0 * 'a1
 
-and region_outlives = (region, region) outlives_pred
-and type_outlives = (ty, region) outlives_pred
-
 (** A constraint over a trait associated type.
 
     Example:
@@ -635,6 +632,9 @@ and type_decl = {
   kind : type_decl_kind;  (** The type kind: enum, struct, or opaque. *)
 }
 
+and variant_id = (VariantId.id[@opaque])
+and field_id = (FieldId.id[@opaque])
+
 and type_decl_kind =
   | Struct of field list
   | Enum of variant list