HCoop
/
hcoop
/
domtool2.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Type annotations on environment variable reads
[hcoop/domtool2.git]
/
src
/
tycheck.sml
diff --git
a/src/tycheck.sml
b/src/tycheck.sml
index
d486603
..
8889540
100644
(file)
--- a/
src/tycheck.sml
+++ b/
src/tycheck.sml
@@
-184,10
+184,21
@@
fun baseCondition t =
| _ => false))
| _ => NONE
| _ => false))
| _ => NONE
+fun simplifyKindOf e =
+ case e of
+ (EApp ((EVar s, _), e'), _) =>
+ (case Env.function s of
+ NONE => e
+ | SOME f =>
+ case f [e'] of
+ NONE => e
+ | SOME e => e)
+ | _ => e
+
fun hasTyp (e, t1, t2) =
if (case baseCondition t2 of
NONE => false
fun hasTyp (e, t1, t2) =
if (case baseCondition t2 of
NONE => false
- | SOME rule => rule
e
) then
+ | SOME rule => rule
(simplifyKindOf e)
) then
()
else
subTyp (t1, t2)
()
else
subTyp (t1, t2)
@@
-237,7
+248,7
@@
fun envVarSetFrom v (e, _) =
SOME e
else
NONE
SOME e
else
NONE
- | EGet (_, _, e) => envVarSetFrom v e
+ | EGet (_, _,
_,
e) => envVarSetFrom v e
| ESeq es => foldr (fn (e, found) =>
case found of
SOME _ => found
| ESeq es => foldr (fn (e, found) =>
case found of
SOME _ => found
@@
-247,6
+258,11
@@
fun envVarSetFrom v (e, _) =
| _ => NONE
| _ => NONE
+fun ununify (tAll as (t, _)) =
+ case t of
+ TUnif (_, ref (SOME t)) => ununify t
+ | _ => tAll
+
fun checkExp G (eAll as (e, loc)) =
let
val dte = Describe.describe_type_error loc
fun checkExp G (eAll as (e, loc)) =
let
val dte = Describe.describe_type_error loc
@@
-346,14
+362,18
@@
fun checkExp G (eAll as (e, loc)) =
SM.insert (SM.empty, evar, t)),
loc)
end
SM.insert (SM.empty, evar, t)),
loc)
end
- | EGet (x, evar, rest) =>
+ | EGet (x,
topt,
evar, rest) =>
let
val xt = (newUnif (), loc)
val G' = bindVal G (x, xt, NONE)
val rt = whnorm (checkExp G' rest)
in
let
val xt = (newUnif (), loc)
val G' = bindVal G (x, xt, NONE)
val rt = whnorm (checkExp G' rest)
in
- case rt of
+ case topt of
+ NONE => ()
+ | SOME t => subTyp (xt, checkTyp G t);
+
+ case ununify rt of
(TAction (p, d, r), _) =>
(case SM.find (d, evar) of
NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
(TAction (p, d, r), _) =>
(case SM.find (d, evar) of
NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)