-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy pathPCFOL2FOL.inline.hs
185 lines (167 loc) · 6.73 KB
/
PCFOL2FOL.inline.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
{-
Module: $Header: /repository/HetCATS/Comorphisms/PFOL2FOL.inline.hs, v
1.20 2004/06/02 19:52:39 mnd Exp $
Copyright : (c) Zicheng Wang, Uni Bremen 2002-2004
Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
Maintainer : hets@tzi.de
Stability : provisional
Portability : portable
-}
{- todo
generate axioms
translate formulas
optimize for total sigs
translate morphisms (remove partiality)
-}
module Comorphisms.PCFOL2FOL where
--import Test
import Logic.Logic
import Logic.Comorphism
import Common.Id
import qualified Common.Lib.Map as Map
import qualified Common.Lib.Set as Set
import qualified Common.Lib.Rel as Rel
import Common.AS_Annotation
--import Comorphisms.CASL2PCFOL
--CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic
import CASL.Overload
import List (nub,delete)
import Common.ListUtils
import Data.List
-- | The identity of the comorphism
data PCFOL2FOL = PCFOL2FOL deriving (Show)
instance Language PCFOL2FOL -- default definition is okay
instance Comorphism PCFOL2FOL
CASL CASL_Sublogics
CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
CASLSign
CASLMor
Symbol RawSymbol ()
CASL CASL_Sublogics
CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
CASLSign
CASLMor
Symbol RawSymbol () where
sourceLogic PCFOL2FOL = CASL
sourceSublogic PCFOL2FOL = CASL_SL
{ has_sub = False,
has_part = True,
has_cons = True,
has_eq = True,
has_pred = True,
which_logic = FOL
}
targetLogic PCFOL2FOL = CASL
targetSublogic PCFOL2FOL = CASL_SL
{ has_sub = False,
has_part = False, -- partiality is coded out
has_cons = True,
has_eq = True,
has_pred = True,
which_logic = FOL
}
map_sign PCFOL2FOL sig =
let e = sig2FOL sig in Just (e, generateFOLAxioms sig)
map_morphism PCFOL2FOL = Just . id
map_sentence PCFOL2FOL sig = Just . mapSen
map_symbol PCFOL2FOL = Set.single . id
sig2FOL::Sign f e-> Sign f e
sig2FOL sig =sig {opMap=newOpMap,predMap=newpredMap }
where
sig2sort=Set.toList(sortSet sig)
undef x = OpType{opKind = Total, opArgs=[],opRes=x}
setundef = Set.fromList (map undef sig2sort)
map2list = Map.toList(opMap sig)
set2list = map (\(x,y)->(x,Set.toList y)) map2list
par2total [] = []
par2total (x:xs) = if ((opKind x)==Partial) then (x{opKind=Total}):(par2total xs) else x:(par2total xs)
newTotalMap =Map.fromList [(x,Set.fromList(par2total y))|(x,y)<-set2list]
newOpMap = Map.insert bottom setundef newTotalMap
undefpred x = PredType{predArgs=[x]}
setundefpred = Set.fromList(map undefpred sig2sort)
newpredMap = Map.insert defPred setundefpred (predMap sig)
bottom = mkId[mkSimpleId "_bottom"]
defPred = mkId[mkSimpleId "_D"]
generateFOLAxioms :: Sign f e -> [Named(FORMULA f)]
--generateFOLAxioms _ = []
generateFOLAxioms sig =
concat
([inlineAxioms CASL
" sort s \
\ pred d:s \
\ . exists x:s.d(x) %(ga_nonEmpty)%" ++
inlineAxioms CASL
" sort s \
\ op bottom:s \
\ pred d:s \
\ forall x:s . not d(x) <=> x=bottom %(ga_notDefBottom)%"
| s<-sortList ] ++
[inlineAxioms CASL
" sort t \
\ sorts s_i \
\ sorts s_k \
\ op f:s_i->t \
\ preds d:t; d:s_i; d:s_k \
\ var y_k:s_k \
\ forall y_i:s_i . d(f(y_i)) <=> d(y_k) /\\ d(y_k) %(ga_totality)%"
| (f,typ) <- opList, opKind typ == Total,
let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++
[inlineAxioms CASL
" sort t \
\ sorts s_i \
\ sorts s_k \
\ op f:s_i->t \
\ preds d:t; d:s_i; d:s_k \
\ var y_k:s_k \
\ forall y_i:s_i . d(f(y_i)) => d(y_k) /\\ d(y_k) %(ga_stricntess)%"
| (f,typ) <- opList, opKind typ == Partial,
let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++
[inlineAxioms CASL
" sorts s_i \
\ sorts s_k \
\ pred p:s_i \
\ preds d:s_i; d:s_k \
\ var y_k:s_k \
\ forall y_i:s_i . p(y_i) => d(y_k) /\\ d(y_k) %(ga_predicate_strictness)%"
| (p,typ) <- predList, let s=predArgs typ; y=mkVars (length s) ] )
where
d = defPred
sortList = Set.toList (sortSet sig)
opList = [(f,t) | (f,types) <- Map.assocs $ opMap sig,
t <- Set.toList types ]
predList = [(p,t) | (p,types) <- Map.assocs $ predMap sig,
t <- Set.toList types ]
x = mkSimpleId "x"
bottom = mkId [mkSimpleId "_bottom"]
mkVars n = [mkSimpleId ("x_"++show i) | i<-[1..n]]
defined t s ps =
Predication (Qual_pred_name defPred (Pred_type [s] []) []) [t] ps
defVards [vs@(Var_decl [v] s _)] = head $ defVars vs
defVards vs = Conjunction (concatMap defVars vs) []
defVars (Var_decl vns s _) = map (defVar s) vns
defVar s v = defined (Qual_var v s []) s []
mapSen :: FORMULA f -> FORMULA f
mapSen f = case f of
Quantification q vs frm ps ->
Implication (defVards vs) (Quantification q vs (mapSen frm) ps) False ps
Conjunction fs ps -> Conjunction (map mapSen fs) ps
Disjunction fs ps -> Disjunction (map mapSen fs) ps
Implication f1 f2 b ps -> Implication (mapSen f1) (mapSen f2) b ps
Equivalence f1 f2 ps -> Equivalence (mapSen f1) (mapSen f2) ps
Negation frm ps -> Negation (mapSen frm) ps
True_atom ps -> True_atom ps
False_atom ps -> False_atom ps
Existl_equation t1 t2 ps ->
Conjunction[Strong_equation t1 t2 ps,
defined t1 (term_sort t1) ps] ps
Strong_equation t1 t2 ps -> Strong_equation t1 t2 ps
Predication pn ts qs -> Predication pn ts qs
Definedness t ps -> defined t (term_sort t) ps
Membership t ty ps -> error "PCFOL2FOL: no subsorted formula allowed"
Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree
_ -> error "PCFOL2FOL: wrong formula type"