fix(corpus): the octad test's SCHEME path broke cargo check on main

src/rust/corpus/canonical.rs

@@ -882,11 +882,23 @@ impl Parser {
 
     /// Application, including prefix operator use: `(+ x y)`.
     fn app(&mut self) -> Node {
+        // A bracketed group is already complete: `(eq a b)` must not be
+        // re-read as the prefix form `eq a b`, or the group's own arguments
+        // are swallowed by the enclosing application and the term collapses
+        // to a bare operator name.
+        let from_group = matches!(self.peek(), Some(Tk::Open(_)));
         let head = match self.atom() {
             Some(h) => h,
             None => return Node::Hole,
         };
-        if let Node::Op(op, _) = head.clone() {
+        if let Node::Op(op, args) = head.clone() {
+            if from_group {
+                return if args.is_empty() {
+                    Node::Name(op.to_string())
+                } else {
+                    head
+                };
+            }
             let mut args: Vec<Node> = Vec::new();
             loop {
                 let stop = match self.peek() {
@@ -940,14 +952,9 @@ impl Parser {
 
     fn expr(&mut self, min_prec: u8) -> Node {
         let mut left = self.app();
-        loop {
-            let op = match self.op_at() {
-                Some(op) => op,
-                None => break,
-            };
-            let prec = match precedence(op) {
-                Some(p) => p,
-                None => break,
+        while let Some(op) = self.op_at() {
+            let Some(prec) = precedence(op) else {
+                break;
             };
             if prec < min_prec {
                 break;

src/rust/corpus/creusot.rs

@@ -478,22 +478,23 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile {
     let clean = clean_source(src);
     let toks = tokenise(&clean);
     let attrs = collect_attrs(src, &toks);
-    let mut parsed = ParsedFile::default();
-
-    parsed.imports = collect_uses(src, &toks);
+    let mut parsed = ParsedFile {
+        imports: collect_uses(src, &toks),
+        ..Default::default()
+    };
 
     let mut k = 0;
     while k < toks.len() {
         let t = &toks[k];
+        let next_is_fn = k + 1 < toks.len() && is_kw(&toks[k + 1], "fn");
+        let is_const_item = is_kw(t, "const") && !next_is_fn;
         let (kind, name_idx) = if is_kw(t, "fn") {
             (DeclKind::Function, k + 1)
         } else if is_kw(t, "struct") || is_kw(t, "enum") || is_kw(t, "union") {
             (DeclKind::Data, k + 1)
         } else if is_kw(t, "trait") {
             (DeclKind::Record, k + 1)
-        } else if is_kw(t, "type") || is_kw(t, "static") {
-            (DeclKind::Data, k + 1)
-        } else if is_kw(t, "const") && !(k + 1 < toks.len() && is_kw(&toks[k + 1], "fn")) {
+        } else if is_kw(t, "type") || is_kw(t, "static") || is_const_item {
             (DeclKind::Data, k + 1)
         } else {
             k += 1;
@@ -565,10 +566,10 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile {
             axiom_usage,
         });
 
-        if has_attr(&leading, "cfg(creusot)") {
-            if !parsed.options.iter().any(|o| o == "creusot-gated") {
-                parsed.options.push("creusot-gated".to_string());
-            }
+        if has_attr(&leading, "cfg(creusot)")
+            && !parsed.options.iter().any(|o| o == "creusot-gated")
+        {
+            parsed.options.push("creusot-gated".to_string());
         }
 
         k = advance.max(k + 1);

src/rust/corpus/octad.rs

@@ -755,7 +755,7 @@ mod tests {
             coq.graph.cross_prover_identity_key,
             smtlib.graph.cross_prover_identity_key
         );
-        assert_eq!(coq.graph.identity_scheme, super::canonical::SCHEME);
+        assert_eq!(coq.graph.identity_scheme, crate::corpus::canonical::SCHEME);
         assert_eq!(
             coq.graph.canonical_type,
             "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))"

src/rust/corpus/spark_ada.rs

@@ -725,10 +725,7 @@ fn collect_imports(toks: &[Tok]) -> Vec<String> {
         let mut names: Vec<String> = Vec::new();
         let mut j = i + 1;
         let mut terminated = false;
-        loop {
-            let Some((name, next)) = dotted_name(&toks, j) else {
-                break;
-            };
+        while let Some((name, next)) = dotted_name(toks, j) {
             names.push(name);
             if next < toks.len() && is_punct(&toks[next], ",") {
                 j = next + 1;
@@ -804,10 +801,11 @@ fn body_end_idx(toks: &[Tok], from: usize, name: &str) -> Option<usize> {
 fn find_end_name(toks: &[Tok], from: usize, name: &str) -> Option<usize> {
     let mut j = from;
     while j + 1 < toks.len() {
-        if is_kw(&toks[j], "end") && toks[j + 1].kind == TokKind::Ident {
-            if toks[j + 1].text.eq_ignore_ascii_case(name) {
-                return Some(j);
-            }
+        if is_kw(&toks[j], "end")
+            && toks[j + 1].kind == TokKind::Ident
+            && toks[j + 1].text.eq_ignore_ascii_case(name)
+        {
+            return Some(j);
         }
         j += 1;
     }

src/rust/main.rs

@@ -279,10 +279,9 @@ enum CorpusOp {
     },
 
     /// Look up entries across every synonym table by `semantic_class`.
-    /// Demonstrates cross-prover semantic equivalence — e.g.
-    /// `corpus crossquery well-foundedness` reports `WellFounded` in Agda
-    /// + `well_founded` in Coq + `WellFounded` in Lean + `WellFounded` in
-    /// Idris 2.
+    /// Demonstrates cross-prover semantic equivalence: `corpus crossquery
+    /// well-foundedness` reports `WellFounded` in Agda, `well_founded` in
+    /// Coq, and `WellFounded` in Lean and Idris 2.
     ///
     /// The cross-prover dictionaries are searched too, so classes that
     /// only exist there (`wrapping-arithmetic`, `frame-rule`,