Merge pull request #431 from formal-land/gy@DecoupleImplItemToDoc

Decoupled `ImplItemKind.class_instance_to_doc()`
formal-land · Dec 22, 2023 · 1e58da4 · 1e58da4
2 parents f17a049 + 8490e0f
commit 1e58da4
Show file tree

Hide file tree

Showing 3 changed files with 69 additions and 79 deletions.
diff --git a/CoqOfRust/make_and_detect_warnings.py b/CoqOfRust/make_and_detect_warnings.py
@@ -1,5 +1,6 @@
 from subprocess import Popen, PIPE
 import threading
+import sys
 
 global lines
 lines = []
@@ -66,7 +67,7 @@ def check_warnings():
         print("Checking warnings...")
         for line in errorlines:
             if line.startswith("Warning: "):
-                print("Warnings detected from coqc. Abort.")
+                print("Warnings detected from coqc. Abort.", file=sys.err)
                 exit(1)
         print("Check complete, no warnings detected")
 

diff --git a/lib/src/coq.rs b/lib/src/coq.rs
@@ -690,16 +690,19 @@ impl<'a> Instance<'a> {
         concat([
             nest([
                 nest([
-                    text("Global Instance"),
-                    line(),
+                    text("Global Instance "),
                     text(self.name.to_owned()),
-                    optional_insert(
-                        self.parameters.is_empty(),
-                        concat([
-                            line(),
-                            intersperse(self.parameters.iter().map(|p| p.to_doc()), [line()]),
-                        ]),
-                    ),
+                    optional_insert(self.parameters.is_empty(), {
+                        let non_empty_params: Vec<_> =
+                            self.parameters.iter().filter(|p| !p.is_empty()).collect();
+                        optional_insert(
+                            non_empty_params.is_empty(),
+                            concat([
+                                line(),
+                                intersperse(non_empty_params.iter().map(|p| p.to_doc()), [line()]),
+                            ]),
+                        )
+                    }),
                 ]),
                 text(" :"),
                 line(),
@@ -1020,6 +1023,15 @@ impl<'a> Field<'a> {
 }
 
 impl<'a> ArgDecl<'a> {
+    pub(crate) fn is_empty(&self) -> bool {
+        match self.decl.to_owned() {
+            ArgDeclVar::Simple { idents, .. } => idents.is_empty(),
+            ArgDeclVar::Generalized { .. } => false, // ty would always be exist
+            ArgDeclVar::Traits { traits } => traits.is_empty(),
+            ArgDeclVar::Destructured { .. } => false,
+        }
+    }
+
     /// produces a new coq argument
     pub(crate) fn new(decl: &ArgDeclVar<'a>, kind: ArgSpecKind) -> Self {
         ArgDecl {

diff --git a/lib/src/top_level.rs b/lib/src/top_level.rs
@@ -1539,77 +1539,54 @@ impl FunDefinition {
 }
 
 impl ImplItemKind {
-    fn class_instance_to_doc<'a>(
+    fn class_instance_to_coq<'a>(
         instance_prefix: &'a str,
         name: &'a str,
         ty_params: Option<&'a [String]>,
         where_predicates: Option<&'a [Rc<WherePredicate>]>,
         class_name: &'a str,
         method_name: &'a str,
-    ) -> Doc<'a> {
-        group([
-            nest([
-                nest([
-                    text("Global Instance "),
-                    text(format!("{instance_prefix}_{name}")),
-                    // Type parameters a, b, c... compiles to {a b c ... : Set}
-                    match ty_params {
-                        None | Some([]) => nil(),
-                        Some(ty_params) => concat([
-                            line(),
-                            coq::ArgDecl::of_ty_params(ty_params, coq::ArgSpecKind::Implicit)
-                                .to_doc(),
-                        ]),
-                    },
-                    // where predicates types
-                    match where_predicates {
-                        None | Some([]) => nil(),
-                        Some(where_predicates) => concat([
-                            line(),
-                            WherePredicate::vec_to_coq(where_predicates).to_doc(),
-                        ]),
-                    },
-                    text(" :"),
-                ]),
-                line(),
-                nest([
-                    text(class_name),
-                    line(),
-                    text(format!("\"{name}\"")),
-                    text(" := {"),
-                ]),
-            ]),
-            nest([
-                hardline(),
-                nest([
-                    text(method_name),
-                    line(),
-                    text(":="),
-                    line(),
-                    {
-                        let body = coq::Expression::just_name(name);
-                        match ty_params {
-                            None => body,
-                            Some(ty_params) => body.apply_many_args(
-                                &ty_params
-                                    .iter()
-                                    .map(|ty_param| {
-                                        (
-                                            Some(ty_param.to_owned()),
-                                            coq::Expression::just_name(ty_param),
-                                        )
-                                    })
-                                    .collect::<Vec<_>>(),
-                            ),
-                        }
-                        .to_doc(false)
-                    },
-                    text(";"),
-                ]),
-            ]),
-            hardline(),
-            text("}."),
-        ])
+    ) -> coq::TopLevelItem<'a> {
+        // Type parameters a, b, c... compiles to {a b c ... : Set}
+        let ty_params_arg = coq::ArgDecl::of_ty_params(
+            match ty_params {
+                None | Some([]) => &[],
+                Some(ty_params) => ty_params,
+            },
+            coq::ArgSpecKind::Implicit,
+        );
+        // where predicates types
+        let where_predicates = match where_predicates {
+            None | Some([]) => WherePredicate::vec_to_coq(&[]),
+            Some(where_predicates) => WherePredicate::vec_to_coq(where_predicates),
+        };
+
+        let body = coq::Expression::just_name(name);
+        let entry = match ty_params {
+            None => body,
+            Some(ty_params) => body.apply_many_args(
+                &ty_params
+                    .iter()
+                    .map(|ty_param| {
+                        (
+                            Some(ty_param.to_owned()),
+                            coq::Expression::just_name(ty_param),
+                        )
+                    })
+                    .collect::<Vec<_>>(),
+            ),
+        };
+
+        coq::TopLevelItem::Instance(coq::Instance::new(
+            &format!("{instance_prefix}_{name}"),
+            &[ty_params_arg, where_predicates],
+            coq::Expression::just_name(class_name)
+                .apply(&coq::Expression::just_name(format!("\"{name}\"").as_str())),
+            &coq::Expression::Record {
+                fields: vec![coq::Field::new(&Path::new(&[method_name]), &[], &entry)],
+            },
+            vec![],
+        ))
     }
 
     fn to_coq<'a>(&'a self, name: &'a str) -> coq::TopLevel<'a> {
@@ -1645,26 +1622,26 @@ impl ImplItemKind {
                     )),
                 },
                 coq::TopLevelItem::Line,
-                coq::TopLevelItem::Code(Self::class_instance_to_doc(
+                Self::class_instance_to_coq(
                     "AssociatedFunction",
                     name,
                     None,
                     None,
                     "Notations.DoubleColon Self",
                     "Notations.double_colon",
-                )),
+                ),
             ])]),
             ImplItemKind::Definition { definition, .. } => coq::TopLevel::new(&[
                 coq::TopLevelItem::Code(definition.to_doc(name, None)),
                 coq::TopLevelItem::Line,
-                coq::TopLevelItem::Code(Self::class_instance_to_doc(
+                Self::class_instance_to_coq(
                     "AssociatedFunction",
                     name,
                     Some(&definition.ty_params),
                     Some(&definition.where_predicates),
                     "Notations.DoubleColon Self",
                     "Notations.double_colon",
-                )),
+                ),
             ]),
             ImplItemKind::Type { ty } => {
                 coq::TopLevel::new(&[coq::TopLevelItem::Definition(coq::Definition::new(