src/env.sml

(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006, Adam Chlipala
 * Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
 *)

(* Domtool type-checking and reduction environments *)

structure Env :> ENV = struct

open Ast

structure SS = StringSet
structure SM = StringMap

type typeRule = exp -> bool
val typeRules : typeRule SM.map ref = ref SM.empty
fun registerType (name, rule) = typeRules := SM.insert (!typeRules, name, rule)
fun typeRule name = SM.find (!typeRules, name)

type env_vars = exp SM.map
type action = env_vars * Ast.exp list -> env_vars
val actions : action SM.map ref = ref SM.empty
fun registerAction (name, action) = actions := SM.insert (!actions, name, action)
fun action name = SM.find (!actions, name)

val containers : (action * (unit -> unit)) SM.map ref = ref SM.empty
fun registerContainer (name, befor, after) =
    containers := SM.insert (!containers, name, (befor, after))
fun container name = SM.find (!containers, name)

val functions : (exp list -> exp option) SM.map ref = ref SM.empty
fun registerFunction (name, f) =
    functions := SM.insert (!functions, name, f)
fun function name = SM.find (!functions, name)

local
    val pr = ref (fn () => ())
in

fun registerPre f =
    let
	val old = !pr
    in
	pr := (fn () => (old (); f ()))
    end
fun pre () = !pr ()

end

local
    val pst = ref (fn () => ())
in

fun registerPost f =
    let
	val old = !pst
    in
	pst := (fn () => (old (); f ()))
    end
fun post () = !pst ()

end

local
    val pr = ref (fn () => ())
in

fun registerPreTycheck f =
    let
	val old = !pr
    in
	pr := (fn () => (old (); f ()))
    end
fun preTycheck () = !pr ()

end

fun badArgs (name, args) =
    (print ("Invalid arguments to " ^ name ^ "\n");
     app (fn arg => Print.preface ("Argument: ", Print.p_exp arg)) args;
     raise Domain)
fun badArg (func, arg, v) =
    (print ("Invalid " ^ arg ^ " argument to " ^ func ^ "\n");
     Print.preface ("Argument: ", Print.p_exp v);
     raise Domain)

type 'a arg = exp -> 'a option

fun int (EInt n, _) = SOME n
  | int _ = NONE

fun string (EString s, _) = SOME s
  | string _ = NONE

fun bool (EVar "false", _) = SOME false
  | bool (EVar "true", _) = SOME true
  | bool _ = NONE

fun mapFail f [] = SOME []
  | mapFail f (h :: t) =
    case f h of
	NONE => NONE
      | SOME h' =>
	case mapFail f t of
	    NONE => NONE
	  | SOME t' => SOME (h' :: t')

fun list f (EList ls, _) = mapFail f ls
  | list _ _ = NONE

fun none func f (_, []) = (f ();
			   SM.empty)
  | none func _ (_, es) = badArgs (func, es)

fun one func (name, arg) f (_, [e]) =
    (case arg e of
	 NONE => badArg (func, name, e)
       | SOME v => (f v;
		    SM.empty))
  | one func _ _ (_, es) = badArgs (func, es)

fun two func (name1, arg1, name2, arg2) f (_, [e1, e2]) =
    (case (arg1 e1, arg2 e2) of
	 (NONE, _) => badArg (func, name1, e1)
       | (_, NONE) => badArg (func, name2, e2)
       | (SOME v1, SOME v2) => (f (v1, v2);
				SM.empty))
  | two func _ _ (_, es) = badArgs (func, es)

fun three func (name1, arg1, name2, arg2, name3, arg3) f (_, [e1, e2, e3]) =
    (case (arg1 e1, arg2 e2, arg3 e3) of
	 (NONE, _, _) => badArg (func, name1, e1)
       | (_, NONE, _) => badArg (func, name2, e2)
       | (_, _, NONE) => badArg (func, name3, e3)
       | (SOME v1, SOME v2, SOME v3) => (f (v1, v2, v3);
					 SM.empty))
  | three func _ _ (_, es) = badArgs (func, es)

fun four func (name1, arg1, name2, arg2, name3, arg3, name4, arg4) f (_, [e1, e2, e3, e4]) =
    (case (arg1 e1, arg2 e2, arg3 e3, arg4 e4) of
	 (NONE, _, _, _) => badArg (func, name1, e1)
       | (_, NONE, _, _) => badArg (func, name2, e2)
       | (_, _, NONE, _) => badArg (func, name3, e3)
       | (_, _, _, NONE) => badArg (func, name4, e4)
       | (SOME v1, SOME v2, SOME v3, SOME v4) => (f (v1, v2, v3, v4);
						  SM.empty))
  | four func _ _ (_, es) = badArgs (func, es)

fun noneV func f (evs, []) = (f evs;
			      SM.empty)
  | noneV func _ (_, es) = badArgs (func, es)

fun oneV func (name, arg) f (evs, [e]) =
    (case arg e of
	 NONE => badArg (func, name, e)
       | SOME v => (f (evs, v);
		    SM.empty))
  | oneV func _ _ (_, es) = badArgs (func, es)

fun twoV func (name1, arg1, name2, arg2) f (evs, [e1, e2]) =
    (case (arg1 e1, arg2 e2) of
	 (NONE, _) => badArg (func, name1, e1)
       | (_, NONE) => badArg (func, name2, e2)
       | (SOME v1, SOME v2) => (f (evs, v1, v2);
				SM.empty))
  | twoV func _ _ (_, es) = badArgs (func, es)


fun env arg (evs, name) =
    case SM.find (evs, name) of
	NONE => raise Fail ("Unavailable environment variable " ^ name)
      | SOME e =>
	case arg e of
	    NONE => (Print.preface ("Unexpected value for " ^ name ^ ":",
				    Print.p_exp e);
		     raise Fail ("Bad format for environment variable " ^ name))
	  | SOME v => v

fun type_one func arg f =
    registerType (func, fn e =>
			   case arg e of
			       NONE => false
			     | SOME v => f v)

fun action_none name f = registerAction (name, none name f)
fun action_one name args f = registerAction (name, one name args f)
fun action_two name args f = registerAction (name, two name args f)
fun action_three name args f = registerAction (name, three name args f)
fun action_four name args f = registerAction (name, four name args f)

fun actionV_none name f = registerAction (name, fn (env, _) => (f env; env))
fun actionV_one name args f = registerAction (name, oneV name args f)
fun actionV_two name args f = registerAction (name, twoV name args f)

fun container_none name (f, g) = registerContainer (name, none name f, g)
fun container_one name args (f, g) = registerContainer (name, one name args f, g)

fun containerV_none name (f, g) = registerContainer (name, noneV name f, g)
fun containerV_one name args (f, g) = registerContainer (name, oneV name args f, g)

datatype env = Env of SS.set * (typ * exp option * env) SM.map * SS.set * (typ * exp * env) SM.map
val empty : env = Env (SS.empty, SM.empty, SS.empty, SM.empty)


fun initialDynEnvTypes (Env (_, _, _, ds)) =
    SM.map (fn (t, _, _) => t) ds

(* hack ahead: These are not reduced when declared and must be before
   starting evaluation. Pass in reduceExp, and force an awkward
   calling convention so no one thinks this is the Right Way (tm) *)
fun initialDynEnvVals f (Env (_, _, _, ds)) =
    SM.map (fn (t, v, env) => f env v) ds

fun lookupType (Env (ts, _, _, _)) name = SS.member (ts, name)
fun lookupVal (Env (_, vs, _, _)) name =
    case SM.find (vs, name) of
	NONE => NONE
      | SOME (t, _, _) => SOME t
fun lookupEquation (Env (_, vs, _, _)) name =
    case SM.find (vs, name) of
	NONE => NONE
      | SOME (_, NONE, _) => NONE
      | SOME (_, SOME eq, env) => SOME (eq, env)
fun lookupContext (Env (_, _, cs, _)) name = SS.member (cs, name)
fun lookupInitialDynEnvVal (Env (_, _, _, ds)) name =
    case SM.find (ds, name) of
	NONE => NONE
      | SOME (t, _, _) => SOME t

fun bindType (Env (ts, vs, cs, ds)) name = Env (SS.add (ts, name), vs, cs, ds)
fun bindVal (env as (Env (ts, vs, cs, ds))) (name, t, eqo) = Env (ts, SM.insert (vs, name, (t, eqo, env)), cs, ds)
fun bindContext (Env (ts, vs, cs, ds)) name = Env (ts, vs, SS.add (cs, name), ds)
fun bindInitialDynEnvVal (env as (Env (ts, vs, cs, ds))) (name, t, eqn) = Env (ts, vs, cs, SM.insert (ds, name, (t, eqn, env)))

fun types (Env (ts, _, _, _)) = ts
fun vals (Env (_, vs, _, _)) = SM.foldli (fn (name, _, vs) => SS.add (vs, name)) SS.empty vs
fun contexts (Env (_, _, cs, _)) = cs
fun dynamics (Env (_, _, _, ds)) = SM.foldli (fn (name, _, ds) => SS.add (ds, name)) SS.empty ds

end
Commit	Line	Data
	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