1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
{-# LANGUAGE NoImplicitPrelude #-}
-- | Checked lexical building blocks shared by the TPTP renderers.
module Tptp.UnsortedFirstOrder
( AtomicWord
, atomicWord
, atomicWordText
, isAsciiLetter
, isAsciiAlphaNumOrUnderscore
, isProperAtomicWord
, Variable
, variable
, variableText
, isProperVariable
, buildTuple
, buildAtomicWord
, buildVariable
) where
import Base
import Data.Char
import Data.Text qualified as Text
import TextBuilder
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 ASCII letter.
newtype AtomicWord = AtomicWord Text deriving (Show, Eq, Ord)
atomicWord :: Text -> Maybe AtomicWord
atomicWord word
| isProperAtomicWord word =
Just (AtomicWord word)
| otherwise =
Nothing
atomicWordText :: AtomicWord -> Text
atomicWordText (AtomicWord word) = word
isProperAtomicWord :: Text -> Bool
isProperAtomicWord w = case Text.uncons w of
Nothing -> False
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)
variable :: Text -> Maybe Variable
variable name
| isProperVariable name =
Just (Variable name)
| otherwise =
Nothing
variableText :: Variable -> Text
variableText (Variable name) = name
isProperVariable :: Text -> Bool
isProperVariable name = case Text.uncons name of
Nothing -> False
Just (head, tail) ->
isAsciiUpper head && Text.all isAsciiAlphaNumOrUnderscore tail
buildTuple :: [TextBuilder] -> TextBuilder
buildTuple bs = char '(' <> intercalate (char ',') bs <> char ')'
buildAtomicWord :: AtomicWord -> TextBuilder
buildAtomicWord = text . atomicWordText
buildVariable :: Variable -> TextBuilder
buildVariable = text . variableText
|
