Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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 [] = "•"
- | pp_lhsms (h::t) = pp_pg h ^ " ⊳ " ^ 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 ^ ", ξ, {"^
- (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) ^ " ⊢ " ^ pp_pg p ^ " || " ^
- pp_pg q
- (* (indexed_control * local_state) list *)
- (* Pretty printer for indexed control stacks *)
- fun pp_ic [] = "•"
- | pp_ic ((k,ls)::t) = pp_control k ^ " ⊳ " ^ pp_ls ls ^ " ⊳ " ^ 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
Add Comment
Please, Sign In to add comment