Commit 5b074d61 authored by Axel Simon's avatar Axel Simon
Browse files

fix bug in substitution

parent 37735699
......@@ -272,24 +272,6 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
in
(E.SymbolSet.empty, env)
end
(*| infDecl (st,env) (AST.STATEdecl l) =
let
val envState = E.pushSymbol (stateSymId, SymbolTable.noSpan, env)
val extBVar = BD.freshBVar ()
val extVar = VAR (TVar.freshTVar (), extBVar)
val env = E.meetBoolean (BD.meetVarZero extBVar, env)
val env = E.pushType (false, extVar, env)
val fieldBVar = BD.freshBVar ()
val env = E.meetBoolean (BD.meetVarOne fieldBVar, env)
val env = List.foldl (fn ((_,_,e), env) => infExp (st,env) e) env l
val fieldList = List.rev (List.map (fn (v,_,_) => (fieldBVar,v)) l)
val env = E.reduceToRecord (fieldList, env)
val env = E.meet (envState, env)
val env = E.clearFunction (stateSymId, env)
val env = E.popToFunction (stateSymId, env)
in
checkUsages false (stateSymId, env)
end*)
| infDecl stenv (AST.DECODEdecl dd) = infDecodedecl stenv dd
| infDecl (st,env) (AST.LETRECdecl (v,l,e)) =
infBinding (st,env) (v, l, e)
......@@ -308,7 +290,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
checkUsages false (v,env)
(E.SymbolSet.singleton v, env)
end
| infDecodedecl (st,env) (v, l, Sum.INR el) =
let
......@@ -326,7 +308,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
checkUsages false (v,env)
(E.SymbolSet.singleton v, env)
end
and infExp stenv (AST.MARKexp m) = reportError infExp stenv m
......
......@@ -445,14 +445,14 @@ end = struct
"-" ^ Int.toString(Position.toInt p2) ^
"@" ^ #2 (List.foldl showSym ("","") ctxt) ^
":" ^ tStr
,", ", si)
,"\n\tuse at ", si)
end
fun printB ({name,ty,width,uses}, (str, si)) =
let
val (tStr, si) = prBTyOpt (ty, " : ", si)
val (wStr, si) = prTyOpt (width, ", width = ", si)
val (uStr, _, si) =
List.foldl printU ("", "\n uses: ", si)
List.foldl printU ("", "\n\tuse at ", si)
(SpanMap.listItemsi uses)
in
(str ^
......@@ -1080,20 +1080,11 @@ end = struct
in
if isEmpty substs then (ei, bFun, env1) else
let
(*val (sStr, si) = showSubstsSI (substs, TVar.emptyShowInfo)
val (eStr, si) = topToStringSI (env, si)
val _ = TextIO.print ("applySubst " ^ sStr ^ " to\n" ^ eStr)*)
val (b1, env1) = Scope.unwrap env1
val (b2, env2) = Scope.unwrap env2
val (b1, ei) = substBinding (b1, ei)
val (b2, ei) = substBinding (b2, ei)
val _ = case (b1,b2) of
(KAPPA {ty=t1}, KAPPA {ty=t2}) =>
if TVar.isEmpty (TVar.difference (texpVarset (t1,TVar.empty), texpVarset (t2,TVar.empty))) then () else
(TextIO.print ("t1=" ^ showType t1 ^ "\nt2=" ^ showType t2 ^ "\nexpand info:\n" ^ #1 (showExpandInfoSI (ei,TVar.emptyShowInfo)) ^ "\n")
;raise InferenceBug)
| _ => ()
val (b,bFun) = uniteFlowInfo (b1, b2, bFun)
val (b1', ei) = substBinding (b1, ei)
val (b2', ei) = substBinding (b2, ei)
val (b,bFun) = uniteFlowInfo (b1', b2', bFun)
val (ei, bFun, env) =
applySubsts (substs, ei, bFun, false, env1, env2)
in
......@@ -1154,7 +1145,7 @@ end = struct
Scope.update (sym, fn x => x,
(scs, Scope.setCtxt (sym :: Scope.getCtxt state) state))
fun pushFunctionOrTop (sym, env) =
(*fun pushFunctionOrTop (sym, env) =
let
val tyRef = ref UNIT
val bFunRef = ref BD.empty
......@@ -1173,6 +1164,20 @@ end = struct
val env = pushFunction (sym,env)
in
Scope.wrap (KAPPA {ty = !tyRef}, env)
end*)
fun pushFunctionOrTop (sym, env) =
let
fun setType (COMPOUND {ty = SOME (t,bFun), width, uses}, cons) =
(COMPOUND {ty = SOME (t,bFun), width = width, uses = uses}, cons)
| setType (COMPOUND {ty = NONE, width, uses}, cons) =
(COMPOUND {ty = SOME (freshVar (),BD.empty), width = width, uses = uses}, cons)
| setType _ = raise InferenceBug
val env = Scope.update (sym, setType, env)
val env = pushSymbol (sym, SymbolTable.noSpan, env)
val env = pushFunction (sym,env)
in
env
end
fun unify (env1, env2, substs) =
......
......@@ -217,7 +217,7 @@ structure Types = struct
(if concisePrint then "" else BD.showVar b)
^ ":...}"
| sT (p, MONAD (r,f,t)) = br (p, p_tyn, "S " ^ sT (p_tyn+1, r)) ^
" <" ^ sT (p_app+1, f) ^ " -> " ^ sT (p_app, t) ^ ">"
" <" ^ sT (p_app+1, f) ^ " => " ^ sT (p_app, t) ^ ">"
| sT (p, VAR (v,b)) = showVar v ^
(if concisePrint then "" else BD.showVar b)
and showVar var = let
......
......@@ -259,18 +259,19 @@ end = struct
| aS (CONST c) = CONST c
| aS (ALG (ty, l)) = ALG (ty, List.map aS l)
| aS (RECORD (var, b, fs)) =
let
val (fs, ei) = applySubstToRFields subst (fs, !eiRef)
in
if TVar.eq (var, v) then
case addToExpandInfo (var, b, target, !eiRef) of
case addToExpandInfo (var, b, target, ei) of
(target,ei) => (eiRef := ei; case target of
WITH_FIELD (newFs, newVar, newBVar) =>
RECORD (newVar, newBVar, List.foldl insertField fs newFs)
| WITH_TYPE _ => raise SubstitutionBug
)
else let
val (fs, ei) = applySubstToRFields subst (fs, !eiRef)
in
else
(eiRef := ei; RECORD (var, b, fs))
end
end
| aS (MONAD (r,f,t)) = MONAD (aS r,aS f,aS t)
| aS (VAR (var,b)) = if TVar.eq (var, v) then
case addToExpandInfo (var, b, target, !eiRef) of
......@@ -331,7 +332,10 @@ end = struct
occursCheck (v2, WITH_FIELD (fs, v3, bv3))
end
and occursCheck (v2, WITH_TYPE t2) =
and occursCheck (v2, WITH_TYPE (t2 as (VAR _))) = (v2, WITH_TYPE t2)
(* the previous case ensures that we don't get annoying error
messages like a/a is an infinite substitution *)
| occursCheck (v2, WITH_TYPE t2) =
if TVar.member(texpVarset (t2, TVar.empty),v2) then
let
val (vStr,si) = TVar.varToString (v2,TVar.emptyShowInfo)
......
granularity = 8
export = main decode
export = / decode
# Optional arguments
#
......@@ -30,6 +30,27 @@ val set-addrsz = update@{addrsz='1'}
## Decoding prefixes
val failOver first second = do
update@{tab=second};
r <- first;
update@{tab=42};
return r
end
val continue = do
t <- query$tab;
update@{tab=42};
r <- t;
update@{tab=t};
return r
end
val /66 [] = continue
val /f2 [] = continue
val /f3 [] = continue
val /legacy-p [0x2e] = do clear-rex; set-CS end
val /legacy-p [0x36] = do clear-rex; set-SS end
val /legacy-p [0x3e] = do clear-rex; set-DS end
......@@ -55,123 +76,105 @@ val p/66 [0xf3] = do set-rep; p/66/f3 end
val p/66 [0x66] = do set-opndsz; p/66 end
val p/66 [/legacy-p] = p/66
val p/66 [/rex-p] = p/66
val p/66 [] = do set-tab /; /66 end
val p/66 [] = failOver /66 /
val p/f2 [0x66] = do set-opndsz; p/f2/66 end
val p/f2 [0xf2] = do set-repne; p/f2 end
val p/f2 [0xf3] = do set-rep; p/f2/f3 end
val p/f2 [/legacy-p] = p/f2
val p/f2 [/rex-p] = p/f2
val p/f2 [] = do set-tab /; /f2 end
val p/f2 [] = failOver /f2 /
val p/f3 [0x66] = do set-opndsz; p/f3/66 end
val p/f3 [0xf2] = do set-repne; p/f3/f2 end
val p/f3 [0xf3] = do set-rep; p/f3 end
val p/f3 [/legacy-p] = p/f3
val p/f3 [/rex-p] = p/f3
val p/f3 [] = do set-tab /; /f3 end
val p/f3 [] = failOver /f3 /
val p/f2/f3 [0x66] = do set-opndsz; p/f2/f3/66 end
val p/f2/f3 [0xf2] = do set-repne; p/f3/f2 end
val p/f2/f3 [0xf3] = do set-rep; p/f2/f3 end
val p/f2/f3 [/legacy-p] = p/f2/f3
val p/f2/f3 [/rex-p] = p/f2/f3
val p/f2/f3 [] = do set-tab p/f2; /f3 end
val p/f2/f3 [] = failOver /f3 p/f2
val p/f3/f2 [0x66] = do set-opndsz; p/f2/f3/66 end
val p/f3/f2 [0xf2] = do set-repne; p/f3/f2 end
val p/f3/f2 [0xf3] = do set-rep; p/f2/f3 end
val p/f3/f2 [/legacy-p] = p/f3/f2
val p/f3/f2 [/rex-p] = p/f3/f2
val p/f3/f2 [] = do set-tab p/f3; /f2 end
val p/f3/f2 [] = failOver /f2 p/f3
val p/66/f2 [0x66] = do set-opndsz; p/f2/66 end
val p/66/f2 [0xf2] = do set-repne; p/66/f2 end
val p/66/f2 [0xf3] = do set-rep; p/66/f2/f3 end
val p/66/f2 [/legacy-p] = p/66/f2
val p/66/f2 [/rex-p] = p/66/f2
val p/66/f2 [] = do set-tab p/66; /f2 end
val p/66/f2 [] = failOver /f2 p/66
val p/66/f3 [0x66] = do set-opndsz; p/f3/66 end
val p/66/f3 [0xf2] = do set-repne; p/66/f3/f2 end
val p/66/f3 [0xf3] = do set-rep; p/66/f3 end
val p/66/f3 [/legacy-p] = p/66/f3
val p/66/f3 [/rex-p] = p/66/f3
val p/66/f3 [] = do set-tab p/66; /f3 end
val p/66/f3 [] = failOver /f3 p/66
val p/f2/66 [0x66] = do set-opndsz; p/f2/66 end
val p/f2/66 [0xf2] = do set-repne; p/66/f2 end
val p/f2/66 [0xf3] = do set-rep; p/f2/66/f3 end
val p/f2/66 [/legacy-p] = p/f2/66
val p/f2/66 [/rex-p] = p/f2/66
val p/f2/66 [] = do set-tab p/f2; /66 end
val p/f2/66 [] = failOver /66 p/f2
val p/f3/66 [0x66] = do set-opndsz; p/f3/66 end
val p/f3/66 [0xf2] = do set-repne; p/f3/66/f2 end
val p/f3/66 [0xf3] = do set-rep; p/66/f3 end
val p/f3/66 [/legacy-p] = p/f3/66
val p/f3/66 [/rex-p] = p/f3/66
val p/f3/66 [] = do set-tab p/f3; /66 end
val p/f3/66 [] = failOver /66 p/f3
val p/66/f2/f3 [0x66] = do clear-rex; p/f2/f3/66 end
val p/66/f2/f3 [0xf2] = do clear-rex; p/66/f3/f2 end
val p/66/f2/f3 [0xf3] = do clear-rex; p/66/f2/f3 end
val p/66/f2/f3 [/legacy-p] = p/66/f2/f3
val p/66/f2/f3 [/rex-p] = p/66/f2/f3
val p/66/f2/f3 [] = do set-tab p/66/f2; /f3 end
val p/66/f2/f3 [] = failOver /f3 p/66/f2
val p/66/f3/f2 [0x66] = do clear-rex; p/f3/f2/66 end
val p/66/f3/f2 [0xf2] = do clear-rex; p/66/f3/f2 end
val p/66/f3/f2 [0xf3] = do clear-rex; p/66/f2/f3 end
val p/66/f3/f2 [/legacy-p] = p/66/f3/f2
val p/66/f3/f2 [/rex-p] = p/66/f3/f2
val p/66/f3/f2 [] = do set-tab p/66/f3; /f2 end
val p/66/f3/f2 [] = failOver /f2 p/66/f3
val p/f3/f2/66 [0x66] = do clear-rex; p/f3/f2/66 end
val p/f3/f2/66 [0xf2] = do clear-rex; p/f3/66/f2 end
val p/f3/f2/66 [0xf3] = do clear-rex; p/f2/66/f3 end
val p/f3/f2/66 [/legacy-p] = p/f3/f2/66
val p/f3/f2/66 [/rex-p] = p/f3/f2/66
val p/f3/f2/66 [] = do set-tab p/f3/f2; /66 end
val p/f3/f2/66 [] = failOver /66 p/f3/f2
val p/f2/f3/66 [0x66] = do clear-rex; p/f2/f3/66 end
val p/f2/f3/66 [0xf2] = do clear-rex; p/f3/66/f2 end
val p/f2/f3/66 [0xf3] = do clear-rex; p/f2/66/f3 end
val p/f2/f3/66 [/legacy-p] = p/f2/f3/66
val p/f2/f3/66 [/rex-p] = p/f2/f3/66
val p/f2/f3/66 [] = do set-tab p/f2/f3; /66 end
val p/f2/f3/66 [] = failOver /66 p/f2/f3
val p/f3/66/f2 [0x66] = do clear-rex; p/f3/f2/66 end
val p/f3/66/f2 [0xf2] = do clear-rex; p/f3/66/f2 end
val p/f3/66/f2 [0xf3] = do clear-rex; p/66/f2/f3 end
val p/f3/66/f2 [/legacy-p] = p/f3/66/f2
val p/f3/66/f2 [/rex-p] = p/f3/66/f2
val p/f3/66/f2 [] = do set-tab p/f3/66; /f2 end
val p/f3/66/f2 [] = failOver /f2 p/f3/66
val p/f2/66/f3 [0x66] = do clear-rex; p/f2/f3/66 end
val p/f2/66/f3 [0xf2] = do clear-rex; p/66/f3/f2 end
val p/f2/66/f3 [0xf3] = do clear-rex; p/f2/66/f3 end
val p/f2/66/f3 [/legacy-p] = p/f2/66/f3
val p/f2/66/f3 [/rex-p] = p/f2/66/f3
val p/f2/66/f3 [] = do set-tab p/f2/66; /f3 end
val /66 [] = do
tab <- get-tab;
tab
end
val /f2 [] = do
tab <- get-tab;
tab
end
val /f3 [] = do
tab <- get-tab;
tab
end
val set-tab tab = update@{tab=tab}
val get-tab = query$tab
val p/f2/66/f3 [] = failOver /f3 p/f2/66
### MOV
val / [0x51]
......@@ -199,9 +202,6 @@ val decode = do
p64
end
val setTab tab = update@{tab=tab}
val getTab = query$tab
val & giveA giveB = do
a <- giveA;
b <- giveB;
......
......@@ -51,6 +51,32 @@ val set-addrsz = update@{addrsz='1'}
## Decoding prefixes
# The functions 'failOver' and 'continue' are used to try different decoders
# in sequence. The first function takes two arguments and runs the first
# one until it calls 'continue', at which point the second decoder is run.
val failOver first second = do
update@{tab=second};
r <- first;
update@{tab=42}; # make the type checker happy
return r
end
val continue = do
t <- query$tab;
update@{tab=42}; # make the type checker happy
r <- t;
update@{tab=t}; # make the type checker happy
return r
end
val /66 [] = continue
val /f2 [] = continue
val /f3 [] = continue
val /legacy-p [0x2e] = do clear-rex; set-CS end
val /legacy-p [0x36] = do clear-rex; set-SS end
val /legacy-p [0x3e] = do clear-rex; set-DS end
......@@ -276,123 +302,105 @@ val p/66 [0xf3] = do set-rep; p/66/f3 end
val p/66 [0x66] = do set-opndsz; p/66 end
val p/66 [/legacy-p] = p/66
val p/66 [/rex-p] = p/66
val p/66 [] = do set-tab /; /66 end
val p/66 [] = failOver /66 /
val p/f2 [0x66] = do set-opndsz; p/f2/66 end
val p/f2 [0xf2] = do set-repne; p/f2 end
val p/f2 [0xf3] = do set-rep; p/f2/f3 end
val p/f2 [/legacy-p] = p/f2
val p/f2 [/rex-p] = p/f2
val p/f2 [] = do set-tab /; /f2 end
val p/f2 [] = failOver /f2 /
val p/f3 [0x66] = do set-opndsz; p/f3/66 end
val p/f3 [0xf2] = do set-repne; p/f3/f2 end
val p/f3 [0xf3] = do set-rep; p/f3 end
val p/f3 [/legacy-p] = p/f3
val p/f3 [/rex-p] = p/f3
val p/f3 [] = do set-tab /; /f3 end
val p/f3 [] = failOver /f3 /
val p/f2/f3 [0x66] = do set-opndsz; p/f2/f3/66 end
val p/f2/f3 [0xf2] = do set-repne; p/f3/f2 end
val p/f2/f3 [0xf3] = do set-rep; p/f2/f3 end
val p/f2/f3 [/legacy-p] = p/f2/f3
val p/f2/f3 [/rex-p] = p/f2/f3
val p/f2/f3 [] = do set-tab p/f2; /f3 end
val p/f2/f3 [] = failOver /f3 p/f2
val p/f3/f2 [0x66] = do set-opndsz; p/f2/f3/66 end
val p/f3/f2 [0xf2] = do set-repne; p/f3/f2 end
val p/f3/f2 [0xf3] = do set-rep; p/f2/f3 end
val p/f3/f2 [/legacy-p] = p/f3/f2
val p/f3/f2 [/rex-p] = p/f3/f2
val p/f3/f2 [] = do set-tab p/f3; /f2 end
val p/f3/f2 [] = failOver /f2 p/f3
val p/66/f2 [0x66] = do set-opndsz; p/f2/66 end
val p/66/f2 [0xf2] = do set-repne; p/66/f2 end
val p/66/f2 [0xf3] = do set-rep; p/66/f2/f3 end
val p/66/f2 [/legacy-p] = p/66/f2
val p/66/f2 [/rex-p] = p/66/f2
val p/66/f2 [] = do set-tab p/66; /f2 end
val p/66/f2 [] = failOver /f2 p/66
val p/66/f3 [0x66] = do set-opndsz; p/f3/66 end
val p/66/f3 [0xf2] = do set-repne; p/66/f3/f2 end
val p/66/f3 [0xf3] = do set-rep; p/66/f3 end
val p/66/f3 [/legacy-p] = p/66/f3
val p/66/f3 [/rex-p] = p/66/f3
val p/66/f3 [] = do set-tab p/66; /f3 end
val p/66/f3 [] = failOver /f3 p/66
val p/f2/66 [0x66] = do set-opndsz; p/f2/66 end
val p/f2/66 [0xf2] = do set-repne; p/66/f2 end
val p/f2/66 [0xf3] = do set-rep; p/f2/66/f3 end
val p/f2/66 [/legacy-p] = p/f2/66
val p/f2/66 [/rex-p] = p/f2/66
val p/f2/66 [] = do set-tab p/f2; /66 end
val p/f2/66 [] = failOver /66 p/f2
val p/f3/66 [0x66] = do set-opndsz; p/f3/66 end
val p/f3/66 [0xf2] = do set-repne; p/f3/66/f2 end
val p/f3/66 [0xf3] = do set-rep; p/66/f3 end
val p/f3/66 [/legacy-p] = p/f3/66
val p/f3/66 [/rex-p] = p/f3/66
val p/f3/66 [] = do set-tab p/f3; /66 end
val p/f3/66 [] = failOver /66 p/f3
val p/66/f2/f3 [0x66] = do clear-rex; p/f2/f3/66 end
val p/66/f2/f3 [0xf2] = do clear-rex; p/66/f3/f2 end
val p/66/f2/f3 [0xf3] = do clear-rex; p/66/f2/f3 end
val p/66/f2/f3 [/legacy-p] = p/66/f2/f3
val p/66/f2/f3 [/rex-p] = p/66/f2/f3
val p/66/f2/f3 [] = do set-tab p/66/f2; /f3 end
val p/66/f2/f3 [] = failOver /f3 p/66/f2
val p/66/f3/f2 [0x66] = do clear-rex; p/f3/f2/66 end
val p/66/f3/f2 [0xf2] = do clear-rex; p/66/f3/f2 end
val p/66/f3/f2 [0xf3] = do clear-rex; p/66/f2/f3 end
val p/66/f3/f2 [/legacy-p] = p/66/f3/f2
val p/66/f3/f2 [/rex-p] = p/66/f3/f2
val p/66/f3/f2 [] = do set-tab p/66/f3; /f2 end
val p/66/f3/f2 [] = failOver /f2 p/66/f3
val p/f3/f2/66 [0x66] = do clear-rex; p/f3/f2/66 end
val p/f3/f2/66 [0xf2] = do clear-rex; p/f3/66/f2 end
val p/f3/f2/66 [0xf3] = do clear-rex; p/f2/66/f3 end
val p/f3/f2/66 [/legacy-p] = p/f3/f2/66
val p/f3/f2/66 [/rex-p] = p/f3/f2/66
val p/f3/f2/66 [] = do set-tab p/f3/f2; /66 end
val p/f3/f2/66 [] = failOver /66 p/f3/f2
val p/f2/f3/66 [0x66] = do clear-rex; p/f2/f3/66 end
val p/f2/f3/66 [0xf2] = do clear-rex; p/f3/66/f2 end
val p/f2/f3/66 [0xf3] = do clear-rex; p/f2/66/f3 end
val p/f2/f3/66 [/legacy-p] = p/f2/f3/66
val p/f2/f3/66 [/rex-p] = p/f2/f3/66
val p/f2/f3/66 [] = do set-tab p/f2/f3; /66 end
val p/f2/f3/66 [] = failOver /66 p/f2/f3
val p/f3/66/f2 [0x66] = do clear-rex; p/f3/f2/66 end
val p/f3/66/f2 [0xf2] = do clear-rex; p/f3/66/f2 end
val p/f3/66/f2 [0xf3] = do clear-rex; p/66/f2/f3 end
val p/f3/66/f2 [/legacy-p] = p/f3/66/f2
val p/f3/66/f2 [/rex-p] = p/f3/66/f2
val p/f3/66/f2 [] = do set-tab p/f3/66; /f2 end
val p/f3/66/f2 [] = failOver /f2 p/f3/66
val p/f2/66/f3 [0x66] = do clear-rex; p/f2/f3/66 end
val p/f2/66/f3 [0xf2] = do clear-rex; p/66/f3/f2 end
val p/f2/66/f3 [0xf3] = do clear-rex; p/f2/66/f3 end
val p/f2/66/f3 [/legacy-p] = p/f2/66/f3
val p/f2/66/f3 [/rex-p] = p/f2/66/f3
val p/f2/66/f3 [] = do set-tab p/f2/66; /f3 end
val /66 [] = do
tab <- get-tab;
tab
end
val /f2 [] = do
tab <- get-tab;
tab
end
val /f3 [] = do
tab <- get-tab;
tab
end
val set-tab tab = update@{tab=tab}
val get-tab = query$tab
val p/f2/66/f3 [] = failOver /f3 p/f2/66
datatype register =
AL
......
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