fix(provers): migrate parsers to the nom 8 API

Dependabot #204 bumped nom 7.1.3 -> 8.0.0 (a breaking major) without
migrating the parser code, leaving cargo build red on main with 16
E0618/E0282 errors. nom 8 returns Parser structs from alt/opt/many0/
separated_list0 (you call .parse(input), not the value as a function) and
removed the tuple combinator (plain tuples now implement Parser).

Migrate provers/{agda,idris2,lean}.rs: import nom::Parser, route the 16
combinator call-sites through .parse(input), and replace tuple((a,b,c))
with (a,b,c).

Verified: cargo build debug+release clean; cargo test --lib = 1174 passed,
0 failed (601 provers tests incl. the three migrated parsers).

https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv

Author: claude

src/rust/provers/agda.rs

@@ -15,7 +15,7 @@ use nom::{
     bytes::complete::{tag, take_until, take_while},
     character::complete::{alpha1, multispace0, multispace1, space0, space1},
     multi::many0,
-    IResult,
+    IResult, Parser,
 };
 use std::collections::HashMap;
 use std::path::PathBuf;
@@ -496,7 +496,7 @@ fn ws(input: &str) -> IResult<&str, ()> {
 }
 
 fn identifier(input: &str) -> IResult<&str, String> {
-    let (input, first) = alt((alpha1, tag("_")))(input)?;
+    let (input, first) = alt((alpha1, tag("_"))).parse(input)?;
     let (input, rest) =
         take_while(|c: char| c.is_alphanumeric() || c == '_' || c == '-' || c == '\'')(input)?;
     Ok((input, format!("{}{}", first, rest)))
@@ -544,7 +544,7 @@ fn parse_postulate(input: &str) -> IResult<&str, AgdaDecl> {
 }
 
 fn parse_import(input: &str) -> IResult<&str, AgdaDecl> {
-    let (input, _) = alt((tag("import"), tag("open import")))(input)?;
+    let (input, _) = alt((tag("import"), tag("open import"))).parse(input)?;
     let (input, _) = space1(input)?;
     let (input, module) = take_until("\n")(input)?;
     Ok((
@@ -562,11 +562,12 @@ fn parse_decl(input: &str) -> IResult<&str, AgdaDecl> {
         parse_postulate,
         parse_import,
         parse_type_sig,
-    ))(input)
+    ))
+    .parse(input)
 }
 
 fn parse_module(input: &str) -> IResult<&str, Vec<AgdaDecl>> {
-    many0(parse_decl)(input)
+    many0(parse_decl).parse(input)
 }
 
 #[cfg(test)]

src/rust/provers/idris2.rs

@@ -18,7 +18,7 @@ use nom::{
     combinator::opt,
     multi::{many0, separated_list0},
     sequence::preceded,
-    IResult,
+    IResult, Parser,
 };
 use std::collections::HashMap;
 use std::path::PathBuf;
@@ -1012,14 +1012,14 @@ fn block_comment(input: &str) -> IResult<&str, ()> {
 }
 
 fn identifier(input: &str) -> IResult<&str, String> {
-    let (input, first) = alt((alpha1, tag("_")))(input)?;
+    let (input, first) = alt((alpha1, tag("_"))).parse(input)?;
     let (input, rest) =
         take_while(|c: char| c.is_alphanumeric() || c == '_' || c == '\'' || c == '?')(input)?;
     Ok((input, format!("{}{}", first, rest)))
 }
 
 fn qualified_name(input: &str) -> IResult<&str, String> {
-    let (input, parts) = separated_list0(tag("."), identifier)(input)?;
+    let (input, parts) = separated_list0(tag("."), identifier).parse(input)?;
     Ok((input, parts.join(".")))
 }
 
@@ -1033,7 +1033,7 @@ fn parse_module_decl(input: &str) -> IResult<&str, Idris2Decl> {
 
 fn parse_import(input: &str) -> IResult<&str, Idris2Decl> {
     let (input, _) = ws(input)?;
-    let (input, public) = opt(preceded(tag("public"), space1))(input)?;
+    let (input, public) = opt(preceded(tag("public"), space1)).parse(input)?;
     let (input, _) = tag("import")(input)?;
     let (input, _) = space1(input)?;
     let (input, module) = qualified_name(input)?;
@@ -1081,7 +1081,7 @@ fn parse_data(input: &str) -> IResult<&str, Idris2Decl> {
 
     // Parse type parameters (simplified)
     let (input, _) = take_while(|c| c != '=' && c != '\n')(input)?;
-    let (input, _) = opt(tag("="))(input)?;
+    let (input, _) = opt(tag("=")).parse(input)?;
 
     // Parse constructors (simplified - just capture until next declaration)
     let (input, _) = take_while(|c| c != '\n')(input)?;
@@ -1162,11 +1162,12 @@ fn parse_decl(input: &str) -> IResult<&str, Idris2Decl> {
         parse_interface,
         parse_implementation,
         parse_type_sig,
-    ))(input)
+    ))
+    .parse(input)
 }
 
 fn parse_module(input: &str) -> IResult<&str, Vec<Idris2Decl>> {
-    many0(parse_decl)(input)
+    many0(parse_decl).parse(input)
 }
 
 // ============================================================================

src/rust/provers/lean.rs

@@ -21,8 +21,8 @@ use nom::{
     bytes::complete::{tag, take_while},
     character::complete::{alpha1, multispace0, space1},
     combinator::opt,
-    sequence::{preceded, terminated, tuple},
-    IResult,
+    sequence::{preceded, terminated},
+    IResult, Parser,
 };
 use std::collections::HashMap;
 use std::path::PathBuf;
@@ -829,7 +829,7 @@ fn skip_whitespace_and_comments(input: &str) -> &str {
 /// Parse an identifier
 fn parse_identifier(input: &str) -> IResult<&str, String> {
     let (input, _) = multispace0(input)?;
-    let (input, first) = alt((alpha1, tag("_")))(input)?;
+    let (input, first) = alt((alpha1, tag("_"))).parse(input)?;
     let (input, rest) = take_while(|c: char| c.is_alphanumeric() || c == '_' || c == '\'')(input)?;
     Ok((input, format!("{}{}", first, rest)))
 }
@@ -877,7 +877,8 @@ fn parse_declaration(input: &str) -> IResult<&str, LeanDeclaration> {
         parse_inductive_decl,
         parse_structure_decl,
         parse_instance_decl,
-    ))(input)
+    ))
+    .parse(input)
 }
 
 /// Parse a theorem declaration
@@ -897,9 +898,10 @@ fn parse_theorem_decl(input: &str) -> IResult<&str, LeanDeclaration> {
 
     // Parse optional proof
     let (input, value) = opt(preceded(
-        tuple((multispace0, tag(":="), multispace0)),
+        (multispace0, tag(":="), multispace0),
         parse_proof_body,
-    ))(input)?;
+    ))
+    .parse(input)?;
 
     Ok((
         input,
@@ -1026,7 +1028,7 @@ fn parse_instance_decl(input: &str) -> IResult<&str, LeanDeclaration> {
     let (input, _) = multispace0(input)?;
 
     // Optional name
-    let (input, name) = opt(terminated(parse_identifier, multispace0))(input)?;
+    let (input, name) = opt(terminated(parse_identifier, multispace0)).parse(input)?;
 
     let (input, _) = tag(":")(input)?;
     let (input, ty) = parse_type_expr(input)?;