1#![feature(if_let_guard)]
10
11use anyhow::{bail, Context, Result};
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(adt_kind, generics) => {
181 let mut expr = Vec::new();
182 for ty in &generics.types {
183 expr.push(type_to_ocaml_call(ctx, ty))
184 }
185 match adt_kind {
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 expr.pop(); }
196 expr.insert(0, first + "_of_json");
197 }
198 TypeId::Builtin(BuiltinTy::Box) => expr.insert(0, "box_of_json".to_owned()),
199 TypeId::Tuple => {
200 let name = match generics.types.elem_count() {
201 2 => "pair_of_json".to_string(),
202 3 => "triple_of_json".to_string(),
203 len => format!("tuple_{len}_of_json"),
204 };
205 expr.insert(0, name);
206 }
207 _ => unimplemented!("{ty:?}"),
208 }
209 expr.into_iter().map(|f| format!("({f})")).join(" ")
210 }
211 TyKind::TypeVar(DeBruijnVar::Free(id)) => format!("arg{id}_of_json"),
212 _ => unimplemented!("{ty:?}"),
213 }
214}
215
216fn type_to_ocaml_name(ctx: &GenerateCtx, ty: &Ty) -> String {
219 match ty.kind() {
220 TyKind::Literal(LiteralTy::Bool) => "bool".to_string(),
221 TyKind::Literal(LiteralTy::Char) => "(Uchar.t [@visitors.opaque])".to_string(),
222 TyKind::Literal(LiteralTy::Integer(_)) => "int".to_string(),
223 TyKind::Literal(LiteralTy::Float(_)) => "float_of_json".to_string(),
224 TyKind::Adt(adt_kind, generics) => {
225 let mut args = 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 adt_kind {
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 args.pop(); }
260 if base_ty == "vector" {
261 base_ty = "list".to_string();
262 args.remove(0); }
264 let args = match args.as_slice() {
265 [] => String::new(),
266 [arg] => arg.clone(),
267 args => format!("({})", args.iter().join(",")),
268 };
269 format!("{args} {base_ty}")
270 }
271 TypeId::Builtin(BuiltinTy::Box) => args[0].clone(),
272 TypeId::Tuple => args.iter().join("*"),
273 _ => unimplemented!("{ty:?}"),
274 }
275 }
276 TyKind::TypeVar(DeBruijnVar::Free(id)) => format!("'a{id}"),
277 _ => unimplemented!("{ty:?}"),
278 }
279}
280
281fn convert_vars<'a>(ctx: &GenerateCtx, fields: impl IntoIterator<Item = &'a Field>) -> String {
282 fields
283 .into_iter()
284 .filter(|f| !f.is_opaque())
285 .map(|f| {
286 let name = make_ocaml_ident(f.name.as_deref().unwrap());
287 let rename = make_ocaml_ident(f.renamed_name().unwrap());
288 let convert = type_to_ocaml_call(ctx, &f.ty);
289 format!("let* {rename} = {convert} ctx {name} in")
290 })
291 .join("\n")
292}
293
294fn build_branch<'a>(
295 ctx: &GenerateCtx,
296 pat: &str,
297 fields: impl IntoIterator<Item = &'a Field>,
298 construct: &str,
299) -> String {
300 let convert = convert_vars(ctx, fields);
301 format!("| {pat} -> {convert} Ok ({construct})")
302}
303
304fn build_function(_ctx: &GenerateCtx, decl: &TypeDecl, branches: &str) -> String {
305 let ty_name = type_name_to_ocaml_ident(&decl.item_meta);
306 let signature = if decl.generics.types.is_empty() {
307 format!("{ty_name}_of_json (ctx : of_json_ctx) (js : json) : ({ty_name}, string) result =")
308 } else {
309 let types = &decl.generics.types;
310 let gen_vars_space = types
311 .iter()
312 .enumerate()
313 .map(|(i, _)| format!("'a{i}"))
314 .join(" ");
315 let gen_vars_comma = types
316 .iter()
317 .enumerate()
318 .map(|(i, _)| format!("'a{i}"))
319 .join(", ");
320
321 let mut args = Vec::new();
322 let mut ty_args = Vec::new();
323 for (i, _) in types.iter().enumerate() {
324 args.push(format!("arg{i}_of_json"));
325 ty_args.push(format!("(of_json_ctx -> json -> ('a{i}, string) result)"));
326 }
327 args.push("ctx".to_string());
328 ty_args.push("of_json_ctx".to_string());
329 args.push("js".to_string());
330 ty_args.push("json".to_string());
331
332 let ty_args = ty_args.into_iter().join(" -> ");
333 let args = args.into_iter().join(" ");
334 let fun_ty =
335 format!("{gen_vars_space}. {ty_args} -> (({gen_vars_comma}) {ty_name}, string) result");
336 format!("{ty_name}_of_json : {fun_ty} = fun {args} ->")
337 };
338 format!(
339 r#"
340 and {signature}
341 combine_error_msgs js __FUNCTION__
342 (match js with{branches} | _ -> Error "")
343 "#
344 )
345}
346
347fn type_decl_to_json_deserializer(ctx: &GenerateCtx, decl: &TypeDecl) -> String {
348 let return_ty = type_name_to_ocaml_ident(&decl.item_meta);
349 let return_ty = if decl.generics.types.is_empty() {
350 return_ty
351 } else {
352 format!("_ {return_ty}")
353 };
354
355 let branches = match &decl.kind {
356 _ if let Some(def) = ctx.manual_json_impls.get(&decl.def_id) => def.clone(),
357 TypeDeclKind::Struct(fields) if fields.is_empty() => {
358 build_branch(ctx, "`Null", fields, "()")
359 }
360 TypeDeclKind::Struct(fields)
361 if fields.elem_count() == 1
362 && fields[0].name.as_ref().is_some_and(|name| name == "_raw") =>
363 {
364 let short_name = decl
366 .item_meta
367 .name
368 .name
369 .last()
370 .unwrap()
371 .as_ident()
372 .unwrap()
373 .0
374 .clone();
375 format!("| x -> {short_name}.id_of_json ctx x")
376 }
377 TypeDeclKind::Struct(fields)
378 if fields.elem_count() == 1
379 && (fields[0].name.is_none()
380 || decl
381 .item_meta
382 .attr_info
383 .attributes
384 .iter()
385 .filter_map(|a| a.as_unknown())
386 .any(|a| a.to_string() == "serde(transparent)")) =>
387 {
388 let ty = &fields[0].ty;
389 let call = type_to_ocaml_call(ctx, ty);
390 format!("| x -> {call} ctx x")
391 }
392 TypeDeclKind::Alias(ty) => {
393 let call = type_to_ocaml_call(ctx, ty);
394 format!("| x -> {call} ctx x")
395 }
396 TypeDeclKind::Struct(fields) if fields.iter().all(|f| f.name.is_none()) => {
397 let mut fields = fields.clone();
398 for (i, f) in fields.iter_mut().enumerate() {
399 f.name = Some(format!("x{i}"));
400 }
401 let pat: String = fields
402 .iter()
403 .map(|f| f.name.as_deref().unwrap())
404 .map(|n| make_ocaml_ident(n))
405 .join(";");
406 let pat = format!("`List [ {pat} ]");
407 let construct = fields
408 .iter()
409 .map(|f| f.renamed_name().unwrap())
410 .map(|n| make_ocaml_ident(n))
411 .join(", ");
412 let construct = format!("( {construct} )");
413 build_branch(ctx, &pat, &fields, &construct)
414 }
415 TypeDeclKind::Struct(fields) => {
416 let fields = fields
417 .iter()
418 .filter(|field| {
419 !field
420 .attr_info
421 .attributes
422 .iter()
423 .filter_map(|a| a.as_unknown())
424 .any(|a| a.to_string() == "serde(skip)")
425 })
426 .collect_vec();
427 let pat: String = fields
428 .iter()
429 .map(|f| {
430 let name = f.name.as_ref().unwrap();
431 let var = if f.is_opaque() {
432 "_"
433 } else {
434 &make_ocaml_ident(name)
435 };
436 format!("(\"{name}\", {var});")
437 })
438 .join("\n");
439 let pat = format!("`Assoc [ {pat} ]");
440 let construct = fields
441 .iter()
442 .filter(|f| !f.is_opaque())
443 .map(|f| f.renamed_name().unwrap())
444 .map(|n| make_ocaml_ident(n))
445 .join("; ");
446 let construct = format!("({{ {construct} }} : {return_ty})");
447 build_branch(ctx, &pat, fields, &construct)
448 }
449 TypeDeclKind::Enum(variants) => {
450 variants
451 .iter()
452 .filter(|v| !v.is_opaque())
453 .map(|variant| {
454 let name = &variant.name;
455 let rename = variant.renamed_name();
456 if variant.fields.is_empty() {
457 let pat = format!("`String \"{name}\"");
459 build_branch(ctx, &pat, &variant.fields, rename)
460 } else {
461 let mut fields = variant.fields.clone();
462 let inner_pat = if fields.iter().all(|f| f.name.is_none()) {
463 if variant.fields.elem_count() == 1 {
465 let var = make_ocaml_ident(&variant.name);
466 fields[0].name = Some(var.clone());
467 var
468 } else {
469 for (i, f) in fields.iter_mut().enumerate() {
470 f.name = Some(format!("x_{i}"));
471 }
472 let pat =
473 fields.iter().map(|f| f.name.as_ref().unwrap()).join("; ");
474 format!("`List [ {pat} ]")
475 }
476 } else {
477 let pat = 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(" ");
490 format!("`Assoc [ {pat} ]")
491 };
492 let pat = format!("`Assoc [ (\"{name}\", {inner_pat}) ]");
493 let construct_fields = fields
494 .iter()
495 .map(|f| f.name.as_ref().unwrap())
496 .map(|n| make_ocaml_ident(n))
497 .join(", ");
498 let construct = format!("{rename} ({construct_fields})");
499 build_branch(ctx, &pat, &fields, &construct)
500 }
501 })
502 .join("\n")
503 }
504 TypeDeclKind::Union(..) => todo!(),
505 TypeDeclKind::Opaque => todo!(),
506 TypeDeclKind::Error(_) => todo!(),
507 };
508 build_function(ctx, decl, &branches)
509}
510
511fn extract_doc_comments(attr_info: &AttrInfo) -> String {
512 attr_info
513 .attributes
514 .iter()
515 .filter_map(|a| a.as_doc_comment())
516 .join("\n")
517}
518
519fn build_doc_comment(comment: String, indent_level: usize) -> String {
521 #[derive(Default)]
522 struct Exchanger {
523 is_in_open_escaped_block: bool,
524 is_in_open_inline_escape: bool,
525 }
526 impl Exchanger {
527 pub fn exchange_escape_delimiters(&mut self, line: &str) -> String {
528 if line.contains("```") {
529 let (leading, mut rest) = line.split_once("```").unwrap();
531
532 rest = if rest.starts_with("text") {
534 rest.strip_prefix("text").unwrap()
535 } else if rest.starts_with("rust,ignore") {
536 rest.strip_prefix("rust,ignore").unwrap()
537 } else {
538 rest
539 };
540 let mut result = leading.to_owned();
541 if self.is_in_open_escaped_block {
542 result.push_str("]}");
543 self.is_in_open_escaped_block = false;
544 } else {
545 result.push_str("{@rust[");
546 self.is_in_open_escaped_block = true;
547 }
548 result.push_str(rest);
549 result
550 } else if line.contains('`') {
551 let mut parts = line.split('`');
553 let mut result = parts.next().unwrap().to_owned();
555 for part in parts {
556 if self.is_in_open_inline_escape {
557 result.push_str("]");
558 result.push_str(part);
559 self.is_in_open_inline_escape = false;
560 } else {
561 result.push_str("[");
562 result.push_str(part);
563 self.is_in_open_inline_escape = true;
564 }
565 }
566 result
567 } else {
568 line.to_owned()
569 }
570 }
571 }
572
573 if comment == "" {
574 return comment;
575 }
576 let is_multiline = comment.contains("\n");
577 if !is_multiline {
578 let fixed_comment = Exchanger::default().exchange_escape_delimiters(&comment);
579 format!("(**{fixed_comment} *)")
580 } else {
581 let indent = " ".repeat(indent_level);
582 let mut exchanger = Exchanger::default();
583 let comment = comment
584 .lines()
585 .enumerate()
586 .map(|(i, line)| {
587 let line = line.strip_prefix(" ").unwrap_or(line);
590 let fixed_line = exchanger.exchange_escape_delimiters(line);
591
592 if i == 0 || fixed_line.is_empty() {
595 fixed_line
596 } else {
597 format!("{indent} {fixed_line}")
598 }
599 })
600 .join("\n");
601 format!("(** {comment}\n{indent} *)")
602 }
603}
604
605fn build_type(_ctx: &GenerateCtx, decl: &TypeDecl, co_rec: bool, body: &str) -> String {
606 let ty_name = type_name_to_ocaml_ident(&decl.item_meta);
607 let generics = decl
608 .generics
609 .types
610 .iter()
611 .enumerate()
612 .map(|(i, _)| format!("'a{i}"))
613 .collect_vec();
614 let generics = match generics.as_slice() {
615 [] => String::new(),
616 [ty] => ty.clone(),
617 generics => format!("({})", generics.iter().join(",")),
618 };
619 let comment = extract_doc_comments(&decl.item_meta.attr_info);
620 let comment = build_doc_comment(comment, 0);
621 let keyword = if co_rec { "and" } else { "type" };
622 format!("\n{comment} {keyword} {generics} {ty_name} = {body}")
623}
624
625fn type_decl_to_ocaml_decl(ctx: &GenerateCtx, decl: &TypeDecl, co_rec: bool) -> String {
630 let opaque = if ctx.opaque_for_visitor.contains(&decl.def_id) {
631 "[@visitors.opaque]"
632 } else {
633 ""
634 };
635 let body = match &decl.kind {
636 _ if let Some(def) = ctx.manual_type_impls.get(&decl.def_id) => def.clone(),
637 TypeDeclKind::Alias(ty) => {
638 let ty = type_to_ocaml_name(ctx, ty);
639 format!("{ty} {opaque}")
640 }
641 TypeDeclKind::Struct(fields) if fields.is_empty() => "unit".to_string(),
642 TypeDeclKind::Struct(fields)
643 if fields.elem_count() == 1
644 && fields[0].name.as_ref().is_some_and(|name| name == "_raw") =>
645 {
646 let short_name = decl
648 .item_meta
649 .name
650 .name
651 .last()
652 .unwrap()
653 .as_ident()
654 .unwrap()
655 .0
656 .clone();
657 format!("{short_name}.id [@visitors.opaque]")
658 }
659 TypeDeclKind::Struct(fields)
660 if fields.elem_count() == 1
661 && (fields[0].name.is_none()
662 || decl
663 .item_meta
664 .attr_info
665 .attributes
666 .iter()
667 .filter_map(|a| a.as_unknown())
668 .any(|a| a.to_string() == "serde(transparent)")) =>
669 {
670 let ty = type_to_ocaml_name(ctx, &fields[0].ty);
671 format!("{ty} {opaque}")
672 }
673 TypeDeclKind::Struct(fields) if fields.iter().all(|f| f.name.is_none()) => fields
674 .iter()
675 .filter(|f| !f.is_opaque())
676 .map(|f| {
677 let ty = type_to_ocaml_name(ctx, &f.ty);
678 format!("{ty} {opaque}")
679 })
680 .join("*"),
681 TypeDeclKind::Struct(fields) => {
682 let fields = fields
683 .iter()
684 .filter(|f| !f.is_opaque())
685 .map(|f| {
686 let name = f.renamed_name().unwrap();
687 let ty = type_to_ocaml_name(ctx, &f.ty);
688 let comment = extract_doc_comments(&f.attr_info);
689 let comment = build_doc_comment(comment, 2);
690 format!("{name} : {ty} {opaque} {comment}")
691 })
692 .join(";");
693 format!("{{ {fields} }}")
694 }
695 TypeDeclKind::Enum(variants) => {
696 variants
697 .iter()
698 .filter(|v| !v.is_opaque())
699 .map(|variant| {
700 let mut attr_info = variant.attr_info.clone();
701 let rename = variant.renamed_name();
702 let ty = if variant.fields.is_empty() {
703 String::new()
705 } else {
706 if variant.fields.iter().all(|f| f.name.is_some()) {
707 let fields = variant
708 .fields
709 .iter()
710 .map(|f| {
711 let comment = extract_doc_comments(&f.attr_info);
712 let description = if comment.is_empty() {
713 comment
714 } else {
715 format!(": {comment}")
716 };
717 format!("\n - [{}]{description}", f.name.as_ref().unwrap())
718 })
719 .join("");
720 let field_descriptions = format!("\n Fields:{fields}");
721 attr_info
723 .attributes
724 .push(Attribute::DocComment(field_descriptions));
725 }
726 let fields = variant
727 .fields
728 .iter()
729 .map(|f| {
730 let ty = type_to_ocaml_name(ctx, &f.ty);
731 format!("{ty} {opaque}")
732 })
733 .join("*");
734 format!(" of {fields}")
735 };
736 let comment = extract_doc_comments(&attr_info);
737 let comment = build_doc_comment(comment, 3);
738 format!("\n\n | {rename}{ty} {comment}")
739 })
740 .join("")
741 }
742 TypeDeclKind::Union(..) => todo!(),
743 TypeDeclKind::Opaque => todo!(),
744 TypeDeclKind::Error(_) => todo!(),
745 };
746 build_type(ctx, decl, co_rec, &body)
747}
748
749fn generate_visitor_bases(
750 _ctx: &GenerateCtx,
751 name: &str,
752 inherits: &[&str],
753 reduce: bool,
754 ty_names: &[String],
755) -> String {
756 let mut out = String::new();
757 let make_inherit = |variety| {
758 if !inherits.is_empty() {
759 inherits
760 .iter()
761 .map(|ancestor| {
762 if let [module, name] = ancestor.split(".").collect_vec().as_slice() {
763 format!("inherit [_] {module}.{variety}_{name}")
764 } else {
765 format!("inherit [_] {variety}_{ancestor}")
766 }
767 })
768 .join("\n")
769 } else {
770 format!("inherit [_] VisitorsRuntime.{variety}")
771 }
772 };
773
774 let iter_methods = ty_names
775 .iter()
776 .map(|ty| format!("method visit_{ty} : 'env -> {ty} -> unit = fun _ _ -> ()"))
777 .format("\n");
778 let _ = write!(
779 &mut out,
780 "
781 class ['self] iter_{name} =
782 object (self : 'self)
783 {}
784 {iter_methods}
785 end
786 ",
787 make_inherit("iter")
788 );
789
790 let map_methods = ty_names
791 .iter()
792 .map(|ty| format!("method visit_{ty} : 'env -> {ty} -> {ty} = fun _ x -> x"))
793 .format("\n");
794 let _ = write!(
795 &mut out,
796 "
797 class ['self] map_{name} =
798 object (self : 'self)
799 {}
800 {map_methods}
801 end
802 ",
803 make_inherit("map")
804 );
805
806 if reduce {
807 let reduce_methods = ty_names
808 .iter()
809 .map(|ty| format!("method visit_{ty} : 'env -> {ty} -> 'a = fun _ _ -> self#zero"))
810 .format("\n");
811 let _ = write!(
812 &mut out,
813 "
814 class virtual ['self] reduce_{name} =
815 object (self : 'self)
816 {}
817 {reduce_methods}
818 end
819 ",
820 make_inherit("reduce")
821 );
822
823 let mapreduce_methods = ty_names
824 .iter()
825 .map(|ty| {
826 format!("method visit_{ty} : 'env -> {ty} -> {ty} * 'a = fun _ x -> (x, self#zero)")
827 })
828 .format("\n");
829 let _ = write!(
830 &mut out,
831 "
832 class virtual ['self] mapreduce_{name} =
833 object (self : 'self)
834 {}
835 {mapreduce_methods}
836 end
837 ",
838 make_inherit("mapreduce")
839 );
840 }
841
842 out
843}
844
845#[derive(Clone, Copy)]
846struct DeriveVisitors {
847 name: &'static str,
848 ancestors: &'static [&'static str],
849 reduce: bool,
850 extra_types: &'static [&'static str],
851}
852
853#[derive(Clone, Copy)]
855enum GenerationKind {
856 OfJson,
857 TypeDecl(Option<DeriveVisitors>),
858}
859
860struct GenerateCodeFor {
862 template: PathBuf,
863 target: PathBuf,
864 markers: Vec<(GenerationKind, HashSet<TypeDeclId>)>,
870}
871
872impl GenerateCodeFor {
873 fn generate(&self, ctx: &GenerateCtx) -> Result<()> {
874 let mut template = fs::read_to_string(&self.template)
875 .with_context(|| format!("Failed to read template file {}", self.template.display()))?;
876 for (i, (kind, names)) in self.markers.iter().enumerate() {
877 let tys = names.iter().copied().sorted().map(|id| &ctx.crate_data[id]);
878 let generated = match kind {
879 GenerationKind::OfJson => {
880 let fns = tys
881 .map(|ty| type_decl_to_json_deserializer(ctx, ty))
882 .format("\n");
883 format!("let rec ___ = ()\n{fns}")
884 }
885 GenerationKind::TypeDecl(visitors) => {
886 let mut decls = tys
887 .enumerate()
888 .map(|(i, ty)| {
889 let co_recursive = i != 0;
890 type_decl_to_ocaml_decl(ctx, ty, co_recursive)
891 })
892 .join("\n");
893 if let Some(visitors) = visitors {
894 let DeriveVisitors {
895 name,
896 mut ancestors,
897 reduce,
898 extra_types,
899 } = visitors;
900 let varieties: &[_] = if *reduce {
901 &["iter", "map", "reduce", "mapreduce"]
902 } else {
903 &["iter", "map"]
904 };
905 let intermediate_visitor_name;
906 let intermediate_visitor_name_slice;
907 if !extra_types.is_empty() {
908 intermediate_visitor_name = format!("{name}_base");
909 let intermediate_visitor = generate_visitor_bases(
910 ctx,
911 &intermediate_visitor_name,
912 ancestors,
913 *reduce,
914 extra_types
915 .iter()
916 .map(|s| s.to_string())
917 .collect_vec()
918 .as_slice(),
919 );
920 intermediate_visitor_name_slice = [intermediate_visitor_name.as_str()];
921 ancestors = &intermediate_visitor_name_slice;
922 decls = format!("(* Ancestors for the {name} visitors *){intermediate_visitor}\n{decls}");
923 }
924 let visitors = varieties
925 .iter()
926 .map(|variety| {
927 let nude = if !ancestors.is_empty() {
928 format!("nude = true (* Don't inherit VisitorsRuntime *);")
929 } else {
930 String::new()
931 };
932 let ancestors = format!(
933 "ancestors = [ {} ];",
934 ancestors
935 .iter()
936 .map(|a| format!("\"{variety}_{a}\""))
937 .join(";")
938 );
939 format!(
940 r#"
941 visitors {{
942 name = "{variety}_{name}";
943 monomorphic = ["env"];
944 variety = "{variety}";
945 {ancestors}
946 {nude}
947 }}
948 "#
949 )
950 })
951 .format(", ");
952 let _ = write!(&mut decls, "\n[@@deriving show, eq, ord, {visitors}]");
953 };
954 decls
955 }
956 };
957 let placeholder = format!("(* __REPLACE{i}__ *)");
958 template = template.replace(&placeholder, &generated);
959 }
960
961 fs::write(&self.target, template)
962 .with_context(|| format!("Failed to write generated file {}", self.target.display()))?;
963 Ok(())
964 }
965}
966
967fn main() -> Result<()> {
968 let dir = PathBuf::from("src/bin/generate-ml");
969 let charon_llbc = dir.join("charon-itself.ullbc");
970 let reuse_llbc = std::env::var("CHARON_ML_REUSE_LLBC").is_ok(); if !reuse_llbc {
972 let mut cmd = Command::cargo_bin("charon")?;
974 cmd.arg("--cargo-arg=--lib");
975 cmd.arg("--hide-marker-traits");
976 cmd.arg("--ullbc");
977 cmd.arg("--dest-file");
978 cmd.arg(&charon_llbc);
979 let output = cmd.output()?;
980
981 if !output.status.success() {
982 let stderr = String::from_utf8(output.stderr.clone())?;
983 bail!("Compilation failed: {stderr}")
984 }
985 }
986
987 let crate_data: TranslatedCrate = charon_lib::deserialize_llbc(&charon_llbc)?;
988 let output_dir = if std::env::var("IN_CI").as_deref() == Ok("1") {
989 dir.join("generated")
990 } else {
991 dir.join("../../../../charon-ml/src/generated")
992 };
993 generate_ml(crate_data, dir.join("templates"), output_dir)
994}
995
996fn generate_ml(
997 crate_data: TranslatedCrate,
998 template_dir: PathBuf,
999 output_dir: PathBuf,
1000) -> anyhow::Result<()> {
1001 let manual_type_impls = &[
1002 ("FileId", "file"),
1004 (
1007 "ScalarValue",
1008 indoc!(
1009 "
1010 (* Note that we use unbounded integers everywhere.
1011 We then harcode the boundaries for the different types.
1012 *)
1013 { value : big_int; int_ty : integer_type }
1014 "
1015 ),
1016 ),
1017 (
1020 "charon_lib::ast::llbc_ast::RawStatement",
1021 indoc!(
1022 "
1023 | Assign of place * rvalue
1024 | SetDiscriminant of place * variant_id
1025 | CopyNonOverlapping of copy_non_overlapping
1026 (** Equivalent to std::intrinsics::copy_nonoverlapping; this is not modelled as a function
1027 call as it cannot diverge
1028 *)
1029 | StorageLive of local_id
1030 | StorageDead of local_id
1031 | Deinit of place
1032 | Drop of place
1033 | Assert of assertion
1034 | Call of call
1035 | Abort of abort_kind
1036 | Return
1037 | Break of int
1038 (** Break to (outer) loop. The [int] identifies the loop to break to:
1039 * 0: break to the first outer loop (the current loop)
1040 * 1: break to the second outer loop
1041 * ...
1042 *)
1043 | Continue of int
1044 (** Continue to (outer) loop. The loop identifier works
1045 the same way as for {!Break} *)
1046 | Nop
1047 | Sequence of statement * statement
1048 | Switch of switch
1049 | Loop of statement
1050 | Error of string
1051 "
1052 ),
1053 ),
1054 ("charon_lib::ast::llbc_ast::Block", "statement"),
1056 ("RegionVar", "(region_id, string option) indexed_var"),
1059 ("TypeVar", "(type_var_id, string) indexed_var"),
1060 ];
1061 let manual_json_impls = &[
1062 (
1064 "Vector",
1065 indoc!(
1066 r#"
1067 | js ->
1068 let* list = list_of_json (option_of_json arg1_of_json) ctx js in
1069 Ok (List.filter_map (fun x -> x) list)
1070 "#
1071 ),
1072 ),
1073 (
1075 "FileId",
1076 indoc!(
1077 r#"
1078 | json ->
1079 let* file_id = FileId.id_of_json ctx json in
1080 let file = FileId.Map.find file_id ctx in
1081 Ok file
1082 "#,
1083 ),
1084 ),
1085 (
1088 "ScalarValue",
1089 indoc!(
1090 r#"
1091 | `Assoc [ (ty, bi) ] ->
1092 let big_int_of_json (js : json) : (big_int, string) result =
1093 combine_error_msgs js __FUNCTION__
1094 (match js with
1095 | `Int i -> Ok (Z.of_int i)
1096 | `String is -> Ok (Z.of_string is)
1097 | _ -> Error "")
1098 in
1099 let* value = big_int_of_json bi in
1100 let* int_ty = integer_type_of_json ctx (`String ty) in
1101 let sv = { value; int_ty } in
1102 if not (check_scalar_value_in_range sv) then
1103 raise (Failure ("Scalar value not in range: " ^ show_scalar_value sv));
1104 Ok sv
1105 "#
1106 ),
1107 ),
1108 (
1110 "charon_lib::ast::llbc_ast::Block",
1111 indoc!(
1112 r#"
1113 | `Assoc [ ("span", span); ("statements", statements) ] -> begin
1114 let* span = span_of_json ctx span in
1115 let* statements =
1116 list_of_json statement_of_json ctx statements
1117 in
1118 match List.rev statements with
1119 | [] -> Ok { span; content = Nop; comments_before = [] }
1120 | last :: rest ->
1121 let seq =
1122 List.fold_left
1123 (fun acc st -> { span = st.span; content = Sequence (st, acc); comments_before = [] })
1124 last rest
1125 in
1126 Ok seq
1127 end
1128 "#
1129 ),
1130 ),
1131 ];
1132 let dont_generate_ty = &[
1134 "ItemOpacity",
1135 "PredicateOrigin",
1136 "TraitTypeConstraintId",
1137 "Ty",
1138 "Vector",
1139 ];
1140 let opaque_for_visitor = &["Name"];
1142 let ctx = GenerateCtx::new(
1143 &crate_data,
1144 manual_type_impls,
1145 manual_json_impls,
1146 opaque_for_visitor,
1147 );
1148
1149 let manually_implemented: HashSet<_> = [
1151 "ItemOpacity",
1152 "PredicateOrigin",
1153 "Ty", "Opaque",
1155 "Body",
1156 "FunDecl",
1157 "TranslatedCrate",
1158 ]
1159 .iter()
1160 .map(|name| ctx.id_from_name(name))
1161 .collect();
1162
1163 let (gast_types, llbc_types, ullbc_types) = {
1165 let llbc_types: HashSet<_> = ctx.children_of("charon_lib::ast::llbc_ast::Statement");
1166 let ullbc_types: HashSet<_> = ctx.children_of("charon_lib::ast::ullbc_ast::BodyContents");
1167 let all_types: HashSet<_> = ctx.children_of("TranslatedCrate");
1168
1169 let shared_types: HashSet<_> = llbc_types.intersection(&ullbc_types).copied().collect();
1170 let llbc_types: HashSet<_> = llbc_types.difference(&shared_types).copied().collect();
1171 let ullbc_types: HashSet<_> = ullbc_types.difference(&shared_types).copied().collect();
1172
1173 let body_specific_types: HashSet<_> = llbc_types.union(&ullbc_types).copied().collect();
1174 let gast_types: HashSet<_> = all_types
1175 .difference(&body_specific_types)
1176 .copied()
1177 .collect();
1178
1179 let gast_types: HashSet<_> = gast_types
1180 .difference(&manually_implemented)
1181 .copied()
1182 .collect();
1183 let llbc_types: HashSet<_> = llbc_types
1184 .difference(&manually_implemented)
1185 .copied()
1186 .collect();
1187 let ullbc_types: HashSet<_> = ullbc_types
1188 .difference(&manually_implemented)
1189 .copied()
1190 .collect();
1191 (gast_types, llbc_types, ullbc_types)
1192 };
1193
1194 let mut processed_tys: HashSet<TypeDeclId> = dont_generate_ty
1195 .iter()
1196 .map(|name| ctx.id_from_name(name))
1197 .collect();
1198 let mut markers_from_children = |ctx: &GenerateCtx, markers: &[_]| {
1202 markers
1203 .iter()
1204 .copied()
1205 .map(|(kind, type_names)| {
1206 let types: HashSet<_> = ctx.children_of_many(type_names);
1207 let unprocessed_types: HashSet<_> =
1208 types.difference(&processed_tys).copied().collect();
1209 processed_tys.extend(unprocessed_types.iter().copied());
1210 (kind, unprocessed_types)
1211 })
1212 .collect()
1213 };
1214
1215 #[rustfmt::skip]
1216 let generate_code_for = vec![
1217 GenerateCodeFor {
1218 template: template_dir.join("Meta.ml"),
1219 target: output_dir.join("Generated_Meta.ml"),
1220 markers: markers_from_children(&ctx, &[
1221 (GenerationKind::TypeDecl(None), &[
1222 "File",
1223 "Span",
1224 "AttrInfo",
1225 ]),
1226 ]),
1227 },
1228 GenerateCodeFor {
1229 template: template_dir.join("Values.ml"),
1230 target: output_dir.join("Generated_Values.ml"),
1231 markers: markers_from_children(&ctx, &[
1232 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1233 ancestors: &["big_int"],
1234 name: "literal",
1235 reduce: true,
1236 extra_types: &[],
1237 })), &[
1238 "Literal",
1239 "IntegerTy",
1240 "LiteralTy",
1241 ]),
1242 ]),
1243 },
1244 GenerateCodeFor {
1245 template: template_dir.join("Types.ml"),
1246 target: output_dir.join("Generated_Types.ml"),
1247 markers: markers_from_children(&ctx, &[
1248 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1249 ancestors: &["literal"],
1250 name: "const_generic",
1251 reduce: true,
1252 extra_types: &[],
1253 })), &[
1254 "TypeVarId",
1255 "ConstGeneric",
1256 "TraitClauseId",
1257 "DeBruijnVar",
1258 "AnyTransId",
1259 ]),
1260 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1263 ancestors: &["ty_base_base"],
1264 name: "ty",
1265 reduce: false,
1266 extra_types: &[],
1267 })), &[
1268 "TyKind",
1269 "TraitImplRef",
1270 "FunDeclRef",
1271 "GlobalDeclRef",
1272 ]),
1273 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1275 ancestors: &["ty"],
1276 name: "type_decl",
1277 reduce: false,
1278 extra_types: &[
1279 "span", "attr_info"
1280 ],
1281 })), &[
1282 "Binder",
1283 "AbortKind",
1284 "TypeDecl",
1285 ]),
1286 ]),
1287 },
1288 GenerateCodeFor {
1289 template: template_dir.join("Expressions.ml"),
1290 target: output_dir.join("Generated_Expressions.ml"),
1291 markers: markers_from_children(&ctx, &[
1292 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1293 ancestors: &["type_decl"],
1294 name: "rvalue",
1295 reduce: false,
1296 extra_types: &[],
1297 })), &[
1298 "Rvalue",
1299 ]),
1300 ]),
1301 },
1302 GenerateCodeFor {
1303 template: template_dir.join("GAst.ml"),
1304 target: output_dir.join("Generated_GAst.ml"),
1305 markers: markers_from_children(&ctx, &[
1306 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1307 ancestors: &["rvalue"],
1308 name: "fun_sig",
1309 reduce: false,
1310 extra_types: &[],
1311 })), &[
1312 "Call",
1313 "Assert",
1314 "ItemKind",
1315 "Locals",
1316 "FunSig",
1317 "CopyNonOverlapping",
1318 ]),
1319 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1321 ancestors: &["fun_sig"],
1322 name: "global_decl",
1323 reduce: false,
1324 extra_types: &[],
1325 })), &[
1326 "GlobalDecl",
1327 ]),
1328 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1329 ancestors: &["global_decl"],
1330 name: "trait_decl",
1331 reduce: false,
1332 extra_types: &[],
1333 })), &[
1334 "TraitDecl",
1335 ]),
1336 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1337 ancestors: &["trait_decl"],
1338 name: "trait_impl",
1339 reduce: false,
1340 extra_types: &[],
1341 })), &[
1342 "TraitImpl",
1343 ]),
1344 (GenerationKind::TypeDecl(None), &[
1345 "CliOpts",
1346 "GExprBody",
1347 "DeclarationGroup",
1348 ]),
1349 ]),
1350 },
1351 GenerateCodeFor {
1352 template: template_dir.join("LlbcAst.ml"),
1353 target: output_dir.join("Generated_LlbcAst.ml"),
1354 markers: markers_from_children(&ctx, &[
1355 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1356 name: "statement",
1357 ancestors: &["trait_impl"],
1358 reduce: false,
1359 extra_types: &[],
1360 })), &[
1361 "charon_lib::ast::llbc_ast::Statement",
1362 ]),
1363 ]),
1364 },
1365 GenerateCodeFor {
1366 template: template_dir.join("UllbcAst.ml"),
1367 target: output_dir.join("Generated_UllbcAst.ml"),
1368 markers: markers_from_children(&ctx, &[
1369 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1370 ancestors: &["trait_impl"],
1371 name: "statement",
1372 reduce: false,
1373 extra_types: &[],
1374 })), &[
1375 "charon_lib::ast::ullbc_ast::Statement",
1376 "charon_lib::ast::ullbc_ast::SwitchTargets",
1377 ]),
1378 (GenerationKind::TypeDecl(Some(DeriveVisitors {
1380 ancestors: &["statement"],
1381 name: "ullbc_ast",
1382 reduce: false,
1383 extra_types: &[],
1384 })), &[
1385 "charon_lib::ast::ullbc_ast::BodyContents",
1386 ]),
1387 ]),
1388 },
1389 GenerateCodeFor {
1390 template: template_dir.join("GAstOfJson.ml"),
1391 target: output_dir.join("Generated_GAstOfJson.ml"),
1392 markers: vec![(GenerationKind::OfJson, gast_types)],
1393 },
1394 GenerateCodeFor {
1395 template: template_dir.join("LlbcOfJson.ml"),
1396 target: output_dir.join("Generated_LlbcOfJson.ml"),
1397 markers: vec![(GenerationKind::OfJson, llbc_types)],
1398 },
1399 GenerateCodeFor {
1400 template: template_dir.join("UllbcOfJson.ml"),
1401 target: output_dir.join("Generated_UllbcOfJson.ml"),
1402 markers: vec![(GenerationKind::OfJson, ullbc_types)],
1403 },
1404 ];
1405 for file in generate_code_for {
1406 file.generate(&ctx)?;
1407 }
1408 Ok(())
1409}