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