chore(coq/assertions): Simplification

rr_frontend/radium/src/coq.rs

@@ -728,14 +728,14 @@ impl Display for Definition {
 }
 
 #[derive(Clone, Eq, PartialEq, Debug, Display)]
-pub enum TopLevelAssertion {
+pub enum TopLevelAssertion<'a> {
     /// A declaration of a Coq Inductive
     #[display("{}", _0)]
-    InductiveDecl(Inductive),
+    InductiveDecl(&'a Inductive),
 
     /// A declaration of a Coq instance
     #[display("{}", _0)]
-    InstanceDecl(InstanceDecl),
+    InstanceDecl(&'a InstanceDecl),
 
     /// A declaration of a Coq record
     #[display("{}", _0)]
@@ -751,11 +751,11 @@ pub enum TopLevelAssertion {
 
     /// A Coq comment
     #[display("(* {} *)", _0)]
-    Comment(String),
+    Comment(&'a str),
 
     /// A Coq section
     #[display("Section {}.\n{}End{}.", _0, Indented::new(_1), _0)]
-    Section(String, TopLevelAssertions),
+    Section(String, TopLevelAssertions<'a>),
 
     /// A Coq section start
     #[display("Section {}.", _0)]
@@ -784,15 +784,15 @@ impl<T: Display> Display for Indented<T> {
 
 #[derive(Clone, Eq, PartialEq, Debug, Display)]
 #[display("{}", display_list!(_0, "\n"))]
-pub struct TopLevelAssertions(pub Vec<TopLevelAssertion>);
+pub struct TopLevelAssertions<'a>(pub Vec<TopLevelAssertion<'a>>);
 
-impl TopLevelAssertions {
+impl<'a> TopLevelAssertions<'a> {
     #[must_use]
     pub(crate) const fn empty() -> Self {
         Self(vec![])
     }
 
-    pub(crate) fn push(&mut self, a: TopLevelAssertion) {
+    pub(crate) fn push(&mut self, a: TopLevelAssertion<'a>) {
         self.0.push(a);
     }
 }

rr_frontend/radium/src/specs.rs

@@ -2075,26 +2075,32 @@ impl<'def> AbstractEnum<'def> {
 
         // write the Coq inductive, if applicable
         if let Some(ind) = &self.optional_inductive_def {
-            let mut assertions = coq::TopLevelAssertions::empty();
-
-            assertions.push(coq::TopLevelAssertion::Comment(format!(
-                "auto-generated representation of {}",
-                ind.get_name()
-            )));
-            // TODO don't clone
-            assertions.push(coq::TopLevelAssertion::InductiveDecl(ind.clone()));
-            // prove that it is inhabited
-            let instance_decl = coq::InstanceDecl::new(
-                coq::Type::Literal(format!("Inhabited {}", ind.get_name())),
-                coq::DefBody::Script(
-                    coq::ProofScript(vec![coq::ProofItem::Literal("solve_inhabited".to_owned())]),
-                    coq::ProofScriptTerminator::Qed,
-                ),
-            );
-            assertions.push(coq::TopLevelAssertion::InstanceDecl(instance_decl));
+            let mut out = IndentWriter::new(BASE_INDENT, &mut out);
+            writeln!(out).unwrap();
+
+            let name = ind.get_name();
+            writeln!(
+                out,
+                "{}",
+                coq::TopLevelAssertion::Comment(&format!("auto-generated representation of {}", name))
+            )
+            .unwrap();
 
-            let mut code_fmt = IndentWriter::new(BASE_INDENT, &mut out);
-            write!(code_fmt, "\n{assertions}\n").unwrap();
+            writeln!(out, "{}", coq::TopLevelAssertion::InductiveDecl(ind)).unwrap();
+
+            // prove that it is inhabited
+            writeln!(
+                out,
+                "{}",
+                coq::TopLevelAssertion::InstanceDecl(&coq::InstanceDecl::new(
+                    coq::Type::Literal(format!("Inhabited {}", name)),
+                    coq::DefBody::Script(
+                        coq::ProofScript(vec![coq::ProofItem::Literal("solve_inhabited".to_owned())]),
+                        coq::ProofScriptTerminator::Qed,
+                    ),
+                ))
+            )
+            .unwrap();
         }
 
         // build the els term applied to generics
@@ -3467,7 +3473,7 @@ fn make_trait_instance<'def>(
     is_base_spec: bool,
     spec_record_name: &str,
     spec_record_params_name: &str,
-) -> Result<coq::TopLevelAssertions, fmt::Error> {
+) -> Result<coq::TopLevelAssertions<'def>, fmt::Error> {
     let mut assertions = Vec::new();
 
     // write the param record decl