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 val conjoin
: Env
.env_vars
* Env
.env_vars
-> Env
.env_vars
=
40 EVar name
=> (name
, [])
43 val (name
, args
) = findPrim e1
47 | _
=> raise Fail
"Non-primitive action left after reduction"
49 val (name
, args
) = findPrim e
56 fun exec
' evs (eAll
as (e
, _
)) =
59 |
ESet (ev
, e
) => SM
.insert (SM
.empty
, ev
, e
)
60 |
EGet (x
, ev
, e
) => exec
' evs (Reduce
.subst
x (lookup (evs
, ev
)) e
)
64 foldl (fn (e
, (new
, keep
)) =>
66 val new
' = exec
' keep e
70 end) (SM
.empty
, evs
) es
76 val evs
' = exec
' evs e1
77 val evs
'' = exec
' (conjoin (evs
, evs
')) e2
83 val (prim
, args
) = findPrimitive e1
85 case Env
.container prim
of
86 NONE
=> raise Fail
"Unbound primitive container"
87 |
SOME (action
, cleanup
) =>
89 val evs
' = action (evs
, args
)
90 val evs
'' = exec
' evs e2
93 conjoin (conjoin (evs
, evs
'), evs
'')
99 val (prim
, args
) = findPrimitive eAll
101 case Env
.action prim
of
102 NONE
=> raise Fail
"Unbound primitive action"
103 | SOME action
=> action (evs
, args
)
107 val evs
' = exec
' evs e