(* 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