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

improve error messages, again

parent ed9b2bfb
......@@ -220,7 +220,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
" when checking call to ",
SymbolTable.getString(!SymbolTables.varTable, sym),
"\n\tcall provides type " ^ sCall,
"\n\tdefinition has type " ^ sFun]))
"\tdefinition has type " ^ sFun]))
end
val env = E.meetFlow (envCall, envFun)
handle (S.UnificationFailure str) =>
......
......@@ -10,11 +10,13 @@ structure BooleanDomain : sig
val empty : bfun
type bvarset
val showVar : bvar -> string
val showBFun : bfun -> string
exception Unsatisfiable of bvar
exception Unsatisfiable of bvarset
val meetVarImpliesVar : bvar * bvar -> bfun -> bfun
......@@ -28,8 +30,6 @@ structure BooleanDomain : sig
val meetVarOne : bvar -> bfun -> bfun
type bvarset
val meetVarSetZero : bvarset -> bfun -> bfun
val meetVarSetOne : bvarset -> bfun -> bfun
......@@ -39,9 +39,9 @@ structure BooleanDomain : sig
val union : bvarset * bvarset -> bvarset
val addToSet : bvar * bvarset -> bvarset
val isRelated : bvar * bfun -> bvar -> bool
val member : bvarset * bvar -> bool
val setToString : bvarset -> string
val projectOnto : bvarset * bfun -> bfun
......@@ -99,6 +99,9 @@ end = struct
type bfun = units * clauses
structure IS = IntBinarySet
type bvarset = IS.set
val empty = (US.empty, CS.empty)
fun i v = Int.toString v
......@@ -117,12 +120,12 @@ end = struct
) ""
fun showBFun (us, cs) = showUS us ^ showCS cs
exception Unsatisfiable of bvar
exception Unsatisfiable of bvarset
fun addUnits ([], f) = f
| addUnits (v :: vs, f as (us, cs)) = (
(*TextIO.print ("asserting " ^ i v ^ " in:" ^ showBFun f ^ "\n"); *)
if US.member (us,~v) then raise (Unsatisfiable (BVAR (abs v))) else
if US.member (us,~v) then raise (Unsatisfiable (IS.singleton (abs v))) else
if US.member (us, v) then addUnits (vs, f) else
let
fun hasV (v1,v2) = v1=v orelse v1= ~v orelse v2=v orelse v2= ~v
......@@ -130,7 +133,7 @@ end = struct
fun ins v vs =
if List.exists (fn v' => v'=v) vs then vs else
if List.exists (fn v' => v'= ~v) vs then
raise Unsatisfiable (BVAR (abs v))
raise Unsatisfiable (IS.singleton (abs v))
else v :: vs
fun calcUnits ((v1,v2), units) = (
(*TextIO.print ("\nlooking at " ^ i v1 ^ " v " ^ i v2);*)
......@@ -152,6 +155,16 @@ end = struct
if v1=v2 then addUnits ([v1], f) else f
) else (us, CS.add' (if v1<v2 then (v1,v2) else (v2,v1), cs))
fun getRelated (vs, (us, cs)) =
let
val set = CS.foldl (fn ((v1,v2),set) =>
if IS.member(set,Int.abs v1) then IS.add' (Int.abs v2, set) else
if IS.member(set,Int.abs v2) then IS.add' (Int.abs v1, set) else set)
vs cs
in
set
end
(*fun meetVarImpliesVar (BVAR v1, BVAR v2) f = f
fun meetNotBoth (BVAR v1, BVAR v2, f) = f
fun meetEither (BVAR v1, BVAR v2, f) = f
......@@ -162,19 +175,33 @@ end = struct
fun meetVarImpliesVar (BVAR v1, BVAR v2) f = (
(*TextIO.print ("meet with " ^ i v1 ^ " -> " ^ i v2 ^ "\n");*)
if v1=v2 then f else addClause ((~v1,v2), f)
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (IS.add' (v1,IS.add'(v2,set)),f))
)
fun meetNotBoth (BVAR v1, BVAR v2, f) = addClause ((~v1,~v2),f)
fun meetEither (BVAR v1, BVAR v2, f) = addClause ((v1,v2),f)
fun meetNotBoth (BVAR v1, BVAR v2, f) =
addClause ((~v1,~v2),f)
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (IS.add' (v1,IS.add'(v2,set)),f))
fun meetEither (BVAR v1, BVAR v2, f) =
addClause ((v1,v2),f)
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (IS.add' (v1,IS.add'(v2,set)),f))
fun meetEqual (BVAR v1, BVAR v2, f) =
if v1=v2 then f else addClause ((~v1,v2), addClause ((~v2,v1),f))
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (IS.add' (v1,IS.add'(v2,set)),f))
fun meetVarOne (BVAR v) f = (
(*TextIO.print ("\nmeet with " ^ i v ^ " = t\n");*)
addUnits ([v], f)
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (IS.add' (v,set),f))
)
fun meetVarZero (BVAR v) f = (
(*TextIO.print ("\nmeet with " ^ i v ^ " = f\n");*)
addUnits ([~v], f)
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (IS.add' (v,set),f))
)
fun resolve ([], (us, cs)) = (us, cs)
......@@ -193,9 +220,6 @@ end = struct
resolve (vs, comb (us, cs) (posVars, negVars))
end
structure IS = IntBinarySet
type bvarset = IS.set
fun meetVarSetOne is f = (
addUnits (IS.listItems is, f)
)
......@@ -209,6 +233,8 @@ end = struct
fun addToSet (BVAR v, set) = IS.add' (v,set)
fun member (set, BVAR v) = IS.member(set, v)
fun setToString set =
let
fun show (v, (str, sep)) = (str ^ sep ^ i v, ", ")
......@@ -216,18 +242,6 @@ end = struct
#1 (List.foldl show ("{", "") (IS.listItems set)) ^ "}"
end
fun isRelated (BVAR v, (us, cs)) =
let
val set = CS.foldl (fn ((v1,v2),vs) =>
if IS.member(vs,Int.abs v1) then IS.add' (Int.abs v2, vs) else
if IS.member(vs,Int.abs v2) then IS.add' (Int.abs v1, vs) else vs)
(IS.singleton v) cs
(*val _ = TextIO.print ("bVar " ^ i v ^ " is related to " ^ setToString set ^
" in " ^ showBFun (us, cs) ^ "\n")*)
in
fn (BVAR var) => IS.member(set,var)
end
fun projectOnto (keep, (us, cs)) =
let
fun addBad (v,set) = if IS.member (keep,Int.abs v) then set
......@@ -273,6 +287,8 @@ end = struct
^ "\n")*)
in
List.foldl addClause (addUnits (newUnits, (us, cs))) newClauses
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (set,(us,cs)))
end
fun meet ((us1, cs1), (us2, cs2)) =
......@@ -281,6 +297,8 @@ end = struct
val cs1 = CS.difference (cs1,cs2)
in
CS.foldl addClause (addUnits (US.listItems us1,(us2, cs2))) cs1
handle Unsatisfiable set =>
raise Unsatisfiable (getRelated (getRelated (set,(us1,cs1)),(us1,cs1)))
end
(*val b1 = freshBVar ()
......
......@@ -754,24 +754,23 @@ end = struct
aF (SymbolSet.empty, substs, env)
end
fun affectedField (bVar, env as (scs,state)) =
fun affectedField (bVars, env as (scs,state)) =
let
val pred = BD.isRelated(bVar,Scope.getFlow state)
fun aF (_, SOME f) = SOME f
| aF (([],_), NONE) = NONE
| aF (env, NONE) = case Scope.unwrap env of
(KAPPA {ty = t}, env) =>
aF (env, fieldOfBVar (pred, t))
| (SINGLE {name, ty = t}, env) => aF (env, fieldOfBVar (pred, t))
aF (env, fieldOfBVar (bVars, t))
| (SINGLE {name, ty = t}, env) => aF (env, fieldOfBVar (bVars, t))
| (GROUP l, env) =>
let
fun findField ((_,t), SOME f) = SOME f
| findField ((_,t), NONE) = fieldOfBVar (pred, t)
| findField ((_,t), NONE) = fieldOfBVar (bVars, t)
fun aFL {name, ty = tOpt, width, uses} =
List.foldl findField
(case tOpt of
NONE => NONE
| SOME (t,_) => fieldOfBVar (pred, t))
| SOME (t,_) => fieldOfBVar (bVars, t))
(SpanMap.listItems uses)
in
aF (env, case List.mapPartial aFL l of
......@@ -1094,8 +1093,7 @@ end = struct
(t1,
ListPair.foldlEq (genImpl (t1,t2)) bFun
(texpBVarset (op ::) (t1, []), texpBVarset (op ::) (t2, []))
handle (BD.Unsatisfiable bVar) =>
flowError (bVar, affectedField (bVar, env1), [env1,env2]))
handle (BD.Unsatisfiable bVar) => flowError (bVar, NONE, [env1,env2]))
else
let
(*val _ = TextIO.print ("forcing bVars to be equal:" ^
......@@ -1276,8 +1274,7 @@ end = struct
val bVars = texpBVarset onlyInputs (t,[])
fun checkField bVar =
(case BD.meetVarZero bVar bFun of _ => NONE)
handle (BD.Unsatisfiable _) =>
fieldOfBVar (BD.isRelated (bVar,bFun),t)
handle (BD.Unsatisfiable bVars) => fieldOfBVar (bVars,t)
in
List.foldl (fn (bVar,fs) => case checkField bVar of
SOME f => f :: fs
......
......@@ -121,7 +121,7 @@ structure Types = struct
in (tCF co (e, BD.empty))
end
fun fieldOfBVar (pred, e) = let
fun fieldOfBVar (bVars, e) = let
fun takeIfSome (t,fo) = case ff t of SOME f => SOME f | NONE => fo
and ff (FUN (f1, f2)) = takeIfSome (f2,
case List.mapPartial ff f1 of
......@@ -141,7 +141,7 @@ structure Types = struct
| ff (MONAD (r,f,t)) = takeIfSome (r, (takeIfSome (f,ff t)))
| ff (VAR (b,_)) = NONE
and ffF (RField {name = n, fty = t, exists = b}) =
if pred b then SOME n else ff t
if BD.member(bVars,b) then SOME n else ff t
in ff e
end
......
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