blob: e2d659ac180e94d3d5fcf58f9d49fb60d3e1377c (
plain)
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
|
module Encoding where
import Base
import Syntax.Internal
import Tptp.UnsortedFirstOrder qualified as Tptp
import Bound
import Bound.Scope
import Data.Text qualified as Text
import Data.Text.IO qualified as TextIO
import TextBuilder
encodeTask :: Task -> Tptp.Task
encodeTask task = Tptp.Task (conjecture' : hypos')
where
conjecture' =
encodeConjecture
(taskConjectureLabel task)
(taskConjecture task)
hypos' = encodeHypos (taskHypotheses task)
encodeTaskText :: Task -> Text
encodeTaskText = Tptp.toText . encodeTask
-- | Boolean contraction of a task.
contractionTask :: Task -> Task
contractionTask task = task
{ taskConjecture = contraction (taskConjecture task)
}
encodeConjecture :: Marker -> Formula -> Tptp.FofFormula
encodeConjecture (Marker str) f =
Tptp.FofFormula
(Tptp.NameAtomicWord (Tptp.AtomicWord str))
Tptp.Conjecture
(encodeExpr f)
-- NOTE: E's SInE will only filter out axioms and leave hypotheses fixed.
encodeHypos :: [Hypothesis] -> [Tptp.FofFormula]
encodeHypos phis = [makeHypo (hypothesisMarker h) (hypothesisFormula h) | h <- phis]
where
makeHypo :: Marker -> Formula -> Tptp.FofFormula
makeHypo (Marker str) formula =
Tptp.FofFormula
(Tptp.NameAtomicWord (Tptp.AtomicWord str))
Tptp.Axiom
(encodeExpr (contraction formula))
encodeWithRole :: Tptp.Role -> [Hypothesis] -> [Tptp.FofFormula]
encodeWithRole role phis = [makeHypo (hypothesisMarker h) (hypothesisFormula h) | h <- phis]
where
makeHypo :: Marker -> Formula -> Tptp.FofFormula
makeHypo (Marker str) formula =
Tptp.FofFormula
(Tptp.NameAtomicWord (Tptp.AtomicWord str))
role
(encodeExpr (contraction formula))
writeTask :: Handle -> Task -> IO ()
writeTask h =
TextIO.hPutStr h . Tptp.toTextNewline . encodeTask
encodeExpr :: Expr -> TextBuilder
encodeExpr = buildExpr . fmap encodeFreeVar
where
buildExpr :: ExprOf EncodedVar -> TextBuilder
buildExpr = \case
Equals _pos e1 e2 ->
buildExpr e1 <> char '=' <> buildExpr e2
NotEquals _pos e1 e2 ->
buildExpr e1 <> text "!=" <> buildExpr e2
Atomic _pos p es ->
let p' = encodePredicate p
es' = buildExpr <$> toList es
in buildApply p' es'
PropositionalConstant IsBottom ->
text "$false"
PropositionalConstant IsTop ->
text "$true"
Not _pos f ->
char '~' <> buildUnitary f
Connected Conjunction f1 f2 ->
buildAnd f1 <> char '&' <> buildAnd f2
Connected Disjunction f1 f2 ->
buildOr f1 <> char '|' <> buildOr f2
Connected Implication f1 f2 ->
buildUnitary f1 <> text "=>" <> buildUnitary f2
Connected Equivalence f1 f2 ->
buildUnitary f1 <> text "<=>" <> buildUnitary f2
Connected NegatedDisjunction f1 f2 ->
char '~' <> buildUnitary (Connected Disjunction f1 f2)
Connected ExclusiveOr f1 f2 ->
char '~' <> buildUnitary (Connected Equivalence f1 f2)
Quantified quant scope ->
buildQuantified buildExpr buildUnitary quant scope
TermVar v ->
buildTermVar v
Apply e es -> case e of
TermVar (FreeConst x) -> buildApply x (buildExpr <$> toList es)
_ -> error ("encodeExpr: complex term as head of applicaition: " <> show e)
TermSymbol _pos symb es ->
buildApply (encodeSymbol symb) (buildExpr <$> es)
e@ReplaceFun{} ->
error ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " <> show e)
e@ReplacePred{} ->
error ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " <> show e)
e@TermSep{} ->
error ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " <> show e)
TermSymbolStruct symb e -> case e of
Just e' ->
buildApply (Tptp.AtomicWord ("s__" <> (unStructSymbol symb))) [buildExpr e']
Nothing ->
error ("encodeExpr.go (precondition failed): unannotated struct symbol" <> show symb)
_ -> error "encodeExpr.go: missing case"
buildTermVar :: EncodedVar -> TextBuilder
buildTermVar = \case
BoundVar v -> Tptp.buildVariable v
FreeConst w -> Tptp.buildAtomicWord w
buildApply :: Tptp.AtomicWord -> [TextBuilder] -> TextBuilder
buildApply f args = case args of
[] -> Tptp.buildAtomicWord f
_ -> Tptp.buildAtomicWord f <> Tptp.buildTuple args
isAtom :: ExprOf EncodedVar -> Bool
isAtom = \case
TermVar{} -> True
TermSymbol{} -> True
TermSymbolStruct{} -> True
Apply{} -> True
PropositionalConstant{} -> True
Equals{} -> True
NotEquals{} -> True
_ -> False
buildQuantified
:: (ExprOf EncodedVar -> TextBuilder)
-> (ExprOf EncodedVar -> TextBuilder)
-> Quantifier
-> Scope VarSymbol ExprOf EncodedVar
-> TextBuilder
buildQuantified renderEmpty renderBody quant scope =
let phi = instantiate instantiator scope
xs = [encodeBoundVar x | x <- nubOrd (bindings scope)]
in case xs of
[] -> renderEmpty phi
_ -> buildQuantifier quant <> Tptp.buildList (map Tptp.buildVariable xs) <> char ':' <> renderBody phi
buildQuantifier :: Quantifier -> TextBuilder
buildQuantifier = \case
Universally -> text "!"
Existentially -> text "?"
buildUnitary :: ExprOf EncodedVar -> TextBuilder
buildUnitary = \case
atom | isAtom atom -> buildExpr atom
Quantified quant scope -> buildQuantified buildUnitary buildUnitary quant scope
Not _ phi -> char '~' <> buildUnitary phi
phi -> char '(' <> buildExpr phi <> char ')'
buildAnd :: ExprOf EncodedVar -> TextBuilder
buildAnd = \case
Connected Conjunction f1 f2 -> buildAnd f1 <> char '&' <> buildAnd f2
f -> buildUnitary f
buildOr :: ExprOf EncodedVar -> TextBuilder
buildOr = \case
Connected Disjunction f1 f2 -> buildOr f1 <> char '|' <> buildUnitary f2
f -> buildUnitary f
instantiator :: VarSymbol -> ExprOf EncodedVar
instantiator bv = TermVar (BoundVar (encodeBoundVar bv))
encodeSymbol :: Symbol -> Tptp.AtomicWord
encodeSymbol = \case
SymbolMixfix op ->
unMarker (mixfixMarker op)
SymbolFun fun ->
unMarker (lexicalItemSgPlMarker fun)
SymbolInteger n ->
unMarker (Marker (Text.pack (show n)))
SymbolPredicate _ ->
error "IMPOSSIBLE: predicates should already be translated"
encodePredicate :: Predicate -> Tptp.AtomicWord
encodePredicate =
unMarker . predicateObjectMarker
unMarker :: Marker -> Tptp.AtomicWord
unMarker (Marker m) = Tptp.AtomicWord m
data EncodedVar
= BoundVar Tptp.Variable
| FreeConst Tptp.AtomicWord
deriving (Show, Eq, Ord)
encodeFreeVar :: VarSymbol -> EncodedVar
encodeFreeVar fv = FreeConst fv'
where
fv' = Tptp.AtomicWord case fv of
NamedVar x -> Text.cons 'f' x
FreshVar n -> Text.cons 'y' (Text.pack (show n))
-- | Tptp variables must be "upper words", starting with an uppercase letter
-- and continuing with alphanumeric characters. We prefix all variables
-- with "X" to make them easy to decode.
encodeBoundVar :: VarSymbol -> Tptp.Variable
encodeBoundVar bv = Tptp.Variable $ Text.cons 'X' case bv of
NamedVar x -> x
FreshVar n -> Text.pack (show n)
|
