X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/234b917a6149413bbbeab7dccfaeab5f16e43fe1..8a7c40fa29ff18a437fcf4ee3f248a7aeb41c19c:/src/tycheck.sml diff --git a/src/tycheck.sml b/src/tycheck.sml index 854b575..6d58e43 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -14,27 +14,16 @@ * 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 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 @@ -99,7 +88,7 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) = andalso eqRecord eqTy (r1, r2) | (TNested (p1, q1), TNested (p2, q2)) => - eqPred (p1, p2) andalso eqPred (q1, q2) + eqPred (p1, p2) andalso eqTy (q1, q2) | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All) | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2) @@ -123,9 +112,6 @@ datatype type_error = | 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) => @@ -170,7 +156,10 @@ fun describe_type_error loc te = fun predImplies (p1All as (p1, _), p2All as (p2, _)) = case (p1, p2) of - (_, CPrefix (CRoot, _)) => true + (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2) + | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All) + + | (_, CPrefix (CRoot, _)) => true | (CNot (CPrefix (CRoot, _), _), _) => true | (CRoot, CRoot) => true @@ -182,9 +171,6 @@ fun predImplies (p1All as (p1, _), p2All as (p2, _)) = | (CNot p1, CNot p2) => predImplies (p2, p1) - | (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2) - | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All) - | _ => false fun predSimpl (pAll as (p, loc)) = @@ -202,6 +188,8 @@ fun predSimpl (pAll as (p, loc)) = (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc) | _ => if predImplies (p2', p1') then p2' + else if predImplies (p1', p2') then + p1' else (CAnd (p1', p2'), loc) end @@ -226,7 +214,7 @@ fun occurs u (t, _) = | TAction (_, d, r) => List.exists (occurs u) (SM.listItems d) orelse List.exists (occurs u) (SM.listItems r) - | TNested _ => false + | TNested (_, t) => occurs u t | TError => false | TUnif (_, ref (SOME t)) => occurs u t | TUnif (_, u') => u = u' @@ -252,7 +240,7 @@ fun subTyp (t1All as (t1, _), t2All as (t2, _)) = | (TNested (d1, r1), TNested (d2, r2)) => (subPred (d2, d1); - subPred (r1, r2)) + subTyp (r1, r2)) | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All) | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2) @@ -290,6 +278,40 @@ fun whnorm (tAll as (t, loc)) = 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) = + 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 val err = ErrorMsg.error (SOME loc) @@ -303,13 +325,32 @@ fun checkTyp G (tAll as (t, loc)) = (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 _ => tAll + | 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 @@ -325,7 +366,7 @@ fun checkExp G (eAll as (e, loc)) = let val t' = checkExp G e' in - (subTyp (t', t); + (hasTyp (eAll, t', t); if isError t' then (TList (TError, loc), loc) else @@ -347,7 +388,7 @@ fun checkExp G (eAll as (e, loc)) = 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) @@ -365,8 +406,8 @@ fun checkExp G (eAll as (e, loc)) = val tf = checkExp G func val ta = checkExp G arg in - (subTyp (tf, (TArrow (dom, ran), loc)); - subTyp (ta, dom) + (hasTyp (func, tf, (TArrow (dom, ran), loc)); + hasTyp (arg, ta, dom) handle Unify ue => dte (WrongType ("Function argument", arg, @@ -395,7 +436,7 @@ fun checkExp G (eAll as (e, 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 @@ -443,21 +484,25 @@ fun checkExp G (eAll as (e, 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 @@ -483,33 +528,91 @@ fun checkExp G (eAll as (e, loc)) = (TError, loc)) end - | ELocal e => + | ELocal (e1, e2) => let - val rt = whnorm (checkExp G e) + val t1 = whnorm (checkExp G e1) + val t2 = whnorm (checkExp G e2) in - case rt of - (TAction (p, d, _), _) => - (TAction (p, d, SM.empty), loc) - | (TError, _) => rt - | _ => (dte (WrongForm ("Body of local action", + case t1 of + (TAction (p1, d1, r1), _) => + (case t2 of + (TAction (p2, d2, r2), _) => + let + val p' = predSimpl (CAnd (p1, p2), loc) + + val d' = SM.foldli (fn (name, t, d') => + case SM.find (r1, name) of + NONE => + (case SM.find (d', name) of + NONE => SM.insert (d', name, t) + | SOME 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, + SOME ue)); + d')) + | SOME 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, + SOME ue)); + d')) + d1 d2 + in + (TAction (p', d', r2), loc) + end + | (TError, _) => t2 + | _ => (dte (WrongForm ("Action to be sequenced", + "action", + e2, + t2, + NONE)); + (TError, loc))) + | (TError, _) => t1 + | _ => (dte (WrongForm ("Action to be sequenced", "action", - e, - rt, + e1, + t1, NONE)); (TError, loc)) end + | EWith (e1, e2) => let val t1 = whnorm (checkExp G e1) val t2 = whnorm (checkExp G e2) in case t1 of - (TNested (pd, pr), _) => + (TNested (pd, (TAction (pr, d1, r1), _)), _) => (case t2 of (TAction (p, d, r), _) => if predImplies (pd, p) then - (TAction (pr, d, r), loc) + let + val combineRecs = + SM.unionWithi (fn (name, t1, t2) => + (subTyp (t1, t2) + handle Unify ue => + dte (WrongType ("Environment variable", + (EVar name, loc), + t1, + t2, + SOME ue)); + t2)) + in + (TAction (pr, combineRecs (d, d1), + combineRecs (r, r1)), loc) + end else (dte (WrongPred ("nested action", pd, @@ -582,9 +685,29 @@ fun checkUnit G (eAll as (_, loc)) = 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 + hasTyp (e, t, to) + handle Unify ue => + describe_type_error loc + (WrongType ("Bound value", + e, + t, + 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 @@ -594,7 +717,7 @@ fun checkFile G tInit (ds, eo) = let val t = checkExp G' e in - subTyp (t, tInit) + hasTyp (e, t, tInit) handle Unify ue => (ErrorMsg.error (SOME loc) "Bad type for final expression of source file."; preface ("Actual:", p_typ t);