Relax label syntax

3 files changed, 15 insertions, 10 deletions

diff --git a/source/Base.hs b/source/Base.hs
index e7b827f..a407831 100644
--- a/source/Base.hs
+++ b/source/Base.hs
@@ -28,15 +28,16 @@ import Data.Foldable as Export
 import Data.Function as Export (on)
 import Data.Functor as Export (void)
 import Data.Hashable as Export (Hashable(..))
+import Data.HashMap.Strict as Export (HashMap)
+import Data.HashSet as Export (HashSet)
 import Data.IntMap.Strict as Export (IntMap)
 import Data.List.NonEmpty as Export (NonEmpty(..))
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map as Export (Map)
 import Data.Maybe as Export hiding (mapMaybe, catMaybes)  -- Replaced by generalized form from "Data.Filtrable".
+import Data.Monoid (First(..))
 import Data.Sequence as Export (Seq(..), replicateA)
 import Data.Set as Export (Set)
-import Data.HashSet as Export (HashSet)
-import Data.HashMap.Strict as Export (HashMap)
 import Data.String as Export (IsString(..))
 import Data.Text as Export (Text)
 import Data.Traversable as Export
@@ -46,7 +47,6 @@ import Debug.Trace as Export
 import GHC.Generics as Export (Generic(..), Generic1(..))
 import Prettyprinter as Export (pretty)
 import UnliftIO as Export (throwIO)
-import Data.Monoid (First(..))
 
 -- | Signal to the developer that a branch is unreachable or represent
 -- an impossible state. Using @impossible@ instead of @error@ allows
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 2dad049..8149dee 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -27,13 +27,13 @@ import Base hiding (many)
 
 import Control.Monad.Combinators
 import Control.Monad.State.Strict
-import Data.Char (isAsciiLower, isDigit)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as Text
 import Prettyprinter (Pretty(..))
 import Text.Megaparsec hiding (Token, Label, label)
 import Text.Megaparsec.Char qualified as Char
 import Text.Megaparsec.Char.Lexer qualified as Lexer
+import Tptp.UnsortedFirstOrder (isAsciiLetter, isAsciiAlphaNumOrUnderscore)
 
 
 runLexer :: String -> Text -> Either (ParseErrorBundle Text Void) [Located Token]
@@ -418,8 +418,8 @@ ref = lexeme do
 
 marker :: Lexer Text
 marker = do
-    c <- satisfy isAsciiLower
-    cs <- takeWhileP Nothing (\x -> isAsciiLower x || isDigit x || x == '_')
+    c <- satisfy isAsciiLetter
+    cs <- takeWhileP Nothing isAsciiAlphaNumOrUnderscore
     pure (Text.cons c cs)
 
 -- | Parses the end of an environment.
diff --git a/source/Tptp/UnsortedFirstOrder.hs b/source/Tptp/UnsortedFirstOrder.hs
index 277ffc9..4fcf052 100644
--- a/source/Tptp/UnsortedFirstOrder.hs
+++ b/source/Tptp/UnsortedFirstOrder.hs
@@ -16,8 +16,13 @@ import Prettyprinter.Render.Text
 import Text.Builder
 
 
-isAsciiAlphaNum :: Char -> Bool
-isAsciiAlphaNum c = isAsciiLower c || isAsciiUpper c || isDigit c || c == '_'
+
+isAsciiLetter :: Char -> Bool
+isAsciiLetter c = isAsciiLower c || isAsciiUpper c
+
+isAsciiAlphaNumOrUnderscore :: Char -> Bool
+isAsciiAlphaNumOrUnderscore c = isAsciiLower c || isAsciiUpper c || isDigit c || c == '_'
+
 
 -- | A TPTP atomic word, starting with a lowercase letter or enclosed in single quotes.
 newtype AtomicWord = AtomicWord Text deriving (Show, Eq, Ord, IsString)
@@ -25,7 +30,7 @@ newtype AtomicWord = AtomicWord Text deriving (Show, Eq, Ord, IsString)
 isProperAtomicWord :: Text -> Bool
 isProperAtomicWord w = case Text.uncons w of
     Nothing -> False
-    Just (head, tail) -> isAsciiLower head && Text.all isAsciiAlphaNum tail
+    Just (head, tail) -> isAsciiLower head && Text.all isAsciiAlphaNumOrUnderscore tail
 
 -- | A TPTP variable, written as a word starting with an uppercase letter.
 newtype Variable = Variable Text deriving (Show, Eq, Ord, IsString)
@@ -33,7 +38,7 @@ newtype Variable = Variable Text deriving (Show, Eq, Ord, IsString)
 isVariable :: Text -> Bool
 isVariable var = case Text.uncons var of
     Nothing -> False -- Variables must be nonempty.
-    Just (head, tail) -> isAsciiUpper head && Text.all isAsciiAlphaNum tail
+    Just (head, tail) -> isAsciiUpper head && Text.all isAsciiAlphaNumOrUnderscore tail
 
 
 data Expr