* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
-*)
+ *)
(* Domtool configuration language type checking *)
structure SM = StringMap
+val externFlag = ref false
+fun allowExterns () = externFlag := true
+fun disallowExterns () = externFlag := false
+
local
val unifCount = ref 0
in
| UnboundVariable of string
| WrongPred of string * pred * pred
-fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
- [PD.string s, PD.space 1, d]))
-
fun describe_unification_error t ue =
case ue of
UnifyPred (p1, p2) =>
| (_, 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 (_, ref (SOME tAll)) => whnorm tAll
| _ => tAll
+fun baseCondition t =
+ case whnorm t of
+ (TBase name, _) => typeRule name
+ | (TList t, _) =>
+ (case baseCondition t of
+ NONE => NONE
+ | SOME f => SOME (fn (EList ls, _) => List.all f ls
+ | _ => false))
+ | _ => NONE
+
fun hasTyp (e, t1, t2) =
- case whnorm t2 of
- (TBase name, _) =>
- (case typeRule name of
- NONE => subTyp (t1, t2)
- | SOME rule =>
- if rule e then
- ()
- else
- subTyp (t1, t2))
- | _ => subTyp (t1, t2)
+ if (case baseCondition t2 of
+ NONE => false
+ | SOME rule => rule e) then
+ ()
+ else
+ subTyp (t1, t2)
+
+fun checkPred G (p, loc) =
+ let
+ val err = ErrorMsg.error (SOME loc)
+ in
+ case p of
+ CRoot => ()
+ | CConst s =>
+ if lookupContext G s then
+ ()
+ else
+ err ("Unbound context " ^ s)
+ | CPrefix p => checkPred G p
+ | CNot p => checkPred G p
+ | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
+ end
fun checkTyp G (tAll as (t, loc)) =
let
(TError, loc))
| TList t => (TList (checkTyp G t), loc)
| TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
- | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
- SM.map (checkTyp G) r), loc)
- | TNested (p, t) => (TNested (p, checkTyp G t), loc)
+ | TAction (p, d, r) => (checkPred G p;
+ (TAction (p, SM.map (checkTyp G) d,
+ SM.map (checkTyp G) r), loc))
+ | TNested (p, t) => (checkPred G p;
+ (TNested (p, checkTyp G t), loc))
| TError => raise Fail "TError in parser-generated type"
| 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
(TError, loc))
end
+ | EALam (x, p, e) =>
+ let
+ val p' = checkPred G p
+
+ val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
+ val t' = whnorm (checkExp G' e)
+ in
+ case t' of
+ (TAction _, _) => (TNested (p, t'), loc)
+ | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
+ "action",
+ e,
+ t',
+ NONE));
+ (TError, loc))
+ end
+
| ESet (evar, e) =>
let
val t = checkExp G e
(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
fun checkDecl G (d, _, loc) =
case d of
- DExternType name => bindType G name
- | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+ DExternType name =>
+ if !externFlag then
+ bindType G name
+ else
+ (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
+ G)
+ | DExternVal (name, t) =>
+ if !externFlag then
+ bindVal G (name, checkTyp G t, NONE)
+ else
+ (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
+ G)
| DVal (name, to, e) =>
let
val to =
SOME ue));
bindVal G (name, to, SOME e)
end
+ | DContext name => bindContext G name
-fun checkFile G tInit (ds, eo) =
+fun checkFile G tInit (_, ds, eo) =
let
val G' = foldl (fn (d, G) => checkDecl G d) G ds
in
HCoop / hcoop / domtool2.git / blobdiff