| (_, CPrefix p2) => predImplies (p1All, p2)
| (CNot p1, CNot p2) => predImplies (p2, p1)
+ | (CRoot, CNot (CConst _, _)) => true
+ | (CConst s1, CNot (CConst s2, _)) => s1 <> s2
| _ => false
| TUnif _ => raise Fail "TUnif in parser-generated type"
end
+fun envVarSetFrom v (e, _) =
+ case e of
+ ESet (v', e) =>
+ if v = v' then
+ SOME e
+ else
+ NONE
+ | EGet (_, _, e) => envVarSetFrom v e
+ | ESeq es => foldr (fn (e, found) =>
+ case found of
+ SOME _ => found
+ | NONE => envVarSetFrom v e)
+ NONE es
+ | ELocal (_, e) => envVarSetFrom v e
+
+ | _ => NONE
+
fun checkExp G (eAll as (e, loc)) =
let
val dte = describe_type_error loc
(case SM.find (d', name) of
NONE => SM.insert (d', name, t)
| SOME t' =>
- (subTyp (t, t')
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t, t')
+ | SOME e => hasTyp (e, t, t'))
handle Unify ue =>
dte (WrongType ("Shared environment variable",
(EVar name, loc),
- t,
t',
+ t,
SOME ue));
d'))
| SOME t' =>
- (subTyp (t, t')
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t, t')
+ | SOME e => hasTyp (e, t, t'))
handle Unify ue =>
dte (WrongType ("Shared environment variable",
(EVar name, loc),
- t,
t',
+ t,
SOME ue));
d'))
d1 d2
(case SM.find (d', name) of
NONE => SM.insert (d', name, t)
| SOME t' =>
- (subTyp (t, t')
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t', t)
+ | SOME e => hasTyp (e, t', t))
handle Unify ue =>
dte (WrongType ("Shared environment variable",
(EVar name, loc),
- t,
t',
+ t,
SOME ue));
d'))
| SOME t' =>
- (subTyp (t, t')
+ ((case envVarSetFrom name e1 of
+ NONE => subTyp (t', t)
+ | SOME e => hasTyp (e, t', t))
handle Unify ue =>
dte (WrongType ("Shared environment variable",
(EVar name, loc),
- t,
t',
+ t,
SOME ue));
d'))
d1 d2