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

fix annoying unification bug

parent e0474196
......@@ -404,9 +404,9 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
let
val (t,env) = E.pushLambdaVar' (caseExpSymId, env)
val envExp = infExp (st,env) e
(*val _ = TextIO.print ("**** after case exp:\n" ^ E.toString envExp)*)
(*val _ = TextIO.print ("**** after case exp:\n" ^ E.topToString envExp)*)
val envVar = E.pushType (false, t, env)
(*val _ = TextIO.print ("**** after case dup:\n" ^ E.toString envVar)*)
(*val _ = TextIO.print ("**** after case dup:\n" ^ E.topToString envVar)*)
val env = E.meetFlow (envVar, envExp)
val env = E.popKappa env
val envNeutral = E.pushTop env
......@@ -677,20 +677,20 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
and infMatch (st,env) (p,e) =
let
val (n,env) = infPat (st,env) p
(*val _ = TextIO.print ("**** after pat:\n" ^ E.toString env)*)
(*val _ = TextIO.print ("**** after pat:\n" ^ E.topToString env)*)
val envScru = E.popKappa env
val envScru = E.pushSymbol (caseExpSymId, SymbolTable.noSpan, envScru)
(*val _ = TextIO.print ("**** after case dup:\n" ^ E.toString envScru)*)
(*val _ = TextIO.print ("**** after case dup:\n" ^ E.topToString envScru)*)
val env = E.meetFlow (env, envScru)
handle S.UnificationFailure str =>
refineError (str,
" when checking case scrutinee",
[(envScru, "scrutinee and patterns so far "),
(env, "pattern " ^ showProg (22, PP.pat, p))])
(*val _ = TextIO.print ("**** after mgu:\n" ^ E.toString env)*)
(*val _ = TextIO.print ("**** after mgu:\n" ^ E.topToString env)*)
val env = E.popKappa env
val env = infExp (st,env) e
(*val _ = TextIO.print ("**** after expr:\n" ^ E.toString env)*)
(*val _ = TextIO.print ("**** after expr:\n" ^ E.topToString env)*)
in
E.return (n,env)
end
......@@ -720,7 +720,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
NONE => raise S.UnificationFailure (
"pattern with constructor " ^
SymbolTable.getString(!SymbolTables.conTable, c) ^
" requires an argument")
" may not have an argument")
| SOME t => t
val envCon = E.pushType (true, FUN ([t],ALG (dcon, List.map VAR vs)), envCon)
val envCon = E.genConstructorFlow (true,envCon)
......
......@@ -171,20 +171,19 @@ end = struct
in
(app (fn d => fwdDecl (s,d)) declList
;app (fn d => vDecl (s,d)) declList
;let
val res = {tsynDefs= !synTable,
typeDefs= !dtyTable,
conParents= !conTable} : type_info
(*val _ = TextIO.print (typeInfoToString res)*)
in
res
end)
;{tsynDefs= !synTable, typeDefs= !dtyTable, conParents= !conTable} : type_info
)
end
val resolveTypeInfoPass =
BasicControl.mkTracePassSimple
BasicControl.mkKeepPass
{passName="resolveTypeInfoPass",
pass=resolveTypeInfoPass}
registry=BasicControl.topRegistry,
pass=resolveTypeInfoPass,
preExt="ast",
preOutput=fn (os,(err,t)) => AST.PP.prettyTo(os, t),
postExt="decl",
postOutput=fn (os,ti) => TextIO.output (os,typeInfoToString ti)}
fun run spec = let
open CompilationMonad
......
......@@ -44,7 +44,7 @@ end
structure SymbolTable :> SymbolTableSig = struct
val concisePrint : bool = true
val concisePrint : bool = false
structure SymbolTable = IntBinaryMap
structure Reverse = AtomRedBlackMap
......
......@@ -1280,15 +1280,15 @@ end = struct
SOME f => f :: fs
| NONE => fs) [] bVars
end
| (_,COMPOUND {ty = NONE, width, uses}) => [] (*allow type errors*)
| _ => raise InferenceBug
fun unify (env1, env2, newUses1, newUses2, substs) =
(case Scope.unwrapDifferent (env1, env2) of
(SOME (KAPPA {ty = ty1}, KAPPA {ty = ty2}), env1, env2) =>
unify (env1, env2, newUses1, newUses2, mgu(ty1, ty2, substs))
| (SOME (SINGLE {name = _, ty = ty1},
SINGLE {name = _, ty = ty2}), env1, env2) =>
unify (env1, env2, newUses1, newUses2, mgu(ty1, ty2, substs))
(SOME (KAPPA {ty = t1}, KAPPA {ty = t2}), env1, env2) =>
unify (env1, env2, newUses1, newUses2, mgu (t1,t2,substs))
| (SOME (SINGLE {ty = t1, ...}, SINGLE {ty = t2, ...}), env1, env2) =>
unify (env1, env2, newUses1, newUses2, mgu (t1,t2,substs))
| (SOME (GROUP bs1, GROUP bs2), env1, env2) =>
let
fun mguOpt (SOME t1, SOME t2, substs) = mgu (t1,t2,substs)
......@@ -1337,6 +1337,11 @@ end = struct
fun meetGeneral (env1, env2, directed) =
let
(*val (e1Str,si) = topToStringSI (env1, TVar.emptyShowInfo)
val (e2Str,si) = topToStringSI (env2, si)
val kind = if directed then "directed" else "equalizing"
val _ = TextIO.print ("**** meet " ^ kind ^ ":\n" ^ e1Str ^ "++++ intersected with\n" ^ e2Str)*)
val (newUses1, newUses2, substs) =
unify (env1, env2, SymMap.empty, SymMap.empty, emptySubsts)
(*val (scs, cons) = env1
......@@ -1349,12 +1354,6 @@ end = struct
val _ = cons := (bFun, sCons)
val env1 = (scs,cons)*)
(*val (e1Str,si) = kappaToStringSI (env1, TVar.emptyShowInfo)
val (e2Str,si) = kappaToStringSI (env2, si)
val (sStr,si) = showSubstsSI (substs,si)
val kind = if directed then "directed" else "equalizing"
val _ = TextIO.print ("**** meet " ^ kind ^ ":\n" ^ e1Str ^ "++++ intersected with\n" ^ e2Str)*)
val (_, state1) = env1
val (_, state2) = env2
val sCons = SC.merge (Scope.getSize state1,Scope.getSize state2)
......@@ -1386,6 +1385,7 @@ end = struct
(*val (envStr,si) = topToStringSI (env, si)
val (eStr, si) = showExpandInfoSI (ei,si)
val (sStr,si) = showSubstsSI (substs,si)
val _ = TextIO.print ("applying substitution " ^ sStr ^ " to\n" ^ e1Str ^ "and\n" ^ e2Str ^
"resulting in\n" ^ envStr ^
"thereby projecting onto " ^ BD.setToString bVars ^
......
......@@ -6,7 +6,7 @@ structure Types = struct
type varset = TVar.set
val freshTVar = TVar.freshTVar
val concisePrint = false
val concisePrint = true
datatype texp =
(* a function taking at least one argument *)
......
......@@ -329,21 +329,18 @@ end = struct
(*any substitution that is being added must not mention any variable that
already exists in the domain of the current set of substitutions; if this
holds, the resulting substitutions remain fully applied*)
fun addSubst subst (Substs l, ei) =
fun addSubst subst (Substs l) =
let
val eiRef = ref ei
fun doSubst (v2, WITH_TYPE t2) =
let
val (t2, ei) = applySubstToExp subst (t2, !eiRef)
val _ = eiRef := ei
val (t2, ei) = applySubstToExp subst (t2, emptyExpandInfo)
in
occursCheck (v2, WITH_TYPE t2)
end
| doSubst (v2, WITH_FIELD (fs, v3, bv3)) =
let
val t2 = RECORD (v3,bv3,fs)
val (t2,ei) = applySubstToExp subst (t2,!eiRef)
val _ = eiRef := ei
val (t2,ei) = applySubstToExp subst (t2, emptyExpandInfo)
val RECORD (v3,bv3,fs) = t2
in
occursCheck (v2, WITH_FIELD (fs, v3, bv3))
......@@ -375,14 +372,19 @@ end = struct
val (vStr,si) = TVar.varToString (v,TVar.emptyShowInfo)
val (tStr,si) = case repl of
WITH_TYPE t2 => showTypeSI (t2,si)
| WITH_FIELD (fs, v3) => showTypeSI (
RECORD (v3,BooleanDomain.freshBVar (),fs),si)
| WITH_FIELD (fs, v3, bv3) => showTypeSI (
RECORD (v3,bv3,fs),si)
val (sStr,si) = showSubstsSI (Substs l, si)
val (rStr,_ ) = showSubstsSI (Substs (subst::List.map doSubst l),si)
val _ = TextIO.print ("adding " ^ vStr ^ "/" ^ tStr ^ " to " ^ sStr ^
" yielding " ^ rStr ^ "\n")*)
val _ = TextIO.print ("adding " ^ vStr ^ "/" ^ tStr ^ " to " ^ sStr ^ "\n")*)
val substIsIdentity = (case subst of
(tv, WITH_TYPE (VAR (tv',_))) => TVar.eq (tv,tv')
| (tv, WITH_FIELD (_,tv',_)) => TVar.eq (tv,tv')
| _ => false
)
in
(Substs (occursCheck subst::List.map doSubst l), !eiRef)
if substIsIdentity then Substs l else
Substs (occursCheck subst::List.map doSubst l)
end
fun findSubstForVar (v, Substs l) =
......@@ -404,7 +406,7 @@ end = struct
SC.RESULT (is,sCons) =>
(sCons,
List.foldl (fn ((v,c), substs) =>
#1 (addSubst (v,WITH_TYPE (CONST c)) (substs, emptyExpandInfo))
addSubst (v,WITH_TYPE (CONST c)) substs
) substs is)
| SC.UNSATISFIABLE => raise UnificationFailure
"size constraints over vectors are unsatisfiable"
......@@ -477,8 +479,8 @@ end = struct
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))
fun unify (v1, v2, [], [], s) =
addSubst (v2, WITH_FIELD ([], v1, b1)) s
| unify (v1, v2, (f1 as RField e1) :: fs1,
(f2 as RField e2) :: fs2, s) =
(case compare_rfield (f1,f2) of
......@@ -493,7 +495,7 @@ end = struct
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)
val s = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) s
in
unify (v1, newVar, fs1, f2 :: fs2, s)
end
......@@ -502,7 +504,7 @@ end = struct
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)
val s = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) s
in
unify (newVar, v2, f1 :: fs1, fs2, s)
end
......@@ -512,7 +514,7 @@ end = struct
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)
val s = addSubst (v2, WITH_FIELD ([f1], newVar, newBVar)) s
in
unify (v1, newVar, fs1, [], s)
end
......@@ -521,7 +523,7 @@ end = struct
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)
val s = addSubst (v1, WITH_FIELD ([f2], newVar, newBVar)) s
in
unify (newVar, v2, [], fs2, s)
end
......@@ -531,7 +533,8 @@ end = struct
| 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 (
let
fun incompat () = raise UnificationFailure (
"cannot match constructor " ^
SymbolTable.getString(!SymbolTables.typeTable, ty1) ^
" with " ^
......@@ -546,33 +549,27 @@ end = struct
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, emptyExpandInfo)
val (s, ei) = addSubst (v,WITH_TYPE e) (s,ei)
in
s
end
| SOME (WITH_TYPE t) => mgu (e, t, s)
| _ => raise SubstitutionBug
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)
end
(case findSubstForVar (v,s) of
NONE =>
let
val (e, ei) = applySubstsToExp s (e, emptyExpandInfo)
val s = addSubst (v,WITH_TYPE e) s
in
s
end
| SOME (WITH_TYPE t) => mgu (e, t, s)
| _ => raise SubstitutionBug
)
| 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)
val s = addSubst (v,WITH_TYPE e) s
in
s
end
| SOME (WITH_TYPE t) => mgu (e, t, s)
| SOME (WITH_TYPE t) => mgu (t, e, s)
| _ => raise SubstitutionBug
)
| mgu (t1,t2,s) =
......
......@@ -57,12 +57,12 @@ export =
fitree-removeMin
fitree-fold
#type intset = bbtree [a=int]
#type fitree = bbtree [a={lo:int,hi:int}]
#type intset = bbtree [elem=int]
#type fitree = bbtree [elem={lo:int,hi:int}]
type bbtree =
type bbtree[elem] =
Lf
| Br of {size: int, left: bbtree, right: bbtree, payload: int}
| Br of {size: int, left: bbtree, right: bbtree, payload: elem}
val bbtree-size t =
case t of
......
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