diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml index 8375d673..b38f282c 100644 --- a/charon-ml/src/PrintExpressions.ml +++ b/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 diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 3d11823e..64204f6d 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/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 diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml index 13d5deb6..a47b8264 100644 --- a/charon-ml/src/Substitute.ml +++ b/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 diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml index 7227ca93..39e74867 100644 --- a/charon-ml/src/Types.ml +++ b/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 diff --git a/charon-ml/src/generated/Generated_Expressions.ml b/charon-ml/src/generated/Generated_Expressions.ml index 40440632..40844407 100644 --- a/charon-ml/src/generated/Generated_Expressions.ml +++ b/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, diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index 288168fc..c4ba1651 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/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 diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index b7a3f537..2b14d63b 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -144,6 +144,11 @@ impl<'a> GenerateCtx<'a> { self.children_of_inner(vec![start_id]) } + /// List the (recursive) children of these types. + fn children_of_many(&self, names: &[&str]) -> HashSet { + self.children_of_inner(names.iter().map(|name| self.id_from_name(name)).collect()) + } + fn children_of_inner(&self, ty: Vec) -> HashSet { let mut children = HashSet::new(); let mut stack = ty.to_vec(); @@ -163,23 +168,6 @@ impl<'a> GenerateCtx<'a> { } children } - - fn markers_from_names( - &self, - markers: &'a [(GenerationKind, &'a [&'a str])], - ) -> Vec<(GenerationKind, HashSet)> { - markers - .iter() - .copied() - .map(|(kind, type_names)| { - let types = type_names - .iter() - .map(|name| self.id_from_name(*name)) - .collect(); - (kind, types) - }) - .collect() - } } /// Converts a type to the appropriate `*_of_json` call. In case of generics, this combines several @@ -1089,6 +1077,8 @@ fn generate_ml( ), ), ]; + // Types for which we don't want to generate a type at all. + let dont_generate_ty = &["ItemOpacity", "PredicateOrigin", "Ty", "Vector"]; // Types that we don't want visitors to go into. let opaque_for_visitor = &["Name"]; let ctx = GenerateCtx::new( @@ -1112,6 +1102,7 @@ fn generate_ml( .map(|name| ctx.id_from_name(name)) .collect(); + // Compute type sets for json deserializers. let (gast_types, llbc_types, ullbc_types) = { let llbc_types: HashSet<_> = ctx.children_of("charon_lib::ast::llbc_ast::Statement"); let ullbc_types: HashSet<_> = ctx.children_of("charon_lib::ast::ullbc_ast::BodyContents"); @@ -1141,22 +1132,36 @@ fn generate_ml( (gast_types, llbc_types, ullbc_types) }; + let mut processed_tys: HashSet = dont_generate_ty + .iter() + .map(|name| ctx.id_from_name(name)) + .collect(); + // Each call to this will return the children of the listed types that haven't been returned + // yet. By calling it in dependency order, this allows to organize types into files without + // having to list them all. + let mut markers_from_children = |ctx: &GenerateCtx, markers: &[_]| { + markers + .iter() + .copied() + .map(|(kind, type_names)| { + let types: HashSet<_> = ctx.children_of_many(type_names); + let unprocessed_types: HashSet<_> = + types.difference(&processed_tys).copied().collect(); + processed_tys.extend(unprocessed_types.iter().copied()); + (kind, unprocessed_types) + }) + .collect() + }; + #[rustfmt::skip] let generate_code_for = vec![ GenerateCodeFor { template: template_dir.join("Meta.ml"), target: output_dir.join("Generated_Meta.ml"), - markers: ctx.markers_from_names(&[ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(None), &[ - "Loc", - "FileName", - "FileId", "File", - "RawSpan", "Span", - "InlineAttr", - "Attribute", - "RawAttribute", "AttrInfo", ]), ]), @@ -1164,27 +1169,23 @@ fn generate_ml( GenerateCodeFor { template: template_dir.join("Values.ml"), target: output_dir.join("Generated_Values.ml"), - markers: ctx.markers_from_names(&[ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(Some(DeriveVisitors { ancestors: &["big_int"], name: "literal", reduce: true, - extra_types: &[ - ], + extra_types: &[], })), &[ + "Literal", "IntegerTy", - "FloatTy", - "FloatValue", "LiteralTy", - "ScalarValue", - "Literal", ]), ]), }, GenerateCodeFor { template: template_dir.join("Types.ml"), target: output_dir.join("Generated_Types.ml"), - markers: ctx.markers_from_names(&[ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(Some(DeriveVisitors { ancestors: &["literal"], name: "const_generic", @@ -1192,18 +1193,11 @@ fn generate_ml( extra_types: &[], })), &[ "RegionId", - "ConstGenericVarId", - "FunDeclId", - "GlobalDeclId", - "TraitClauseId", - "TraitDeclId", - "TraitImplId", - "TypeDeclId", "TypeVarId", - "DeBruijnId", + "ConstGeneric", + "TraitClauseId", "DeBruijnVar", "AnyTransId", - "ConstGeneric", ]), // Can't merge into above because aeneas uses the above alongside their own partial // copy of `ty`, which causes method type clashes. @@ -1213,23 +1207,10 @@ fn generate_ml( reduce: false, extra_types: &[], })), &[ - "TraitItemName", - "BuiltinTy", - "TypeId", - "ExistentialPredicate", - "RefKind", "TyKind", - "Region", - "RegionVar", - "TraitRef", - "TraitRefKind", - "TraitDeclRef", "TraitImplRef", "FunDeclRef", "GlobalDeclRef", - "GenericsSource", - "GenericArgs", - "RegionBinder", ]), // TODO: can't merge into above because of field name clashes (`types`, `regions` etc). (GenerationKind::TypeDecl(Some(DeriveVisitors { @@ -1237,27 +1218,11 @@ fn generate_ml( name: "type_decl", reduce: false, extra_types: &[ - "span","attr_info" + "span", "attr_info" ], })), &[ - "TraitClause", - "TypeVar", - "OutlivesPred", - "RegionOutlives", - "TypeOutlives", - "GenericParams", - "ConstGenericVar", - "TraitTypeConstraint", "Binder", - "Disambiguator", - "ImplElem", - "PathElem", - "Name", - "Field", - "Variant", - "ItemMeta", "AbortKind", - "TypeDeclKind", "TypeDecl", ]), ]), @@ -1265,34 +1230,13 @@ fn generate_ml( GenerateCodeFor { template: template_dir.join("Expressions.ml"), target: output_dir.join("Generated_Expressions.ml"), - markers: ctx.markers_from_names(&[ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(Some(DeriveVisitors { ancestors: &["type_decl"], name: "rvalue", reduce: false, extra_types: &[], })), &[ - "VarId", - "VariantId", - "FieldId", - "BuiltinIndexOp", - "BuiltinFunId", - "BorrowKind", - "BinOp", - "FieldProjKind", - "ProjectionElem", - "PlaceKind", - "Place", - "CastKind", - "UnOp", - "NullOp", - "RawConstantExpr", - "ConstantExpr", - "FnPtr", - "FunIdOrTraitMethodRef", - "FunId", - "Operand", - "AggregateKind", "Rvalue", ]), ]), @@ -1300,19 +1244,15 @@ fn generate_ml( GenerateCodeFor { template: template_dir.join("GAst.ml"), target: output_dir.join("Generated_GAst.ml"), - markers: ctx.markers_from_names(&[ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(Some(DeriveVisitors { ancestors: &["rvalue"], name: "fun_sig", reduce: false, extra_types: &[], })), &[ - "Var", - "FnOperand", "Call", "Assert", - "ClosureKind", - "ClosureInfo", "ItemKind", "Locals", "FunSig", @@ -1345,7 +1285,6 @@ fn generate_ml( (GenerationKind::TypeDecl(None), &[ "CliOpts", "GExprBody", - "GDeclarationGroup", "DeclarationGroup", ]), ]), @@ -1353,28 +1292,28 @@ fn generate_ml( GenerateCodeFor { template: template_dir.join("LlbcAst.ml"), target: output_dir.join("Generated_LlbcAst.ml"), - markers: vec![ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(Some(DeriveVisitors { - ancestors: &["trait_impl"], name: "statement", + ancestors: &["trait_impl"], reduce: false, extra_types: &[], - })), llbc_types.clone()), - ], + })), &[ + "charon_lib::ast::llbc_ast::Statement", + ]), + ]), }, GenerateCodeFor { template: template_dir.join("UllbcAst.ml"), target: output_dir.join("Generated_UllbcAst.ml"), - markers: ctx.markers_from_names(&[ + markers: markers_from_children(&ctx, &[ (GenerationKind::TypeDecl(Some(DeriveVisitors { ancestors: &["trait_impl"], name: "statement", reduce: false, extra_types: &[], })), &[ - "charon_lib::ast::ullbc_ast::BlockId", "charon_lib::ast::ullbc_ast::Statement", - "charon_lib::ast::ullbc_ast::RawStatement", "charon_lib::ast::ullbc_ast::SwitchTargets", ]), // TODO: Can't merge with above because of field name clashes (`content` and `span`). @@ -1384,9 +1323,6 @@ fn generate_ml( reduce: false, extra_types: &[], })), &[ - "charon_lib::ast::ullbc_ast::Terminator", - "charon_lib::ast::ullbc_ast::RawTerminator", - "charon_lib::ast::ullbc_ast::BlockData", "charon_lib::ast::ullbc_ast::BodyContents", ]), ]),