[hcoop/domtool2.git] / 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
492c1cff AC	1	(* HCoop Domtool (http://hcoop.sourceforge.net/)
492c1cff AC	2	* Copyright (c) 2006, Adam Chlipala
e140629f	3	* Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
492c1cff AC	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.
dac62e84	18	*)
492c1cff AC	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
a3698041 AC	29	type typeRule = exp -> bool
a3698041 AC	30	val typeRules : typeRule SM.map ref = ref SM.empty
6be996d4 AC	31	fun registerType (name, rule) = typeRules := SM.insert (!typeRules, name, rule)
	32	fun typeRule name = SM.find (!typeRules, name)
	33
a3698041 AC	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
cf879b4f AC	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
e0b0abd2 AC	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
12adf55a AC	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
629a34f6 AC	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
8a7c40fa AC	109	fun bool (EVar "false", _) = SOME false
	110	\| bool (EVar "true", _) = SOME true
	111	\| bool _ = NONE
	112
629a34f6 AC	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
ed9fda3a AC	125	fun none func f (_, []) = (f ();
	126	SM.empty)
	127	\| none func _ (_, es) = badArgs (func, es)
	128
629a34f6 AC	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
f8dfbbcc AC	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)
6ae327f8	152
fb09779a AC	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
57e066bb AC	163	fun noneV func f (evs, []) = (f evs;
	164	SM.empty)
	165	\| noneV func _ (_, es) = badArgs (func, es)
	166
6ae327f8 AC	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
e0b0abd2 AC	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
6ae327f8 AC	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
47163553 AC	188	NONE => (Print.preface ("Unexpected value for " ^ name ^ ":",
	189	Print.p_exp e);
	190	raise Fail ("Bad format for environment variable " ^ name))
6ae327f8 AC	191	\| SOME v => v
6ae327f8 AC	192
629a34f6 AC	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
ed9fda3a	199	fun action_none name f = registerAction (name, none name f)
629a34f6 AC	200	fun action_one name args f = registerAction (name, one name args f)
629a34f6 AC	201	fun action_two name args f = registerAction (name, two name args f)
f8dfbbcc	202	fun action_three name args f = registerAction (name, three name args f)
fb09779a	203	fun action_four name args f = registerAction (name, four name args f)
629a34f6	204
e0b0abd2	205	fun actionV_none name f = registerAction (name, fn (env, _) => (f env; env))
6ae327f8	206	fun actionV_one name args f = registerAction (name, oneV name args f)
e0b0abd2	207	fun actionV_two name args f = registerAction (name, twoV name args f)
6ae327f8 AC	208
6ae327f8 AC	209	fun container_none name (f, g) = registerContainer (name, none name f, g)
629a34f6	210	fun container_one name args (f, g) = registerContainer (name, one name args f, g)
a3698041	211
57e066bb	212	fun containerV_none name (f, g) = registerContainer (name, noneV name f, g)
6ae327f8 AC	213	fun containerV_one name args (f, g) = registerContainer (name, oneV name args f, g)
6ae327f8 AC	214
8061fadf CE	215	datatype env = Env of SS.set * (typ * exp option * env) SM.map * SS.set * (typ * exp * env) SM.map
8061fadf CE	216	val empty : env = Env (SS.empty, SM.empty, SS.empty, SM.empty)
492c1cff	217
e140629f	218
8061fadf CE	219	fun initialDynEnvTypes (Env (_, _, _, ds)) =
8061fadf CE	220	SM.map (fn (t, _, _) => t) ds
e140629f	221
254d5faa CE	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) *)
8061fadf CE	225	fun initialDynEnvVals f (Env (_, _, _, ds)) =
8061fadf CE	226	SM.map (fn (t, v, env) => f env v) ds
e140629f	227
8061fadf CE	228	fun lookupType (Env (ts, _, _, _)) name = SS.member (ts, name)
8061fadf CE	229	fun lookupVal (Env (_, vs, _, _)) name =
492c1cff AC	230	case SM.find (vs, name) of
492c1cff AC	231	NONE => NONE
8061fadf CE	232	\| SOME (t, _, _) => SOME t
8061fadf CE	233	fun lookupEquation (Env (_, vs, _, _)) name =
492c1cff AC	234	case SM.find (vs, name) of
492c1cff AC	235	NONE => NONE
8061fadf CE	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 =
e140629f CE	240	case SM.find (ds, name) of
e140629f CE	241	NONE => NONE
8061fadf	242	\| SOME (t, _, _) => SOME t
492c1cff	243
8061fadf CE	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)))
095de39e	248
8061fadf CE	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
492c1cff AC	253
492c1cff AC	254	end