Skip to content

Commit

Permalink
Reorder
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril committed Jan 8, 2025
1 parent d50f609 commit 623752e
Showing 1 changed file with 107 additions and 107 deletions.
214 changes: 107 additions & 107 deletions charon/src/bin/generate-ml/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1143,94 +1143,6 @@ fn generate_ml(

#[rustfmt::skip]
let generate_code_for = vec![
GenerateCodeFor {
template: template_dir.join("GAst.ml"),
target: output_dir.join("Generated_GAst.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "fun_sig",
ancestors: &["rvalue"],
reduce: false,
extra_types: &[],
})), &[
"Var",
"FnOperand",
"Call",
"Assert",
"ClosureKind",
"ClosureInfo",
"ItemKind",
"Locals",
"FunSig",
]),
// These have to be kept separate to avoid field name clashes
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "global_decl",
ancestors: &["fun_sig"],
reduce: false,
extra_types: &[],
})), &[
"GlobalDecl",
]),
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "trait_decl",
ancestors: &["global_decl"],
reduce: false,
extra_types: &[],
})), &[
"TraitDecl",
]),
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "trait_impl",
ancestors: &["trait_decl"],
reduce: false,
extra_types: &[],
})), &[
"TraitImpl",
]),
(GenerationKind::TypeDecl(None), &[
"CliOpts",
"GExprBody",
"GDeclarationGroup",
"DeclarationGroup",
]),
]),
},
GenerateCodeFor {
template: template_dir.join("Expressions.ml"),
target: output_dir.join("Generated_Expressions.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "rvalue",
ancestors: &["type_decl"],
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",
]),
]),
},
GenerateCodeFor {
template: template_dir.join("Meta.ml"),
target: output_dir.join("Generated_Meta.ml"),
Expand All @@ -1249,13 +1161,33 @@ fn generate_ml(
]),
]),
},
GenerateCodeFor {
template: template_dir.join("Values.ml"),
target: output_dir.join("Generated_Values.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
ancestors: &["big_int"],
name: "literal",
reduce: true,
extra_types: &[
],
})), &[
"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(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "const_generic",
ancestors: &["literal"],
name: "const_generic",
reduce: true,
extra_types: &[],
})), &[
Expand All @@ -1276,8 +1208,8 @@ fn generate_ml(
// Can't merge into above because aeneas uses the above alongside their own partial
// copy of `ty`, which causes method type clashes.
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "ty",
ancestors: &["ty_base_base"],
name: "ty",
reduce: false,
extra_types: &[],
})), &[
Expand All @@ -1301,8 +1233,8 @@ fn generate_ml(
]),
// TODO: can't merge into above because of field name clashes (`types`, `regions` etc).
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "type_decl",
ancestors: &["ty"],
name: "type_decl",
reduce: false,
extra_types: &[
"span","attr_info"
Expand Down Expand Up @@ -1331,22 +1263,90 @@ fn generate_ml(
]),
},
GenerateCodeFor {
template: template_dir.join("Values.ml"),
target: output_dir.join("Generated_Values.ml"),
template: template_dir.join("Expressions.ml"),
target: output_dir.join("Generated_Expressions.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "literal",
ancestors: &["big_int"],
reduce: true,
extra_types: &[
],
ancestors: &["type_decl"],
name: "rvalue",
reduce: false,
extra_types: &[],
})), &[
"IntegerTy",
"FloatTy",
"FloatValue",
"LiteralTy",
"ScalarValue",
"Literal",
"VarId",
"VariantId",
"FieldId",
"BuiltinIndexOp",
"BuiltinFunId",
"BorrowKind",
"BinOp",
"FieldProjKind",
"ProjectionElem",
"PlaceKind",
"Place",
"CastKind",
"UnOp",
"NullOp",
"RawConstantExpr",
"ConstantExpr",
"FnPtr",
"FunIdOrTraitMethodRef",
"FunId",
"Operand",
"AggregateKind",
"Rvalue",
]),
]),
},
GenerateCodeFor {
template: template_dir.join("GAst.ml"),
target: output_dir.join("Generated_GAst.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
ancestors: &["rvalue"],
name: "fun_sig",
reduce: false,
extra_types: &[],
})), &[
"Var",
"FnOperand",
"Call",
"Assert",
"ClosureKind",
"ClosureInfo",
"ItemKind",
"Locals",
"FunSig",
]),
// These have to be kept separate to avoid field name clashes
(GenerationKind::TypeDecl(Some(DeriveVisitors {
ancestors: &["fun_sig"],
name: "global_decl",
reduce: false,
extra_types: &[],
})), &[
"GlobalDecl",
]),
(GenerationKind::TypeDecl(Some(DeriveVisitors {
ancestors: &["global_decl"],
name: "trait_decl",
reduce: false,
extra_types: &[],
})), &[
"TraitDecl",
]),
(GenerationKind::TypeDecl(Some(DeriveVisitors {
ancestors: &["trait_decl"],
name: "trait_impl",
reduce: false,
extra_types: &[],
})), &[
"TraitImpl",
]),
(GenerationKind::TypeDecl(None), &[
"CliOpts",
"GExprBody",
"GDeclarationGroup",
"DeclarationGroup",
]),
]),
},
Expand All @@ -1355,8 +1355,8 @@ fn generate_ml(
target: output_dir.join("Generated_LlbcAst.ml"),
markers: vec![
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "statement",
ancestors: &["trait_impl"],
name: "statement",
reduce: false,
extra_types: &[],
})), llbc_types.clone()),
Expand All @@ -1367,8 +1367,8 @@ fn generate_ml(
target: output_dir.join("Generated_UllbcAst.ml"),
markers: ctx.markers_from_names(&[
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "statement",
ancestors: &["trait_impl"],
name: "statement",
reduce: false,
extra_types: &[],
})), &[
Expand All @@ -1379,8 +1379,8 @@ fn generate_ml(
]),
// TODO: Can't merge with above because of field name clashes (`content` and `span`).
(GenerationKind::TypeDecl(Some(DeriveVisitors {
name: "ullbc_ast",
ancestors: &["statement"],
name: "ullbc_ast",
reduce: false,
extra_types: &[],
})), &[
Expand Down

0 comments on commit 623752e

Please sign in to comment.