structure Tycheck :> TYCHECK = struct
-open Ast Print
+open Ast Print Env
-structure SS = StringSet
structure SM = StringMap
-type env = SS.set * typ SM.map
-val empty : env = (SS.add (SS.singleton "int", "string"),
- SM.empty)
-
-fun lookupType (ts, _) name = SS.member (ts, name)
-fun lookupVal (_, vs) name = SM.find (vs, name)
-
-fun bindType (ts, vs) name = (SS.add (ts, name), vs)
-fun bindVal (ts, vs) (name, t) = (ts, SM.insert (vs, name, t))
-
local
val unifCount = ref 0
in
NONE => (newUnif (), loc)
| SOME t => checkTyp G t
- val G' = bindVal G (x, t)
+ val G' = bindVal G (x, t, NONE)
val t' = checkExp G' e
in
(TArrow (t, t'), loc)
| EGet (x, evar, rest) =>
let
val xt = (newUnif (), loc)
- val G' = bindVal G (x, xt)
+ val G' = bindVal G (x, xt, NONE)
val rt = whnorm (checkExp G' rest)
in
fun checkDecl G (d, _, loc) =
case d of
DExternType name => bindType G name
- | DExternVal (name, t) => bindVal G (name, checkTyp G t)
+ | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+ | DVal (name, to, e) =>
+ let
+ val to =
+ case to of
+ NONE => (newUnif (), loc)
+ | SOME to => checkTyp G to
+
+ val t = checkExp G e
+ in
+ subTyp (t, to)
+ handle Unify ue =>
+ describe_type_error loc
+ (WrongType ("Bound value",
+ e,
+ t,
+ to,
+ SOME ue));
+ bindVal G (name, to, SOME e)
+ end
fun checkFile G tInit (ds, eo) =
let