From 5d51d86b0973fe6996b4b64ec78d9fc810177e02 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Oct 2010 14:41:03 -0400 Subject: Hopeful fix for the Great Unification Bug --- src/elab_ops.sml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'src/elab_ops.sml') diff --git a/src/elab_ops.sml b/src/elab_ops.sml index 6465668f..15d8e106 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -97,11 +97,13 @@ fun liftConInCon by = c else CRel (xn + by) - (*| CUnif _ => raise SynUnif*) + | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r) | _ => c, bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} +exception SubUnif + fun subConInCon' rep = U.Con.mapB {kind = fn _ => fn k => k, con = fn (by, xn) => fn c => @@ -111,7 +113,8 @@ fun subConInCon' rep = EQUAL => #1 (liftConInCon by 0 rep) | GREATER => CRel (xn' - 1) | LESS => c) - (*| CUnif _ => raise SynUnif*) + | CUnif (0, _, _, _, _) => raise SubUnif + | CUnif (n, loc, k, s, r) => CUnif (n-1, loc, k, s, r) | _ => c, bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1) | (ctx, _) => ctx} @@ -153,7 +156,7 @@ fun reset () = (identity := 0; fun hnormCon env (cAll as (c, loc)) = case c of - CUnif (_, _, _, ref (SOME c)) => hnormCon env c + CUnif (nl, _, _, _, ref (SOME c)) => hnormCon env (E.mliftConInCon nl c) | CNamed xn => (case E.lookupCNamed env xn of @@ -276,7 +279,7 @@ fun hnormCon env (cAll as (c, loc)) = let val r = ref NONE in - (r, (CUnif (loc, (KType, loc), "_", r), loc)) + (r, (CUnif (0, loc, (KType, loc), "_", r), loc)) end val (vR, v) = cunif () @@ -284,7 +287,7 @@ fun hnormCon env (cAll as (c, loc)) = val c = (CApp (f, v), loc) in case unconstraint c of - (CUnif (_, _, _, vR'), _) => + (CUnif (_, _, _, _, vR'), _) => if vR' = vR then (inc identity; hnormCon env c2) -- cgit v1.2.3