src/env.sml

   1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
   2  * Copyright (c) 2006, Adam Chlipala
   3  * Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
   4  *
   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.
   9  *
  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.
  14  *
  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.
  18  *)
  19
  20 (* Domtool type-checking and reduction environments *)
  21
  22 structure Env :> ENV = struct
  23
  24 open Ast
  25
  26 structure SS = StringSet
  27 structure SM = StringMap
  28
  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)
  33
  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)
  39
  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)
  44
  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)
  49
  50 local
  51     val pr = ref (fn () => ())
  52 in
  53
  54 fun registerPre f =
  55     let
  56         val old = !pr
  57     in
  58         pr := (fn () => (old (); f ()))
  59     end
  60 fun pre () = !pr ()
  61
  62 end
  63
  64 local
  65     val pst = ref (fn () => ())
  66 in
  67
  68 fun registerPost f =
  69     let
  70         val old = !pst
  71     in
  72         pst := (fn () => (old (); f ()))
  73     end
  74 fun post () = !pst ()
  75
  76 end
  77
  78 local
  79     val pr = ref (fn () => ())
  80 in
  81
  82 fun registerPreTycheck f =
  83     let
  84         val old = !pr
  85     in
  86         pr := (fn () => (old (); f ()))
  87     end
  88 fun preTycheck () = !pr ()
  89
  90 end
  91
  92 fun badArgs (name, args) =
  93     (print ("Invalid arguments to " ^ name ^ "\n");
  94      app (fn arg => Print.preface ("Argument: ", Print.p_exp arg)) args;
  95      raise Domain)
  96 fun badArg (func, arg, v) =
  97     (print ("Invalid " ^ arg ^ " argument to " ^ func ^ "\n");
  98      Print.preface ("Argument: ", Print.p_exp v);
  99      raise Domain)
 100
 101 type 'a arg = exp -> 'a option
 102
 103 fun int (EInt n, _) = SOME n
 104   | int _ = NONE
 105
 106 fun string (EString s, _) = SOME s
 107   | string _ = NONE
 108
 109 fun bool (EVar "false", _) = SOME false
 110   | bool (EVar "true", _) = SOME true
 111   | bool _ = NONE
 112
 113 fun mapFail f [] = SOME []
 114   | mapFail f (h :: t) =
 115     case f h of
 116         NONE => NONE
 117       | SOME h' =>
 118         case mapFail f t of
 119             NONE => NONE
 120           | SOME t' => SOME (h' :: t')
 121
 122 fun list f (EList ls, _) = mapFail f ls
 123   | list _ _ = NONE
 124
 125 fun none func f (_, []) = (f ();
 126                            SM.empty)
 127   | none func _ (_, es) = badArgs (func, es)
 128
 129 fun one func (name, arg) f (_, [e]) =
 130     (case arg e of
 131          NONE => badArg (func, name, e)
 132        | SOME v => (f v;
 133                     SM.empty))
 134   | one func _ _ (_, es) = badArgs (func, es)
 135
 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);
 141                                 SM.empty))
 142   | two func _ _ (_, es) = badArgs (func, es)
 143
 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);
 150                                          SM.empty))
 151   | three func _ _ (_, es) = badArgs (func, es)
 152
 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);
 160                                                   SM.empty))
 161   | four func _ _ (_, es) = badArgs (func, es)
 162
 163 fun noneV func f (evs, []) = (f evs;
 164                               SM.empty)
 165   | noneV func _ (_, es) = badArgs (func, es)
 166
 167 fun oneV func (name, arg) f (evs, [e]) =
 168     (case arg e of
 169          NONE => badArg (func, name, e)
 170        | SOME v => (f (evs, v);
 171                     SM.empty))
 172   | oneV func _ _ (_, es) = badArgs (func, es)
 173
 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);
 179                                 SM.empty))
 180   | twoV func _ _ (_, es) = badArgs (func, es)
 181
 182
 183 fun env arg (evs, name) =
 184     case SM.find (evs, name) of
 185         NONE => raise Fail ("Unavailable environment variable " ^ name)
 186       | SOME e =>
 187         case arg e of
 188             NONE => (Print.preface ("Unexpected value for " ^ name ^ ":",
 189                                     Print.p_exp e);
 190                      raise Fail ("Bad format for environment variable " ^ name))
 191           | SOME v => v
 192
 193 fun type_one func arg f =
 194     registerType (func, fn e =>
 195                            case arg e of
 196                                NONE => false
 197                              | SOME v => f v)
 198
 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)
 204
 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)
 208
 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)
 211
 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)
 214
 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)
 217
 218
 219 fun initialDynEnvTypes (Env (_, _, _, ds)) =
 220     SM.map (fn (t, _, _) => t) ds
 221
 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
 227
 228 fun lookupType (Env (ts, _, _, _)) name = SS.member (ts, name)
 229 fun lookupVal (Env (_, vs, _, _)) name =
 230     case SM.find (vs, name) of
 231         NONE => NONE
 232       | SOME (t, _, _) => SOME t
 233 fun lookupEquation (Env (_, vs, _, _)) name =
 234     case SM.find (vs, name) of
 235         NONE => NONE
 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
 241         NONE => NONE
 242       | SOME (t, _, _) => SOME t
 243
 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)))
 248
 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
 253
 254 end