From b53593923a1423ae145c47c66306a68b6d0fbf44 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Fri, 2 Feb 2024 22:41:28 -0500
Subject: [PATCH] TPTP Parser Bug Fix

---
 Auto/Parser/TPTP.lean | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/Auto/Parser/TPTP.lean b/Auto/Parser/TPTP.lean
index 891364e..a8a12ea 100644
--- a/Auto/Parser/TPTP.lean
+++ b/Auto/Parser/TPTP.lean
@@ -274,13 +274,25 @@ partial def addOpAndRhs (lhs : Term) (minbp : Nat) : ParserM Term := do
       return ← addOpAndRhs (Term.mk op [lhs, rhs]) minbp
 
 partial def parseTypeDecl : ParserM Term := do
-  let ident ← parseIdent
-  if (← peek?) == some (.op ":") then
-    parseToken (.op ":")
-    let ty ← parseTerm
-    return Term.mk (.ident ident) [ty]
+  if (← peek?) == some (.op "(") then
+    parseToken (.op "(")
+    let ident ← parseIdent
+    if (← peek?) == some (.op ":") then
+      parseToken (.op ":")
+      let ty ← parseTerm
+      parseToken (.op ")")
+      return Term.mk (.ident ident) [ty]
+    else
+      parseToken (.op ")")
+      return Term.mk (.ident ident) []
   else
-    return Term.mk (.ident ident) []
+    let ident ← parseIdent
+    if (← peek?) == some (.op ":") then
+      parseToken (.op ":")
+      let ty ← parseTerm
+      return Term.mk (.ident ident) [ty]
+    else
+      return Term.mk (.ident ident) []
 end
 
 structure Command where