1use crate::{
8 desugar_hoas, is_num, key_of, parse_inductive_form, parse_lino, parse_one, tokenize_one, Node,
9};
10use std::collections::HashMap;
11use std::error::Error;
12use std::fmt;
13use std::panic::{catch_unwind, AssertUnwindSafe};
14
15#[derive(Debug, Clone, PartialEq, Eq)]
16pub struct RocqExportError {
17 message: String,
18}
19
20impl RocqExportError {
21 fn new(message: impl Into<String>) -> Self {
22 Self {
23 message: message.into(),
24 }
25 }
26}
27
28impl fmt::Display for RocqExportError {
29 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
30 write!(f, "{}", self.message)
31 }
32}
33
34impl Error for RocqExportError {}
35
36#[derive(Debug, Clone)]
37struct Binding {
38 name: String,
39 typ: Node,
40}
41
42struct RocqEmitter {
43 names: HashMap<String, String>,
44 used: HashMap<String, String>,
45}
46
47pub fn export_rocq(text: &str, source_path: Option<&str>) -> Result<String, RocqExportError> {
48 let mut emitter = RocqEmitter::new();
49 let mut lines = vec!["(* Generated by rml export rocq. *)".to_string()];
50 if let Some(path) = source_path {
51 lines.push(format!("(* Source: {} *)", sanitize_comment(path)));
52 }
53 lines.push(String::new());
54 lines.push("Set Universe Polymorphism.".to_string());
55 lines.push(String::new());
56
57 for link in parse_lino(text) {
58 let tokens = tokenize_one(&link);
59 let node = parse_one(&tokens)
60 .map(desugar_hoas)
61 .map_err(|e| RocqExportError::new(format!("failed to parse `{}`: {}", link, e)))?;
62 if let Some(statement) = emitter.translate_form(&node)? {
63 lines.push(statement);
64 }
65 }
66 lines.push(String::new());
67 Ok(lines.join("\n"))
68}
69
70impl RocqEmitter {
71 fn new() -> Self {
72 Self {
73 names: HashMap::new(),
74 used: HashMap::new(),
75 }
76 }
77
78 fn err<T>(&self, message: impl Into<String>) -> Result<T, RocqExportError> {
79 Err(RocqExportError::new(message))
80 }
81
82 fn symbol(&mut self, raw: &str) -> Result<String, RocqExportError> {
83 if raw == "_" {
84 return Ok("_".to_string());
85 }
86 if let Some(rendered) = self.names.get(raw) {
87 return Ok(rendered.clone());
88 }
89 let rendered = sanitize_identifier(raw);
90 if let Some(previous) = self.used.get(&rendered) {
91 if previous != raw {
92 return self.err(format!(
93 "Rocq identifier collision: `{}` and `{}` both export as `{}`",
94 previous, raw, rendered
95 ));
96 }
97 }
98 self.names.insert(raw.to_string(), rendered.clone());
99 self.used.insert(rendered.clone(), raw.to_string());
100 Ok(rendered)
101 }
102
103 fn translate_type(&mut self, node: &Node) -> Result<String, RocqExportError> {
104 match node {
105 Node::Leaf(s) => {
106 if s == "Type" {
107 return Ok("Type".to_string());
108 }
109 if s == "Prop" {
110 return Ok("Prop".to_string());
111 }
112 if is_num(s) {
113 return self.err(format!("numeric literal `{}` is not a Rocq type", s));
114 }
115 self.symbol(s)
116 }
117 Node::List(children) => {
118 if let Some(level) = type_universe_level(node) {
119 return Ok(if level == "0" { "Set" } else { "Type" }.to_string());
120 }
121 if children.len() == 1 && leaf_eq(&children[0], "Prop") {
122 return Ok("Prop".to_string());
123 }
124 if children.len() == 3
125 && (leaf_eq(&children[0], "Pi") || leaf_eq(&children[0], "forall"))
126 {
127 return self.translate_pi(node);
128 }
129 if children.len() == 3 && leaf_eq(&children[1], "=") {
130 return Ok(format!(
131 "{} = {}",
132 self.translate_term(&children[0])?,
133 self.translate_term(&children[2])?
134 ));
135 }
136 self.translate_term(node)
137 }
138 }
139 }
140
141 fn translate_pi(&mut self, node: &Node) -> Result<String, RocqExportError> {
142 let mut current = node;
143 let mut binders: Vec<Binding> = Vec::new();
144 loop {
145 let Node::List(children) = current else {
146 break;
147 };
148 if children.len() != 3
149 || !(leaf_eq(&children[0], "Pi") || leaf_eq(&children[0], "forall"))
150 {
151 break;
152 }
153 let binding = parse_binding_node(&children[1]).ok_or_else(|| {
154 RocqExportError::new(format!("unsupported Pi binder `{}`", key_of(&children[1])))
155 })?;
156 binders.push(binding);
157 current = &children[2];
158 }
159
160 let mut rendered = self.translate_type(current)?;
161 for binding in binders.iter().rev() {
162 rendered = format!(
163 "forall {} : {}, {}",
164 self.symbol(&binding.name)?,
165 self.translate_type(&binding.typ)?,
166 rendered
167 );
168 }
169 Ok(rendered)
170 }
171
172 fn translate_lambda(&mut self, node: &Node) -> Result<String, RocqExportError> {
173 let Node::List(children) = node else {
174 return self.err(format!("unsupported lambda expression `{}`", key_of(node)));
175 };
176 if children.len() != 3 || !leaf_eq(&children[0], "lambda") {
177 return self.err(format!("unsupported lambda expression `{}`", key_of(node)));
178 }
179 let bindings = parse_binding_nodes(&children[1]).ok_or_else(|| {
180 RocqExportError::new(format!(
181 "unsupported lambda binder `{}`",
182 key_of(&children[1])
183 ))
184 })?;
185 if bindings.is_empty() {
186 return self.err(format!(
187 "unsupported lambda binder `{}`",
188 key_of(&children[1])
189 ));
190 }
191
192 let mut rendered = self.translate_term(&children[2])?;
193 for binding in bindings.iter().rev() {
194 rendered = format!(
195 "fun {} : {} => {}",
196 self.symbol(&binding.name)?,
197 self.translate_type(&binding.typ)?,
198 rendered
199 );
200 }
201 Ok(rendered)
202 }
203
204 fn translate_term(&mut self, node: &Node) -> Result<String, RocqExportError> {
205 match node {
206 Node::Leaf(s) => {
207 if is_num(s) {
208 return self.err(format!(
209 "numeric literal `{}` is outside the Rocq export subset",
210 s
211 ));
212 }
213 self.symbol(s)
214 }
215 Node::List(children) => {
216 if children.is_empty() {
217 return self.err(format!(
218 "unsupported Rocq term expression `{}`",
219 key_of(node)
220 ));
221 }
222 if type_universe_level(node).is_some() {
223 return self.translate_type(node);
224 }
225 if children.len() == 1 && leaf_eq(&children[0], "Prop") {
226 return Ok("Prop".to_string());
227 }
228 if children.len() == 3 && leaf_eq(&children[0], "lambda") {
229 return self.translate_lambda(node);
230 }
231 if children.len() == 3
232 && (leaf_eq(&children[0], "Pi") || leaf_eq(&children[0], "forall"))
233 {
234 return self.translate_pi(node);
235 }
236 if children.len() == 3 && leaf_eq(&children[1], "=") {
237 return Ok(format!(
238 "({} = {})",
239 self.translate_term(&children[0])?,
240 self.translate_term(&children[2])?
241 ));
242 }
243 if children.len() == 3 && leaf_eq(&children[1], "of") {
244 return Ok(format!(
245 "({} : {})",
246 self.translate_term(&children[0])?,
247 self.translate_type(&children[2])?
248 ));
249 }
250 if leaf_eq(&children[0], "apply") {
251 if children.len() != 3 {
252 return self.err(format!(
253 "Rocq export supports binary `apply` forms, got `{}`",
254 key_of(node)
255 ));
256 }
257 return Ok(format!(
258 "({} {})",
259 self.translate_term(&children[1])?,
260 self.translate_term(&children[2])?
261 ));
262 }
263 let Some(head) = leaf(&children[0]) else {
264 return self.err(format!(
265 "unsupported Rocq term expression `{}`",
266 key_of(node)
267 ));
268 };
269 if unsupported_form_head(head) {
270 return self.err(format!("`{}` is outside the Rocq export subset", head));
271 }
272 if matches!(
273 head,
274 "+" | "-" | "*" | "/" | "and" | "or" | "not" | "both" | "neither"
275 ) {
276 return self.err(format!(
277 "operator `{}` is outside the Rocq export subset",
278 head
279 ));
280 }
281 let mut parts = vec![self.symbol(head)?];
282 for arg in &children[1..] {
283 parts.push(self.translate_term(arg)?);
284 }
285 Ok(format!("({})", parts.join(" ")))
286 }
287 }
288 }
289
290 fn translate_query(&mut self, node: &Node) -> Result<String, RocqExportError> {
291 let Node::List(children) = node else {
292 return self.err(format!("unsupported query form `{}`", key_of(node)));
293 };
294 if children.len() == 4 {
295 return self.err("proof-producing queries are outside the Rocq export subset");
296 }
297 if children.len() != 2 || !leaf_eq(&children[0], "?") {
298 return self.err(format!("unsupported query form `{}`", key_of(node)));
299 }
300 let expr = &children[1];
301 if let Node::List(items) = expr {
302 if items.len() == 3 && leaf_eq(&items[0], "type") && leaf_eq(&items[1], "of") {
303 return Ok(format!("Check {}.", self.translate_term(&items[2])?));
304 }
305 if items.len() == 3 && leaf_eq(&items[1], "of") {
306 return Ok(format!(
307 "Check ({} : {}).",
308 self.translate_term(&items[0])?,
309 self.translate_type(&items[2])?
310 ));
311 }
312 }
313 Ok(format!("Check {}.", self.translate_term(expr)?))
314 }
315
316 fn translate_definition(
317 &mut self,
318 node: &Node,
319 children: &[Node],
320 ) -> Result<String, RocqExportError> {
321 let Some(head_with_colon) = leaf(&children[0]) else {
322 return self.err(format!(
323 "definition `{}` is outside the Rocq export subset",
324 key_of(node)
325 ));
326 };
327 let head = head_with_colon.trim_end_matches(':');
328 let rhs = &children[1..];
329 if head == "Type" {
330 return self.err("self-referential `(Type: Type Type)` is not in the Rocq export subset; use `(Type N)` universes");
331 }
332 if config_head(head) || operator_head(head) || head.contains('=') || head.contains('!') {
333 return self.err(format!(
334 "definition `{}:` is an operator or configuration form, not a typed Rocq declaration",
335 head
336 ));
337 }
338 if rhs.len() == 1 {
339 if let Some(value) = leaf(&rhs[0]) {
340 if is_num(value) {
341 return self.err(format!(
342 "numeric prior `({}: {})` is outside the Rocq export subset",
343 head, value
344 ));
345 }
346 }
347 }
348 if rhs.len() == 3 && leaf_eq(&rhs[1], "is") {
349 return self.err(format!(
350 "untyped term declaration `({}: ... is ...)` is outside the Rocq export subset",
351 head
352 ));
353 }
354 if !rhs.is_empty() && leaf_eq(&rhs[0], "lambda") {
355 let mut lambda_items = vec![Node::Leaf("lambda".to_string())];
356 lambda_items.extend_from_slice(&rhs[1..]);
357 let lambda = Node::List(lambda_items);
358 return Ok(format!(
359 "Definition {} := {}.",
360 self.symbol(head)?,
361 self.translate_lambda(&lambda)?
362 ));
363 }
364 if rhs.len() == 2 {
365 if let Some(value) = leaf(&rhs[1]) {
366 if value == head {
367 return Ok(format!(
368 "Parameter {} : {}.",
369 self.symbol(head)?,
370 self.translate_type(&rhs[0])?
371 ));
372 }
373 }
374 }
375 if rhs.len() == 1 && matches!(rhs[0], Node::List(_)) {
376 return Ok(format!(
377 "Parameter {} : {}.",
378 self.symbol(head)?,
379 self.translate_type(&rhs[0])?
380 ));
381 }
382 self.err(format!(
383 "definition `{}` is outside the Rocq export subset",
384 key_of(node)
385 ))
386 }
387
388 fn translate_inductive(&mut self, node: &Node) -> Result<String, RocqExportError> {
389 let decl = catch_unwind(AssertUnwindSafe(|| parse_inductive_form(node)))
390 .map_err(|payload| RocqExportError::new(panic_payload_message(payload)))?
391 .ok_or_else(|| {
392 RocqExportError::new(format!(
393 "unsupported inductive declaration `{}`",
394 key_of(node)
395 ))
396 })?;
397 let mut lines = vec![format!("Inductive {} : Set :=", self.symbol(&decl.name)?)];
398 for (i, ctor) in decl.constructors.iter().enumerate() {
399 let suffix = if i + 1 == decl.constructors.len() {
400 "."
401 } else {
402 ""
403 };
404 lines.push(format!(
405 "| {} : {}{}",
406 self.symbol(&ctor.name)?,
407 self.translate_type(&ctor.typ)?,
408 suffix
409 ));
410 }
411 Ok(lines.join("\n"))
412 }
413
414 fn translate_form(&mut self, node: &Node) -> Result<Option<String>, RocqExportError> {
415 let Node::List(children) = node else {
416 return self.err(format!("unsupported top-level form `{}`", key_of(node)));
417 };
418 if children.is_empty() {
419 return self.err(format!("unsupported top-level form `{}`", key_of(node)));
420 }
421 if leaf(&children[0]).is_some_and(|s| s.ends_with(':')) {
422 return self.translate_definition(node, children).map(Some);
423 }
424 if type_universe_level(node).is_some()
425 || (children.len() == 1 && leaf_eq(&children[0], "Prop"))
426 {
427 return Ok(None);
428 }
429 if children.len() == 4
430 && leaf_eq(&children[1], "has")
431 && leaf_eq(&children[2], "probability")
432 {
433 return self.err("probabilistic assignment is outside the Rocq export subset");
434 }
435 if leaf_eq(&children[0], "inductive") {
436 return self.translate_inductive(node).map(Some);
437 }
438 if leaf_eq(&children[0], "?") {
439 return self.translate_query(node).map(Some);
440 }
441 if let Some(head) = leaf(&children[0]) {
442 if unsupported_form_head(head) {
443 return self.err(format!("`{}` is outside the Rocq export subset", head));
444 }
445 }
446 self.err(format!(
447 "top-level form `{}` is outside the Rocq export subset",
448 key_of(node)
449 ))
450 }
451}
452
453fn leaf(node: &Node) -> Option<&str> {
454 match node {
455 Node::Leaf(s) => Some(s.as_str()),
456 Node::List(_) => None,
457 }
458}
459
460fn leaf_eq(node: &Node, expected: &str) -> bool {
461 leaf(node) == Some(expected)
462}
463
464fn parse_binding_node(binding: &Node) -> Option<Binding> {
465 let Node::List(children) = binding else {
466 return None;
467 };
468 if children.len() != 2 {
469 return None;
470 }
471 if let Some(name) = leaf(&children[0]).and_then(|s| s.strip_suffix(':')) {
472 return Some(Binding {
473 name: name.to_string(),
474 typ: children[1].clone(),
475 });
476 }
477 if let (Some(type_name), Some(var_name)) = (leaf(&children[0]), leaf(&children[1])) {
478 if type_name
479 .chars()
480 .next()
481 .is_some_and(|c| c.is_ascii_uppercase())
482 && !var_name.ends_with(':')
483 {
484 return Some(Binding {
485 name: var_name.to_string(),
486 typ: Node::Leaf(type_name.to_string()),
487 });
488 }
489 }
490 if matches!(children[0], Node::List(_)) {
491 if let Some(var_name) = leaf(&children[1]) {
492 if !var_name.ends_with(':') {
493 return Some(Binding {
494 name: var_name.to_string(),
495 typ: children[0].clone(),
496 });
497 }
498 }
499 }
500 None
501}
502
503fn parse_binding_nodes(binding: &Node) -> Option<Vec<Binding>> {
504 if let Some(single) = parse_binding_node(binding) {
505 return Some(vec![single]);
506 }
507 let Node::List(children) = binding else {
508 return None;
509 };
510 let mut tokens = Vec::new();
511 for child in children {
512 let token = leaf(child)?;
513 if let Some(stripped) = token.strip_suffix(',') {
514 tokens.push(stripped.to_string());
515 tokens.push(",".to_string());
516 } else {
517 tokens.push(token.to_string());
518 }
519 }
520 let mut bindings = Vec::new();
521 let mut i = 0;
522 while i < tokens.len() {
523 if tokens[i] == "," {
524 i += 1;
525 continue;
526 }
527 if i + 1 < tokens.len() && tokens[i + 1] != "," {
528 let pair = Node::List(vec![
529 Node::Leaf(tokens[i].clone()),
530 Node::Leaf(tokens[i + 1].clone()),
531 ]);
532 if let Some(binding) = parse_binding_node(&pair) {
533 bindings.push(binding);
534 i += 2;
535 continue;
536 }
537 }
538 return None;
539 }
540 if bindings.is_empty() {
541 None
542 } else {
543 Some(bindings)
544 }
545}
546
547fn type_universe_level(node: &Node) -> Option<&str> {
548 let Node::List(children) = node else {
549 return None;
550 };
551 if children.len() != 2 || !leaf_eq(&children[0], "Type") {
552 return None;
553 }
554 let level = leaf(&children[1])?;
555 if level.is_empty() || !level.chars().all(|c| c.is_ascii_digit()) {
556 return None;
557 }
558 if level.len() > 1 && level.starts_with('0') {
559 return None;
560 }
561 Some(level)
562}
563
564fn sanitize_comment(text: &str) -> String {
565 text.replace("*)", "* )")
566}
567
568fn sanitize_identifier(raw: &str) -> String {
569 let mut out = String::new();
570 let mut previous_underscore = false;
571 for ch in raw.chars() {
572 if ch.is_ascii_alphanumeric() || ch == '_' {
573 out.push(ch);
574 previous_underscore = false;
575 } else if !previous_underscore {
576 out.push('_');
577 previous_underscore = true;
578 }
579 }
580 if out.is_empty()
581 || !out
582 .chars()
583 .next()
584 .is_some_and(|c| c.is_ascii_alphabetic() || c == '_')
585 {
586 out = format!("rml_{}", out);
587 }
588 if rocq_reserved(&out) {
589 out.push_str("_rml");
590 }
591 out
592}
593
594fn rocq_reserved(value: &str) -> bool {
595 matches!(
596 value,
597 "as" | "at"
598 | "by"
599 | "Check"
600 | "Definition"
601 | "else"
602 | "end"
603 | "fix"
604 | "forall"
605 | "fun"
606 | "if"
607 | "in"
608 | "Inductive"
609 | "let"
610 | "match"
611 | "Parameter"
612 | "Prop"
613 | "return"
614 | "Set"
615 | "struct"
616 | "then"
617 | "Type"
618 | "where"
619 | "with"
620 )
621}
622
623fn config_head(head: &str) -> bool {
624 matches!(head, "range" | "valence")
625}
626
627fn operator_head(head: &str) -> bool {
628 matches!(
629 head,
630 "=" | "!=" | "and" | "or" | "not" | "is" | "?:" | "both" | "neither"
631 )
632}
633
634fn unsupported_form_head(head: &str) -> bool {
635 matches!(
636 head,
637 "coinductive"
638 | "coverage"
639 | "define"
640 | "import"
641 | "mode"
642 | "namespace"
643 | "relation"
644 | "terminating"
645 | "total"
646 | "world"
647 )
648}
649
650fn panic_payload_message(payload: Box<dyn std::any::Any + Send>) -> String {
651 if let Some(message) = payload.downcast_ref::<&str>() {
652 return (*message).to_string();
653 }
654 if let Some(message) = payload.downcast_ref::<String>() {
655 return message.clone();
656 }
657 "invalid inductive declaration".to_string()
658}