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 ((root
, evs
), ev
) =
28 case SM
.find (evs
, ev
) of
29 NONE
=> (case SM
.find (root
, ev
) of
30 NONE
=> raise Fail ("Couldn't find an environment variable "
31 ^ ev ^
" that type-checking has guaranteed")
35 fun printEvs (name
, evs
) =
36 (print ("Environment " ^ name ^
"\n");
37 SM
.appi (fn (name
, i
) => Print
.preface (name
, Print
.p_exp i
)) evs
;
40 val conjoin
: Env
.env_vars
* Env
.env_vars
-> Env
.env_vars
=
47 EVar name
=> (name
, [])
50 val (name
, args
) = findPrim e1
54 | _
=> raise Fail
"Non-primitive action left after reduction"
56 val (name
, args
) = findPrim e
61 fun exec
' (evsAll
as (root
, evs
)) (eAll
as (e
, _
)) =
64 |
ESet (ev
, e
) => SM
.insert (SM
.empty
, ev
, e
)
65 |
EGet (x
, _
, ev
, e
) =>
67 val e
' = Reduce
.subst
x (lookup (evsAll
, ev
)) e
69 exec
' evsAll (Reduce
.reduceExp Env
.empty e
')
74 foldl (fn (e
, (new
, keep
)) =>
76 val new
' = exec
' (root
, keep
) e
80 end) (SM
.empty
, evs
) es
86 val evs
' = exec
' evsAll e1
88 exec
' (root
, (conjoin (evs
, evs
'))) e2
92 val (prim
, args
) = findPrimitive e1
94 case Env
.container prim
of
95 NONE
=> raise Fail
"Unbound primitive container"
96 |
SOME (action
, cleanup
) =>
98 val evs
' = action (conjoin (root
, evs
), args
)
99 val evs
'' = exec
' evsAll e2
108 val (prim
, args
) = findPrimitive eAll
110 case Env
.action prim
of
111 NONE
=> raise Fail
"Unbound primitive action"
112 | SOME action
=> action (conjoin (root
, evs
), List.map (Reduce
.reduceExp Env
.empty
) args
)
118 val evs
' = exec
' evs e
123 val exec
' = fn evs
as (root
, evs
') => fn e
=> conjoin (evs
', exec
' evs e
)