src/env.sml

   1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
   2  * Copyright (c) 2006, Adam Chlipala
   3  *
   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.
   8  *
   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.
  13  *
  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.
  17  *)
  18
  19 (* Domtool type-checking and reduction environments *)
  20
  21 structure Env :> ENV = struct
  22
  23 open Ast
  24
  25 structure SS = StringSet
  26 structure SM = StringMap
  27
  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)
  32
  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)
  38
  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)
  43
  44 local
  45     val pr = ref (fn () => ())
  46 in
  47
  48 fun registerPre f =
  49     let
  50         val old = !pr
  51     in
  52         pr := (fn () => (old (); f ()))
  53     end
  54 fun pre () = !pr ()
  55
  56 end
  57
  58 local
  59     val pst = ref (fn () => ())
  60 in
  61
  62 fun registerPost f =
  63     let
  64         val old = !pst
  65     in
  66         pst := (fn () => (old (); f ()))
  67     end
  68 fun post () = !pst ()
  69
  70 end
  71
  72 local
  73     val pr = ref (fn () => ())
  74 in
  75
  76 fun registerPreTycheck f =
  77     let
  78         val old = !pr
  79     in
  80         pr := (fn () => (old (); f ()))
  81     end
  82 fun preTycheck () = !pr ()
  83
  84 end
  85
  86 fun badArgs (name, args) =
  87     (print ("Invalid arguments to " ^ name ^ "\n");
  88      app (fn arg => Print.preface ("Argument: ", Print.p_exp arg)) args;
  89      raise Domain)
  90 fun badArg (func, arg, v) =
  91     (print ("Invalid " ^ arg ^ " argument to " ^ func ^ "\n");
  92      Print.preface ("Argument: ", Print.p_exp v);
  93      raise Domain)
  94
  95 type 'a arg = exp -> 'a option
  96
  97 fun int (EInt n, _) = SOME n
  98   | int _ = NONE
  99
 100 fun string (EString s, _) = SOME s
 101   | string _ = NONE
 102
 103 fun bool (EVar "false", _) = SOME false
 104   | bool (EVar "true", _) = SOME true
 105   | bool _ = NONE
 106
 107 fun mapFail f [] = SOME []
 108   | mapFail f (h :: t) =
 109     case f h of
 110         NONE => NONE
 111       | SOME h' =>
 112         case mapFail f t of
 113             NONE => NONE
 114           | SOME t' => SOME (h' :: t')
 115
 116 fun list f (EList ls, _) = mapFail f ls
 117   | list _ _ = NONE
 118
 119 fun none func f (_, []) = (f ();
 120                            SM.empty)
 121   | none func _ (_, es) = badArgs (func, es)
 122
 123 fun one func (name, arg) f (_, [e]) =
 124     (case arg e of
 125          NONE => badArg (func, name, e)
 126        | SOME v => (f v;
 127                     SM.empty))
 128   | one func _ _ (_, es) = badArgs (func, es)
 129
 130 fun two func (name1, arg1, name2, arg2) f (_, [e1, e2]) =
 131     (case (arg1 e1, arg2 e2) of
 132          (NONE, _) => badArg (func, name1, e1)
 133        | (_, NONE) => badArg (func, name2, e2)
 134        | (SOME v1, SOME v2) => (f (v1, v2);
 135                                 SM.empty))
 136   | two func _ _ (_, es) = badArgs (func, es)
 137
 138 fun three func (name1, arg1, name2, arg2, name3, arg3) f (_, [e1, e2, e3]) =
 139     (case (arg1 e1, arg2 e2, arg3 e3) of
 140          (NONE, _, _) => badArg (func, name1, e1)
 141        | (_, NONE, _) => badArg (func, name2, e2)
 142        | (_, _, NONE) => badArg (func, name3, e3)
 143        | (SOME v1, SOME v2, SOME v3) => (f (v1, v2, v3);
 144                                          SM.empty))
 145   | three func _ _ (_, es) = badArgs (func, es)
 146
 147 fun oneV func (name, arg) f (evs, [e]) =
 148     (case arg e of
 149          NONE => badArg (func, name, e)
 150        | SOME v => (f (evs, v);
 151                     SM.empty))
 152   | oneV func _ _ (_, es) = badArgs (func, es)
 153
 154 fun twoV func (name1, arg1, name2, arg2) f (evs, [e1, e2]) =
 155     (case (arg1 e1, arg2 e2) of
 156          (NONE, _) => badArg (func, name1, e1)
 157        | (_, NONE) => badArg (func, name2, e2)
 158        | (SOME v1, SOME v2) => (f (evs, v1, v2);
 159                                 SM.empty))
 160   | twoV func _ _ (_, es) = badArgs (func, es)
 161
 162
 163 fun env arg (evs, name) =
 164     case SM.find (evs, name) of
 165         NONE => raise Fail ("Unavailable environment variable " ^ name)
 166       | SOME e =>
 167         case arg e of
 168             NONE => raise Fail ("Bad format for environment variable " ^ name)
 169           | SOME v => v
 170
 171 fun type_one func arg f =
 172     registerType (func, fn e =>
 173                            case arg e of
 174                                NONE => false
 175                              | SOME v => f v)
 176
 177 fun action_none name f = registerAction (name, none name f)
 178 fun action_one name args f = registerAction (name, one name args f)
 179 fun action_two name args f = registerAction (name, two name args f)
 180 fun action_three name args f = registerAction (name, three name args f)
 181
 182 fun actionV_none name f = registerAction (name, fn (env, _) => (f env; env))
 183 fun actionV_one name args f = registerAction (name, oneV name args f)
 184 fun actionV_two name args f = registerAction (name, twoV name args f)
 185
 186 fun container_none name (f, g) = registerContainer (name, none name f, g)
 187 fun container_one name args (f, g) = registerContainer (name, one name args f, g)
 188
 189 fun containerV_one name args (f, g) = registerContainer (name, oneV name args f, g)
 190
 191 type env = SS.set * (typ * exp option) SM.map * SS.set
 192 val empty : env = (SS.empty, SM.empty, SS.empty)
 193
 194 fun lookupType (ts, _, _) name = SS.member (ts, name)
 195 fun lookupVal (_, vs, _) name =
 196     case SM.find (vs, name) of
 197         NONE => NONE
 198       | SOME (t, _) => SOME t
 199 fun lookupEquation (_, vs, _) name =
 200     case SM.find (vs, name) of
 201         NONE => NONE
 202       | SOME (_, eqo) => eqo
 203 fun lookupContext (_, _, cs) name = SS.member (cs, name)
 204
 205 fun bindType (ts, vs, cs) name = (SS.add (ts, name), vs, cs)
 206 fun bindVal (ts, vs, cs) (name, t, eqo) = (ts, SM.insert (vs, name, (t, eqo)), cs)
 207 fun bindContext (ts, vs, cs) name = (ts, vs, SS.add (cs, name))
 208
 209 fun types (ts, _, _) = ts
 210 fun vals (_, vs, _) = SM.foldli (fn (name, _, vs) => SS.add (vs, name)) SS.empty vs
 211 fun contexts (_, _, cs) = cs
 212
 213 end