1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006, Adam Chlipala
4 * This program is free software
; you can redistribute it
and/or
5 * modify it under the terms
of the GNU General Public License
6 * as published by the Free Software Foundation
; either version
2
7 * of the License
, or (at your option
) any later version
.
9 * This program is distributed
in the hope that it will be useful
,
10 * but WITHOUT ANY WARRANTY
; without even the implied warranty
of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE
. See the
12 * GNU General Public License for more details
.
14 * You should have received a copy
of the GNU General Public License
15 * along
with this program
; if not
, write to the Free Software
16 * Foundation
, Inc
., 51 Franklin Street
, Fifth Floor
, Boston
, MA
02110-1301, USA
.
19 (* Execution
of Domtool programs reduced to primitive actions
*)
21 structure Eval
:> EVAL
= struct
25 structure SM
= StringMap
27 fun lookup (evs
, ev
) =
28 case SM
.find (evs
, ev
) of
29 NONE
=> raise Fail ("Couldn't find an environment variable "
30 ^ ev ^
" that type-checking has guaranteed")
33 fun printEvs (name
, evs
) =
34 (print ("Environment " ^ name ^
"\n");
35 SM
.appi (fn (name
, i
) => Print
.preface (name
, Print
.p_exp i
)) evs
;
38 val conjoin
: Env
.env_vars
* Env
.env_vars
-> Env
.env_vars
=
45 EVar name
=> (name
, [])
48 val (name
, args
) = findPrim e1
52 | _
=> raise Fail
"Non-primitive action left after reduction"
54 val (name
, args
) = findPrim e
61 fun exec
' evs (eAll
as (e
, _
)) =
64 |
ESet (ev
, e
) => SM
.insert (SM
.empty
, ev
, e
)
65 |
EGet (x
, ev
, e
) => exec
' evs (Reduce
.subst
x (lookup (evs
, ev
)) e
)
69 foldl (fn (e
, (new
, keep
)) =>
71 val new
' = exec
' keep e
75 end) (SM
.empty
, evs
) es
81 val evs
' = exec
' evs e1
82 val evs
'' = exec
' (conjoin (evs
, evs
')) e2
88 val (prim
, args
) = findPrimitive e1
90 case Env
.container prim
of
91 NONE
=> raise Fail
"Unbound primitive container"
92 |
SOME (action
, cleanup
) =>
94 val evs
' = action (evs
, args
)
95 val evs
'' = exec
' evs e2
104 val (prim
, args
) = findPrimitive eAll
106 case Env
.action prim
of
107 NONE
=> raise Fail
"Unbound primitive action"
108 | SOME action
=> action (evs
, args
)
112 val evs
' = exec
' evs e