Add quantified calcs and relax tokenization

Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.

1 files changed, 8 insertions, 5 deletions

diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 53e1e6a..2dad049 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -321,14 +321,17 @@ var = guardM isMathMode *> lexeme (fmap Variable var')
     where
     var' = do
         alphabeticPart <- letter <|> bb <|> greek
-        variationPart  <- subscriptNumber <|> ticked <|> pure ""
+        variationPart  <- subscript <|> ticked <|> pure ""
         pure (alphabeticPart <> variationPart)
 
-    subscriptNumber :: Lexer Text
-    subscriptNumber = do
+    subscript :: Lexer Text
+    subscript = do
         Char.char '_'
-        n <- some Char.digitChar
-        pure (Text.pack n)
+        unbraced <|> braced <|> text
+        where
+            unbraced = Text.singleton <$> Char.alphaNumChar
+            braced = Text.pack <$> (Char.char '{' *> many Char.alphaNumChar <* Char.char '}')
+            text = Char.string "\\text" *> braced -- for rendering the subscript in roman type
 
     -- Temporary hack to fit the TPTP format.
     ticked :: Lexer Text