Commit 1b3aff4c authored by Axel Simon's avatar Axel Simon
Browse files

project out Boolean variables from recursive calls when pushing function...

project out Boolean variables from recursive calls when pushing function symbol, fixes bug in type checking bbtree
parent f77c3ba8
......@@ -18,6 +18,8 @@ structure TypeInference : sig
end = struct
(*val debugSymbol = 128*)
structure AST = SpecAbstractTree
structure E = Environment
structure BD = BooleanDomain
......@@ -611,8 +613,13 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
let
val envFun = infExp (st,env) e1
val envArg = List.foldl (fn (e2,env) => infExp (st,env) e2) env es2
(*val _ = TextIO.print ("**** app func:\n" ^ E.topToString envFun)
val _ = TextIO.print ("**** app arg:\n" ^ E.topToString envArg)*)
(*val ctxt = E.getCtxt env
val _ = if List.all (fn x => SymbolTable.toInt x<>debugSymbol) ctxt then () else
TextIO.print ("**** app func:\n" ^ E.topToString envFun)
val _ = if List.all (fn x => SymbolTable.toInt x<>debugSymbol) ctxt then () else
TextIO.print ("**** app arg:\n" ^ E.topToString envArg)*)
val envArgRes = E.pushTop envArg
val envArgRes = E.reduceToFunction (envArgRes, List.length es2)
(*val _ = TextIO.print ("**** app turning arg:\n" ^ E.toString envArgRes)*)
......@@ -715,7 +722,10 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
| infExp (st,env) (AST.IDexp v) =
let
val env = E.pushSymbol (v, getSpan st, hasSymbol (st,v), env)
(*val _ = TextIO.print ("**** after pushing symbol " ^ SymbolTable.getString(!SymbolTables.varTable, v) ^ ":\n" ^ E.topToString env)*)
(*val ctxt = E.getCtxt env
val _ = if List.all (fn x => SymbolTable.toInt x<>debugSymbol) ctxt then () else
TextIO.print ("**** after pushing symbol " ^ SymbolTable.getString(!SymbolTables.varTable, v) ^ ":\n" ^ E.topToString env)*)
in
env
end
......
......@@ -423,7 +423,7 @@ end = struct
val bsStr = BD.setToString boolVars
in
("ver=" ^ Int.toString(ver) ^
(*", bvars = " ^ bsStr ^ *) ", vars=" ^ vsStr ^ "\n", si)
(*", bvars = " ^ bsStr ^ ", vars=" ^ vsStr ^ *)"\n", si)
end
fun toString ({bindInfo = bi, typeVars, boolVars, version}, si) =
......@@ -701,7 +701,7 @@ end = struct
let
fun tts acc (sc :: scs, state) =
(case Scope.unwrap (sc :: scs, state) of
(GROUP _, (_, state)) => toStringSI ((acc @ [sc], state), si)
(GROUP _, (_, state)) => toStringSI ((acc, state), si)
| (_, env) => tts (acc @ [sc]) env)
| tts acc ([], state) = toStringSI ((acc, state), si)
in
......@@ -878,6 +878,9 @@ end = struct
| (tvs, COMPOUND {ty = SOME (t,bFunFun), width = w, uses, nested}) =>
let
val (scs,state) = env
val bFunFun = BD.projectOnto (
texpBVarset (fn ((_,v),vs) => BD.addToSet (v,vs)) (t, BD.emptySet),
bFunFun)
val bFun = BD.meet (bFunFun, Scope.getFlow state)
val decVars = case w of
SOME t => texpVarset (t,TVar.empty)
......@@ -1254,7 +1257,9 @@ end = struct
fun popToFunction (sym, env) =
let
(*val _ = TextIO.print ("popToFunction " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ ":\n" ^ toString env)*)
(*val ctxt = getCtxt env
val _ = if List.all (fn x => SymbolTable.toInt x<>128) ctxt then () else
TextIO.print ("popToFunction " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ ":\n" ^ toString env)*)
fun setType t (COMPOUND {ty = NONE, width, uses, nested}, cons) =
(COMPOUND {ty = SOME t, width = width, uses = uses, nested = nested},
cons)
......
......@@ -6,7 +6,7 @@ structure Types = struct
type varset = TVar.set
val freshTVar = TVar.freshTVar
val concisePrint = true
val concisePrint = false
datatype texp =
(* a function taking at least one argument *)
......
......@@ -46,15 +46,15 @@ export =
intset-remove-min
intset-fold
fitree-lt?
fitree-lt? { lo, hi }
fitree-size
fitree-empty
fitree-singleton
fitree-add
fitree-add { lo, hi }
fitree-intersection
fitree-difference
fitree-interval-difference
fitree-contains?
fitree-contains? { lo, hi }
fitree-union
#fitree-remove
fitree-remove-min
......@@ -550,8 +550,7 @@ val fitree-interval-split t x =
fitree-fold interval-split (fitree-empty {}) t
end
val fitree-interval-difference a b =
let
val rebuild t overlapping x =
fitree-union
(fitree-difference t overlapping)
......@@ -559,9 +558,9 @@ val fitree-interval-difference a b =
val rebuild-overlapping t x =
rebuild t (fitree-collect-overlapping t x) x
in
val fitree-interval-difference a b =
fitree-fold rebuild-overlapping a b
end
val fitree-mk l h = {lo=l, hi=h}
val fitree-add s x = bbtree-add fitree-lt? s x
......
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