1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006, Adam Chlipala
3 * Copyright (c
) 2014 Clinton Ebadi
<clinton@unknownlamer
.org
>
5 * This program is free software
; you can redistribute it
and/or
6 * modify it under the terms
of the GNU General Public License
7 * as published by the Free Software Foundation
; either version
2
8 * of the License
, or (at your option
) any later version
.
10 * This program is distributed
in the hope that it will be useful
,
11 * but WITHOUT ANY WARRANTY
; without even the implied warranty
of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE
. See the
13 * GNU General Public License for more details
.
15 * You should have received a copy
of the GNU General Public License
16 * along
with this program
; if not
, write to the Free Software
17 * Foundation
, Inc
., 51 Franklin Street
, Fifth Floor
, Boston
, MA
02110-1301, USA
.
20 (* Domtool
type-checking
and reduction environments
*)
22 structure Env
:> ENV
= struct
26 structure SS
= StringSet
27 structure SM
= StringMap
29 type typeRule
= exp
-> bool
30 val typeRules
: typeRule SM
.map ref
= ref SM
.empty
31 fun registerType (name
, rule
) = typeRules
:= SM
.insert (!typeRules
, name
, rule
)
32 fun typeRule name
= SM
.find (!typeRules
, name
)
34 type env_vars
= exp SM
.map
35 type action
= env_vars
* Ast
.exp list
-> env_vars
36 val actions
: action SM
.map ref
= ref SM
.empty
37 fun registerAction (name
, action
) = actions
:= SM
.insert (!actions
, name
, action
)
38 fun action name
= SM
.find (!actions
, name
)
40 val containers
: (action
* (unit
-> unit
)) SM
.map ref
= ref SM
.empty
41 fun registerContainer (name
, befor
, after
) =
42 containers
:= SM
.insert (!containers
, name
, (befor
, after
))
43 fun container name
= SM
.find (!containers
, name
)
45 val functions
: (exp list
-> exp option
) SM
.map ref
= ref SM
.empty
46 fun registerFunction (name
, f
) =
47 functions
:= SM
.insert (!functions
, name
, f
)
48 fun function name
= SM
.find (!functions
, name
)
51 val pr
= ref (fn () => ())
58 pr
:= (fn () => (old (); f ()))
65 val pst
= ref (fn () => ())
72 pst
:= (fn () => (old (); f ()))
79 val pr
= ref (fn () => ())
82 fun registerPreTycheck f
=
86 pr
:= (fn () => (old (); f ()))
88 fun preTycheck () = !pr ()
92 fun badArgs (name
, args
) =
93 (print ("Invalid arguments to " ^ name ^
"\n");
94 app (fn arg
=> Print
.preface ("Argument: ", Print
.p_exp arg
)) args
;
96 fun badArg (func
, arg
, v
) =
97 (print ("Invalid " ^ arg ^
" argument to " ^ func ^
"\n");
98 Print
.preface ("Argument: ", Print
.p_exp v
);
101 type 'a arg
= exp
-> 'a option
103 fun int (EInt n
, _
) = SOME n
106 fun string (EString s
, _
) = SOME s
109 fun bool (EVar
"false", _
) = SOME
false
110 |
bool (EVar
"true", _
) = SOME
true
113 fun mapFail f
[] = SOME
[]
114 | mapFail
f (h
:: t
) =
120 | SOME t
' => SOME (h
' :: t
')
122 fun list
f (EList ls
, _
) = mapFail f ls
125 fun none func
f (_
, []) = (f ();
127 | none func
_ (_
, es
) = badArgs (func
, es
)
129 fun one
func (name
, arg
) f (_
, [e
]) =
131 NONE
=> badArg (func
, name
, e
)
134 | one func _
_ (_
, es
) = badArgs (func
, es
)
136 fun two
func (name1
, arg1
, name2
, arg2
) f (_
, [e1
, e2
]) =
137 (case (arg1 e1
, arg2 e2
) of
138 (NONE
, _
) => badArg (func
, name1
, e1
)
139 |
(_
, NONE
) => badArg (func
, name2
, e2
)
140 |
(SOME v1
, SOME v2
) => (f (v1
, v2
);
142 | two func _
_ (_
, es
) = badArgs (func
, es
)
144 fun three
func (name1
, arg1
, name2
, arg2
, name3
, arg3
) f (_
, [e1
, e2
, e3
]) =
145 (case (arg1 e1
, arg2 e2
, arg3 e3
) of
146 (NONE
, _
, _
) => badArg (func
, name1
, e1
)
147 |
(_
, NONE
, _
) => badArg (func
, name2
, e2
)
148 |
(_
, _
, NONE
) => badArg (func
, name3
, e3
)
149 |
(SOME v1
, SOME v2
, SOME v3
) => (f (v1
, v2
, v3
);
151 | three func _
_ (_
, es
) = badArgs (func
, es
)
153 fun four
func (name1
, arg1
, name2
, arg2
, name3
, arg3
, name4
, arg4
) f (_
, [e1
, e2
, e3
, e4
]) =
154 (case (arg1 e1
, arg2 e2
, arg3 e3
, arg4 e4
) of
155 (NONE
, _
, _
, _
) => badArg (func
, name1
, e1
)
156 |
(_
, NONE
, _
, _
) => badArg (func
, name2
, e2
)
157 |
(_
, _
, NONE
, _
) => badArg (func
, name3
, e3
)
158 |
(_
, _
, _
, NONE
) => badArg (func
, name4
, e4
)
159 |
(SOME v1
, SOME v2
, SOME v3
, SOME v4
) => (f (v1
, v2
, v3
, v4
);
161 | four func _
_ (_
, es
) = badArgs (func
, es
)
163 fun noneV func
f (evs
, []) = (f evs
;
165 | noneV func
_ (_
, es
) = badArgs (func
, es
)
167 fun oneV
func (name
, arg
) f (evs
, [e
]) =
169 NONE
=> badArg (func
, name
, e
)
170 | SOME v
=> (f (evs
, v
);
172 | oneV func _
_ (_
, es
) = badArgs (func
, es
)
174 fun twoV
func (name1
, arg1
, name2
, arg2
) f (evs
, [e1
, e2
]) =
175 (case (arg1 e1
, arg2 e2
) of
176 (NONE
, _
) => badArg (func
, name1
, e1
)
177 |
(_
, NONE
) => badArg (func
, name2
, e2
)
178 |
(SOME v1
, SOME v2
) => (f (evs
, v1
, v2
);
180 | twoV func _
_ (_
, es
) = badArgs (func
, es
)
183 fun env
arg (evs
, name
) =
184 case SM
.find (evs
, name
) of
185 NONE
=> raise Fail ("Unavailable environment variable " ^ name
)
188 NONE
=> (Print
.preface ("Unexpected value for " ^ name ^
":",
190 raise Fail ("Bad format for environment variable " ^ name
))
193 fun type_one func arg f
=
194 registerType (func
, fn e
=>
199 fun action_none name f
= registerAction (name
, none name f
)
200 fun action_one name args f
= registerAction (name
, one name args f
)
201 fun action_two name args f
= registerAction (name
, two name args f
)
202 fun action_three name args f
= registerAction (name
, three name args f
)
203 fun action_four name args f
= registerAction (name
, four name args f
)
205 fun actionV_none name f
= registerAction (name
, fn (env
, _
) => (f env
; env
))
206 fun actionV_one name args f
= registerAction (name
, oneV name args f
)
207 fun actionV_two name args f
= registerAction (name
, twoV name args f
)
209 fun container_none
name (f
, g
) = registerContainer (name
, none name f
, g
)
210 fun container_one name
args (f
, g
) = registerContainer (name
, one name args f
, g
)
212 fun containerV_none
name (f
, g
) = registerContainer (name
, noneV name f
, g
)
213 fun containerV_one name
args (f
, g
) = registerContainer (name
, oneV name args f
, g
)
215 datatype env
= Env
of SS
.set
* (typ
* exp option
* env
) SM
.map
* SS
.set
* (typ
* exp
* env
) SM
.map
216 val empty
: env
= Env (SS
.empty
, SM
.empty
, SS
.empty
, SM
.empty
)
219 fun initialDynEnvTypes (Env (_
, _
, _
, ds
)) =
220 SM
.map (fn (t
, _
, _
) => t
) ds
222 (* hack ahead
: These are not reduced when declared
and must be
before
223 starting evaluation
. Pass
in reduceExp
, and force an awkward
224 calling convention so no one thinks this is the Right
Way (tm
) *)
225 fun initialDynEnvVals
f (Env (_
, _
, _
, ds
)) =
226 SM
.map (fn (t
, v
, env
) => f env v
) ds
228 fun lookupType (Env (ts
, _
, _
, _
)) name
= SS
.member (ts
, name
)
229 fun lookupVal (Env (_
, vs
, _
, _
)) name
=
230 case SM
.find (vs
, name
) of
232 |
SOME (t
, _
, _
) => SOME t
233 fun lookupEquation (Env (_
, vs
, _
, _
)) name
=
234 case SM
.find (vs
, name
) of
236 |
SOME (_
, NONE
, _
) => NONE
237 |
SOME (_
, SOME eq
, env
) => SOME (eq
, env
)
238 fun lookupContext (Env (_
, _
, cs
, _
)) name
= SS
.member (cs
, name
)
239 fun lookupInitialDynEnvVal (Env (_
, _
, _
, ds
)) name
=
240 case SM
.find (ds
, name
) of
242 |
SOME (t
, _
, _
) => SOME t
244 fun bindType (Env (ts
, vs
, cs
, ds
)) name
= Env (SS
.add (ts
, name
), vs
, cs
, ds
)
245 fun bindVal (env
as (Env (ts
, vs
, cs
, ds
))) (name
, t
, eqo
) = Env (ts
, SM
.insert (vs
, name
, (t
, eqo
, env
)), cs
, ds
)
246 fun bindContext (Env (ts
, vs
, cs
, ds
)) name
= Env (ts
, vs
, SS
.add (cs
, name
), ds
)
247 fun bindInitialDynEnvVal (env
as (Env (ts
, vs
, cs
, ds
))) (name
, t
, eqn
) = Env (ts
, vs
, cs
, SM
.insert (ds
, name
, (t
, eqn
, env
)))
249 fun types (Env (ts
, _
, _
, _
)) = ts
250 fun vals (Env (_
, vs
, _
, _
)) = SM
.foldli (fn (name
, _
, vs
) => SS
.add (vs
, name
)) SS
.empty vs
251 fun contexts (Env (_
, _
, cs
, _
)) = cs
252 fun dynamics (Env (_
, _
, _
, ds
)) = SM
.foldli (fn (name
, _
, ds
) => SS
.add (ds
, name
)) SS
.empty ds