Mercurial > urweb

comparison src/elab_util.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 d008c4c43a0a
children 9e0fa4f6ac93
comparison
equal deleted inserted replaced
1302:d008c4c43a0a 1303:c7b9a33c26c8
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
115 S.Continue (k, ())) k () of 115 S.Continue (k, ())) k () of
116 S.Return _ => true 116 S.Return _ => true
117 | S.Continue _ => false 117 | S.Continue _ => false
118 118
119 end 119 end
120
121 val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con)
120 122
121 structure Con = struct 123 structure Con = struct
122 124
123 datatype binder = 125 datatype binder =
124 RelK of string 126 RelK of string
213 S.map2 (mfc ctx c, 215 S.map2 (mfc ctx c,
214 fn c' => 216 fn c' =>
215 (CProj (c', n), loc)) 217 (CProj (c', n), loc))
216 218
217 | CError => S.return2 cAll 219 | CError => S.return2 cAll
218 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c 220 | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c)
219 | CUnif _ => S.return2 cAll 221 | CUnif _ => S.return2 cAll
220 222
221 | CKAbs (x, c) => 223 | CKAbs (x, c) =>
222 S.map2 (mfc (bind (ctx, RelK x)) c, 224 S.map2 (mfc (bind (ctx, RelK x)) c,
223 fn c' => 225 fn c' =>