1#![feature(if_let_guard)]
10
11use anyhow::{Context, Result, bail};
12use assert_cmd::cargo::CommandCargoExt;
13use charon_lib::ast::*;
14use convert_case::{Case, Casing};
15use indoc::indoc;
16use itertools::Itertools;
17use std::collections::{HashMap, HashSet};
18use std::fmt::Write;
19use std::fs;
20use std::path::PathBuf;
21use std::process::Command;
22
23fn repr_name(_crate_data: &TranslatedCrate, n: &Name) -> String {
25 n.name
26 .iter()
27 .map(|path_elem| match path_elem {
28 PathElem::Ident(i, _) => i.clone(),
29 PathElem::Impl(..) => "<impl>".to_string(),
30 PathElem::Monomorphized(..) => "<mono>".to_string(),
31 })
32 .join("::")
33}
34
35fn make_ocaml_ident(name: &str) -> String {
36 let mut name = name.to_case(Case::Snake);
37 if matches!(
38 &*name,
39 "virtual"
40 | "bool"
41 | "char"
42 | "struct"
43 | "type"
44 | "let"
45 | "fun"
46 | "open"
47 | "rec"
48 | "assert"
49 | "float"
50 | "end"
51 | "include"
52 | "to"
53 ) {
54 name += "_";
55 }
56 name
57}
58fn type_name_to_ocaml_ident(item_meta: &ItemMeta) -> String {
59 let name = item_meta
60 .attr_info
61 .rename
62 .as_ref()
63 .unwrap_or(item_meta.name.name.last().unwrap().as_ident().unwrap().0);
64 make_ocaml_ident(name)
65}
66
67struct GenerateCtx<'a> {
68 crate_data: &'a TranslatedCrate,
69 name_to_type: HashMap<String, &'a TypeDecl>,
70 type_tree: HashMap<TypeDeclId, HashSet<TypeDeclId>>,
72 manual_type_impls: HashMap<TypeDeclId, String>,
73 manual_json_impls: HashMap<TypeDeclId, String>,
74 opaque_for_visitor: HashSet<TypeDeclId>,
75}
76
77impl<'a> GenerateCtx<'a> {
78 fn new(
79 crate_data: &'a TranslatedCrate,
80 manual_type_impls: &[(&str, &str)],
81 manual_json_impls: &[(&str, &str)],
82 opaque_for_visitor: &[&str],
83 ) -> Self {
84 let mut name_to_type: HashMap<String, &TypeDecl> = Default::default();
85 let mut type_tree = HashMap::default();
86 for ty in &crate_data.type_decls {
87 let long_name = repr_name(crate_data, &ty.item_meta.name);
88 if long_name.starts_with("charon_lib") {
89 let short_name = ty
90 .item_meta
91 .name
92 .name
93 .last()
94 .unwrap()
95 .as_ident()
96 .unwrap()
97 .0
98 .clone();
99 name_to_type.insert(short_name, ty);
100 }
101 name_to_type.insert(long_name, ty);
102
103 let mut contained = HashSet::new();
104 ty.dyn_visit(|id: &TypeDeclId| {
105 contained.insert(*id);
106 });
107 type_tree.insert(ty.def_id, contained);
108 }
109
110 let mut ctx = GenerateCtx {
111 crate_data: &crate_data,
112 name_to_type,
113 type_tree,
114 manual_type_impls: Default::default(),
115 manual_json_impls: Default::default(),
116 opaque_for_visitor: Default::default(),
117 };
118 ctx.manual_type_impls = manual_type_impls
119 .iter()
120 .map(|(name, def)| (ctx.id_from_name(name), def.to_string()))
121 .collect();
122 ctx.manual_json_impls = manual_json_impls
123 .iter()
124 .map(|(name, def)| (ctx.id_from_name(name), def.to_string()))
125 .collect();
126 ctx.opaque_for_visitor = opaque_for_visitor
127 .iter()
128 .map(|name| ctx.id_from_name(name))
129 .collect();
130 ctx
131 }
132
133 fn id_from_name(&self, name: &str) -> TypeDeclId {
134 self.name_to_type
135 .get(name)
136 .expect(&format!("Name not found: `{name}`"))
137 .def_id
138 }
139
140 fn children_of(&self, name: &str) -> HashSet<TypeDeclId> {
142 let start_id = self.id_from_name(name);
143 self.children_of_inner(vec![start_id])
144 }
145
146 fn children_of_many(&self, names: &[&str]) -> HashSet<TypeDeclId> {
148 self.children_of_inner(names.iter().map(|name| self.id_from_name(name)).collect())
149 }
150
151 fn children_of_inner(&self, ty: Vec<TypeDeclId>) -> HashSet<TypeDeclId> {
152 let mut children = HashSet::new();
153 let mut stack = ty.to_vec();
154 while let Some(id) = stack.pop() {
155 if !children.contains(&id)
156 && self
157 .crate_data
158 .type_decls
159 .get(id)
160 .is_some_and(|decl| decl.item_meta.is_local)
161 {
162 children.insert(id);
163 if let Some(contained) = self.type_tree.get(&id) {
164 stack.extend(contained);
165 }
166 }
167 }
168 children
169 }
170}
171
172fn type_to_ocaml_call(ctx: &GenerateCtx, ty: &Ty) -> String {
175 match ty.kind() {
176 TyKind::Literal(LiteralTy::Bool) => "bool_of_json".to_string(),
177 TyKind::Literal(LiteralTy::Char) => "char_of_json".to_string(),
178 TyKind::Literal(LiteralTy::Integer(_)) => "int_of_json".to_string(),
179 TyKind::Literal(LiteralTy::Float(_)) => "float_of_json".to_string(),
180 TyKind::Adt(tref) => {
181 let mut expr = Vec::new();
182 for ty in &tref.generics.types {
183 expr.push(type_to_ocaml_call(ctx, ty))
184 }
185 match tref.id {
186 TypeId::Adt(id) => {
187 let mut first = if let Some(tdecl) = ctx.crate_data.type_decls.get(id) {
188 type_name_to_ocaml_ident(&tdecl.item_meta)
189 } else {
190 format!("missing_type_{id}")
191 };
192 if first == "vec" {
193 first = "list".to_string();
194 }
195 expr.insert(0, first + "_of_json");
196 }
197 TypeId::Builtin(BuiltinTy::Box) => expr.insert(0, "box_of_json".to_owned()),
198 TypeId::Tuple => {
199 let name = match tref.generics.types.elem_count() {
200 2 => "pair_of_json".to_string(),
201 3 => "triple_of_json".to_string(),
202 len => format!("tuple_{len}_of_json"),
203 };
204 expr.insert(0, name);
205 }
206 _ => unimplemented!("{ty:?}"),
207 }
208 expr.into_iter().map(|f| format!("({f})")).join(" ")
209 }
210 TyKind::TypeVar(DeBruijnVar::Free(id)) => format!("arg{id}_of_json"),
211 _ => unimplemented!("{ty:?}"),
212 }
213}
214
215fn type_to_ocaml_name(ctx: &GenerateCtx, ty: &Ty) -> String {
218 match ty.kind() {
219 TyKind::Literal(LiteralTy::Bool) => "bool".to_string(),
220 TyKind::Literal(LiteralTy::Char) => "(Uchar.t [@visitors.opaque])".to_string(),
221 TyKind::Literal(LiteralTy::Integer(_)) => "int".to_string(),
222 TyKind::Literal(LiteralTy::Float(_)) => "float_of_json".to_string(),
223 TyKind::Adt(tref) => {
224 let mut args = tref
225 .generics
226 .types
227 .iter()
228 .map(|ty| type_to_ocaml_name(ctx, ty))
229 .map(|name| {
230 if !name.chars().all(|c| c.is_alphanumeric()) {
231 format!("({name})")
232 } else {
233 name
234 }
235 })
236 .collect_vec();
237 match tref.id {
238 TypeId::Adt(id) => {
239 let mut base_ty = if let Some(tdecl) = ctx.crate_data.type_decls.get(id) {
240 type_name_to_ocaml_ident(&tdecl.item_meta)
241 } else if let Some(name) = ctx.crate_data.item_name(id) {
242 eprintln!(
243 "Warning: type {} missing from llbc",
244 repr_name(ctx.crate_data, name)
245 );
246 name.name
247 .last()
248 .unwrap()
249 .as_ident()
250 .unwrap()
251 .0
252 .to_lowercase()
253 } else {
254 format!("missing_type_{id}")
255 };
256 if base_ty == "vec" {
257 base_ty = "list".to_string();
258 }
259 if base_ty == "vector" {
260 base_ty = "list".to_string();
261 args.remove(0); }
263 let args = match args.as_slice() {
264 [] => String::new(),
265 [arg] => arg.clone(),
266 args => format!("({})", args.iter().join(",")),
267 };
268 format!("{args} {base_ty}")
269 }
270 TypeId::Builtin(BuiltinTy::Box) => args[0].clone(),
271 TypeId::Tuple => args.iter().join("*"),
272 _ => unimplemented!("{ty:?}"),
273 }
274 }
275 TyKind::TypeVar(DeBruijnVar::Free(id)) => format!("'a{id}"),
276 _ => unimplemented!("{ty:?}"),
277 }
278}
279
280fn convert_vars<'a>(ctx: &GenerateCtx, fields: impl IntoIterator<Item = &'a Field>) -> String {
281 fields
282 .into_iter()
283 .filter(|f| !f.is_opaque())
284 .map(|f| {
285 let name = make_ocaml_ident(f.name.as_deref().unwrap());
286 let rename = make_ocaml_ident(f.renamed_name().unwrap());
287 let convert = type_to_ocaml_call(ctx, &f.ty);
288 format!("let* {rename} = {convert} ctx {name} in")
289 })
290 .join("\n")
291}
292
293fn build_branch<'a>(
294 ctx: &GenerateCtx,
295 pat: &str,
296 fields: impl IntoIterator<Item = &'a Field>,
297 construct: &str,
298) -> String {
299 let convert = convert_vars(ctx, fields);
300 format!("| {pat} -> {convert} Ok ({construct})")
301}
302
303fn build_function(_ctx: &GenerateCtx, decl: &TypeDecl, branches: &str) -> String {
304 let ty_name = type_name_to_ocaml_ident(&decl.item_meta);
305 let signature = if decl.generics.types.is_empty() {
306 format!("{ty_name}_of_json (ctx : of_json_ctx) (js : json) : ({ty_name}, string) result =")
307 } else {
308 let types = &decl.generics.types;
309 let gen_vars_space = types
310 .iter()
311 .enumerate()
312 .map(|(i, _)| format!("'a{i}"))
313 .join(" ");
314 let gen_vars_comma = types
315 .iter()
316 .enumerate()
317 .map(|(i, _)| format!("'a{i}"))
318 .join(", ");
319
320 let mut args = Vec::new();
321 let mut ty_args = Vec::new();
322 for (i, _) in types.iter().enumerate() {
323 args.push(format!("arg{i}_of_json"));
324 ty_args.push(format!("(of_json_ctx -> json -> ('a{i}, string) result)"));
325 }
326 args.push("ctx".to_string());
327 ty_args.push("of_json_ctx".to_string());
328 args.push("js".to_string());
329 ty_args.push("json".to_string());
330
331 let ty_args = ty_args.into_iter().join(" -> ");
332 let args = args.into_iter().join(" ");
333 let fun_ty =
334 format!("{gen_vars_space}. {ty_args} -> (({gen_vars_comma}) {ty_name}, string) result");
335 format!("{ty_name}_of_json : {fun_ty} = fun {args} ->")
336 };
337 format!(
338 r#"
339 and {signature}
340 combine_error_msgs js __FUNCTION__
341 (match js with{branches} | _ -> Error "")
342 "#
343 )
344}
345
346fn type_decl_to_json_deserializer(ctx: &GenerateCtx, decl: &TypeDecl) -> String {
347 let return_ty = type_name_to_ocaml_ident(&decl.item_meta);
348 let return_ty = if decl.generics.types.is_empty() {
349 return_ty
350 } else {
351 format!("_ {return_ty}")
352 };
353
354 let branches = match &decl.kind {
355 _ if let Some(def) = ctx.manual_json_impls.get(&decl.def_id) => def.clone(),
356 TypeDeclKind::Struct(fields) if fields.is_empty() => {
357 build_branch(ctx, "`Null", fields, "()")
358 }
359 TypeDeclKind::Struct(fields)
360 if fields.elem_count() == 1
361 && fields[0].name.as_ref().is_some_and(|name| name == "_raw") =>
362 {
363 let short_name = decl
365 .item_meta
366 .name
367 .name
368 .last()
369 .unwrap()
370 .as_ident()
371 .unwrap()
372 .0
373 .clone();
374 format!("| x -> {short_name}.id_of_json ctx x")
375 }
376 TypeDeclKind::Struct(fields)
377 if fields.elem_count() == 1
378 && (fields[0].name.is_none()
379 || decl
380 .item_meta
381 .attr_info
382 .attributes
383 .iter()
384 .filter_map(|a| a.as_unknown())
385 .any(|a| a.to_string() == "serde(transparent)")) =>
386 {
387 let ty = &fields[0].ty;
388 let call = type_to_ocaml_call(ctx, ty);
389 format!("| x -> {call} ctx x")
390 }
391 TypeDeclKind::Alias(ty) => {
392 let call = type_to_ocaml_call(ctx, ty);
393 format!("| x -> {call} ctx x")
394 }
395 TypeDeclKind::Struct(fields) if fields.iter().all(|f| f.name.is_none()) => {
396 let mut fields = fields.clone();
397 for (i, f) in fields.iter_mut().enumerate() {
398 f.name = Some(format!("x{i}"));
399 }
400 let pat: String = fields
401 .iter()
402 .map(|f| f.name.as_deref().unwrap())
403 .map(|n| make_ocaml_ident(n))
404 .join(";");
405 let pat = format!("`List [ {pat} ]");
406 let construct = fields
407 .iter()
408 .map(|f| f.renamed_name().unwrap())
409 .map(|n| make_ocaml_ident(n))
410 .join(", ");
411 let construct = format!("( {construct} )");
412 build_branch(ctx, &pat, &fields, &construct)
413 }
414 TypeDeclKind::Struct(fields) => {
415 let fields = fields
416 .iter()
417 .filter(|field| {
418 !field
419 .attr_info
420 .attributes
421 .iter()
422 .filter_map(|a| a.as_unknown())
423 .any(|a| a.to_string() == "serde(skip)")
424 })
425 .collect_vec();
426 let pat: String = fields
427 .iter()
428 .map(|f| {
429 let name = f.name.as_ref().unwrap();
430 let var = if f.is_opaque() {
431 "_"
432 } else {
433 &make_ocaml_ident(name)
434 };
435 format!("(\"{name}\", {var});")
436 })
437 .join("\n");
438 let pat = format!("`Assoc [ {pat} ]");
439 let construct = fields
440 .iter()
441 .filter(|f| !f.is_opaque())
442 .map(|f| f.renamed_name().unwrap())
443 .map(|n| make_ocaml_ident(n))
444 .join("; ");
445 let construct = format!("({{ {construct} }} : {return_ty})");
446 build_branch(ctx, &pat, fields, &construct)
447 }
448 TypeDeclKind::Enum(variants) => {
449 variants
450 .iter()
451 .filter(|v| !v.is_opaque())
452 .map(|variant| {
453 let name = &variant.name;
454 let rename = variant.renamed_name();
455 if variant.fields.is_empty() {
456 let pat = format!("`String \"{name}\"");
458 build_branch(ctx, &pat, &variant.fields, rename)
459 } else {
460 let mut fields = variant.fields.clone();
461 let inner_pat = if fields.iter().all(|f| f.name.is_none()) {
462 if variant.fields.elem_count() == 1 {
464 let var = make_ocaml_ident(&variant.name);
465 fields[0].name = Some(var.clone());
466 var
467 } else {
468 for (i, f) in fields.iter_mut().enumerate() {
469 f.name = Some(format!("x_{i}"));
470 }
471 let pat =
472 fields.iter().map(|f| f.name.as_ref().unwrap()).join("; ");
473 format!("`List [ {pat} ]")
474 }
475 } else {
476 let pat = fields
478 .iter()
479 .map(|f| {
480 let name = f.name.as_ref().unwrap();
481 let var = if f.is_opaque() {
482 "_"
483 } else {
484 &make_ocaml_ident(name)
485 };
486 format!("(\"{name}\", {var});")
487 })
488 .join(" ");
489 format!("`Assoc [ {pat} ]")
490 };
491 let pat = format!("`Assoc [ (\"{name}\", {inner_pat}) ]");
492 let construct_fields = fields
493 .iter()
494 .map(|f| f.name.as_ref().unwrap())
495 .map(|n| make_ocaml_ident(n))
496 .join(", ");
497 let construct = format!("{rename} ({construct_fields})");
498 build_branch(ctx, &pat, &fields, &construct)
499 }
500 })
501 .join("\n")
502 }
503 TypeDeclKind::Union(..) => todo!(),
504 TypeDeclKind::Opaque => todo!(),
505 TypeDeclKind::Error(_) => todo!(),
506 };
507 build_function(ctx, decl, &branches)
508}
509
510fn extract_doc_comments(attr_info: &AttrInfo) -> String {
511 attr_info
512 .attributes
513 .iter()
514 .filter_map(|a| a.as_doc_comment())
515 .join("\n")
516}
517
518fn build_doc_comment(comment: String, indent_level: usize) -> String {
520 #[derive(Default)]
521 struct Exchanger {
522 is_in_open_escaped_block: bool,
523 is_in_open_inline_escape: bool,
524 }
525 impl Exchanger {
526 pub fn exchange_escape_delimiters(&mut self, line: &str) -> String {
527 if line.contains("```") {
528 let (leading, mut rest) = line.split_once("```").unwrap();
530
531 rest = if rest.starts_with("text") {
533 rest.strip_prefix("text").unwrap()
534 } else if rest.starts_with("rust,ignore") {
535 rest.strip_prefix("rust,ignore").unwrap()
536 } else {
537 rest
538 };
539 let mut result = leading.to_owned();
540 if self.is_in_open_escaped_block {
541 result.push_str("]}");
542 self.is_in_open_escaped_block = false;
543 } else {
544 result.push_str("{@rust[");
545 self.is_in_open_escaped_block = true;
546 }
547 result.push_str(rest);
548 result
549 } else if line.contains('`') {
550 let mut parts = line.split('`');
552 let mut result = parts.next().unwrap().to_owned();
554 for part in parts {
555 if self.is_in_open_inline_escape {
556 result.push_str("]");
557 result.push_str(part);
558 self.is_in_open_inline_escape = false;
559 } else {
560 result.push_str("[");
561 result.push_str(part);
562 self.is_in_open_inline_escape = true;
563 }
564 }
565 result
566 } else {
567 line.to_owned()
568 }
569 }
570 }
571
572 if comment == "" {
573 return comment;
574 }
575 let is_multiline = comment.contains("\n");
576 if !is_multiline {
577 let fixed_comment = Exchanger::default().exchange_escape_delimiters(&comment);
578 format!("(**{fixed_comment} *)")
579 } else {
580 let indent = " ".repeat(indent_level);
581 let mut exchanger = Exchanger::default();
582 let comment = comment
583 .lines()
584 .enumerate()
585 .map(|(i, line)| {
586 let line = line.strip_prefix(" ").unwrap_or(line);
589 let fixed_line = exchanger.exchange_escape_delimiters(line);
590
591 if i == 0 || fixed_line.is_empty() {
594 fixed_line
595 } else {
596 format!("{indent} {fixed_line}")
597 }
598 })
599 .join("\n");
600 format!("(** {comment}\n{indent} *)")
601 }
602}
603
604fn build_type(_ctx: &GenerateCtx, decl: &TypeDecl, co_rec: bool, body: &str) -> String {
605 let ty_name = type_name_to_ocaml_ident(&decl.item_meta);
606 let generics = decl
607 .generics
608 .types
609 .iter()
610 .enumerate()
611 .map(|(i, _)| format!("'a{i}"))
612 .collect_vec();
613 let generics = match generics.as_slice() {
614 [] => String::new(),
615 [ty] => ty.clone(),
616 generics => format!("({})", generics.iter().join(",")),
617 };
618 let comment = extract_doc_comments(&decl.item_meta.attr_info);
619 let comment = build_doc_comment(comment, 0);
620 let keyword = if co_rec { "and" } else { "type" };
621 format!("\n{comment} {keyword} {generics} {ty_name} = {body}")
622}
623
624fn type_decl_to_ocaml_decl(ctx: &GenerateCtx, decl: &TypeDecl, co_rec: bool) -> String {
629 let opaque = if ctx.opaque_for_visitor.contains(&decl.def_id) {
630 "[@visitors.opaque]"
631 } else {
632 ""
633 };
634 let body = match &decl.kind {
635 _ if let Some(def) = ctx.manual_type_impls.get(&decl.def_id) => def.clone(),
636 TypeDeclKind::Alias(ty) => {
637 let ty = type_to_ocaml_name(ctx, ty);
638 format!("{ty} {opaque}")
639 }
640 TypeDeclKind::Struct(fields) if fields.is_empty() => "unit".to_string(),
641 TypeDeclKind::Struct(fields)
642 if fields.elem_count() == 1
643 && fields[0].name.as_ref().is_some_and(|name| name == "_raw") =>
644 {
645 let short_name = decl
647 .item_meta
648 .name
649 .name
650 .last()
651 .unwrap()
652 .as_ident()
653 .unwrap()
654 .0
655 .clone();
656 format!("{short_name}.id [@visitors.opaque]")
657 }
658 TypeDeclKind::Struct(fields)
659 if fields.elem_count() == 1
660 && (fields[0].name.is_none()
661 || decl
662 .item_meta
663 .attr_info
664 .attributes
665 .iter()
666 .filter_map(|a| a.as_unknown())
667 .any(|a| a.to_string() == "serde(transparent)")) =>
668 {
669 let ty = type_to_ocaml_name(ctx, &fields[0].ty);
670 format!("{ty} {opaque}")
671 }
672 TypeDeclKind::Struct(fields) if fields.iter().all(|f| f.name.is_none()) => fields
673 .iter()
674 .filter(|f| !f.is_opaque())
675 .map(|f| {
676 let ty = type_to_ocaml_name(ctx, &f.ty);
677 format!("{ty} {opaque}")
678 })
679 .join("*"),
680 TypeDeclKind::Struct(fields) => {
681 let fields = fields
682 .iter()
683 .filter(|f| !f.is_opaque())
684 .map(|f| {
685 let name = f.renamed_name().unwrap();
686 let ty = type_to_ocaml_name(ctx, &f.ty);
687 let comment = extract_doc_comments(&f.attr_info);
688 let comment = build_doc_comment(comment, 2);
689 format!("{name} : {ty} {opaque} {comment}")
690 })
691 .join(";");
692 format!("{{ {fields} }}")
693 }
694 TypeDeclKind::Enum(variants) => {
695 variants
696 .iter()
697 .filter(|v| !v.is_opaque())
698 .map(|variant| {
699 let mut attr_info = variant.attr_info.clone();
700 let rename = variant.renamed_name();
701 let ty = if variant.fields.is_empty() {
702 String::new()
704 } else {
705 if variant.fields.iter().all(|f| f.name.is_some()) {
706 let fields = variant
707 .fields
708 .iter()
709 .map(|f| {
710 let comment = extract_doc_comments(&f.attr_info);
711 let description = if comment.is_empty() {
712 comment
713 } else {
714 format!(": {comment}")
715 };
716 format!("\n - [{}]{description}", f.name.as_ref().unwrap())
717 })
718 .join("");
719 let field_descriptions = format!("\n Fields:{fields}");
720 attr_info
722 .attributes
723 .push(Attribute::DocComment(field_descriptions));
724 }
725 let fields = variant
726 .fields
727 .iter()
728 .map(|f| {
729 let ty = type_to_ocaml_name(ctx, &f.ty);
730 format!("{ty} {opaque}")
731 })
732 .join("*");
733 format!(" of {fields}")
734 };
735 let comment = extract_doc_comments(&attr_info);
736 let comment = build_doc_comment(comment, 3);
737 format!("\n\n | {rename}{ty} {comment}")
738 })
739 .join("")
740 }
741 TypeDeclKind::Union(..) => todo!(),
742 TypeDeclKind::Opaque => todo!(),
743 TypeDeclKind::Error(_) => todo!(),
744 };
745 build_type(ctx, decl, co_rec, &body)
746}
747
748fn generate_visitor_bases(
749 _ctx: &GenerateCtx,
750 name: &str,
751 inherits: &[&str],
752 reduce: bool,
753 ty_names: &[String],
754) -> String {
755 let mut out = String::new();
756 let make_inherit = |variety| {
757 if !inherits.is_empty() {
758 inherits
759 .iter()
760 .map(|ancestor| {
761 if let [module, name] = ancestor.split(".").collect_vec().as_slice() {
762 format!("inherit [_] {module}.{variety}_{name}")
763 } else {
764 format!("inherit [_] {variety}_{ancestor}")
765 }
766 })
767 .join("\n")
768 } else {
769 format!("inherit [_] VisitorsRuntime.{variety}")
770 }
771 };
772
773 let iter_methods = ty_names
774 .iter()
775 .map(|ty| format!("method visit_{ty} : 'env -> {ty} -> unit = fun _ _ -> ()"))
776 .format("\n");
777 let _ = write!(
778 &mut out,
779 "
780 class ['self] iter_{name} =
781 object (self : 'self)
782 {}
783 {iter_methods}
784 end
785 ",
786 make_inherit("iter")
787 );
788
789 let map_methods = ty_names
790 .iter()
791 .map(|ty| format!("method visit_{ty} : 'env -> {ty} -> {ty} = fun _ x -> x"))
792 .format("\n");
793 let _ = write!(
794 &mut out,
795 "
796 class ['self] map_{name} =
797 object (self : 'self)
798 {}
799 {map_methods}
800 end
801 ",
802 make_inherit("map")
803 );
804
805 if reduce {
806 let reduce_methods = ty_names
807 .iter()
808 .map(|ty| format!("method visit_{ty} : 'env -> {ty} -> 'a = fun _ _ -> self#zero"))
809 .format("\n");
810 let _ = write!(
811 &mut out,
812 "
813 class virtual ['self] reduce_{name} =
814 object (self : 'self)
815 {}
816 {reduce_methods}
817 end
818 ",
819 make_inherit("reduce")
820 );
821
822 let mapreduce_methods = ty_names
823 .iter()
824 .map(|ty| {
825 format!("method visit_{ty} : 'env -> {ty} -> {ty} * 'a = fun _ x -> (x, self#zero)")
826 })
827 .format("\n");
828 let _ = write!(
829 &mut out,
830 "
831 class virtual ['self] mapreduce_{name} =
832 object (self : 'self)
833 {}
834 {mapreduce_methods}
835 end
836 ",
837 make_inherit("mapreduce")
838 );
839 }
840
841 out
842}
843
844#[derive(Clone, Copy)]
845struct DeriveVisitors {
846 name: &'static str,
847 ancestors: &'static [&'static str],
848 reduce: bool,
849 extra_types: &'static [&'static str],
850}
851
852#[derive(Clone, Copy)]
854enum GenerationKind {
855 OfJson,
856 TypeDecl(Option<DeriveVisitors>),
857}
858
859struct GenerateCodeFor {
861 template: PathBuf,
862 target: PathBuf,
863 markers: Vec<(GenerationKind, HashSet<TypeDeclId>)>,
869}
870
871impl GenerateCodeFor {
872 fn generate(&self, ctx: &GenerateCtx) -> Result<()> {
873 let mut template = fs::read_to_string(&self.template)
874 .with_context(|| format!("Failed to read template file {}", self.template.display()))?;
875 for (i, (kind, names)) in self.markers.iter().enumerate() {
876 let tys = names
877 .iter()
878 .map(|&id| &ctx.crate_data[id])
879 .sorted_by_key(|tdecl| {
880 tdecl
881 .item_meta
882 .name
883 .name
884 .last()
885 .unwrap()
886 .as_ident()
887 .unwrap()
888 });
889 let generated = match kind {
890 GenerationKind::OfJson => {
891 let fns = tys
892 .map(|ty| type_decl_to_json_deserializer(ctx, ty))
893 .format("\n");
894 format!("let rec ___ = ()\n{fns}")
895 }
896 GenerationKind::TypeDecl(visitors) => {
897 let mut decls = tys
898 .enumerate()
899 .map(|(i, ty)| {
900 let co_recursive = i != 0;
901 type_decl_to_ocaml_decl(ctx, ty, co_recursive)
902 })
903 .join("\n");
904 if let Some(visitors) = visitors {
905 let &DeriveVisitors {
906 name,
907 mut ancestors,
908 reduce,
909 extra_types,
910 } = visitors;
911 let varieties: &[_] = if reduce {
912 &["iter", "map", "reduce", "mapreduce"]
913 } else {
914 &["iter", "map"]
915 };
916 let intermediate_visitor_name;
917 let intermediate_visitor_name_slice;
918 if !extra_types.is_empty() {
919 intermediate_visitor_name = format!("{name}_base");
920 let intermediate_visitor = generate_visitor_bases(
921 ctx,
922 &intermediate_visitor_name,
923 ancestors,
924 reduce,
925 extra_types
926 .iter()
927 .map(|s| s.to_string())
928 .collect_vec()
929 .as_slice(),
930 );
931 intermediate_visitor_name_slice = [intermediate_visitor_name.as_str()];
932 ancestors = &intermediate_visitor_name_slice;
933 decls = format!(
934 "(* Ancestors for the {name} visitors *){intermediate_visitor}\n{decls}"
935 );
936 }
937 let visitors = varieties
938 .iter()
939 .map(|variety| {
940 let nude = if !ancestors.is_empty() {
941 format!("nude = true (* Don't inherit VisitorsRuntime *);")
942 } else {
943 String::new()
944 };
945 let ancestors = format!(
946 "ancestors = [ {} ];",
947 ancestors
948 .iter()
949 .map(|a| format!("\"{variety}_{a}\""))
950 .join(";")
951 );
952 format!(
953 r#"
954 visitors {{
955 name = "{variety}_{name}";
956 monomorphic = ["env"];
957 variety = "{variety}";
958 {ancestors}
959 {nude}
960 }}
961 "#
962 )
963 })
964 .format(", ");
965 let _ = write!(&mut decls, "\n[@@deriving show, eq, ord, {visitors}]");
966 };
967 decls
968 }
969 };
970 let placeholder = format!("(* __REPLACE{i}__ *)");
971 template = template.replace(&placeholder, &generated);
972 }
973
974 fs::write(&self.target, template)
975 .with_context(|| format!("Failed to write generated file {}", self.target.display()))?;
976 Ok(())
977 }
978}
979
980fn main() -> Result<()> {
981 let dir = PathBuf::from("src/bin/generate-ml");
982 let charon_llbc = dir.join("charon-itself.ullbc");
983 let reuse_llbc = std::env::var("CHARON_ML_REUSE_LLBC").is_ok(); if !reuse_llbc {
985 let mut cmd = Command::cargo_bin("charon")?;
987 cmd.arg("cargo");
988 cmd.arg("--hide-marker-traits");
989 cmd.arg("--hide-allocator");
990 cmd.arg("--ullbc");
991 cmd.arg("--start-from=charon_lib::ast::krate::TranslatedCrate");
992 cmd.arg("--start-from=charon_lib::ast::ullbc_ast::BodyContents");
993 cmd.arg("--exclude=charon_lib::common::hash_consing::HashConsed");
994 cmd.arg("--dest-file");
995 cmd.arg(&charon_llbc);
996 cmd.arg("--");
997 cmd.arg("--lib");
998 let output = cmd.output()?;
999
1000 if !output.status.success() {
1001 let stderr = String::from_utf8(output.stderr.clone())?;
1002 bail!("Compilation failed: {stderr}")
1003 }
1004 }
1005
1006 let crate_data: TranslatedCrate = charon_lib::deserialize_llbc(&charon_llbc)?;
1007 let output_dir = if std::env::var("IN_CI").as_deref() == Ok("1") {
1008 dir.join("generated")
1009 } else {
1010 dir.join("../../../../charon-ml/src/generated")
1011 };
1012 generate_ml(crate_data, dir.join("templates"), output_dir)
1013}
1014
1015fn generate_ml(
1016 crate_data: TranslatedCrate,
1017 template_dir: PathBuf,
1018 output_dir: PathBuf,
1019) -> anyhow::Result<()> {
1020 let manual_type_impls = &[
1021 ("FileId", "file"),
1023 (
1026 "ScalarValue",
1027 indoc!(
1028 "
1029 (* Note that we use unbounded integers everywhere.
1030 We then harcode the boundaries for the different types.
1031 *)
1032 { value : big_int; int_ty : integer_type }
1033 "
1034 ),
1035 ),
1036 ("RegionVar", "(region_id, string option) indexed_var"),
1039 ("TypeVar", "(type_var_id, string) indexed_var"),
1040 ];
1041 let manual_json_impls = &[
1042 (
1044 "Vector",
1045 indoc!(
1046 r#"
1047 | js ->
1048 let* list = list_of_json (option_of_json arg1_of_json) ctx js in
1049 Ok (List.filter_map (fun x -> x) list)
1050 "#
1051 ),
1052 ),
1053 (
1055 "FileId",
1056 indoc!(
1057 r#"
1058 | json ->
1059 let* file_id = FileId.id_of_json ctx json in
1060 let file = FileId.Map.find file_id ctx in
1061 Ok file
1062 "#,
1063 ),
1064 ),
1065 (
1068 "ScalarValue",
1069 indoc!(
1070 r#"
1071 | `Assoc [ (ty, bi) ] ->
1072 let big_int_of_json (js : json) : (big_int, string) result =
1073 combine_error_msgs js __FUNCTION__
1074 (match js with
1075 | `Int i -> Ok (Z.of_int i)
1076 | `String is -> Ok (Z.of_string is)
1077 | _ -> Error "")
1078 in
1079 let* value = big_int_of_json bi in
1080 let* int_ty = integer_type_of_json ctx (`String ty) in
1081 let sv = { value; int_ty } in
1082 if not (check_scalar_value_in_range sv) then
1083 raise (Failure ("Scalar value not in range: " ^ show_scalar_value sv));
1084 Ok sv
1085 "#
1086 ),
1087 ),
1088 ];
1089 let dont_generate_ty = &[
1091 "ItemOpacity",
1092 "PredicateOrigin",
1093 "TraitTypeConstraintId",
1094 "Ty",
1095 "Vector",
1096 ];
1097 let opaque_for_visitor = &["Name"];
1099 let ctx = GenerateCtx::new(
1100 &crate_data,
1101 manual_type_impls,
1102 manual_json_impls,
1103 opaque_for_visitor,
1104 );
1105
1106 let manually_implemented: HashSet<_> = [
1108 "ItemOpacity",
1109 "PredicateOrigin",
1110 "Ty", "Opaque",
1112 "Body",
1113 "FunDecl",
1114 "TranslatedCrate",
1115 ]
1116 .iter()
1117 .map(|name| ctx.id_from_name(name))
1118 .collect();
1119
1120 let (gast_types, llbc_types, ullbc_types) = {
1122 let llbc_types: HashSet<_> = ctx.children_of("charon_lib::ast::llbc_ast::Statement");
1123 let ullbc_types: HashSet<_> = ctx.children_of("charon_lib::ast::ullbc_ast::BodyContents");
1124 let all_types: HashSet<_> = ctx.children_of("TranslatedCrate");
1125
1126 let shared_types: HashSet<_> = llbc_types.intersection(&ullbc_types).copied().collect();
1127 let llbc_types: HashSet<_> = llbc_types.difference(&shared_types).copied().collect();
1128 let ullbc_types: HashSet<_> = ullbc_types.difference(&shared_types).copied().collect();
1129
1130 let body_specific_types: HashSet<_> = llbc_types.union(&ullbc_types).copied().collect();
1131 let gast_types: HashSet<_> = all_types
1132 .difference(&body_specific_types)
1133 .copied()
1134 .collect();
1135
1136 let gast_types: HashSet<_> = gast_types
1137 .difference(&manually_implemented)
1138 .copied()
1139 .collect();
1140 let llbc_types: HashSet<_> = llbc_types
1141 .difference(&manually_implemented)
1142 .copied()
1143 .collect();
1144 let ullbc_types: HashSet<_> = ullbc_types
1145 .difference(&manually_implemented)
1146 .copied()
1147 .collect();
1148 (gast_types, llbc_types, ullbc_types)
1149 };
1150
1151 let mut processed_tys: HashSet<TypeDeclId> = dont_generate_ty
1152 .iter()
1153 .map(|name| ctx.id_from_name(name))
1154 .collect();
1155 let mut markers_from_children = |ctx: &GenerateCtx, markers: &[_]| {
1159 markers
1160 .iter()
1161 .copied()
1162 .map(|(kind, type_names)| {
1163 let types: HashSet<_> = ctx.children_of_many(type_names);
1164 let unprocessed_types: HashSet<_> =
1165 types.difference(&processed_tys).copied().collect();
1166 processed_tys.extend(unprocessed_types.iter().copied());
1167 (kind, unprocessed_types)
1168 })
1169 .collect()
1170 };
1171
1172 #[rustfmt::skip]
1173 let generate_code_for = vec![
1174 GenerateCodeFor {
1175 template: template_dir.join("Meta.ml"),
1176 target: output_dir.join("Generated_Meta.ml"),
1177 markers: markers_from_children(&ctx, &[
1178 (GenerationKind::TypeDecl(None), &[
1179 "File",
1180 "Span",
1181 "AttrInfo",
1182 ]),
1183 ]),
1184 },
1185 GenerateCodeFor {
1186 template: template_dir.join("Values.ml"),
1187 target: output_dir.join("Generated_Values.ml"),
1188 markers: markers_from_children(&ctx, &[
1189 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1190 ancestors: &["big_int"],
1191 name: "literal",
1192 reduce: true,
1193 extra_types: &[],
1194 })), &[
1195 "Literal",
1196 "IntegerTy",
1197 "LiteralTy",
1198 ]),
1199 ]),
1200 },
1201 GenerateCodeFor {
1202 template: template_dir.join("Types.ml"),
1203 target: output_dir.join("Generated_Types.ml"),
1204 markers: markers_from_children(&ctx, &[
1205 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1206 ancestors: &["literal"],
1207 name: "const_generic",
1208 reduce: true,
1209 extra_types: &[],
1210 })), &[
1211 "TypeVarId",
1212 "ConstGeneric",
1213 "TraitClauseId",
1214 "DeBruijnVar",
1215 "AnyTransId",
1216 ]),
1217 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1220 ancestors: &["ty_base_base"],
1221 name: "ty",
1222 reduce: false,
1223 extra_types: &["span"],
1224 })), &[
1225 "TyKind",
1226 "TraitImplRef",
1227 "FunDeclRef",
1228 "GlobalDeclRef",
1229 ]),
1230 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1232 ancestors: &["ty"],
1233 name: "type_decl",
1234 reduce: false,
1235 extra_types: &[
1236 "attr_info"
1237 ],
1238 })), &[
1239 "Binder",
1240 "AbortKind",
1241 "TypeDecl",
1242 ]),
1243 ]),
1244 },
1245 GenerateCodeFor {
1246 template: template_dir.join("Expressions.ml"),
1247 target: output_dir.join("Generated_Expressions.ml"),
1248 markers: markers_from_children(&ctx, &[
1249 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1250 ancestors: &["type_decl"],
1251 name: "rvalue",
1252 reduce: false,
1253 extra_types: &[],
1254 })), &[
1255 "Rvalue",
1256 ]),
1257 ]),
1258 },
1259 GenerateCodeFor {
1260 template: template_dir.join("GAst.ml"),
1261 target: output_dir.join("Generated_GAst.ml"),
1262 markers: markers_from_children(&ctx, &[
1263 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1264 ancestors: &["rvalue"],
1265 name: "fun_sig",
1266 reduce: false,
1267 extra_types: &[],
1268 })), &[
1269 "Call",
1270 "Assert",
1271 "ItemKind",
1272 "Locals",
1273 "FunSig",
1274 "CopyNonOverlapping",
1275 ]),
1276 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1278 ancestors: &["fun_sig"],
1279 name: "global_decl",
1280 reduce: false,
1281 extra_types: &[],
1282 })), &[
1283 "GlobalDecl",
1284 ]),
1285 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1286 ancestors: &["global_decl"],
1287 name: "trait_decl",
1288 reduce: false,
1289 extra_types: &[],
1290 })), &[
1291 "TraitDecl",
1292 ]),
1293 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1294 ancestors: &["trait_decl"],
1295 name: "trait_impl",
1296 reduce: false,
1297 extra_types: &[],
1298 })), &[
1299 "TraitImpl",
1300 ]),
1301 (GenerationKind::TypeDecl(None), &[
1302 "CliOpts",
1303 "GExprBody",
1304 "DeclarationGroup",
1305 ]),
1306 ]),
1307 },
1308 GenerateCodeFor {
1309 template: template_dir.join("LlbcAst.ml"),
1310 target: output_dir.join("Generated_LlbcAst.ml"),
1311 markers: markers_from_children(&ctx, &[
1312 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1313 name: "statement_base",
1314 ancestors: &["trait_impl"],
1315 reduce: false,
1316 extra_types: &[],
1317 })), &[
1318 "charon_lib::ast::llbc_ast::Statement",
1319 ]),
1320 ]),
1321 },
1322 GenerateCodeFor {
1323 template: template_dir.join("UllbcAst.ml"),
1324 target: output_dir.join("Generated_UllbcAst.ml"),
1325 markers: markers_from_children(&ctx, &[
1326 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1327 ancestors: &["trait_impl"],
1328 name: "statement",
1329 reduce: false,
1330 extra_types: &[],
1331 })), &[
1332 "charon_lib::ast::ullbc_ast::Statement",
1333 "charon_lib::ast::ullbc_ast::SwitchTargets",
1334 ]),
1335 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1337 ancestors: &["statement"],
1338 name: "ullbc_ast",
1339 reduce: false,
1340 extra_types: &[],
1341 })), &[
1342 "charon_lib::ast::ullbc_ast::BodyContents",
1343 ]),
1344 ]),
1345 },
1346 GenerateCodeFor {
1347 template: template_dir.join("GAstOfJson.ml"),
1348 target: output_dir.join("Generated_GAstOfJson.ml"),
1349 markers: vec![(GenerationKind::OfJson, gast_types)],
1350 },
1351 GenerateCodeFor {
1352 template: template_dir.join("LlbcOfJson.ml"),
1353 target: output_dir.join("Generated_LlbcOfJson.ml"),
1354 markers: vec![(GenerationKind::OfJson, llbc_types)],
1355 },
1356 GenerateCodeFor {
1357 template: template_dir.join("UllbcOfJson.ml"),
1358 target: output_dir.join("Generated_UllbcOfJson.ml"),
1359 markers: vec![(GenerationKind::OfJson, ullbc_types)],
1360 },
1361 ];
1362 for file in generate_code_for {
1363 file.generate(&ctx)?;
1364 }
1365 Ok(())
1366}