Commit b32df83f authored by mb0's avatar mb0
Browse files

Merge.

parent 5e52e8a7
......@@ -131,11 +131,10 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(* define a second traversal that is a full inference of the tree *)
(*local helper function to infer types for a binding group*)
val maxIter = 2
fun checkUsages printWarn (sym, env) =
val maxIter = 3
fun calcSubset printWarn env =
let
(*val _ = TextIO.print ("***** usages of " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ "\n")*)
fun checkUsage (s, (unstable, env)) =
fun checkUsage sym (s, unstable) =
let
val fs = E.getContextOfUsage (sym, s, env)
val oldCtxt = E.getCtxt env
......@@ -145,21 +144,8 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(*val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)*)
val envCall = E.pushUsage (sym, s, !sm, env)
(*val _ = TextIO.print ("pushed usage:\n" ^ E.topToString envCall)*)
(*inform about a unification failure when checking call site
with definition*)
fun raiseError str =
let
val si = TVar.emptyShowInfo
val (sFun, si) = E.kappaToStringSI (envFun, si)
val (sCall, si) = E.kappaToStringSI (envCall, si)
in
(Error.errorAt (errStrm, s, [str,
" when checking call to ",
SymbolTable.getString(!SymbolTables.varTable, sym),
"\n\tcall provides type " ^ sCall,
"\n\tdefinition has type " ^ sFun]))
end
(*warn about refinement of definition due to a call site*)
(*warn about refinement of the definition due to a call site*)
fun raiseWarning (substs, syms) =
if E.SymbolSet.isEmpty syms orelse not printWarn then ()
else
......@@ -172,49 +158,99 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(!SymbolTables.varTable, sym)
val (sType, si) = E.funTypeToStringSI (env, sym, si)
in
(res ^ pre ^ sStr ^ " : " ^ sType, ", ", si)
(res ^ pre ^ sStr ^ " : " ^ sType, "\n\tand call ", si)
end
val (symsStr, _, _) =
List.foldl showSyms ("", "", si)
List.foldl showSyms ("","\n\tfor call ", si)
(E.SymbolSet.listItems syms)
in
(Error.warningAt (errStrm, s, [
"call to ",
SymbolTable.getString(!SymbolTables.varTable, sym),
" requires refinement ", sSubst,
"\n\tfor " ^ symsStr]))
symsStr]))
end
val substs = E.subseteq (envCall, envFun)
val affectedSyms = E.affectedFunctions (substs,env)
(*val (sStr, si) = S.showSubstsSI (substs, TVar.emptyShowInfo)
val _ = TextIO.print ("subset: subst=:" ^ sStr ^ ", unstable: " ^
List.foldl (fn (sym, res) => res ^ ", " ^ SymbolTable.getString
(!SymbolTables.varTable, sym)) "" (E.SymbolSet.listItems affectedSyms) ^ "\n")*)
val _ = raiseWarning (substs, affectedSyms)
in
if E.SymbolSet.isEmpty affectedSyms then unstable else
E.SymbolSet.add (unstable, sym)
end
handle (S.UnificationFailure str) =>
E.SymbolSet.add (unstable, sym)
fun checkUsages (sym, unstable) =
let
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 unstable = List.foldl (checkUsage sym) unstable usages
in
unstable
end
in
List.foldl checkUsages E.SymbolSet.empty (E.getGroupSyms env)
end
fun calcIteration (unstable, env) =
let
fun checkUsage sym (s, env) =
let
val fs = E.getContextOfUsage (sym, s, env)
val oldCtxt = E.getCtxt env
val env = List.foldl E.pushFunction env fs
val envFun = E.pushSymbol (sym, s, env)
(*val _ = TextIO.print ("pushed instance " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ " symbol:\n" ^ E.topToString envFun)*)
val envCall = E.pushUsage (sym, s, !sm, env)
(*val _ = TextIO.print ("pushed usage:\n" ^ E.topToString envCall)*)
(*inform about a unification failure when checking call site
with definition*)
fun raiseError str =
let
val si = TVar.emptyShowInfo
val (sFun, si) = E.kappaToStringSI (envFun, si)
val (sCall, si) = E.kappaToStringSI (envCall, si)
in
(Error.errorAt (errStrm, s, [str,
" when checking call to ",
SymbolTable.getString(!SymbolTables.varTable, sym),
"\n\tcall provides type " ^ sCall,
"\n\tdefinition has type " ^ sFun]))
end
val (substs, env) = (E.subseteq (envCall, envFun),
E.meetFlow (envCall, envFun))
val env = E.meetFlow (envCall, envFun)
handle (S.UnificationFailure str) =>
(raiseError str; (S.emptySubsts, envCall))
(raiseError str; envCall)
val (changed, env) = E.popToUsage (sym, s, oldCtxt, env)
val _ = sm := List.foldl
(fn (sym,sm) => (sym, E.getFunctionInfo (sym, env)) ::
List.filter (fn (s,_) =>
not (SymbolTable.eq_symid(s,sym))) sm)
(!sm) changed
val affectedSyms = E.affectedFunctions (substs,envCall)
val _ = raiseWarning (substs, affectedSyms)
in
(E.SymbolSet.union (unstable, affectedSyms), env)
env
end
fun calcUsages (sym, env) =
let
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 env = List.foldl (checkUsage sym) env usages
in
env
end
in
List.foldl checkUsage (E.SymbolSet.empty, env) (E.getUsages (sym, env))
List.foldl calcUsages env (E.SymbolSet.listItems unstable)
end
fun checkCallSites printWarn (syms, env) =
List.foldl (fn (sym, (unstable, env)) =>
case checkUsages printWarn (sym, env) of
(newUnstable, env) =>
(E.SymbolSet.union (unstable,newUnstable), env)
) (E.SymbolSet.empty, env) (E.SymbolSet.listItems syms)
fun calcFixpoint curIter (syms, env) =
if E.SymbolSet.isEmpty syms then env else
fun calcFixpoint curIter env =
case calcSubset (curIter>0) env of unstable =>
if E.SymbolSet.isEmpty unstable then env else
if curIter<maxIter then
calcFixpoint (curIter+1)
(checkCallSites (curIter=maxIter) (syms, env))
calcFixpoint (curIter+1) (calcIteration (unstable,env))
else
let
val si = TVar.emptyShowInfo
......@@ -227,7 +263,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
in
(res ^ pre ^ sStr ^ " : " ^ sType, ", ", si)
end
val symIds = E.SymbolSet.listItems syms
val symIds = E.SymbolSet.listItems unstable
val (symsStr, _, _) = List.foldl showSyms ("", "", si) symIds
val s = case symIds of [] => raise TypeError | (sym :: _) =>
SymbolTable.getSpan(!SymbolTables.varTable, sym)
......@@ -235,7 +271,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(Error.errorAt (errStrm, s, [
"no typing found for ",
symsStr,
"\n\tpass --inference-iterations=",
"\tpass --inference-iterations=",
Int.toString (maxIter+1),
" to try a little harder"]); env)
end
......@@ -280,9 +316,8 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val env = E.popToFunction (sym, env)
val fInfo = E.getFunctionInfo (sym, env)
val _ = sm := (sym, fInfo) :: !sm
val (unstable, env) = checkUsages false (sym, env)
in
(unstable, env)
env
end
and infDecl stenv (AST.MARKdecl m) = reportError infDecl stenv m
......@@ -293,12 +328,11 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val env = E.meet (envGra, envInt)
val env = E.popKappa env
in
(E.SymbolSet.empty, env)
env
end
| infDecl stenv (AST.DECODEdecl dd) = infDecodedecl stenv dd
| infDecl (st,env) (AST.LETRECdecl (v,l,e)) =
infBinding (st,env) (v, l, e)
| infDecl (st,env) _ = (E.SymbolSet.empty, env)
| infDecl (st,env) (AST.LETRECdecl (v,l,e)) = infBinding (st,env) (v, l, e)
| infDecl (st,env) _ = env
and infDecodedecl (st,env) (v, l, Sum.INL e) =
let
......@@ -313,7 +347,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
not (SymbolTable.eq_symid(s,v))) (!sm)
in
(E.SymbolSet.singleton v, env)
env
end
| infDecodedecl (st,env) (v, l, Sum.INR el) =
let
......@@ -331,7 +365,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val _ = sm := (v, fInfo) :: List.filter (fn (s,_) =>
not (SymbolTable.eq_symid(s,v))) (!sm)
in
(E.SymbolSet.singleton v, env)
env
end
and infExp stenv (AST.MARKexp m) = reportError infExp stenv m
......@@ -339,12 +373,10 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
let
val names = List.map topLetrecDecl l
val env = E.pushGroup (List.concat names, env)
val (unstable, env) = List.foldl (fn ((v,l,e), (unstable, env)) =>
case infBinding (st, env) (v, l, e) of
(newUnstable, env) =>
(E.SymbolSet.union (newUnstable, unstable), env)
) (E.SymbolSet.empty, env) l
val env = calcFixpoint (unstable, env)
val env = List.foldl (fn ((v,l,e), env) =>
infBinding (st, env) (v, l, e)
) env l
val env = calcFixpoint env
val env = infExp (st,env) e
val (badSizes, env) = E.popGroup (env, true)
val _ = reportBadSizes badSizes
......@@ -700,14 +732,11 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(List.map topDecl (ast : SpecAbstractTree.specification))
, primEnv)
(*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
val (unstable, toplevelEnv) = List.foldl (fn (d,(unstable, env)) =>
(case infDecl ({span = SymbolTable.noSpan},env) d of
(newUnstable, env) =>
(E.SymbolSet.union (newUnstable, unstable), env))
handle TypeError => (unstable, env)
) (E.SymbolSet.empty, toplevelEnv)
(ast : SpecAbstractTree.specification)
val toplevelEnv = calcFixpoint (unstable, toplevelEnv)
val toplevelEnv = List.foldl (fn (d,env) =>
infDecl ({span = SymbolTable.noSpan},env) d
handle TypeError => env
) toplevelEnv (ast : SpecAbstractTree.specification)
val toplevelEnv = calcFixpoint toplevelEnv
handle TypeError => toplevelEnv
(*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
......
......@@ -30,6 +30,10 @@ structure Environment : sig
group*)
val popGroup : environment * bool ->
(Error.span * string) list * environment
(*ask for all the symbols in the binding group *)
val getGroupSyms : environment -> VarInfo.symid list
val pushTop : environment -> environment
(*pushes the given type onto the stack, if the flag is true, type variables
......@@ -553,6 +557,10 @@ end = struct
end
| _ => raise InferenceBug
fun getGroupSyms env = case Scope.unwrap env of
(GROUP bs, env) => List.map #name bs
| _ => raise InferenceBug
fun pushTop env =
let
val a = TVar.freshTVar ()
......
......@@ -48,13 +48,13 @@ end = struct
fun name idx = (if idx>25 then name (Int.div (idx,26)-1) else "") ^
Char.toString (Char.chr (Char.ord #"a"+Int.mod (idx,26)))
fun varToString (TVAR var, tab) = (name var, tab) (*case VarMap.find (tab, var) of
SOME str => (str, tab)
| NONE => let
val str = name (VarMap.numItems(tab))
in
(str, VarMap.insert(tab, var, str))
end *)
fun varToString (TVAR var, tab) = (*(name var, tab)*) case VarMap.find (tab, var) of
SOME str => (str, tab)
| NONE => let
val str = name (VarMap.numItems(tab))
in
(str, VarMap.insert(tab, var, str))
end
structure IntSet = SplaySetFn(struct
type ord_key = int
......
......@@ -539,8 +539,13 @@ type varity =
| VA4 of arity4
type insn =
ADC of arity2
AAA
| AAD of arity1
| AAM of arity1
| AAS
| ADC of arity2
| ADD of arity2
| ADDPD of arity2
| AND of arity2
| BSF of arity2
| BSR of arity2
......@@ -878,6 +883,7 @@ type insn =
| TEST of arity2
| UCOMISD of arity2
| UD2
| VADDPD of varity
| VCMPEQB of varity
| VCMPEQD of varity
| VCMPEQW of varity
......@@ -1692,6 +1698,27 @@ end
val one = return (IMM8 '00000001')
val // a =
do b <- a;
return (not b)
end
### AAA
### - ASCII Adjust After Addition
val / [0x37] | // mode64? = arity0 AAA
### AAD
### - ASCII Adjust AX Before Division
val / [0xd5] | // mode64? = unop AAD imm8
### AAM
### - ASCII Adjust AX After Multiply
val / [0xd4] | // mode64? = unop AAM imm8
### AAS
### - ASCII Adjust AL After Subtraction
val / [0x3f] | // mode64? = arity0 AAS
### ADC
### - Add with Carry
val / [0x14] = binop ADC al imm8
......@@ -1746,6 +1773,13 @@ val / [0x03 /r]
| rexw? = binop ADD r64 r/m64
| otherwise = binop ADD r32 r/m32
### ADDPD
### - Add Packed Double-Precision Floating-Point Values
val /66 [0x0f 0x58 /r] = binop ADDPD xmm128 xmm/m128
val /vex/66/0f/vexv [0x58 /r]
| vex128? = varity3 VADDPD xmm128 v/xmm xmm/m128
| vex256? = varity3 VADDPD ymm256 v/ymm ymm/m256
### AND
### - Logical AND
val / [0x24] = binop AND al imm8
......
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