-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy pathConversions.hs
228 lines (205 loc) · 9.05 KB
/
Conversions.hs
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
224
225
226
227
228
{- |
Module : ./SoftFOL/Conversions.hs
Description : Functions to convert to internal SP* data structures.
Copyright : (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : provisional
Portability : unknown
Functions to convert to internal SP* data structures.
-}
module SoftFOL.Conversions where
import Control.Exception
import Data.Time
import Data.Maybe
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
import Common.AS_Annotation
import Common.Id
import Common.Utils (number)
import SoftFOL.Sign
{- |
Converts a Sign to an initial (no axioms or goals) SPLogicalPart.
-}
signToSPLogicalPart :: Sign -> SPLogicalPart
signToSPLogicalPart s =
assert (checkArities s)
(emptySPLogicalPart {symbolList = sList,
declarationList = Just decList,
formulaLists = if null decList
then []
else [predArgRestrictions]
}
)
where
sList = if Rel.nullKeys (sortRel s) && Map.null (funcMap s) &&
Map.null (predMap s) && Map.null (sortMap s)
then Nothing
else Just emptySymbolList
{ functions =
map (\ (f, ts) ->
SPSignSym {sym = f,
arity = length (fst (head
(Set.toList ts)))})
(Map.toList (funcMap s)),
predicates =
map (\ (p, ts) ->
SPSignSym {sym = p,
arity = length (head
(Set.toList ts))})
(Map.toList (predMap s)),
sorts = map SPSimpleSignSym $ Map.keys $ sortMap s }
decList = if singleSorted s && null (Map.elems $ sortMap s) then []
else subsortDecl ++ termDecl ++ predDecl ++ genDecl
subsortDecl = map (\ (a, b) -> SPSubsortDecl {sortSymA = a, sortSymB = b})
(Rel.toList (Rel.transReduce (sortRel s)))
termDecl = concatMap termDecls (Map.toList (funcMap s))
termDecls (fsym, tset) = map (toFDecl fsym) (Set.toList tset)
toFDecl fsym (args, ret) =
if null args
then SPSimpleTermDecl $ compTerm (spSym ret) [simpTerm $ spSym fsym]
else let
xTerm :: Int -> SPTerm
xTerm i = simpTerm $ mkSPCustomSymbol $ 'X' : show i
in SPTermDecl
{ termDeclTermList =
map (\ (t, i) -> compTerm (spSym t) [xTerm i]) $ number args
, termDeclTerm = compTerm (spSym ret) [compTerm (spSym fsym)
$ map (xTerm . snd) $ number args] }
predArgRestrictions =
SPFormulaList { originType = SPOriginAxioms
, formulae = Map.foldrWithKey toArgRestriction []
$ predMap s
}
toArgRestriction psym tset acc
| Set.null tset = error
"SoftFOL.Conversions.toArgRestriction: empty set"
| Set.size tset == 1 = acc ++
maybe []
((: []) . makeNamed ("arg_restriction_" ++ tokStr psym))
(listToMaybe (toPDecl psym $ head $ Set.toList tset)
>>= predDecl2Term)
| otherwise = acc ++
let argLists = Set.toList tset
in [makeNamed ("arg_restriction_o_" ++ tokStr psym) $
makeTerm psym $
foldl (zipWith (flip (:)))
(map (const []) $ head argLists) argLists]
makeTerm psym tss =
let varList = zipWith const (genVarList psym $ nub $ concat tss) tss
varListTerms = spTerms varList
in if null varList
then error
"SoftFOL.Conversions.makeTerm: no propositional constants"
else SPQuantTerm {
quantSym = SPForall,
variableList = varListTerms,
qFormula = compTerm SPImplies
[ compTerm (spSym psym) varListTerms
, foldl1 mkConj $ zipWith
(\ v -> foldl1 mkDisj . map (typedVarTerm v))
varList tss ]}
predDecl = concatMap predDecls $ Map.toList $ predMap s
predDecls (p, tset) = -- assert (Set.size tset == 1)
concatMap (toPDecl p) (Set.toList tset)
toPDecl p t
| null t = []
| otherwise = [SPPredDecl {predSym = p, sortSyms = t}]
genDecl = Map.foldrWithKey (\ ssym ->
maybe id (\ gen ->
(SPGenDecl {sortSym = ssym,
freelyGenerated = freely gen,
funcList = byFunctions gen} :)))
[] $ sortMap s
{- |
Inserts a Named Sentence (axiom or goal) into an SPLogicalPart.
-}
insertSentence :: SPLogicalPart -> Named Sentence -> SPLogicalPart
insertSentence lp nSen = lp {formulaLists = fLists'}
where
insertFormula oType x [] =
[SPFormulaList {originType = oType, formulae = [x]}]
insertFormula oType x (l : ls) =
if originType l == oType
then l {formulae = case formulae l of
[f] | oType == SPOriginConjectures ->
[reName (const "ga_conjunction_of_theorem")
$ mapNamed (const $ mkConj (sentence f) $ sentence x) f]
fs -> x : fs} : ls
else l : insertFormula oType x ls
fLists' = if isAxiom nSen
then insertFormula SPOriginAxioms nSen fLists
else insertFormula SPOriginConjectures nSen fLists
fLists = formulaLists lp
{- |
Generate a SoftFOL problem with time stamp while maybe adding a goal.
-}
genSoftFOLProblem :: String -> SPLogicalPart
-> Maybe (Named SPTerm) -> IO SPProblem
genSoftFOLProblem thName lp m_nGoal =
do d <- getCurrentTime
return $ problem $ show d
where
problem sd = SPProblem
{identifier = "hets_exported",
description = SPDescription
{name = thName ++ maybe "" (('_' :) . senAttr) m_nGoal,
author = "hets",
SoftFOL.Sign.version = Nothing,
logic = Nothing,
status = SPStateUnknown,
desc = "",
date = Just sd},
logicalPart = maybe lp (insertSentence lp) m_nGoal,
settings = []}
{- |
generates a variable for each for each symbol in the input list
without symbol overlap
-}
genVarList :: SPIdentifier -> [SPIdentifier] -> [SPIdentifier]
genVarList chSym symList =
let reservSym = chSym : symList
varSource = filter (`notElem` reservSym)
$ map (mkSimpleId . showChar 'Y' . show) [(0 :: Int) ..]
in take (length symList) varSource
predDecl2Term :: SPDeclaration -> Maybe SPTerm
predDecl2Term pd = case pd of
SPPredDecl {} -> mkPredTerm
_ -> Nothing
where mkPredTerm = let varList = genVarList (predSym pd)
(sortSyms pd)
varListTerms = spTerms varList
in if null varList
then Nothing
else Just
SPQuantTerm {
quantSym = SPForall,
variableList = varListTerms,
qFormula = SPComplexTerm {
symbol = SPImplies,
arguments = [SPComplexTerm {
symbol = SPCustomSymbol
(predSym pd),
arguments = varListTerms},
foldl1 mkConj $
zipWith typedVarTerm
varList $ sortSyms pd]
}
}
{- |
'checkArities'
checks if the signature has only overloaded symbols with the same arity
-}
checkArities :: Sign -> Bool
checkArities s =
checkPredArities (predMap s) && checkFuncArities (funcMap s)
checkPredArities :: PredMap -> Bool
checkPredArities = Map.foldr checkSet True
where checkSet s bv = bv && not (Set.null s) &&
all (\ x -> length x == length hd) tl
where hd : tl = Set.toList s
checkFuncArities :: FuncMap -> Bool
checkFuncArities = checkPredArities . mapToPredMap
where mapToPredMap = Map.map (Set.map fst)