TPTP Parser Bug Fix

leanprover-community · Feb 3, 2024 · b535939 · b535939
1 parent 9310520
commit b535939
Showing 1 changed file with 18 additions and 6 deletions.
diff --git 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