Commit 0e33df6b authored by Axel Simon's avatar Axel Simon
Browse files

report an error if exported functions require record fields

parent 27d8e240
......@@ -105,9 +105,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
| topDecl (AST.DECODEdecl dd) = topDecodeDecl dd
| topDecl (AST.LETRECdecl vd) = topLetrecDecl vd
| topDecl _ = []
and topDecodeDecl (v, _, _) = [(v, true)]
and topLetrecDecl (v, _, _) = [(v,false)]
(* define a second traversal that is a full inference of the tree *)
......@@ -686,7 +684,27 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(#tree (ast : SpecAbstractTree.specification))
val toplevelEnv = calcFixpoint (unstable, toplevelEnv)
handle TypeError => toplevelEnv
(*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)
(* check if all exported functions can be run with an empty state *)
fun checkDecoder s sym = case E.forceNoInputs (sym,toplevelEnv) of
[] => ()
| fs =>
let
val decStr = SymbolTable.getString(!SymbolTables.varTable, sym)
fun genFieldStr (f,(sep,str)) = (", ", str ^ sep ^
SymbolTable.getString(!SymbolTables.fieldTable, f))
val (_,fsStr) = List.foldl genFieldStr ("", "") fs
in
Error.errorAt (errStrm, s,
[decStr," cannot be exported due to lacking fields: ", fsStr]
)
end
fun checkExports _ (AST.MARKdecl {span=s, tree=t}) = checkExports s t
| checkExports s (AST.EXPORTdecl vs) = List.app (checkDecoder s) vs
| checkExports s _ = ()
val _ = List.app (checkExports (#span ast)) (#tree ast)
val (badSizes, primEnv) = E.popGroup (toplevelEnv, false)
val _ = reportBadSizes badSizes
val (badSizes, _) = E.popGroup (primEnv, false)
......
......@@ -99,10 +99,13 @@ structure Environment : sig
(*as above, additionally push a function type if it is set, otherwise push
top*)
val pushFunctionOrTop : VarInfo.symid * environment -> environment
val pushFunctionOrTop : VarInfo.symid * environment -> environment
(*apply the Boolean function*) val meetBoolean : (BooleanDomain.bfun ->
BooleanDomain.bfun) * environment -> environment
val forceNoInputs : VarInfo.symid * environment -> FieldInfo.symid list
(*apply the Boolean function*)
val meetBoolean : (BooleanDomain.bfun -> BooleanDomain.bfun) *
environment -> environment
val meetSizeConstraint : (SizeConstraint.size_constraint_set ->
SizeConstraint.size_constraint_set) *
......@@ -1183,6 +1186,22 @@ end = struct
env
end
fun forceNoInputs (sym, env) = case Scope.lookup (sym,env) of
(_,COMPOUND {ty = SOME (t,bFun), width, uses}) =>
let
fun onlyInputs ((true,v),vs) = v :: vs
| onlyInputs ((false,v),vs) = vs
val bVars = texpBVarset onlyInputs (t,[])
fun checkField bVar =
(case BD.meetVarZero bVar bFun of _ => NONE)
handle (BD.Unsatisfiable _) => fieldOfBVar (bVar,t)
in
List.foldl (fn (bVar,fs) => case checkField bVar of
SOME f => f :: fs
| NONE => fs) [] bVars
end
| _ => raise InferenceBug
fun unify (env1, env2, substs) =
(case Scope.unwrapDifferent (env1, env2) of
(SOME (KAPPA {ty = ty1}, KAPPA {ty = ty2}), env1, env2) =>
......
......@@ -56,18 +56,23 @@ end = struct
(str, VarMap.insert(tab, var, str))
end
type set = IntRedBlackSet.set
structure IntSet = SplaySetFn(struct
type ord_key = int
val compare = Int.compare
end)
val empty = IntRedBlackSet.empty
fun singleton (TVAR v) = IntRedBlackSet.singleton v
fun fromList l = IntRedBlackSet.fromList (List.map (fn (TVAR v) => v) l)
fun listItems vs = List.map (fn v => (TVAR v)) (IntRedBlackSet.listItems vs)
fun add (TVAR v, l) = IntRedBlackSet.add' (v, l)
val union = IntRedBlackSet.union
val intersection = IntRedBlackSet.intersection
val difference = IntRedBlackSet.difference
fun member (l,TVAR v) = IntRedBlackSet.member (l,v)
val isEmpty = IntRedBlackSet.isEmpty
type set = IntSet.set
val empty = IntSet.empty
fun singleton (TVAR v) = IntSet.singleton v
fun fromList l = IntSet.fromList (List.map (fn (TVAR v) => v) l)
fun listItems vs = List.map (fn v => (TVAR v)) (IntSet.listItems vs)
fun add (TVAR v, l) = IntSet.add' (v, l)
val union = IntSet.union
val intersection = IntSet.intersection
val difference = IntSet.difference
fun member (l,TVAR v) = IntSet.member (l,v)
val isEmpty = IntSet.isEmpty
fun setToString (set, si) =
let
fun show (v, (str, sep, si)) =
......@@ -77,7 +82,7 @@ end = struct
(str ^ sep ^ vStr, ", ", si)
end
val (res, _, si) =
List.foldl show ("", "{", si) (IntRedBlackSet.listItems set)
List.foldl show ("", "{", si) (IntSet.listItems set)
in
(res ^ "}", si)
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