Cross Reference: /hets/HasCASL/MixAna.hs
MixAna.hs revision fc8c6570c7b4ee13f375eb607bed2290438573bf
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
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
{- |
Module : $Header$
Copyright : (c) Christian Maeder and Uni Bremen 2003
Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
Maintainer : maeder@tzi.de
Stability : experimental
Portability : portable
Mixfix analysis of terms and patterns, type annotations are also analysed
-}
module HasCASL.MixAna where
import Common.GlobalAnnotations
import Common.Result
import Common.Id
import Common.Keywords
import Common.Earley
import Common.ConvertLiteral
import Common.Lib.State
import qualified Common.Lib.Map as Map
import qualified Common.Lib.Set as Set
import HasCASL.As
import HasCASL.AsUtils
import HasCASL.VarDecl
import HasCASL.Le
import Data.Maybe
import Control.Exception(assert)
opKindFilter :: Int -> Int -> Maybe Bool
opKindFilter arg op =
if op < arg then Just True
else if arg < op then Just False
else Nothing
getIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
getIdPrec (pm, r, m) ps i = if i == applId then m + 1
else Map.findWithDefault
(if begPlace i || endPlace i then if Set.member i ps then r else m
else m + 2) i pm
addType :: Term -> Term -> Term
addType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
addType _ _ = error "addType"
type TermChart = Chart Term
iterateCharts :: GlobalAnnos -> [Term] -> TermChart
-> State Env TermChart
iterateCharts ga terms chart =
do e <- get
let self = iterateCharts ga
oneStep = nextChart addType opKindFilter
toMixTerm ga chart
as = assumps e
tm = typeMap e
if null terms then return chart else
do let t:tt = terms
recurse trm = self tt $
oneStep (trm, exprTok {tokPos = posOfTerm trm})
case t of
MixfixTerm ts -> self (ts ++ tt) chart
MixTypeTerm q typ ps -> do
mTyp <- anaStarType typ
case mTyp of
Nothing -> recurse t
Just nTyp -> self tt $ oneStep
(MixTypeTerm q nTyp ps,
typeTok {tokPos = headPos ps})
BracketTerm b ts ps -> self
(expandPos TermToken (getBrackets b) ts ps ++ tt) chart
QualVar (VarDecl v typ ok ps) -> do
mTyp <- anaStarType typ
case mTyp of
Nothing -> recurse t
Just nTyp -> do
let mi = findOpId e v $ simpleTypeScheme nTyp
case mi of
Nothing -> addDiags [mkDiag Error
"value not found" v]
_ -> return ()
recurse $ QualVar $ VarDecl v nTyp ok ps
QualOp b (InstOpId v ts qs) sc ps -> do
mSc <- anaTypeScheme sc
newTs <- anaInstTypes ts
case mSc of
Nothing -> recurse t
Just nSc -> do
let mi = findOpId e v nSc
case mi of
Nothing -> addDiags [mkDiag Error
"value not found" v]
_ -> return ()
recurse $ QualOp b (InstOpId v newTs qs) nSc ps
QuantifiedTerm quant decls hd ps -> do
newDs <- mapM anaGenVarDecl decls
mt <- resolve ga hd
putAssumps as
putTypeMap tm
let newT = case mt of Just trm -> trm
_ -> hd
recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
LambdaTerm decls part hd ps -> do
mDecls <- mapM (resolvePattern ga) decls
let newDecls = catMaybes mDecls
anaDecls <- mapM anaPattern newDecls
let bs = concatMap extractVars anaDecls
checkUniqueVars bs
mapM_ addVarDecl bs
mt <- resolve ga hd
putAssumps as
let newT = case mt of Just trm -> trm
_ -> hd
recurse $ LambdaTerm anaDecls part newT ps
CaseTerm hd eqs ps -> do
mt <- resolve ga hd
let newT = case mt of Just trm -> trm
_ -> hd
newEs <- resolveCaseEqs ga eqs
recurse $ CaseTerm newT newEs ps
LetTerm b eqs hd ps -> do
newEs <- resolveLetEqs ga eqs
mt <- resolve ga hd
let newT = case mt of Just trm -> trm
_ -> hd
putAssumps as
recurse $ LetTerm b newEs newT ps
TermToken tok -> do
let (ds1, trm) = convertMixfixToken
(literal_annos ga)
ResolvedMixTerm TermToken tok
addDiags ds1
self tt $ oneStep $
case trm of
TermToken _ -> (trm, tok)
_ -> (trm, exprTok
{tokPos = tokPos tok})
AsPattern vd p ps -> do
mp <- resolvePattern ga p
let newP = case mp of Just pat -> pat
Nothing -> p
recurse $ AsPattern vd newP ps
_ -> error ("iterCharts: " ++ show t)
-- * equation stuff
resolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
resolveCaseEq ga (ProgEq p t ps) =
do mp <- resolvePattern ga p
case mp of
Nothing -> return Nothing
Just np -> do
as <- gets assumps
newP <- anaPattern np
let bs = extractVars newP
checkUniqueVars bs
mapM_ addVarDecl bs
mtt <- resolve ga t
putAssumps as
return $ case mtt of
Nothing -> Nothing
Just newT -> Just $ ProgEq newP newT ps
resolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
resolveCaseEqs _ [] = return []
resolveCaseEqs ga (eq:rt) =
do mEq <- resolveCaseEq ga eq
eqs <- resolveCaseEqs ga rt
return $ case mEq of
Nothing -> eqs
Just newEq -> newEq : eqs
resolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
resolveLetEqs _ [] = return []
resolveLetEqs ga (ProgEq pat trm ps : rt) =
do mPat <- resolvePattern ga pat
case mPat of
Nothing -> do resolve ga trm
resolveLetEqs ga rt
Just nPat -> do
newPat <- anaPattern nPat
let bs = extractVars newPat
checkUniqueVars bs
mapM addVarDecl bs
mTrm <- resolve ga trm
case mTrm of
Nothing -> resolveLetEqs ga rt
Just newTrm -> do
eqs <- resolveLetEqs ga rt
return (ProgEq newPat newTrm ps : eqs)
mkPatAppl :: Term -> Term -> [Pos] -> Term
mkPatAppl op arg qs =
case op of
QualVar (VarDecl i (MixfixType []) _ _) ->
ResolvedMixTerm i [arg] qs
_ -> ApplTerm op arg qs
toMixTerm :: Id -> [Term] -> [Pos] -> Term
toMixTerm i ar qs =
if i == applId then assert (length ar == 2) $
let [op, arg] = ar in mkPatAppl op arg qs
else if i == tupleId || i == unitId then
mkTupleTerm ar qs
else if isUnknownId i then
QualVar $ VarDecl (simpleIdToId $ unToken i)
(MixfixType []) Other qs
else ResolvedMixTerm i ar qs
getKnowns :: Id -> Knowns
getKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $
Set.unions (map getKnowns cs)
resolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)
resolvePattern ga = resolver ga (unknownId : builtinIds)
resolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
resolve ga = resolver ga builtinIds
resolver :: GlobalAnnos -> [Id] -> Term
-> State Env (Maybe Term)
resolver ga bs trm =
do as <- gets assumps
ps@((_, _, m), _) <- gets preIds
let ids = Map.keys as
ks = Set.union (Set.fromList (tokStr exprTok: inS :
map (:[]) ":{}[](),"))
$ Set.unions $ map getKnowns ids
chart<- iterateCharts ga [trm] $
initChart (listRules (m + 3) ga ++
(initRules ps bs
ids)) (if unknownId `elem` bs then ks else Set.empty)
let Result ds mr = getResolved showPretty (posOfTerm trm)
toMixTerm chart
addDiags ds
return mr
builtinIds :: [Id]
builtinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
initRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
initRules (pm@(_, _, m), ps) bs is =
map ( \ i -> mixRule (getIdPrec pm ps i) i)
(bs ++ is) ++
map ( \ i -> (protect i, m + 3, getPlainTokenList i))
(filter isMixfix is)