Mercurial > urweb

comparison src/elab_ops.sml @ 339:075b36dbb1a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud supports INSERT
author Adam Chlipala <adamc@hcoop.net>
date Sun, 14 Sep 2008 15:10:04 -0400
parents eec65c11d3e2
children b85e6ba56618
comparison
equal deleted inserted replaced
338:e976b187d73a 339:075b36dbb1a4
147 fun unconstraint c = 147 fun unconstraint c =
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
153 fun tryFusion () =
154 let
155 fun fuse (dom, new_v, r') =
156 let
157 val ran = #2 ks
158
159 val f = (CApp (f, (CRel 2, loc)), loc)
160 val f = (CApp (f, new_v), loc)
161 val f = (CApp (f, (CRel 0, loc)), loc)
162 val f = (CAbs ("acc", ran, f), loc)
163 val f = (CAbs ("v", dom, f), loc)
164 val f = (CAbs ("nm", (KName, loc), f), loc)
165
166 val c = (CFold (dom, ran), loc)
167 val c = (CApp (c, f), loc)
168 val c = (CApp (c, i), loc)
169 val c = (CApp (c, r'), loc)
170 in
171 hnormCon env c
172 end
173 in
174 case #1 (hnormCon env c2) of
175 CApp (f, r') =>
176 (case #1 (hnormCon env f) of
177 CApp (f, inner_i) =>
178 (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of
179 (CApp (f, inner_f), CRecord (_, [])) =>
180 (case #1 (hnormCon env f) of
181 CFold (dom, _) =>
182 let
183 val c = inner_f
184 val c = (CApp (c, nm), loc)
185 val c = (CApp (c, v), loc)
186 val c = (CApp (c, r), loc)
187 val c = unconstraint c
188
189 (*val () = Print.prefaces "Onto something!"
190 [("c", ElabPrint.p_con env cAll),
191 ("c'", ElabPrint.p_con env c)]*)
192
193 in
194 case #1 (hnormCon env c) of
195 CConcat (first, rest) =>
196 (case (#1 (hnormCon env first),
197 #1 (hnormCon env rest)) of
198 (CRecord (_, [(nm', v')]),
199 CUnif (_, _, _, rR')) =>
200 (case #1 (hnormCon env nm') of
201 CUnif (_, _, _, nmR') =>
202 if rR' = rR andalso nmR' = nmR then
203 (nmR := SOME (CRel 2, loc);
204 vR := SOME (CRel 1, loc);
205 rR := SOME (CError, loc);
206 fuse (dom, v', r'))
207 else
208 default ()
209 | _ => default ())
210 | _ => default ())
211 | _ => default ()
212 end
213 | _ => default ())
214 | _ => default ())
215 | _ => default ())
216 | _ => default ()
217 end
152 in 218 in
153 (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) 219 (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
154 case (hnormCon env i, unconstraint c) of 220 case (hnormCon env i, unconstraint c) of
155 ((CRecord (_, []), _), 221 ((CRecord (_, []), _),
156 (CConcat (c1, c2'), _)) => 222 (CConcat (c1, c2'), _)) =>
161 ((CUnif (_, _, _, nmR'), _), 227 ((CUnif (_, _, _, nmR'), _),
162 (CUnif (_, _, _, vR'), _)) => 228 (CUnif (_, _, _, vR'), _)) =>
163 if nmR' = nmR andalso vR' = vR andalso rR' = rR then 229 if nmR' = nmR andalso vR' = vR andalso rR' = rR then
164 hnormCon env c2 230 hnormCon env c2
165 else 231 else
166 default () 232 tryFusion ()
167 | _ => default ()) 233 | _ => tryFusion ())
168 | _ => default ()) 234 | _ => tryFusion ())
169 | _ => default () 235 | _ => tryFusion ()
170 end) 236 end)
171 | _ => default ()) 237 | _ => default ())
172 | _ => default () 238 | _ => default ()
173 end 239 end
174 | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) 240 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))