Commit 46b6f4a4 authored by Axel Simon's avatar Axel Simon
Browse files

fix nested fixpoint computations

parent 0ecf0d21
......@@ -282,15 +282,14 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
fun checkUsage sym s =
let
val fid = E.getContextOfUsage (sym, s, env)
val env = E.enterFunction (fid,env)
val (n1,env) = E.pushNested (sym, env)
val (n2,env) = E.pushNested (fid, env)
val _ = TextIO.print ("subset, in context of " ^ SymbolTable.getString(!SymbolTables.varTable, fid) ^ ":\n" ^ E.toString env ^ "\n")
val envFun = E.pushSymbol (sym, s, false, env)
val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)
(*val _ = TextIO.print ("pushed instance (subset) " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)*)
val envCall = E.pushUsage (sym, s, env)
val _ = TextIO.print ("pushed usage:\n" ^ E.topToString envCall)
(*val _ = TextIO.print ("pushed usage (subset):\n" ^ E.topToString envCall)*)
(*warn about refinement of the definition due to a call site*)
fun raiseWarning (substs, syms) =
......@@ -329,7 +328,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
E.SymbolSet.isEmpty affectedSyms
end
val usages = E.getUsages (sym, env)
val _ = TextIO.print ("***** checking subset of " ^ Int.toString (List.length usages) ^ " usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")
(*val _ = TextIO.print ("***** checking subset of " ^ Int.toString (List.length usages) ^ " usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
in
List.all (checkUsage sym) usages
end
......@@ -347,13 +346,14 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
fun checkUsage (s, env) =
let
val fid = E.getContextOfUsage (sym, s, env)
val env = E.enterFunction (fid,env)
val (n1,env) = E.pushNested (sym, env)
val (n2,env) = E.pushNested (fid, env)
val envFun = E.pushSymbol (sym, s, false, env)
val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.kappaToString envFun)
(*val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.kappaToString envFun)*)
val envCall = E.pushUsage (sym, s, env)
val _ = TextIO.print ("pushed usage:\n" ^ E.kappaToString envCall)
(*val _ = TextIO.print ("pushed usage:\n" ^ E.kappaToString envCall)*)
(*inform about a unification failure when checking call site
with definition*)
fun raiseError str =
......@@ -371,14 +371,16 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val env = E.meetFlow (envCall, envFun)
handle (S.UnificationFailure str) =>
(raiseError str; envFun)
(*val _ = TextIO.print ("popping to usage of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ ":\n" ^ E.topToString env)*)
val env = E.popToUsage (sym, s, env)
val _ = TextIO.print ("popping to usage of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ ":\n" ^ E.toString env)
val env = E.popNested (n1+n2,env)
val env = E.leaveFunction (fid,env)
in
env
end
val usages = E.getUsages (sym, env)
val _ = TextIO.print ("***** re-eval of " ^ Int.toString (List.length usages) ^ " usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")
(*val _ = TextIO.print ("***** re-eval of " ^ Int.toString (List.length usages) ^ " usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
in
List.foldl checkUsage env usages
end
......@@ -530,7 +532,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(if not (hasSymbol (st,v)) then env else
infBinding (st, env) (v, l, e))
handle TypeError => env) env l
val _ = TextIO.print ("after checking local components " ^ prComp comp ^ E.topToString env)
(*val _ = TextIO.print ("after checking local components " ^ prComp comp ^ E.topToString env)*)
val env = case comp of
SCC.SIMPLE _ => env
| SCC.RECURSIVE syms => calcFixpoints (syms, env)
......@@ -544,7 +546,8 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val st' = List.foldl addComponent st sccs
val env = infExp (st',env) e
val (badSizes, env) = E.popGroup (env, true)
val _ = reportBadSizes badSizes
(*do not report bad sizes here since we must first calculate a
fixpoint to instantiate all variables maximally*)
in
env
end
......@@ -932,11 +935,11 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
infDecl ({span = SymbolTable.noSpan,
component = comp},env) d
handle TypeError => env) env ast
val _ = TextIO.print ("after checking component " ^ prComp comp ^ E.topToString env)
val env = case comp of
SCC.SIMPLE _ => env
| SCC.RECURSIVE syms => calcFixpoints (syms, env)
handle TypeError => env
(*val _ = TextIO.print ("after checking component " ^ prComp comp ^ E.topToString env)*)
in
env
end
......@@ -962,7 +965,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
| checkExports s _ = ()
val _ = List.app (checkExports SymbolTable.noSpan) ast
val _ = TextIO.print ("toplevel environment:\n" ^ E.topToString toplevelEnv)
(*val _ = TextIO.print ("toplevel environment:\n" ^ E.topToString toplevelEnv)*)
val (badSizes, primEnv) = E.popGroup (toplevelEnv, false)
val _ = reportBadSizes badSizes
......
......@@ -50,10 +50,9 @@ structure Environment : sig
existing type should be used (False) *)
val pushSymbol : VarInfo.symid * Error.span * bool * environment -> environment
(*in case the given symbol is not in the top-most group, search in the
nested definitions of the current function for definitions of the symbol
and push them onto the stack, returns the new stack and the number of
nested groups that had to be pushed*)
(*search in the current stack for the symbol and, if unsuccessful, in the
nested definitions and push all nested groups onto the stack, returns the
new stack and the number of nested groups that had to be pushed*)
val pushNested : VarInfo.symid * environment -> (int * environment)
(*pops the nested groups that were pushed by pushNested*)
......@@ -408,7 +407,8 @@ end = struct
in
upd ([],bs)
end
fun unravel (bs, env) = case unwrap env of
fun unravel (bs, ([],_)) = raise InferenceBug
| unravel (bs, env) = case unwrap env of
(b, env as (scs, cons)) =>
(case tryUpdate (b, cons) of
NONE => unravel (b::bs, env)
......@@ -569,14 +569,21 @@ end = struct
val (cStr, si) = SC.toStringSI (Scope.getSize state, SOME vs, si)
in
(siRef := si
; nStr ^ " : " ^ tStr ^ " has ambiguous vector sizes" ^
; nStr ^ " : call to " ^ tStr ^ " has ambiguous vector sizes" ^
(if String.size cStr=0 then "" else " where " ^ cStr))
end
val unbounded = List.foldl (fn
({name,ty=SOME (t,_),width,uses,nested},vs) =>
TVar.difference (vs, texpVarset (t,TVar.empty))
| (_,vs) => vs)
unbounded bs
fun remBoundVars ({name,ty=SOME (t,_),width,uses,nested=ns},vs) =
List.foldl remBoundVars
(TVar.difference (vs, texpVarset (t,TVar.empty)))
(List.concat (List.map (fn g => case g of
GROUP bs => bs
| _ => raise InferenceBug) ns))
| remBoundVars (_,vs) = vs
val unbounded = List.foldl remBoundVars unbounded bs
(*TODO: we should also descend into the nested definitions,
since the letrec expression cannot report ambigueties since
when letrec groups are popped, the fixpoint has not been
calculated yet*)
val badSizes = List.concat (
List.map (fn {name = n,ty,width,uses = us,nested} =>
List.map (fn (sp,t) => (sp, showUse (n, t))) (
......@@ -1295,7 +1302,8 @@ in () end;*)
else inScope (sym,env)
| (_,env) => inScope (sym,env)
fun pushNested (sym, env) = if inScope (sym,env) then (0,env) else
fun pushNested (sym, env) =
if inScope (sym,env) then (0,env) else
let
val (sc,_) = Scope.unwrap env
fun findSymInGroups (n, ns, env) =
......@@ -1308,12 +1316,12 @@ in () end;*)
(case List.find (fn {name, ty, width, uses, nested} =>
SymbolTable.eq_symid (sym,name)) bs of
SOME {name, ty, width, uses, nested} =>
SOME (n, enterFunction (name,env))
SOME (n, env)
| NONE =>
List.foldl (fn ({name, ty, width, uses, nested=ns},res) =>
case res of
SOME r => SOME r
| NONE => findSymInGroups (n, ns, enterFunction (name,env))
| NONE => findSymInGroups (n, ns, env)
) NONE bs
)
| findSymInGroup (n,_,env) = raise InferenceBug
......@@ -1324,24 +1332,24 @@ in () end;*)
end
fun popNested (n, env) =
(TextIO.print ("popping further " ^ Int.toString n ^ " scopes:\n" ^ topToString env);
if n<=0 then env else case Scope.unwrap env of
(GROUP bs, (scs,state)) =>
(GROUP bs, env) =>
let
val (curFun, remFuns) = case Scope.getCtxt state of
(curFun :: remFuns) => (curFun, remFuns)
| _ => raise InferenceBug
val state = Scope.setCtxt remFuns state
fun replGroup (GROUP bs' :: gs) =
if List.all (fn (b,b') =>
SymbolTable.eq_symid (#name b, #name b'))
(ListPair.zip (bs,bs'))
then GROUP bs :: gs else GROUP bs' :: replGroup gs
| replGroup _ = raise InferenceBug
fun action (COMPOUND {ty, width, uses, nested},cons) =
(COMPOUND {ty = ty, width = width,
uses = uses, nested = (GROUP bs) :: nested}, cons)
uses = uses, nested = replGroup nested}, cons)
| action _ = raise InferenceBug
val env = Scope.update (curFun, action, (scs,state))
val env = Scope.update (Scope.getCurFun (#2 env), action, env)
in
popNested (n-1,env)
end
| (_, env) => raise InferenceBug
)
fun clearFunction (sym, env) =
let
......
......@@ -44,7 +44,8 @@ end = struct
fun filter (vs, scs) =
let
fun hasDeadLeading {terms = (_,v)::_, const} = TVar.member (vs,v)
fun hasDeadLeading {terms = ts as (_::_), const} =
List.exists (fn (_,v) => TVar.member (vs,v)) ts
| hasDeadLeading _ = raise SizeConstraintBug
val scs = List.filter hasDeadLeading scs
in
......
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