Mercurial > urweb

comparison src/elab_ops.sml @ 494:1bbcc3345d12

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Map distributivity rule in hnormCon
author Adam Chlipala <adamc@hcoop.net>
date Tue, 11 Nov 2008 19:58:25 -0500
parents b85e6ba56618
children 11fc77fb8257
comparison
equal deleted inserted replaced
493:ae03d09043c1 494:1bbcc3345d12
148 case hnormCon env c of 148 case hnormCon env c of
149 (CDisjoint (_, _, _, c), _) => unconstraint c 149 (CDisjoint (_, _, _, c), _) => unconstraint c
150 | c => c 150 | c => c
151 val c = unconstraint c 151 val c = unconstraint c
152 152
153 fun tryDistributivity () =
154 let
155 fun distribute (c1, c2) =
156 let
157 val c = (CFold ks, loc)
158 val c = (CApp (c, f), loc)
159 val c = (CApp (c, i), loc)
160
161 val c1 = (CApp (c, c1), loc)
162 val c2 = (CApp (c, c2), loc)
163 val c = (CConcat (c1, c2), loc)
164 in
165 hnormCon env c
166 end
167 in
168 case (hnormCon env i, hnormCon env c2, hnormCon env c) of
169 ((CRecord (_, []), _),
170 (CConcat (arg1, arg2), _),
171 (CConcat (c1, c2'), _)) =>
172 (case (hnormCon env c1, hnormCon env c2') of
173 ((CRecord (_, [(nm', v')]), _),
174 (CUnif (_, _, _, rR'), _)) =>
175 (case hnormCon env nm' of
176 (CUnif (_, _, _, nmR'), _) =>
177 if nmR' = nmR andalso rR' = rR then
178 distribute (arg1, arg2)
179 else
180 default ()
181 | _ => default ())
182 | _ => default ())
183 | _ => default ()
184 end
185
153 fun tryFusion () = 186 fun tryFusion () =
154 let 187 let
155 fun fuse (dom, new_v, r') = 188 fun fuse (dom, new_v, r') =
156 let 189 let
157 val ran = #2 ks 190 val ran = #2 ks
203 (nmR := SOME (CRel 2, loc); 236 (nmR := SOME (CRel 2, loc);
204 vR := SOME (CRel 1, loc); 237 vR := SOME (CRel 1, loc);
205 rR := SOME (CError, loc); 238 rR := SOME (CError, loc);
206 fuse (dom, v', r')) 239 fuse (dom, v', r'))
207 else 240 else
208 default () 241 tryDistributivity ()
209 | _ => default ()) 242 | _ => tryDistributivity ())
210 | _ => default ()) 243 | _ => tryDistributivity ())
211 | _ => default () 244 | _ => tryDistributivity ()
212 end 245 end
213 | _ => default ()) 246 | _ => tryDistributivity ())
214 | _ => default ()) 247 | _ => tryDistributivity ())
215 | _ => default ()) 248 | _ => tryDistributivity ())
216 | _ => default () 249 | _ => tryDistributivity ()
217 end 250 end
251
218 in 252 in
219 (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) 253 (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
220 case (hnormCon env i, unconstraint c) of 254 case (hnormCon env i, unconstraint c) of
221 ((CRecord (_, []), _), 255 ((CRecord (_, []), _),
222 (CConcat (c1, c2'), _)) => 256 (CConcat (c1, c2'), _)) =>