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