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 (* Domtool
type-checking
and reduction environments
*)
21 structure Env
:> ENV
= struct
25 structure SS
= StringSet
26 structure SM
= StringMap
28 type typeRule
= exp
-> bool
29 val typeRules
: typeRule SM
.map ref
= ref SM
.empty
30 fun registerType (name
, rule
) = typeRules
:= SM
.insert (!typeRules
, name
, rule
)
31 fun typeRule name
= SM
.find (!typeRules
, name
)
33 type env_vars
= exp SM
.map
34 type action
= env_vars
* Ast
.exp list
-> env_vars
35 val actions
: action SM
.map ref
= ref SM
.empty
36 fun registerAction (name
, action
) = actions
:= SM
.insert (!actions
, name
, action
)
37 fun action name
= SM
.find (!actions
, name
)
39 val containers
: (action
* (unit
-> unit
)) SM
.map ref
= ref SM
.empty
40 fun registerContainer (name
, befor
, after
) =
41 containers
:= SM
.insert (!containers
, name
, (befor
, after
))
42 fun container name
= SM
.find (!containers
, name
)
45 val pr
= ref (fn () => ())
52 pr
:= (fn () => (old (); f ()))
59 val pst
= ref (fn () => ())
66 pst
:= (fn () => (old (); f ()))
73 val pr
= ref (fn () => ())
76 fun registerPreTycheck f
=
80 pr
:= (fn () => (old (); f ()))
82 fun preTycheck () = !pr ()
86 fun badArgs (name
, args
) =
87 (print ("Invalid arguments to " ^ name ^
"\n");
88 app (fn arg
=> Print
.preface ("Argument: ", Print
.p_exp arg
)) args
;
90 fun badArg (func
, arg
, v
) =
91 (print ("Invalid " ^ arg ^
" argument to " ^ func ^
"\n");
92 Print
.preface ("Argument: ", Print
.p_exp v
);
95 type 'a arg
= exp
-> 'a option
97 fun int (EInt n
, _
) = SOME n
100 fun string (EString s
, _
) = SOME s
103 fun mapFail f
[] = SOME
[]
104 | mapFail
f (h
:: t
) =
110 | SOME t
' => SOME (h
' :: t
')
112 fun list
f (EList ls
, _
) = mapFail f ls
115 fun none func
f (_
, []) = (f ();
117 | none func
_ (_
, es
) = badArgs (func
, es
)
119 fun one
func (name
, arg
) f (_
, [e
]) =
121 NONE
=> badArg (func
, name
, e
)
124 | one func _
_ (_
, es
) = badArgs (func
, es
)
126 fun two
func (name1
, arg1
, name2
, arg2
) f (_
, [e1
, e2
]) =
127 (case (arg1 e1
, arg2 e2
) of
128 (NONE
, _
) => badArg (func
, name1
, e1
)
129 |
(_
, NONE
) => badArg (func
, name2
, e2
)
130 |
(SOME v1
, SOME v2
) => (f (v1
, v2
);
132 | two func _
_ (_
, es
) = badArgs (func
, es
)
135 fun oneV
func (name
, arg
) f (evs
, [e
]) =
137 NONE
=> badArg (func
, name
, e
)
138 | SOME v
=> (f (evs
, v
);
140 | oneV func _
_ (_
, es
) = badArgs (func
, es
)
142 fun twoV
func (name1
, arg1
, name2
, arg2
) f (evs
, [e1
, e2
]) =
143 (case (arg1 e1
, arg2 e2
) of
144 (NONE
, _
) => badArg (func
, name1
, e1
)
145 |
(_
, NONE
) => badArg (func
, name2
, e2
)
146 |
(SOME v1
, SOME v2
) => (f (evs
, v1
, v2
);
148 | twoV func _
_ (_
, es
) = badArgs (func
, es
)
151 fun env
arg (evs
, name
) =
152 case SM
.find (evs
, name
) of
153 NONE
=> raise Fail ("Unavailable environment variable " ^ name
)
156 NONE
=> raise Fail ("Bad format for environment variable " ^ name
)
159 fun type_one func arg f
=
160 registerType (func
, fn e
=>
165 fun action_none name f
= registerAction (name
, none name f
)
166 fun action_one name args f
= registerAction (name
, one name args f
)
167 fun action_two name args f
= registerAction (name
, two name args f
)
169 fun actionV_none name f
= registerAction (name
, fn (env
, _
) => (f env
; env
))
170 fun actionV_one name args f
= registerAction (name
, oneV name args f
)
171 fun actionV_two name args f
= registerAction (name
, twoV name args f
)
173 fun container_none
name (f
, g
) = registerContainer (name
, none name f
, g
)
174 fun container_one name
args (f
, g
) = registerContainer (name
, one name args f
, g
)
176 fun containerV_one name
args (f
, g
) = registerContainer (name
, oneV name args f
, g
)
178 type env
= SS
.set
* (typ
* exp option
) SM
.map
* SS
.set
179 val empty
: env
= (SS
.empty
, SM
.empty
, SS
.empty
)
181 fun lookupType (ts
, _
, _
) name
= SS
.member (ts
, name
)
182 fun lookupVal (_
, vs
, _
) name
=
183 case SM
.find (vs
, name
) of
185 |
SOME (t
, _
) => SOME t
186 fun lookupEquation (_
, vs
, _
) name
=
187 case SM
.find (vs
, name
) of
189 |
SOME (_
, eqo
) => eqo
190 fun lookupContext (_
, _
, cs
) name
= SS
.member (cs
, name
)
192 fun bindType (ts
, vs
, cs
) name
= (SS
.add (ts
, name
), vs
, cs
)
193 fun bindVal (ts
, vs
, cs
) (name
, t
, eqo
) = (ts
, SM
.insert (vs
, name
, (t
, eqo
)), cs
)
194 fun bindContext (ts
, vs
, cs
) name
= (ts
, vs
, SS
.add (cs
, name
))
196 fun types (ts
, _
, _
) = ts
197 fun vals (_
, vs
, _
) = SM
.foldli (fn (name
, _
, vs
) => SS
.add (vs
, name
)) SS
.empty vs
198 fun contexts (_
, _
, cs
) = cs