From e140629ff492a6440c7b0d892d27ed443a2f9cd9 Mon Sep 17 00:00:00 2001 From: Clinton Ebadi Date: Wed, 9 Apr 2014 13:56:05 -0400 Subject: [PATCH] Move ambient environment defaults into Env.env * Compute initial type in `checkFile' rather than passing in `env_vars' * Not happy with function names (initialDynEnvFOO is not very nice looking) --- src/autodoc.sml | 2 +- src/env.sig | 7 +++++++ src/env.sml | 38 ++++++++++++++++++++++++++------------ src/main.sml | 12 ++++++++---- src/order.sml | 6 ++++++ src/tycheck.sig | 3 ++- src/tycheck.sml | 49 ++++++++++++++++++++++++++++++++++++++++++++++++- 7 files changed, 98 insertions(+), 19 deletions(-) diff --git a/src/autodoc.sml b/src/autodoc.sml index bdf2527..b642214 100644 --- a/src/autodoc.sml +++ b/src/autodoc.sml @@ -36,7 +36,7 @@ fun check' G fname = if !ErrorMsg.anyErrors then G else - Tycheck.checkFile G (Defaults.tInit prog) prog + Tycheck.checkFile G prog end fun autodoc {outdir, infiles} = diff --git a/src/env.sig b/src/env.sig index 8e5962c..c8371a8 100644 --- a/src/env.sig +++ b/src/env.sig @@ -1,5 +1,6 @@ (* HCoop Domtool (http://hcoop.sourceforge.net/) * Copyright (c) 2006, Adam Chlipala + * Copyright (c) 2014 Clinton Ebadi * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -93,16 +94,22 @@ signature ENV = sig type env val empty : env + val initialDynEnvTypes : env -> Ast.typ Ast.StringMap.map + val initialDynEnvVals : env -> env_vars + val bindType : env -> string -> env val bindVal : env -> string * Ast.typ * Ast.exp option -> env val bindContext : env -> string -> env + val bindInitialDynEnvVal : env -> string * Ast.typ * Ast.exp -> env val lookupType : env -> string -> bool val lookupVal : env -> string -> Ast.typ option val lookupEquation : env -> string -> Ast.exp option val lookupContext : env -> string -> bool + val lookupInitialDynEnvVal : env -> string -> Ast.typ option val types : env -> Ast.StringSet.set val vals : env -> Ast.StringSet.set val contexts : env -> Ast.StringSet.set + val dynamics : env -> Ast.StringSet.set end diff --git a/src/env.sml b/src/env.sml index 8ebcaf4..3b08094 100644 --- a/src/env.sml +++ b/src/env.sml @@ -1,5 +1,6 @@ (* HCoop Domtool (http://hcoop.sourceforge.net/) * Copyright (c) 2006, Adam Chlipala + * Copyright (c) 2014 Clinton Ebadi * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -211,26 +212,39 @@ fun container_one name args (f, g) = registerContainer (name, one name args f, g fun containerV_none name (f, g) = registerContainer (name, noneV name f, g) fun containerV_one name args (f, g) = registerContainer (name, oneV name args f, g) -type env = SS.set * (typ * exp option) SM.map * SS.set -val empty : env = (SS.empty, SM.empty, SS.empty) +type env = SS.set * (typ * exp option) SM.map * SS.set * (typ * exp) SM.map +val empty : env = (SS.empty, SM.empty, SS.empty, SM.empty) -fun lookupType (ts, _, _) name = SS.member (ts, name) -fun lookupVal (_, vs, _) name = + +fun initialDynEnvTypes (_, _, _, ds) = + SM.map (fn (t, e) => t) ds + +fun initialDynEnvVals (_, _, _, ds) = + SM.map (fn (t, v) => v) ds + +fun lookupType (ts, _, _, _) name = SS.member (ts, name) +fun lookupVal (_, vs, _, _) name = case SM.find (vs, name) of NONE => NONE | SOME (t, _) => SOME t -fun lookupEquation (_, vs, _) name = +fun lookupEquation (_, vs, _, _) name = case SM.find (vs, name) of NONE => NONE | SOME (_, eqo) => eqo -fun lookupContext (_, _, cs) name = SS.member (cs, name) +fun lookupContext (_, _, cs, _) name = SS.member (cs, name) +fun lookupInitialDynEnvVal (_, _, _, ds) name = + case SM.find (ds, name) of + NONE => NONE + | SOME (t, _) => SOME t -fun bindType (ts, vs, cs) name = (SS.add (ts, name), vs, cs) -fun bindVal (ts, vs, cs) (name, t, eqo) = (ts, SM.insert (vs, name, (t, eqo)), cs) -fun bindContext (ts, vs, cs) name = (ts, vs, SS.add (cs, name)) +fun bindType (ts, vs, cs, ds) name = (SS.add (ts, name), vs, cs, ds) +fun bindVal (ts, vs, cs, ds) (name, t, eqo) = (ts, SM.insert (vs, name, (t, eqo)), cs, ds) +fun bindContext (ts, vs, cs, ds) name = (ts, vs, SS.add (cs, name), ds) +fun bindInitialDynEnvVal (ts, vs, cs, ds) (name, t, eqn) = (ts, vs, cs, SM.insert (ds, name, (t, eqn))) -fun types (ts, _, _) = ts -fun vals (_, vs, _) = SM.foldli (fn (name, _, vs) => SS.add (vs, name)) SS.empty vs -fun contexts (_, _, cs) = cs +fun types (ts, _, _, _) = ts +fun vals (_, vs, _, _) = SM.foldli (fn (name, _, vs) => SS.add (vs, name)) SS.empty vs +fun contexts (_, _, cs, _) = cs +fun dynamics (_, _, _, ds) = SM.foldli (fn (name, _, ds) => SS.add (ds, name)) SS.empty ds end diff --git a/src/main.sml b/src/main.sml index be50982..6cb3ef1 100644 --- a/src/main.sml +++ b/src/main.sml @@ -51,7 +51,7 @@ fun check' G fname = () else Option.app (Unused.check G) (#3 prog); - Tycheck.checkFile G (Defaults.tInit prog) prog) + Tycheck.checkFile G prog) end fun basis () = @@ -101,7 +101,7 @@ fun check G fname = raise ErrorMsg.Error else let - val G' = Tycheck.checkFile G (Defaults.tInit prog) prog + val G' = Tycheck.checkFile G prog in if !ErrorMsg.anyErrors then raise ErrorMsg.Error @@ -1149,7 +1149,9 @@ fun regenerateEither tc checker context = ok := false) else (); - ignore (foldl checker' (basis (), Defaults.eInit ()) files) + let val basis' = basis () in + ignore (foldl checker' (basis', Env.initialDynEnvVals basis') files) + end end else if String.isSuffix "_admin" user then () @@ -1314,7 +1316,9 @@ fun service () = end in doIt (fn () => (Env.pre (); - ignore (foldl doOne (basis (), Defaults.eInit ()) codes); + let val basis' = basis () in + ignore (foldl doOne (basis', Env.initialDynEnvVals basis') codes) + end; Env.post (); Msg.send (bio, MsgOk); ("Configuration complete.", NONE))) diff --git a/src/order.sml b/src/order.sml index b58c9f7..117a0ea 100644 --- a/src/order.sml +++ b/src/order.sml @@ -1,5 +1,6 @@ (* HCoop Domtool (http://hcoop.sourceforge.net/) * Copyright (c) 2006, Adam Chlipala + * Copyright (c) 2014 Clinton Ebadi * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -134,6 +135,11 @@ fun declNeeded G (d, _, _) = NONE => expNeeded G e | SOME t => unionCTE ((typNeeded G t, SS.empty), expNeeded G e)) + | DEnv (name, to, e) => (Env.bindInitialDynEnvVal G (name, dt, (Ast.ESkip, ErrorMsg.dummyLoc)), + case to of + NONE => expNeeded G e + | SOME t => unionCTE ((typNeeded G t, SS.empty), + expNeeded G e)) | DContext name => (Env.bindContext G name, empty) fun fileSig (_, ds, eo) = diff --git a/src/tycheck.sig b/src/tycheck.sig index 19ec6d4..52630b8 100644 --- a/src/tycheck.sig +++ b/src/tycheck.sig @@ -1,5 +1,6 @@ (* HCoop Domtool (http://hcoop.sourceforge.net/) * Copyright (c) 2006, Adam Chlipala + * Copyright (c) 2014 Clinton Ebadi * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -28,7 +29,7 @@ signature TYCHECK = sig val checkDecl : Env.env -> Ast.decl -> Env.env - val checkFile : Env.env -> Ast.typ -> Ast.file -> Env.env + val checkFile : Env.env -> Ast.file -> Env.env val resetUnif : unit -> unit val newUnif : unit -> Ast.typ' diff --git a/src/tycheck.sml b/src/tycheck.sml index 12efce3..38ef822 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -1,5 +1,6 @@ (* HCoop Domtool (http://hcoop.sourceforge.net/) * Copyright (c) 2006-2007, Adam Chlipala + * Copyright (c) 2014 Clinton Ebadi * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License @@ -671,6 +672,25 @@ fun checkDecl G (d, _, loc) = SOME ue)); bindVal G (name, to, SOME e) end + | DEnv (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.describe_type_error loc + (WrongType ("Dynamically bound value", + e, + t, + to, + SOME ue)); + bindInitialDynEnvVal G (name, to, e) + end | DContext name => bindContext G name fun printActionDiffs {have, need} = @@ -723,15 +743,42 @@ fun printActionDiffs {have, need} = | _ => false -fun checkFile G tInit (_, ds, eo) = +fun checkFile G (prog as (_, ds, eo)) = let val G' = foldl (fn (d, G) => checkDecl G d) G ds + + fun tInitial prog env = + (* This should likely only take the dynamic env as an argument *) + let + fun allSets (e, _) = + case e of + ESkip => true + | ESet _ => true + | ESeq es => List.all allSets es + | _ => false + + val dmy = ErrorMsg.dummyLoc + + fun bodyType (_, _, SOME e) = + if allSets e then + (CPrefix (CRoot, dmy), dmy) + else + (CRoot, dmy) + | bodyType _ = (CRoot, dmy) + in + (TAction (bodyType prog, + Env.initialDynEnvTypes env, + StringMap.empty), + dmy) + end + in case eo of NONE => () | SOME (e as (_, loc)) => let val t = checkExp G' e + val tInit = tInitial prog G' in hasTyp (e, t, tInit) handle Unify _ => -- 2.20.1