Mercurial > urweb

comparison src/elab_ops.sml @ 1303:c7b9a33c26c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hopeful fix for the Great Unification Bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 14:41:03 -0400
parents a779402841f6
children 20f898c29525
comparison
equal deleted inserted replaced
1302:d008c4c43a0a 1303:c7b9a33c26c8
95 CRel xn => 95 CRel xn =>
96 if xn < bound then 96 if xn < bound then
97 c 97 c
98 else 98 else
99 CRel (xn + by) 99 CRel (xn + by)
100 (*| CUnif _ => raise SynUnif*) 100 | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r)
101 | _ => c, 101 | _ => c,
102 bind = fn (bound, U.Con.RelC _) => bound + 1 102 bind = fn (bound, U.Con.RelC _) => bound + 1
103 | (bound, _) => bound} 103 | (bound, _) => bound}
104
105 exception SubUnif
104 106
105 fun subConInCon' rep = 107 fun subConInCon' rep =
106 U.Con.mapB {kind = fn _ => fn k => k, 108 U.Con.mapB {kind = fn _ => fn k => k,
107 con = fn (by, xn) => fn c => 109 con = fn (by, xn) => fn c =>
108 case c of 110 case c of
109 CRel xn' => 111 CRel xn' =>
110 (case Int.compare (xn', xn) of 112 (case Int.compare (xn', xn) of
111 EQUAL => #1 (liftConInCon by 0 rep) 113 EQUAL => #1 (liftConInCon by 0 rep)
112 | GREATER => CRel (xn' - 1) 114 | GREATER => CRel (xn' - 1)
113 | LESS => c) 115 | LESS => c)
114 (*| CUnif _ => raise SynUnif*) 116 | CUnif (0, _, _, _, _) => raise SubUnif
117 | CUnif (n, loc, k, s, r) => CUnif (n-1, loc, k, s, r)
115 | _ => c, 118 | _ => c,
116 bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1) 119 bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
117 | (ctx, _) => ctx} 120 | (ctx, _) => ctx}
118 121
119 val liftConInCon = liftConInCon 1 122 val liftConInCon = liftConInCon 1
151 distribute := 0; 154 distribute := 0;
152 fuse := 0) 155 fuse := 0)
153 156
154 fun hnormCon env (cAll as (c, loc)) = 157 fun hnormCon env (cAll as (c, loc)) =
155 case c of 158 case c of
156 CUnif (_, _, _, ref (SOME c)) => hnormCon env c 159 CUnif (nl, _, _, _, ref (SOME c)) => hnormCon env (E.mliftConInCon nl c)
157 160
158 | CNamed xn => 161 | CNamed xn =>
159 (case E.lookupCNamed env xn of 162 (case E.lookupCNamed env xn of
160 (_, _, SOME c') => hnormCon env c' 163 (_, _, SOME c') => hnormCon env c'
161 | _ => cAll) 164 | _ => cAll)
274 let 277 let
275 fun cunif () = 278 fun cunif () =
276 let 279 let
277 val r = ref NONE 280 val r = ref NONE
278 in 281 in
279 (r, (CUnif (loc, (KType, loc), "_", r), loc)) 282 (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
280 end 283 end
281 284
282 val (vR, v) = cunif () 285 val (vR, v) = cunif ()
283 286
284 val c = (CApp (f, v), loc) 287 val c = (CApp (f, v), loc)
285 in 288 in
286 case unconstraint c of 289 case unconstraint c of
287 (CUnif (_, _, _, vR'), _) => 290 (CUnif (_, _, _, _, vR'), _) =>
288 if vR' = vR then 291 if vR' = vR then
289 (inc identity; 292 (inc identity;
290 hnormCon env c2) 293 hnormCon env c2)
291 else 294 else
292 tryFusion () 295 tryFusion ()