Commit d0841750 authored by Axel Simon's avatar Axel Simon
Browse files

cleanup mgu

parent d3f0db54
......@@ -295,7 +295,8 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val env = E.meet (env, envRhs)
val env = E.popToFunction (v, env)
val fInfo = E.getFunctionInfo (v, env)
val _ = sm := (v, fInfo) :: !sm
val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
not (SymbolTable.eq_symid(s,v))) (!sm)
in
checkUsages false (v,env)
end
......@@ -312,7 +313,8 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
end) env el
val env = E.popToFunction (v, env)
val fInfo = E.getFunctionInfo (v, env)
val _ = sm := (v, fInfo) :: !sm
val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
not (SymbolTable.eq_symid(s,v))) (!sm)
in
checkUsages false (v,env)
end
......
......@@ -1028,21 +1028,6 @@ end = struct
(texpBVarset (op ::) (t1, []), texpBVarset (op ::) (t2, []))
handle (BD.Unsatisfiable bVar) =>
flowError (bVar, affectedField (bVar, env1), [env1,env2]))
handle (ListPair.UnequalLengths) =>
let
val (t1Str, si) = showTypeSI (t1, TVar.emptyShowInfo)
val (t2Str, si) = showTypeSI (t2, si)
val (k1Str, si) = kappaToStringSI (env1, si)
val (k2Str, si) = kappaToStringSI (env2, si)
val (sStr, si) = showSubstsSI (substs, si)
val (b,env) = Scope.unwrap env1
val (b,_) = substBinding (b,emptyExpandInfo)
val (k11Str, si) = kappaToStringSI (Scope.wrap (b,env), si)
in
(TextIO.print ("cannot gen impl flow from\n" ^ k1Str ^ "to\n" ^ k2Str ^
"after applying substitution " ^ sStr ^ "\nto " ^ t1Str ^
"\nand " ^ t2Str ^ "\nb11" ^ k11Str); raise InferenceBug)
end
else
let
(*val _ = TextIO.print ("forcing bVars to be equal:" ^
......@@ -1203,41 +1188,40 @@ end = struct
Scope.wrap (KAPPA {ty = !tyRef}, env)
end
fun unify (env1, env2, (substs, ei)) =
fun unify (env1, env2, substs) =
(case Scope.unwrapDifferent (env1, env2) of
(SOME (KAPPA {ty = ty1}, KAPPA {ty = ty2}), env1, env2) =>
unify (env1, env2, mgu(ty1, ty2, substs, ei))
unify (env1, env2, mgu(ty1, ty2, substs))
| (SOME (SINGLE {name = _, ty = ty1},
SINGLE {name = _, ty = ty2}), env1, env2) =>
unify (env1, env2, mgu(ty1, ty2, substs, ei))
unify (env1, env2, mgu(ty1, ty2, substs))
| (SOME (GROUP bs1, GROUP bs2), env1, env2) =>
let
fun mguOpt (SOME t1, SOME t2, (s,ei)) = mgu (t1,t2,s,ei)
| mguOpt (NONE, NONE, sEi) = sEi
fun mguOpt (SOME t1, SOME t2, substs) = mgu (t1,t2,substs)
| mguOpt (NONE, NONE, substs) = substs
| mguOpt (_, _, _) = raise InferenceBug
fun mguBOpt (SOME (t1,_), SOME (t2,_), (s,ei)) = mgu (t1,t2,s,ei)
| mguBOpt (NONE, NONE, sEi) = sEi
fun mguBOpt (SOME (t1,_), SOME (t2,_), substs) = mgu (t1,t2,substs)
| mguBOpt (NONE, NONE, substs) = substs
| mguBOpt (_, _, _) = raise InferenceBug
fun mguUses ((s1,(ctxt1,t1)) :: us1, (s2,(ctxt2,t2)) :: us2, (s,ei)) =
fun mguUses ((s1,(ctxt1,t1)) :: us1, (s2,(ctxt2,t2)) :: us2, substs) =
(case compare_span (s1,s2) of
EQUAL => mguUses (us1, us2, mgu (t1,t2,s,ei))
| LESS => mguUses (us1, (s2,(ctxt2,t2)) :: us2, (s,ei))
| GREATER => mguUses ((s1,(ctxt1,t1)) :: us1, us2, (s,ei))
EQUAL => mguUses (us1, us2, mgu (t1,t2,substs))
| LESS => mguUses (us1, (s2,(ctxt2,t2)) :: us2, substs)
| GREATER => mguUses ((s1,(ctxt1,t1)) :: us1, us2, substs)
)
| mguUses (_, _, sEi) = sEi
| mguUses (_, _, substs) = substs
fun uB (({name = n1, ty = t1, width = w1, uses = u1},
{name = n2, ty = t2, width = w2, uses = u2}), sEi) =
{name = n2, ty = t2, width = w2, uses = u2}), substs) =
if not (ST.eq_symid (n1,n2)) then raise InferenceBug else
mguUses (SpanMap.listItemsi u1, SpanMap.listItemsi u2,
mguBOpt (t1, t2, mguOpt (w1, w2, sEi)))
mguBOpt (t1, t2, mguOpt (w1, w2, substs)))
(*val _ = if List.length bs1=List.length bs2 then () else
TextIO.print ("*************** mgu of\n" ^ topToString (Scope.wrap (GROUP bs1,env1)) ^ "\ndoes not match\n" ^ topToString (Scope.wrap (GROUP bs2,env2)))*)
val (substs, ei) = List.foldl uB (substs, ei)
(ListPair.zipEq (bs1,bs2))
val substs = List.foldl uB substs (ListPair.zipEq (bs1,bs2))
in
unify (env1, env2, (substs, ei))
unify (env1, env2, substs)
end
| (NONE, env1, env2) => (substs, ei)
| (NONE, env1, env2) => substs
| (SOME _, _, _) => raise InferenceBug
)
......@@ -1288,7 +1272,7 @@ end = struct
(*val (e1Str', si) = topToStringSI (env1,TVar.emptyShowInfo)
val (e2Str', si) = topToStringSI (env2,si)*)
val (substs, ei) = unify (env1, env2, (emptySubsts, emptyExpandInfo))
val substs = unify (env1, env2, emptySubsts)
(*val (scs, cons) = env1
val (_, cons') = env2
val _ = if cons<>cons' then raise InferenceBug else ()
......@@ -1348,7 +1332,7 @@ end = struct
fun subseteq (env1, env2) =
let
val (substs,_) = unify (env1, env2, (emptySubsts, emptyExpandInfo))
val substs = unify (env1, env2, emptySubsts)
(*val si = TVar.emptyShowInfo
val (e1Str, si) = toStringSI (env1, si)
val (e2Str, si) = toStringSI (env2, si)
......
......@@ -40,8 +40,7 @@ structure Substitutions : sig
BooleanDomain.bfun * SizeConstraint.size_constraint_set ->
Types.texp * BooleanDomain.bfun * SizeConstraint.size_constraint_set
val mgu : Types.texp * Types.texp * Substs * expand_info ->
Substs * expand_info
val mgu : Types.texp * Types.texp * Substs -> Substs
end = struct
......@@ -424,162 +423,144 @@ end = struct
(tNew, bFunNew, mergedSCons)
end
fun mgu (t1,t2,s,ei) =
fun mgu (FUN (f1, f2), FUN (g1, g2), s) = mgu (f2, g2, mgu (f1, g1, s))
| mgu (SYN (_, t1), t2, s) = mgu (t1, t2, s)
| mgu (t1, SYN (_, t2), s) = mgu (t1, t2, s)
| mgu (ZENO, ZENO, s) = s
| mgu (FLOAT, FLOAT, s) = s
| mgu (UNIT, UNIT, s) = s
| mgu (VEC t1, VEC t2, s) = mgu (t1, t2, s)
| mgu (CONST c1, CONST c2, s) =
if c1=c2 then s else raise UnificationFailure (
"incompatible bit vectors sizes (" ^ Int.toString c1 ^ " and " ^
Int.toString c2 ^ ")")
| mgu (RECORD (v1,b1,l1), RECORD (v2,b2,l2), s) =
let
val eiRef = ref ei
fun mgu (FUN (f1, f2), FUN (g1, g2), s) = mgu (f2, g2, mgu (f1, g1, s))
| mgu (SYN (_, t1), t2, s) = mgu (t1, t2, s)
| mgu (t1, SYN (_, t2), s) = mgu (t1, t2, s)
| mgu (ZENO, ZENO, s) = s
| mgu (FLOAT, FLOAT, s) = s
| mgu (UNIT, UNIT, s) = s
| mgu (VEC t1, VEC t2, s) = mgu (t1, t2, s)
| mgu (CONST c1, CONST c2, s) =
if c1=c2 then s else raise UnificationFailure (
"incompatible bit vectors sizes (" ^ Int.toString c1 ^ " and " ^
Int.toString c2 ^ ")")
| mgu (RECORD (v1,b1,l1), RECORD (v2,b2,l2), s) =
fun applySubsts (v, b, fs) = (case findSubstForVar (v, s) of
NONE => (v,b,fs)
| SOME (WITH_FIELD (fs',v',b')) => (v', b', List.foldl insertField fs fs')
| _ => raise SubstitutionBug
)
val (v1,b1,l1) = applySubsts (v1,b1,l1)
val (v2,b2,l2) = applySubsts (v2,b2,l2)
fun unify (v1, v2, [], [], s) = if TVar.eq (v1,v2) then s else
#1 (addSubst (v2, WITH_FIELD ([], v1, b1)) (s,emptyExpandInfo))
| unify (v1, v2, (f1 as RField e1) :: fs1,
(f2 as RField e2) :: fs2, s) =
(case compare_rfield (f1,f2) of
EQUAL =>
let
val s = mgu (#fty e1, #fty e2, s)
in
unify (v1, v2, fs1, fs2, s)
end
| LESS =>
let
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f1,ei) = applySubstsToRField s (f1,emptyExpandInfo)
val (s,ei) = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) (s,ei)
in
unify (v1, newVar, fs1, f2 :: fs2, s)
end
| GREATER =>
let
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f2,ei) = applySubstsToRField s (f2,emptyExpandInfo)
val (s,ei) = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) (s,ei)
in
unify (newVar, v2, f1 :: fs1, fs2, s)
end
)
| unify (v1, v2, f1 :: fs1, [], s) =
let
fun applySubsts (v, b, fs) = (case findSubstForVar (v, s) of
NONE => (v,b,fs)
| SOME (WITH_FIELD (fs',v',b')) => (v', b', List.foldl insertField fs fs')
| _ => raise SubstitutionBug
)
val (v1,b1,l1) = applySubsts (v1,b1,l1)
val (v2,b2,l2) = applySubsts (v2,b2,l2)
fun unify (v1, v2, [], [], s) = if TVar.eq (v1,v2) then s else
let
val (s, ei) = addSubst (v2, WITH_FIELD ([], v1, b1))
(s,!eiRef)
val _ = eiRef := ei
in
s
end
| unify (v1, v2, (f1 as RField e1) :: fs1,
(f2 as RField e2) :: fs2, s) =
(case compare_rfield (f1,f2) of
EQUAL =>
let
val s = mgu (#fty e1, #fty e2, s)
in
unify (v1, v2, fs1, fs2, s)
end
| LESS =>
let
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f1,ei) = applySubstsToRField s (f1,!eiRef)
val (s,ei) = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) (s,ei)
val _ = eiRef := ei
in
unify (v1, newVar, fs1, f2 :: fs2, s)
end
| GREATER =>
let
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f2,ei) = applySubstsToRField s (f2,!eiRef)
val (s,ei) = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) (s,ei)
val _ = eiRef := ei
in
unify (newVar, v2, f1 :: fs1, fs2, s)
end
)
| unify (v1, v2, f1 :: fs1, [], s) =
let
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f1,ei) = applySubstsToRField s (f1,!eiRef)
val (s,ei) = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) (s,ei)
val _ = eiRef := ei
in
unify (v1, newVar, fs1, [], s)
end
| unify (v1, v2, [], f2 :: fs2, s) =
let
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f2,ei) = applySubstsToRField s (f2,!eiRef)
val (s,ei) = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) (s,ei)
val _ = eiRef := ei
in
unify (newVar, v2, [], fs2, s)
end
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f1,ei) = applySubstsToRField s (f1,emptyExpandInfo)
val (s,ei) = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) (s,ei)
in
unify (v1,v2,l1,l2,s)
unify (v1, newVar, fs1, [], s)
end
| mgu (MONAD (r1,f1,t1), MONAD (r2,f2,t2), s) =
mgu (r1, r2, mgu (f1, f2, mgu (t1, t2, s)))
| mgu (ALG (ty1, l1), ALG (ty2, l2), s) =
let fun incompat () = raise UnificationFailure (
"cannot match constructor " ^
SymbolTable.getString(!SymbolTables.typeTable, ty1) ^
" with " ^
SymbolTable.getString(!SymbolTables.typeTable, ty2))
in case SymbolTable.compare_symid (ty1, ty2) of
LESS => incompat ()
| GREATER => incompat ()
| EQAL => List.foldl (fn ((e1,e2),s) => mgu (e1,e2,s)) s
(ListPair.zipEq (l1,l2))
end
(*mgu is right-biased in that mgu(a,b) always creates b/a which means
that the resulting substitution never modifies the lhs if that is
avoidable*)
| mgu (e, VAR (v,b), s) =
| unify (v1, v2, [], f2 :: fs2, s) =
let
fun unifyVars (v,b,e,s) =
case findSubstForVar (v,s) of
NONE =>
let
val (e, ei) = applySubstsToExp s (e, !eiRef)
val (s, ei) = addSubst (v,WITH_TYPE e) (s,ei)
val _ = eiRef := ei
in
s
end
| SOME (WITH_TYPE t) => mgu (e, t, s)
| _ => raise SubstitutionBug
val newVar = freshTVar ()
val newBVar = BD.freshBVar ()
val (f2,ei) = applySubstsToRField s (f2,emptyExpandInfo)
val (s,ei) = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) (s,ei)
in
case e of
VAR (v',b') => if TVar.eq (v',v) then s else unifyVars (v,b,e,s)
| _ => unifyVars (v,b,e,s)
unify (newVar, v2, [], fs2, s)
end
| mgu (VAR (v,b), e, s) =
(case findSubstForVar (v,s) of
NONE =>
in
unify (v1,v2,l1,l2,s)
end
| mgu (MONAD (r1,f1,t1), MONAD (r2,f2,t2), s) =
mgu (r1, r2, mgu (f1, f2, mgu (t1, t2, s)))
| mgu (ALG (ty1, l1), ALG (ty2, l2), s) =
let fun incompat () = raise UnificationFailure (
"cannot match constructor " ^
SymbolTable.getString(!SymbolTables.typeTable, ty1) ^
" with " ^
SymbolTable.getString(!SymbolTables.typeTable, ty2))
in case SymbolTable.compare_symid (ty1, ty2) of
LESS => incompat ()
| GREATER => incompat ()
| EQAL => List.foldl (fn ((e1,e2),s) => mgu (e1,e2,s)) s
(ListPair.zipEq (l1,l2))
end
(*mgu is right-biased in that mgu(a,b) always creates b/a which means
that the resulting substitution never modifies the lhs if that is
avoidable*)
| mgu (e, VAR (v,b), s) =
let
fun unifyVars (v,b,e,s) =
case findSubstForVar (v,s) of
NONE =>
let
val (e, ei) = applySubstsToExp s (e, !eiRef)
val (s,ei) = addSubst (v,WITH_TYPE e) (s,ei)
val _ = eiRef := ei
val (e, ei) = applySubstsToExp s (e, emptyExpandInfo)
val (s, ei) = addSubst (v,WITH_TYPE e) (s,ei)
in
s
end
| SOME (WITH_TYPE t) => mgu (e, t, s)
| _ => raise SubstitutionBug
)
| mgu (t1,t2,s) =
let fun descr (FUN _) = "a function type"
| descr (ZENO) = "int"
| descr (FLOAT) = "float"
| descr (UNIT) = "()"
| descr (VEC (CONST c)) = "a vector of " ^
Int.toString c ^ " bits"
| descr (VEC _) = "a bit vector"
| descr (ALG (ty, _)) = "type " ^
SymbolTable.getString(!SymbolTables.typeTable, ty)
| descr (RECORD (_,_,fs)) = "a record {" ^
#2 (List.foldl (fn (RField {name = n, ...},(sep,str)) =>
(", ", SymbolTable.getString(!SymbolTables.fieldTable, n) ^
sep ^ str)) ("","") fs) ^ "}"
| descr (MONAD _) = "an action"
| descr _ = "something that shouldn't be here"
in
raise UnificationFailure ("cannot match " ^ descr t1 ^
" against " ^ descr t2)
end
in
(mgu (t1,t2,s), !eiRef)
case e of
VAR (v',b') => if TVar.eq (v',v) then s else unifyVars (v,b,e,s)
| _ => unifyVars (v,b,e,s)
end
| mgu (VAR (v,b), e, s) =
(case findSubstForVar (v,s) of
NONE =>
let
val (e, ei) = applySubstsToExp s (e, emptyExpandInfo)
val (s,ei) = addSubst (v,WITH_TYPE e) (s,ei)
in
s
end
| SOME (WITH_TYPE t) => mgu (e, t, s)
| _ => raise SubstitutionBug
)
| mgu (t1,t2,s) =
let fun descr (FUN _) = "a function type"
| descr (ZENO) = "int"
| descr (FLOAT) = "float"
| descr (UNIT) = "()"
| descr (VEC (CONST c)) = "a vector of " ^
Int.toString c ^ " bits"
| descr (VEC _) = "a bit vector"
| descr (ALG (ty, _)) = "type " ^
SymbolTable.getString(!SymbolTables.typeTable, ty)
| descr (RECORD (_,_,fs)) = "a record {" ^
#2 (List.foldl (fn (RField {name = n, ...},(sep,str)) =>
(", ", SymbolTable.getString(!SymbolTables.fieldTable, n) ^
sep ^ str)) ("","") fs) ^ "}"
| descr (MONAD _) = "an action"
| descr _ = "something that shouldn't be here"
in
raise UnificationFailure ("cannot match " ^ descr t1 ^
" against " ^ descr t2)
end
......@@ -587,7 +568,7 @@ end = struct
let
val (t1Str, si) = showTypeSI (t1, TVar.emptyShowInfo)
val (t2Str, si) = showTypeSI (t2, si)
val (substs,_) = mgu (t1,t2,emptySubsts,emptyExpandInfo)
val substs = mgu (t1,t2,emptySubsts)
val (sStr, si) = showSubstsSI (substs, si)
in
("unifying t1=" ^ t1Str ^ "\nwith t2=" ^ t2Str ^ "\n" ^ sStr)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment