--- /dev/null
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * 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.
+*)
+
+(* Domain-related primitive actions *)
+
+signature DOMAIN = sig
+
+ val registerBefore : (string -> unit) -> unit
+ val registerAfter : (string -> unit) -> unit
+ (* Register handlers to run just before and after entering a domain
+ * block. *)
+
+end
--- /dev/null
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * 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.
+*)
+
+(* Domain-related primitive actions *)
+
+structure Domain :> DOMAIN = struct
+
+open Ast
+
+val befores = ref (fn (_ : string) => ())
+val afters = ref (fn (_ : string) => ())
+
+fun registerBefore f =
+ let
+ val old = !befores
+ in
+ befores := (fn x => (old x; f x))
+ end
+
+fun registerAfter f =
+ let
+ val old = !afters
+ in
+ afters := (fn x => (old x; f x))
+ end
+
+val current = ref ""
+
+val _ = Env.registerContainer ("domain",
+ fn (_, [(EString dom, _)]) => (current := dom;
+ !befores dom;
+ StringMap.empty)
+ | _ => Env.badArgs "domain",
+ fn () => !afters (!current))
+
+end
reduce.sig
reduce.sml
+eval.sig
+eval.sml
+
baseTypes.sig
baseTypes.sml
+domain.sig
+domain.sml
+
main.sig
main.sml
signature ENV = sig
- val registerType : string * (Ast.exp -> bool) -> unit
- val typeRule : string -> (Ast.exp -> bool) option
+ type typeRule = Ast.exp -> bool
+ val registerType : string * typeRule -> unit
+ val typeRule : string -> typeRule option
+
+ type env_vars = Ast.exp Ast.StringMap.map
+ type action = env_vars * Ast.exp list -> env_vars
+ val registerAction : string * action -> unit
+ val action : string -> action option
+
+ val registerContainer : string * action * (unit -> unit) -> unit
+ val container : string -> (action * (unit -> unit)) option
+
+ val badArgs : string -> 'a
type env
val empty : env
structure SS = StringSet
structure SM = StringMap
-val typeRules : (exp -> bool) SM.map ref = ref SM.empty
+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)
+
+fun badArgs name = raise Fail ("Invalid arguments to " ^ name)
+
type env = SS.set * (typ * exp option) SM.map
val empty : env = (SS.add (SS.singleton "int", "string"),
SM.empty)
--- /dev/null
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * 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.
+*)
+
+(* Execution of Domtool programs reduced to primitive actions *)
+
+signature EVAL = sig
+
+ val exec : Env.env_vars -> Ast.exp -> unit
+
+end
--- /dev/null
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * 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.
+*)
+
+(* Execution of Domtool programs reduced to primitive actions *)
+
+structure Eval :> EVAL = struct
+
+open Ast
+
+structure SM = StringMap
+
+fun lookup (evs, ev) =
+ case SM.find (evs, ev) of
+ NONE => raise Fail ("Couldn't find an environment variable "
+ ^ ev ^ " that type-checking has guaranteed")
+ | SOME v => v
+
+val conjoin : Env.env_vars * Env.env_vars -> Env.env_vars =
+ SM.unionWith #2
+
+fun findPrimitive e =
+ let
+ fun findPrim (e, _) =
+ case e of
+ EVar name => (name, [])
+ | EApp (e1, e2) =>
+ let
+ val (name, args) = findPrim e1
+ in
+ (name, e2 :: args)
+ end
+ | _ => raise Fail "Non-primitive action left after reduction"
+
+ val (name, args) = findPrim e
+ in
+ (name, rev args)
+ end
+
+fun exec evs e =
+ let
+ fun exec' evs (eAll as (e, _)) =
+ case e of
+ ESkip => SM.empty
+ | ESet (ev, e) => SM.insert (SM.empty, ev, e)
+ | EGet (x, ev, e) => exec' evs (Reduce.subst x (lookup (evs, ev)) e)
+ | ESeq es =>
+ let
+ val (new, _) =
+ foldl (fn (e, (new, keep)) =>
+ let
+ val new' = exec' keep e
+ in
+ (conjoin (new, new'),
+ conjoin (keep, new'))
+ end) (SM.empty, evs) es
+ in
+ new
+ end
+ | ELocal (e1, e2) =>
+ let
+ val evs' = exec' evs e1
+ val evs'' = exec' (conjoin (evs, evs')) e2
+ in
+ conjoin (evs, evs'')
+ end
+ | EWith (e1, e2) =>
+ let
+ val (prim, args) = findPrimitive e1
+ in
+ case Env.container prim of
+ NONE => raise Fail "Unbound primitive container"
+ | SOME (action, cleanup) =>
+ let
+ val evs' = action (evs, args)
+ val evs'' = exec' evs e2
+ in
+ cleanup ();
+ conjoin (conjoin (evs, evs'), evs'')
+ end
+ end
+
+ | _ =>
+ let
+ val (prim, args) = findPrimitive eAll
+ in
+ case Env.action prim of
+ NONE => raise Fail "Unbound primitive action"
+ | SOME action => action (evs, args)
+ end
+
+ val evs' = exec' evs e
+ in
+ ()
+ end
+
+end
val tInit : Ast.typ
val check : string -> unit
+ val reduce : string -> unit
+ val eval : string -> unit
end
dmy)
fun check fname =
+ let
+ val prog = Parse.parse fname
+ in
+ if !ErrorMsg.anyErrors then
+ ()
+ else
+ let
+ val G' = Tycheck.checkFile Env.empty tInit prog
+ in
+ ()
+ end
+ end
+
+fun reduce fname =
let
val prog = Parse.parse fname
in
end
end
+fun eval fname =
+ let
+ val prog = Parse.parse fname
+ in
+ if !ErrorMsg.anyErrors then
+ ()
+ else
+ let
+ val G' = Tycheck.checkFile Env.empty tInit prog
+ in
+ if !ErrorMsg.anyErrors then
+ ()
+ else
+ case prog of
+ (_, SOME body) => Eval.exec StringMap.empty body
+ | _ => ()
+ end
+ end
+
end
--- /dev/null
+extern val domain : string -> Domain => [Root];
+
+domain "hcoop.net" with
+
+end