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
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : maeder@tzi.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Map as Map
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Set as Set
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian MaederopKindFilter :: Int -> Int -> Maybe Bool
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian MaederopKindFilter arg op =
1bc3627bdb66ecc1efe23eeaeca0ee1f3151ab14Christian Maeder if op < arg then Just True
f7587308f5d51590cd61e4316f6a367156c45141Christian Maeder else if arg < op then Just False
1bc3627bdb66ecc1efe23eeaeca0ee1f3151ab14Christian MaedergetIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
454b2a26b6ea95206df2f82768a8e12765f182bfChristian MaedergetIdPrec (pm, r, m) ps i = if i == applId then m + 1
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder (if begPlace i || endPlace i then if Set.member i ps then r else m
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder else m + 2) i pm
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maedertype TermChart = Chart Term
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederiterateCharts :: GlobalAnnos -> [Term] -> TermChart
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder -> State Env TermChart
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederiterateCharts ga terms chart =
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian Maeder let self = iterateCharts ga
b44c934092b277ea7fa55bdaa89f723384b0c23cChristian Maeder oneStep = nextChart addType opKindFilter
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder toMixTerm ga chart
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder as = assumps e
48708376ccab0e56251f53b0ec21499a277e9102Christian Maeder tm = typeMap e
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if null terms then return chart else
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do let t:tt = terms
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder recurse trm = self tt $
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder oneStep (trm, exprTok {tokPos = posOfTerm trm})
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder MixTypeTerm q typ ps -> do
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder mTyp <- anaStarType typ
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder Nothing -> recurse t
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder Just nTyp -> self tt $ oneStep
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder (MixTypeTerm q nTyp ps,
da768cb4801fbb3bb2f352532d62f6ac60f5ad29Christian Maeder typeTok {tokPos = headPos ps})
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder BracketTerm b ts ps -> self
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (expandPos TermToken (getBrackets b) ts ps ++ tt) chart
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar (VarDecl v typ ok ps) -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mTyp <- anaStarType typ
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> recurse t
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just nTyp -> do
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder let mi = findOpId e v $ simpleTypeScheme nTyp
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> addDiags [mkDiag Error
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder "value not found" v]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> return ()
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder recurse $ QualVar $ VarDecl v nTyp ok ps
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder QualOp b (InstOpId v ts qs) sc ps -> do
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder mSc <- anaTypeScheme sc
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder newTs <- anaInstTypes ts
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> recurse t
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder Just nSc -> do
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder let mi = findOpId e v nSc
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> addDiags [mkDiag Error
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder "value not found" v]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> return ()
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maeder recurse $ QualOp b (InstOpId v newTs qs) nSc ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder QuantifiedTerm quant decls hd ps -> do
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder newDs <- mapM anaGenVarDecl decls
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putAssumps as
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putTypeMap tm
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder LambdaTerm decls part hd ps -> do
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder mDecls <- mapM (resolvePattern ga) decls
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newDecls = catMaybes mDecls
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder anaDecls <- mapM anaPattern newDecls
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let bs = concatMap extractVars anaDecls
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder checkUniqueVars bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mapM_ addVarDecl bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putAssumps as
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder recurse $ LambdaTerm anaDecls part newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder CaseTerm hd eqs ps -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder newEs <- resolveCaseEqs ga eqs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder recurse $ CaseTerm newT newEs ps
64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder LetTerm b eqs hd ps -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder newEs <- resolveLetEqs ga eqs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolve ga hd
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let newT = case mt of Just trm -> trm
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putAssumps as
64558a09e6f6b95d2689d02dd5251339f8ac505bChristian Maeder recurse $ LetTerm b newEs newT ps
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder TermToken tok -> do
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder let (ds1, trm) = convertMixfixToken
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder (literal_annos ga)
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder ResolvedMixTerm TermToken tok
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder self tt $ oneStep $
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder TermToken _ -> (trm, tok)
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder _ -> (trm, exprTok
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maeder {tokPos = tokPos tok})
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder AsPattern vd p ps -> do
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder mp <- resolvePattern ga p
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let newP = case mp of Just pat -> pat
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder recurse $ AsPattern vd newP ps
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> error ("iterCharts: " ++ show t)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- * equation stuff
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEq ga (ProgEq p t ps) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mp <- resolvePattern ga p
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> return Nothing
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just np -> do
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder as <- gets assumps
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder newP <- anaPattern np
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let bs = extractVars newP
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder checkUniqueVars bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mapM_ addVarDecl bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mtt <- resolve ga t
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder putAssumps as
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return $ case mtt of
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> Nothing
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just newT -> Just $ ProgEq newP newT ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs _ [] = return []
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs ga (eq:rt) =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do mEq <- resolveCaseEq ga eq
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder eqs <- resolveCaseEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return $ case mEq of
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder Nothing -> eqs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just newEq -> newEq : eqs
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mPat <- resolvePattern ga pat
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> do resolve ga trm
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder resolveLetEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just nPat -> do
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder newPat <- anaPattern nPat
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder let bs = extractVars newPat
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder checkUniqueVars bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mapM addVarDecl bs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mTrm <- resolve ga trm
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder Nothing -> resolveLetEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Just newTrm -> do
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder eqs <- resolveLetEqs ga rt
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return (ProgEq newPat newTrm ps : eqs)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedermkPatAppl :: Term -> Term -> [Pos] -> Term
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedermkPatAppl op arg qs =
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder ResolvedMixTerm i [arg] qs
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder _ -> ApplTerm op arg qs
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedertoMixTerm :: Id -> [Term] -> [Pos] -> Term
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedertoMixTerm i ar qs =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if i == applId then assert (length ar == 2) $
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else if i == tupleId || i == unitId then
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder mkTupleTerm ar qs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder else if isUnknownId i then
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder QualVar $ VarDecl (simpleIdToId $ unToken i)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder (MixfixType []) Other qs
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else ResolvedMixTerm i ar qs
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian MaedergetKnowns :: Id -> Knowns
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder Set.unions (map getKnowns cs)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaederresolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederresolvePattern ga = resolver ga (unknownId : builtinIds)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve ga = resolver ga builtinIds
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolver :: GlobalAnnos -> [Id] -> Term
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolver ga bs trm =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do as <- gets assumps
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder ps@((_, _, m), _) <- gets preIds
a1d523aa255a291c0154af764fbdb8597c445918Christian Maeder ks = Set.union (Set.fromList (tokStr exprTok: inS :
a1d523aa255a291c0154af764fbdb8597c445918Christian Maeder map (:[]) ":{}[](),"))
48708376ccab0e56251f53b0ec21499a277e9102Christian Maeder $ Set.unions $ map getKnowns ids
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder chart<- iterateCharts ga [trm] $
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder initChart (listRules (m + 3) ga ++
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (initRules ps bs
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder ids)) (if unknownId `elem` bs then ks else Set.empty)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder let Result ds mr = getResolved showPretty (posOfTerm trm)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder toMixTerm chart
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederinitRules (pm@(_, _, m), ps) bs is =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder map ( \ i -> mixRule (getIdPrec pm ps i) i)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (bs ++ is) ++
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder map ( \ i -> (protect i, m + 3, getPlainTokenList i))
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder (filter isMixfix is)