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
59 fun exec
' evs (eAll
as (e
, _
)) =
62 |
ESet (ev
, e
) => SM
.insert (SM
.empty
, ev
, e
)
63 |
EGet (x
, _
, ev
, e
) => exec
' evs (Reduce
.subst
x (lookup (evs
, ev
)) e
)
67 foldl (fn (e
, (new
, keep
)) =>
69 val new
' = exec
' keep e
73 end) (SM
.empty
, evs
) es
79 val evs
' = exec
' evs e1
81 exec
' (conjoin (evs
, evs
')) e2
85 val (prim
, args
) = findPrimitive e1
87 case Env
.container prim
of
88 NONE
=> raise Fail
"Unbound primitive container"
89 |
SOME (action
, cleanup
) =>
91 val evs
' = action (evs
, args
)
92 val evs
'' = exec
' evs e2
101 val (prim
, args
) = findPrimitive eAll
103 case Env
.action prim
of
104 NONE
=> raise Fail
"Unbound primitive action"
105 | SOME action
=> action (evs
, List.map (Reduce
.reduceExp Env
.empty
) args
)
111 val evs
' = exec
' evs e