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
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuModule : $Header$
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuDescription : prenex normal form for sentences of a CASL theory
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuCopyright : (c) Mihai Codescu, 2016
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuLicense : GPLv2 or higher, see LICENSE.txt
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuMaintainer : codescu@iws.cs.uni-magdeburg.de
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuStability : provisional
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuPortability : non-portable (imports Logic.Comorphism)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuimport CASL.Sublogic as SL hiding (bottom)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuimport qualified Data.Set as Set
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescudata CASL2Prenex = CASL2Prenex deriving Show
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuinstance Language CASL2Prenex where
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu language_name CASL2Prenex = "CASL2Prenex"
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescuinstance Comorphism CASL2Prenex
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASL CASL_Sublogics
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Symbol RawSymbol ProofTree
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASL CASL_Sublogics
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu Symbol RawSymbol ProofTree where
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu sourceLogic CASL2Prenex = CASL
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sourceSublogic CASL2Prenex = SL.caslTop
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu targetLogic CASL2Prenex = CASL
645f50eda40bb36ae1260f56910cdd32a4597578mcodescu mapSublogic CASL2Prenex sl =
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_theory CASL2Prenex = mapTheory
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu map_morphism CASL2Prenex = return
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu map_sentence CASL2Prenex sig = return . (mapSentence sig)
2954f6dd519742dd6d6dd8de6f3e5902ed6c07abmcodescu map_symbol CASL2Prenex _ = Set.singleton . id
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu has_model_expansion CASL2Prenex = True
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu is_weakly_amalgamable CASL2Prenex = True
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- remove equivalences
e8001d65a73bf355ac769f1a3c959bd949be5763mcodescupreprocessSen :: CASLFORMULA -> CASLFORMULA
e8001d65a73bf355ac769f1a3c959bd949be5763mcodescupreprocessSen sen = case sen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls sen' r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls (preprocessSen sen') r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j sens r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j (map preprocessSen sens) r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 Equivalence sen2 _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen1' = Relation sen1 Implication sen2 nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen2' = Relation sen2 Implication sen1 nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in Junction Con [sen1', sen2'] nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 rel sen2 r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation (preprocessSen sen1) rel
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (preprocessSen sen2) r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation sen' r ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation (preprocessSen sen') r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- make variables distinct:
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- if a variable v of sort s already appears in a formula
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu-- substitute it with a fresh variable
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVars :: CASLFORMULA -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVars sen =
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu let (_, _, sen') = mkDistVarsAux 0 [] sen
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVarsAux :: Int -- first available suffix for vars
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -> [(VAR, SORT)] -- vars encountered so far
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -> (Int, [(VAR, SORT)], CASLFORMULA)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumkDistVarsAux n vlist sen = case sen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls form range -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -- first make variables distinct for form
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu dvars = flatVAR_DECLs vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n', _, form') = mkDistVarsAux n (dvars ++ vlist) form
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -- here we are not interested in the variables generated for the quantified form, so we can forget them
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu replVarDecl vds oN nN s = reverse $
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu foldl (\usedD vd@(Var_decl names sort r) ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu if sort == s then -- found it, replace oN with nN in names
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu let vd' = Var_decl (map (\x -> if x == oN then nN else x) names) sort r
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in vd':usedD
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu else vd:usedD
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu checkAndReplace (n0, knownV, quantF, quants) (x, s) =
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu if (x,s) `elem` knownV
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu x' = genNumVar "x" n0
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu quants' = replVarDecl quants x x' s
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu quantF' = substitute x s (Qual_var x' s nullRange) quantF
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n0 + 1, (x', s):knownV, quantF', quants')
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu else (n0 , (x , s):knownV, quantF , quants )
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n'', vlist', form'', vdecls') = foldl checkAndReplace (n', vlist, form', vdecls) dvars
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n'', vlist', Quantification q vdecls' form'' range)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j sens r -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n', vlist', sens') = foldl (\(x, vs, osens) s ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (x', vs', s') = mkDistVarsAux x vs s
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (x', vs', s':osens)) (n, vlist, []) sens
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n', vlist', Junction j (reverse sens') r)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 rel sen2 r -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n1, vlist1, sen1') = mkDistVarsAux n vlist sen1
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n2, vlist2, sen2') = mkDistVarsAux n1 vlist1 sen2
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n2, vlist2, Relation sen1' rel sen2' r)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation sen' r -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (n', vlist', sen'') = mkDistVarsAux n vlist sen'
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in (n', vlist', Negation sen'' r)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> (n, vlist, sen)
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescucomputePNF :: CASLFORMULA -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescucomputePNF sen = case sen of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Negation nsen _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu nsen' = computePNF nsen
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in case nsen' of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification (dualQuant q) vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (computePNF $ Negation qsen nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> Negation nsen' nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 Implication sen2 _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen1' = computePNF sen1
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sen2' = computePNF sen2
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu in case sen1' of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification (dualQuant q) vdecls (computePNF $ Relation qsen Implication sen2 nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> case sen2' of
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu (computePNF $ Relation sen1' Implication qsen nullRange) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu -- recursive call to catch multiple quantifiers for sen2'
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu _ -> -- no quantifications
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1' Implication sen2' nullRange
414029fc573cb2506241ed5a17643f9f721502b8Eugen Kuksa -- During parsing, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Relation sen1 RevImpl sen2 _ ->
414029fc573cb2506241ed5a17643f9f721502b8Eugen Kuksa computePNF $ Relation sen1 Implication sen2 nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls qsen _ ->
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Quantification q vdecls (computePNF qsen) nullRange
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu Junction j sens _ -> let
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sens' = map computePNF sens
eb1cc766464057293793108d07dd50b9b9d82d9bmcodescu collectQuants s = case s of
eb1cc766464057293793108d07dd50b9b9d82d9bmcodescu Quantification q vd qs _ -> let (vs, qs') = collectQuants qs in ((q,vd):vs, qs')
eb1cc766464057293793108d07dd50b9b9d82d9bmcodescu _ -> ([], s)
645f50eda40bb36ae1260f56910cdd32a4597578mcodescu (vdecls, sens'') = foldl (\(vs, ss) s -> case s of
eb1cc766464057293793108d07dd50b9b9d82d9bmcodescu Quantification q vd qs _ -> let (vs', qs') = collectQuants qs
eb1cc766464057293793108d07dd50b9b9d82d9bmcodescu in (vs' ++ (q,vd):vs, qs':ss)
645f50eda40bb36ae1260f56910cdd32a4597578mcodescu _ -> (vs, s:ss))
645f50eda40bb36ae1260f56910cdd32a4597578mcodescu ([], []) sens'
645f50eda40bb36ae1260f56910cdd32a4597578mcodescu qsen = Junction j (reverse sens'') nullRange
645f50eda40bb36ae1260f56910cdd32a4597578mcodescu rsen = foldl (\s (q, vd) -> Quantification q vd s nullRange) qsen vdecls
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumapSentence :: CASLSign -> CASLFORMULA -> CASLFORMULA
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescumapSentence _ =
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu computePNF . mkDistVars . preprocessSen
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescumapTheory :: (CASLSign, [Named CASLFORMULA]) ->
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescu Result (CASLSign, [Named CASLFORMULA])
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescumapTheory (sig, nsens) = do
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu let nsens' = map (\nsen -> nsen{
e2fdd28e29f151215a081dd95fcc443a4c8ccf23mcodescu sentence = mapSentence sig $ sentence nsen
a81a3e6bff3e7b764d78c2864a1324b15e4135famcodescu return (sig, nsens')