BAM definitions

gistfile1.fs

structure Syntax =
struct
	open Set

   type control = {name : string, active : bool, index : int option}

   val fresh = ref 0
   fun freshIndex {name=name, active=active, index=_} =
      {name=name, active=active, index=SOME (fresh := !fresh + 1; !fresh)}

   fun indexOf (k : control) =
      case #index k of
         NONE => []
       | SOME i => [i]

   (* Definition 1, 4 and 5 *)
	(* Definition 5 is covered because controls can optionally be
	   indexed. *)
   datatype graph = Par of graph * graph (* P | P *)
                  | Prefix of control * graph (* k.P *)
                  | Hole of int (* [ ]_int *)
                  | Index of graph * int (* <graph>_int *)
                  | Nil (* nil *)

   (* Definition 2 *)
   type inst_map = (int * int) set 
   type reaction_rule = graph * graph * inst_map
  
  	(* The identity instantiation map *)
   fun inst_id [] = [] : inst_map  | inst_id (h::t) = (h,h) :: inst_id t

   (* Definitions of notational helpers *)
   infix 6 || 
   infix 5 |-
   infix 4 |->
   infixr 7 $
   fun a || b = (a,b)
   fun a |- b = (a,b)
   fun (v,i) |-> e = Vector.update(v,i,e)

   (* Retrieve the set J of hole indices from a given process term *)
   fun holes (Hole j) = [j]
     | holes Stop = []
     | holes (Prefix(_,p)) = holes p
     | holes (Par(a,b)) = holes a @ holes b
     | holes (Index (p,_)) = holes p

   (* Pretty printer for place graphs *)

	fun pp_control {name=name, active=active, index=SOME i} = 
	  		name ^ "_" ^ Int.toString i
     | pp_control {name=name, ...} = name

   fun pp_pg (Par(a,b)) = pp_pg a ^ " | " ^ pp_pg b
     | pp_pg (Prefix(c,p)) = pp_control c ^ "." ^ pp_pg p
     | pp_pg (Hole i) = "[" ^ Int.toString i ^ "]"
     | pp_pg (Index (p,i)) = "<" ^ pp_pg p ^ ">_" ^ Int.toString i
     | pp_pg Stop = "nil"

   (* lhs_match_stack * graph * context_vec * inst_map * int list *)

   fun pp_ctx_vec v = "[" ^
      (Vector.foldli 
         (fn (i,a,b) => b ^ ", " ^ (Int.toString i) ^ ": " ^ pp_pg a) 
        "" 
        v) ^ "]"

   fun pp_lhsms [] = "&bull;"
     | pp_lhsms (h::t) = pp_pg h ^ " &#x22B3; " ^ pp_lhsms t

  fun pp_pm (P_L,L,P_R,D,Xi,I) = 
		"(" ^ pp_pg P_L ^ ", "^ pp_lhsms L ^", " ^ pp_pg P_R ^ ", " ^ pp_ctx_vec D ^ ", &xi;, {"^ 
       (String.concatWith "," (map Int.toString I)) ^ "})" 

   fun pp_pm_list l = String.concatWith "," (map pp_pm l) 

   (* Pretty printer for local states *)
   fun pp_ls (PM,(p,q)) = 
		(pp_pm_list PM) ^ " &#x22A2; " ^ pp_pg p ^ " || " ^ 
      pp_pg q
   (* (indexed_control * local_state) list *)

   (* Pretty printer for indexed control stacks *)
   fun pp_ic [] = "&bull;"
     | pp_ic ((k,ls)::t) = pp_control k ^ " &#x22b3; " ^ pp_ls ls ^ " &#x22B3; " ^ pp_ic t 

   (* Pretty printer for global states *)
   fun pp (ls,ic) = "(" ^ pp_ls ls ^ ", " ^ 
                            pp_ic ic ^ ") " 
end

signature SEMANTICS =
sig
   type control

   datatype graph = datatype Syntax.graph

	val reactionRules : (graph * graph * (int * int) Set.set) Set.set
end

signature PAMSIG = 
sig
   eqtype pam_state
   datatype graph = datatype Syntax.graph

   val PAR : pam_state -> pam_state
   val UNIT_strip : pam_state -> pam_state
   val UNIT_add : pam_state -> pam_state
   val MATCH : pam_state -> pam_state
   val POP : pam_state -> pam_state
   val REACT : pam_state -> pam_state
   val TOP : pam_state -> pam_state

   val initial_state : graph -> pam_state
   val pp : pam_state -> string
end

functor PAM (Semantics : SEMANTICS) : PAMSIG =
struct
	open Set
	open Syntax

   infix 4 |->
   
   exception RuleNotApplicable of string

   (* Definition 6 (Partial match) *)
   type context_vec = graph vector 
   type lhs_match_stack = graph list
   type partial_match = 
        graph * lhs_match_stack * graph * context_vec * inst_map * int set 

	(* Definition 7 (Initial partial matches) *)
   fun make_vec hs = Vector.fromList (map (fn i => Hole i) hs)

   fun init [] = [] : partial_match list
     | init ((P_L,P_R,xi)::t) = (P_L,
                                 [],
                                 P_R,
                                 make_vec (union ((holes P_L),(holes P_R))),
                                 xi,
                                 Set.empty) :: init t

   (* Definition 8 (PAM state) *)
   type local_state = partial_match list * (graph * graph)
   type control_stack = (control * local_state) list
   type pam_state = local_state * control_stack

   (* Definition 9 (Initial PAM state) *)
   fun initial_state p = 
      ((init (Semantics.reactionRules), (Nil,p)), [])

   (* Corollary definitions *)

   (* The first element of the tuple is the "alpha" parameter,
      indicating whether we are in an active context *)
   fun matchpre (true, k_i, PM) = 
         Set.union (matchnode (k_i, PM), init (Semantics.reactionRules))
     | matchpre (false, k_i, PM) = 
         matchnode (k_i, PM)

   and matchnode (k_i, PM) =
   let
      fun m ((Par (Prefix (k,P_L), P'_L), L, P_R, D, Xi, I) :: rest) =
         (P_L, P'_L :: L, P_R, D, Xi, Set.union (I,indexOf k_i)) :: m rest
        | m (h::t) = m t
        | m [] = []
   in
      m PM
   end

	and matchparcon(Prefix(k,p),PM) =
		union (matchpar (Prefix(k,p),PM), matchcontext PM)

	and matchpar(ki_p as Prefix(k,p),PM) =
		let
			fun m [] = []
			  | m ((Par(Hole j,P_L), L, P_R, D, xi, I) :: rest) =
					(Par(Hole j,P_L),
					 L,
					 P_R,
					 (D,j) |-> (Par(ki_p, Vector.sub (D,j))),
					 xi,
					 union (I, indexOf k)) :: m rest
			| m (_::rest) = m rest
		in
			m PM
		end

	and matchcontext [] = []
	  | matchcontext ((m as (_,[],_,_,_,_))::rest) = m :: matchcontext rest
	  | matchcontext (_::rest) = matchcontext rest

   fun act _ = false

	fun pop [] = []
	  | pop ((H, P'_L :: L, P_R, D, xi, I) :: rest) = 
		 let
			 fun c (Par (l,r)) = c l andalso c r
				| c (Hole j) = true
				| c _ = false
		 in
			 if not (c H) then pop rest 
							  else ((P'_L, L, P_R, D, xi, I) :: pop rest)
		 end

   (* Rule PAR *)

   fun PAR ((PM, (q, Par(Par(p,p'),p''))), S) =
      ((PM, (q, Par(p,Par(p',p'')))), S)
     | PAR _ = raise RuleNotApplicable "PAR"

   (* Rule UNIT_strip *)
   
   fun UNIT_strip ((PM, (q, Par(Nil,p))), S) =
      ((PM, (q, p)), S)
     | UNIT_strip _ = raise RuleNotApplicable "UNIT_strip"

   (* Rule UNIT_add *)

   fun UNIT_add ((PM, (q, Prefix (k_i,p))), S) =
      ((PM, (q, Par (Prefix (k_i,p),Nil))), S)
     | UNIT_add _ = raise RuleNotApplicable "UNIT_add"

   (* Rule MATCH *)

   fun MATCH ((PM, (q, Par (Prefix (k_i,p), p'))), S) =
      ((matchpre(act S, k_i, PM), (Nil, p)), 
         (k_i, (matchparcon (Prefix (k_i,p),PM), (q,p'))) :: S)
     | MATCH _ = raise RuleNotApplicable "MATCH"

   (* Rule POP *)

   fun POP ((PM, (q,Nil)), (k_j, (PM', (q',p))) :: S) =
      ((Set.union (PM',pop PM), (Par(q',Prefix(k_j,q)),p)), S)
     | POP _ = raise RuleNotApplicable "POP"

   (* Rule REACT *)

   fun pIndMemb (k : control,I) = 
      case #index k of NONE => false
                     | SOME i => Set.member (i,I)

   fun excl (Prefix (k,g),I) = 
         if pIndMemb (k,I) then Nil else Prefix (k, excl (g,I))
     | excl (Par (g1,g2),I) = Par (excl (g1,I), excl (g2,I))
     | excl (x,I) = x

   fun exclPM ([],I) = []
     | exclPM (PM,I) = 
	  		Set.filter (fn (_, _, _, _, _, I') => Set.inter (I,I') = []) PM

   fun exclS ([],I) = []
     | exclS ((k,(PM,(p,q)))::S_t,I) =
         if pIndMemb (k,I) then exclS (S_t,I)
         else (k,(exclPM (PM, I), (excl (p,I),excl (q,I)))) :: exclS (S_t,I)

   fun index (Par (g1,g2)) = Par (index g1, index g2)
     | index (Prefix (k,g)) = Prefix (freshIndex k, index g)
     | index x = x

	fun inst(P_R,D,xi) = 
	let
		fun s (Hole j) = 
			let
				fun inst_lk [] = Hole j
				  | inst_lk ((a,b)::t) = 
						if a = j then Vector.sub(D,b) else inst_lk t
			in
				inst_lk xi
			end
		  | s (Par(a,b)) = Par(s a, s b)
		  | s (Prefix(a,b)) = Prefix(a,s b)
		  | s (Index(a,i)) = Index(s a,i)
		  | s Nil = Nil
	in
		s P_R
	end

   fun REACT ((PM_all, (q,p)), S) =
   let
      val s = ref NONE : partial_match option ref

      fun allHoles (Hole j) = true
        | allHoles (Par (a,b)) = allHoles a andalso allHoles b
        | allHoles _ = false

      fun pmmatch ((P_L,[],P_R,D,Xi,I)::rest) =
         if allHoles P_L then (s := SOME (P_L,[],P_R,D,Xi,I); rest)
            else (P_L,[],P_R,D,Xi,I) :: pmmatch rest
        | pmmatch (h::t) = h :: pmmatch t
        | pmmatch [] = []
   in
      case (pmmatch PM_all,!s) of
         (_,NONE) => raise RuleNotApplicable "REACT"
       | (PM,SOME (P_L,_,P_R,D,Xi,I)) =>
         ((exclPM (PM,I), 
            (Par (excl (q,I), index (inst (P_R,D,Xi))), p)),
           exclS (S,I))
   end
		
   (* Rule TOP *)
   fun TOP ((PM, (q,Nil)), []) = 
      ((init (Semantics.reactionRules), (Nil,q)), [])
     | TOP _ = raise RuleNotApplicable "TOP"

end