+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * 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.
+*)
+
+(* Execution of Domtool programs reduced to primitive actions *)
+
+structure Eval :> EVAL = struct
+
+open Ast
+
+structure SM = StringMap
+
+fun lookup (evs, ev) =
+ case SM.find (evs, ev) of
+ NONE => raise Fail ("Couldn't find an environment variable "
+ ^ ev ^ " that type-checking has guaranteed")
+ | SOME v => v
+
+val conjoin : Env.env_vars * Env.env_vars -> Env.env_vars =
+ SM.unionWith #2
+
+fun findPrimitive e =
+ let
+ fun findPrim (e, _) =
+ case e of
+ EVar name => (name, [])
+ | EApp (e1, e2) =>
+ let
+ val (name, args) = findPrim e1
+ in
+ (name, e2 :: args)
+ end
+ | _ => raise Fail "Non-primitive action left after reduction"
+
+ val (name, args) = findPrim e
+ in
+ (name, rev args)
+ end
+
+fun exec evs e =
+ let
+ fun exec' evs (eAll as (e, _)) =
+ case e of
+ ESkip => SM.empty
+ | ESet (ev, e) => SM.insert (SM.empty, ev, e)
+ | EGet (x, ev, e) => exec' evs (Reduce.subst x (lookup (evs, ev)) e)
+ | ESeq es =>
+ let
+ val (new, _) =
+ foldl (fn (e, (new, keep)) =>
+ let
+ val new' = exec' keep e
+ in
+ (conjoin (new, new'),
+ conjoin (keep, new'))
+ end) (SM.empty, evs) es
+ in
+ new
+ end
+ | ELocal (e1, e2) =>
+ let
+ val evs' = exec' evs e1
+ val evs'' = exec' (conjoin (evs, evs')) e2
+ in
+ conjoin (evs, evs'')
+ end
+ | EWith (e1, e2) =>
+ let
+ val (prim, args) = findPrimitive e1
+ in
+ case Env.container prim of
+ NONE => raise Fail "Unbound primitive container"
+ | SOME (action, cleanup) =>
+ let
+ val evs' = action (evs, args)
+ val evs'' = exec' evs e2
+ in
+ cleanup ();
+ conjoin (conjoin (evs, evs'), evs'')
+ end
+ end
+
+ | _ =>
+ let
+ val (prim, args) = findPrimitive eAll
+ in
+ case Env.action prim of
+ NONE => raise Fail "Unbound primitive action"
+ | SOME action => action (evs, args)
+ end
+
+ val evs' = exec' evs e
+ in
+ ()
+ end
+
+end