RCS "$Id: Agent.str,v 1.41 1999/07/18 10:53:55 pxs Exp $";
functor Agent (structure A : ACT_PROTECTED) : AGENT_PROTECTED =
struct
   structure A' = A
   structure A = A
   structure Value = A'.Value'
   open MaybeVar
  
   structure Eval : EVAL = Eval(structure Value = Value);
   structure P : PREFIX = Prefix(structure A = A');

  exception Unguarded of V.var
  exception Unguarded_rec of V.var

  val processAlgebra = CCS
    
   type actionSet = A.ActionSet.set MaybeVar.maybeVar

   (* Restriction invariant: a literally given set is never empty *)
(* Perdita, ensure this! *)
   type literalRestriction = A.PortSet.set
   type restriction = literalRestriction MaybeVar.maybeVar
			  
   structure RelabellingKey:ORD_KEY =
     struct
       type ord_key = A.port
       fun  compare (v,v') = if A.portEq (v, v')
			      then General.EQUAL
			    else if A.portLe (v',v)
				   then General.LESS
				 else General.GREATER
     end;

   structure LiteralRelabelling = SmallDict (RelabellingKey);

(* key is a port, value is more general so you can relabel a -> 'b *)
(* Do not now capture exactly the legal things, though *)
   type literalRelabelling = A.act LiteralRelabelling.map
   type relabelling = literalRelabelling MaybeVar.maybeVar

(* stuff about formal params. Times aren't distinguished from actions. *)
   datatype paramType = ActParamType | ActionSetParamType
     | AgentParamType
   type formalParams = paramType SmallVarDict.map
   fun noFormalParams _ = SmallVarDict.empty : formalParams

   fun makeParamType "act" = ActParamType
     | makeParamType "set" = ActionSetParamType
     | makeParamType "agent" = AgentParamType
     | makeParamType s = raise PanicNoisily ("Agent.str, makeParamType "^s)

   fun paramTypeString ActParamType = "act"
     | paramTypeString ActionSetParamType = "set"
     | paramTypeString AgentParamType = "agent"

(* hmm, what do we *really* want to be able to parameterise on Perdita? *)
(* E.g. why not on relabellings?? Need to rethink all this! *)
(* It's crazy that formal params have this type as well as actual params, *)
(* but they do. *)
   datatype param = ActParam   of A.act
   | ActionSetParam of actionSet
   | TimeParam  of int			(* never used as formal param! *)
   | AgentParam of agent'

   and privateAgent = Nil
                  | DNil
                  | Bottom
                  | Var      of V.var * param list
                  | Prefix   of P.prefix list * agent' (* should be multiset! *)
                  | Delta    of P.prefix * agent'
                  | Time     of int * agent'
                  | WSum     of agent' list
                  | SSum     of agent' list
                  | Parallel of agent' list
                  | SMerge   of (agent' * actionSet) list
                  | Restrict of agent' * restriction
                  | Relabel  of agent' * relabelling
                  | Open     of agent' * Eval.evaluation

   and agent' = DUMMY of (privateAgent * Word.word) ref
   type agent = agent'
     
   fun real (DUMMY i) = fst (!i)

  
(********************** stuff about relabellings *************************)
(* Take a list of action pairs. Complain if self-contradictory. Values in *)
(* the From actions will be ignored, but you *can* relabel 'a to 'b(5)    *)
(* Caveat user! *)
(* Remove redundant relabellings of an action to itself (which may arise  *)
(* from composition of relabellings, as well as from lusers *)
   fun makeLiteralRelabelling x =
(* Insert the given pairs, checking that there are no inconsistencies *)
     let
       fun insert current [] = current
	 | insert current ((to, from)::t) =
	   if A.eq (to, from) then insert current t
	   else
	     let
	       val (key, value) = case ((A.portOf from), (A.isInput from)) of
		 (NONE, NONE) =>
		   raise (Error ("Can't relabel "^(A.mkstr from)))
	       | (SOME p, SOME b) => (p, if b then to else A.inverse to)
	       | _ => raise PanicNoisily "Agent.str, makeLiteralRelabelling"
	     in	
	       case LiteralRelabelling.find(current, key) of NONE =>
		 insert (LiteralRelabelling.insert (current, key, value)) t
	     | SOME (act) =>
		 if A.eq (value, act) 
		   then insert current t (* duplicate, ignore it *)
		 else raise (Error "Relabelling must be a function!")
	     end
     in insert (LiteralRelabelling.empty) x
     end

(* The pairs we return are in the order you write them in in CCS: (to,from) *)
   fun unmakeLiteralRelabelling l =
     SL.sort
(* there can be no equal actions in second place, so simple *)
     (fn ((_,a),(_,b)) => A.le (a,b))
     true
     (map (fn (port, act) => (act, A.makeAct (port,true,NONE)))
      (LiteralRelabelling.listItemsi l))	(* HACK! *)
     
(* relabel an action a according to the literalRelabelling r, return a[r]  *)
   fun relabelAction r a = case A.portOf a of
     NONE => a				(* it can't be relabelled *)
   | SOME p => (case LiteralRelabelling.find (r,p) of
		  NONE => a		(* it isn't relabelled *)
		| SOME b => A.change b a)

(* composition of literalRelabellings: A[f O g] is (A[f])[g] *)
(* NB pairs in one relabelling are simultaneous: A[a/b,b/a] behaves as A *)
(* with a and b swapped; (A[a/b])[b/a] behaves as A. This sounds simple  *)
(* enough but a previous version had a related bug -- beware!            *)
   infix O
   fun f O g =
(* here's the final effect on things in the domain of f. Cumbersome way, but*)
(* easily means no redundant [a/a] pairs *)
     let val partial = (makeLiteralRelabelling
			(map (fn (a,b) => (relabelAction g a,b))
			 (unmakeLiteralRelabelling f)))
(* now we need to add the effects of things in the domain of g but not f *)
       fun update (current, []) = current
	 | update (current, (key, value)::t) =
(* NB really do mean in domain of f, not partial! Consider f = [b/a],    *)
(* g = [a/b,c/a]. Partial is empty, but c/a must not end up in the answer *)
	   (case LiteralRelabelling.find(f, key) of
	      NONE =>
		update (LiteralRelabelling.insert (current, key, value), t)
	    | SOME (act) => current)
     in
       update (partial, LiteralRelabelling.listItemsi g)
     end

(****************** Stuff about literal restrictions *****************)
fun forbids r a =
  case A.portOf a of NONE => false | SOME p => A.PortSet.member (r, p)
(* one-off fn just used by normalform -- can't think of a better way now! *)
(* Remove restrictions which do not affect the given portset f *)
fun cropRestriction effectiveToRestrict r =
  let val restriction = A.PortSet.intersection (r, effectiveToRestrict)
  in case A.PortSet.unmake restriction of [] => NONE | _ => SOME restriction
  end
(**************************** STRING-MAKING **********************************)
   fun meije _ = false	     (* Perdita, should be some kind of UI option *)
     
   fun prio Nil               = 99
     | prio DNil              = 99
     | prio Bottom            = 99
     | prio (Var _)           = 99
     | prio (Prefix _)        = 50
     | prio (Delta _)         = 50
     | prio (Time _)          = 50
     | prio (WSum [])         = prio Nil
     | prio (WSum [A])        = prio (real A)
     | prio (WSum _)          = 20
     | prio (SSum [])         = prio DNil
     | prio (SSum [A])        = prio (real A)
     | prio (SSum _)          = 30
     | prio (Parallel [])     = prio Nil
     | prio (Parallel [A])    = prio (real A)
     | prio (Parallel _)      = 40
     | prio (SMerge [])       = prio Nil
     | prio (SMerge [(A,_)])  = prio (real A)
     | prio (SMerge _)        = 45
     | prio (Restrict _)      = 60
     | prio (Relabel _)       = 60
     | prio (Open(A,_))       = prio (real A)

   val actionSetString = MaybeVar.maybeVarString A.ActionSet.setString

   fun restrictionString r =
     let fun stringer r = case A.PortSet.unmake r of
       [] =>  raise PanicNoisily "Agent.str, restrictionString"
     | [a] => A.portString a
     | l => (if meije() then "" else "{")^
	 (Lib.mkstr A.portString (if meije() then "\\" else ",") l)^
	 (if meije() then "" else "}")
     in "\\"^(MaybeVar.maybeVarString stringer r)
     end

   fun literalRelabellingString l =
     let fun mkstrelt (a,b) = (A.mkstr a)^"/"^(A.mkstr b)
     in Lib.mkstr mkstrelt "," (unmakeLiteralRelabelling l)
     end
   
   fun relabellingString r =
     "["^(MaybeVar.maybeVarString literalRelabellingString r)^"]"

   fun paramString (ActParam a) = A.mkstr a
     | paramString (ActionSetParam s) = actionSetString s
     | paramString (AgentParam A) = mkstr A
     | paramString (TimeParam t) = Int.toString t

   and m Nil = "0"
     | m DNil = "$0"
     | m Bottom = "@"
     | m (Var(v,[])) = V.mkstr v
     | m (Var(v,l)) = (V.mkstr v)^"("^(Lib.mkstr paramString "," l)^")"
     | m (a as Prefix([ac],a')) =
       P.prefixString ac ^ (if meije() then ":" else ".")
       ^ (bracket a a')
     | m (a as Prefix(l,a')) =
       "(" ^ (Lib.mkstr P.prefixString "," l) ^ ")"
       ^ (if meije() then ":" else ".")
       ^ (bracket a a')
     | m (a as Delta(ac,a')) = "$"^(m (Prefix([ac],a')))
     | m (a as Time(i,a')) =
       Int.toString i ^ (if meije() then ":" else ".")
       ^ (bracket a a')
     | m (WSum []) = m Nil
     | m (WSum [A]) = mkstr A
     | m (P as WSum [A,B]) =
       (bracket2 P A) ^ " + " ^ (bracket2 P B)
     | m (P as WSum (A::t)) =
       (bracket2 P A) ^ " + " ^ (m (WSum t))
     | m (SSum []) = m DNil
     | m (SSum [A]) = mkstr A
     | m (P as SSum [A,B]) =
       (bracket2 P A) ^ " ++ " ^ (bracket2 P B)
     | m (P as SSum (A::t)) =
       (bracket2 P A) ^ " ++ " ^ (m (SSum t))
     | m (Parallel []) = m Nil
     | m (Parallel [A]) = mkstr A
     | m (P as Parallel [A,B]) =
       (bracket2 P A) ^ (if meije() then " // " else " | ")
       ^ (bracket2 P B)
     | m (P as Parallel (A::t)) =
       (bracket2 P A) ^ (if meije() then " // " else " | ")
       ^ (m (Parallel t))
     | m (SMerge []) = m Nil
     | m (SMerge [(A,S)]) = (mkstr A) ^ " : " ^ (actionSetString S)
     | m (P as SMerge [A,B]) =
       (bracket3 P A) ^ " || " ^ (bracket3 P B)
     | m (P as SMerge (A::t)) =
               (bracket3 P A) ^ " || " ^ (m (SMerge t))
     | m (P as Restrict(A,r)) =
       (bracket P A)^(restrictionString r)
     | m (P as Relabel(A,r)) = 
       (bracket P A)^(relabellingString r)
     | m (P as Open(A,e)) = (mkstr A)^(Eval.evaluationString e)

   and mkstr a = m (real a)
(* privateAgent  agent *)
   and bracket a a' = if prio a <= prio (real a') then mkstr a'
			    else "(" ^ (mkstr a') ^")"
			      
   and bracket2 a a' = if prio a < prio (real a') then mkstr a'
			     else "(" ^ (mkstr a') ^ ")"
			       
   and bracket3 a (a',s) = 
     if prio a < prio (real a')
       then (mkstr a')^ " : " ^(actionSetString s)
     else "(" ^ (mkstr a') ^ ") : " ^(actionSetString s)

(* Hack: really need to fix this thing about formal params being the same *)
(* type as actual params!! *)
   fun getVar a = case real a of Var (v,[]) => SOME v | _ => NONE
     
(* Caution -- I really don't know anything about how to     *)
(* write hash functions, and need to find out! Even this is a win, though.*)
(* The reason for "factor" is that it was the only way I could find to *)
(* eliminate unwanted symmetries: hash(a.a.X + X) = hash(a.X + a.X) etc. *)

local
  val prime = 0w8388593			(* < 2^23 *)
in
(* produces an answer no greater than prime. *)
(* FACTOR MUST BE < 2^7 = 128, so that this doesn't overflow, and gives *)
(* an answer no greater than prime. *)
  fun sxmash factor (a,b) =
    let val n = a +  factor * b (* < 2^23 + 2^23 * 2^7 < 2^31  *)
    in n - prime * Word.div (n, prime)	(* < 2^23 *)
    end handle Overflow => raise PanicNoisily
      ("Agent, combine: with "^(Word.toString a)^" and "^(Word.toString b))
end

fun hash (Nil) = 0w0
  | hash (DNil) = 0w1
  | hash (Bottom) = 0w2
  | hash (Var(v,pl)) 
    = sxmash (0w31)
    (V.hashval v, List.foldr Word.andb (0w31) (map phashval
							  pl))	  
  | hash (Prefix(prefixlist,P))
    = sxmash (0w37) (List.foldr (sxmash (0w37)) (0w37)
		 (map P.hashval prefixlist),hashval P) 
  | hash (Delta(a,P)) = sxmash (0w20) ((P.hashval a), hashval P)
  | hash (Time(t,P)) = sxmash (0w19) ((0w5),hashval P)
  | hash (WSum(PP)) = List.foldr (sxmash (0w57))
    (0w7)
    (map hashval PP)
    
  | hash (SSum(PP)) = List.foldr (sxmash (0w73))
    (0w11)
    (map hashval PP)
  | hash (Parallel(PP)) = List.foldr (sxmash (0w13))
    (0w13)
    (map hashval PP)
  | hash (SMerge(PP)) = List.foldr (sxmash (0w17))
    (0w17) (* hmm *)
    (map (hashval o fst) PP)
  | hash (Restrict(P,actionlist)) = sxmash (0w19)
    ((0w19),hashval P)
  (* restrictions are usually all the same*)
  | hash (Relabel(P,relabelling)) = sxmash (0w77) (hashval P,rhashval
					       relabelling)
  | hash (Open(P,_)) = hashval P
and phashval (ActParam(action)) = A.hashval action
  | phashval (ActionSetParam(Variable v)) = V.hashval v
  | phashval (ActionSetParam(Literal s)) = (0w7) (* well, I dunno *)
  | phashval (TimeParam n) = Word.fromInt n
  | phashval (AgentParam agent) = hashval agent
and rhashval (Literal l) =  (0w29)	(* well? perdita, what should it be? *)
  | rhashval (Variable v) = V.hashval v
    
and hashval (DUMMY i) = snd (!i)

(* Equality *)
val eq = op = 
val actionSetEq = MaybeVar.eq A.ActionSet.eq
val portSetEq = MaybeVar.eq A.PortSet.eq
fun relabeleq (l1,l2) =
  Lib.eq (fn ((a,x),(b,y)) => A.portEq(a,b) andalso A.eq(x,y))
  (LiteralRelabelling.listItemsi l1, LiteralRelabelling.listItemsi l2)
val relabellingEq = MaybeVar.eq relabeleq
fun parameq (ActParam a,ActParam b) = A.eq(a,b)
  | parameq (ActionSetParam s,ActionSetParam t) = actionSetEq(s,t) 
  | parameq (TimeParam s,TimeParam t) = s=t 
  | parameq (AgentParam x,AgentParam y) = eq(x,y)
  | parameq _ = false 
and pEq (Nil,Nil) = true 
  | pEq (DNil,DNil) = true 
  | pEq (Bottom,Bottom) = true 
  | pEq (Var(x,xl),Var(y,yl)) = V.eq(x,y) andalso Lib.eq parameq (xl,yl) 
  | pEq (Prefix(Al,A),Prefix(Bl,B)) = Lib.eq P.eq (Al,Bl)
    andalso eq(A,B)  
  | pEq (Delta(a,A),Delta(b,B)) = P.eq(a,b) andalso eq(A,B) 
  | pEq (Time(s,A),Time(t,B)) = s=t andalso eq(A,B) 
  | pEq (WSum L1,WSum L2) = Lib.eq eq (L1,L2) 
  | pEq (SSum L1,SSum L2) = Lib.eq eq (L1,L2) 
  | pEq (Parallel L1,Parallel L2) = Lib.eq eq (L1,L2) 
  | pEq (SMerge l1,SMerge l2) = Lib.eq
    (fn ((A,As),(B,Bs)) => eq(A,B) andalso actionSetEq(As,Bs)) (l1,l2) 
  | pEq (Restrict(A,resA),Restrict(B,resB)) =
    eq(A,B) andalso portSetEq(resA,resB) 
  | pEq (Relabel(A,relA),Relabel(B,relB)) = 
    eq(A,B) andalso relabellingEq(relA,relB)
  | pEq (Open(A,f),Open(B,g)) =
(* dubious! Equal up to alpha conversion?? *)
    eq (A,B) andalso Eval.evaluationEq (f,g)
  | pEq _ = false

exception NotKnownHere

val agents = HashTable.mkTable (snd,(fn ((a,i),(b,j)) => pEq (a,b)))
  (1024,NotKnownHere)
      : ((privateAgent * Word.word), (privateAgent * Word.word) ref)
  HashTable.hash_table 
fun makeAgent a =
  let val item = (a, hash a)
  in case (HashTable.find agents item) of
      NONE =>
	let val itemRef = ref item 
	in (HashTable.insert agents (item, itemRef); (DUMMY itemRef))
	end
    | SOME(x) => DUMMY(x)
  end
fun efficiencyInfo _ = List.foldr
  (fn (string1, string2) => string1^" "^string2)
   "" (map Int.toString (HashTable.bucketSizes agents))

(* take an agent and a *literal* restriction. Don't attempt to compose *)
(* unless both restrictions are literal, because of the CWB's late binding. *)
fun restrict (agent, l) =
  case real agent of
    Restrict (a, Literal r) => 
      makeAgent(Restrict (a, Literal (A.PortSet.union (r,l))))
  | _ => makeAgent(Restrict (agent, Literal l))

(* Don't attempt to compose relabellings unless both are literal, because   *)
(* of the CWB's late binding. *)
(* Attempt to eliminate empty relabellings -- but of course these may arise *)
(* from variables anyway. *)
fun relabel (agent, litRel) = case real agent of
  Relabel (a, Literal r) =>
    let val rl = r O litRel
      val n = LiteralRelabelling.numItems rl
    in if n = 0 then a else makeAgent(Relabel (a, Literal rl))
    end
| _ =>
    let val n = LiteralRelabelling.numItems litRel
    in if n = 0 then agent else makeAgent(Relabel (agent, Literal litRel))
    end

fun relabelWithList (agent, l) = relabel (agent, makeLiteralRelabelling l)

fun relabelWithVar (agent, v) = makeAgent (Relabel(agent,Variable v))

   fun place Nil           =  0
     | place DNil          =  1
     | place Bottom        =  2
     | place (Var _)       =  3
     | place (Prefix _)    =  4
     | place (Delta _)     =  5
     | place (Time _)      =  6
     | place (WSum _)      =  7
     | place (SSum _)      =  8
     | place (Parallel _)  =  9
     | place (SMerge _)    =  10
     | place (Restrict _)  =  11
     | place (Relabel _)   =  12
     | place (Open _)      =  13

val actionSetLe = MaybeVar.le A.ActionSet.le  
val portSetLe = MaybeVar.le A.PortSet.le
fun relabelle (l1,l2) = Lib.le (Lib.lexicographicLe (A.le, A.le))
  (unmakeLiteralRelabelling l1,unmakeLiteralRelabelling l2)
val relabellingLe = MaybeVar.le relabelle

   fun paramle (ActParam a,ActParam b) = A.le(a,b)
     | paramle (ActionSetParam a,ActionSetParam b) = actionSetLe (a,b)
     | paramle (TimeParam s,TimeParam t) = s <= t
     | paramle (AgentParam x,AgentParam y) = le(x,y)
     | paramle (ActParam _,_) = true
     | paramle (_,AgentParam _) = true
     | paramle _ = false

   and leq (Nil,Nil) = true
     | leq (DNil,DNil) = true
     | leq (Bottom,Bottom) = true
     | leq (Var a,Var b) =
       Lib.lexicographicLe (V.le, Lib.le paramle) (a,b)
     | leq (Prefix a,Prefix b) =
       Lib.lexicographicLe ((Lib.le P.le), le) (a,b)
     | leq (Delta a,Delta b) = Lib.lexicographicLe (P.le, le) (a,b)
     | leq (Time a,Time b) = Lib.lexicographicLe (op <=, le) (a,b)
     | leq (WSum L1,WSum L2) = Lib.le le (L1,L2)
     | leq (SSum L1,SSum L2) = Lib.le le (L1,L2)
     | leq (Parallel L1,Parallel L2) = Lib.le le (L1,L2)
     | leq (SMerge l1,SMerge l2) =
       Lib.le (Lib.lexicographicLe (le, actionSetLe)) (l1,l2)
     | leq (Restrict a,Restrict b) =
       Lib.lexicographicLe (le, portSetLe) (a,b)
     | leq (Relabel a,Relabel b) =
       Lib.lexicographicLe (le, relabellingLe) (a,b)
     | leq (A,B) = place A < place B

   and le (agent1, agent2) = let val (i,j) = (hashval agent1, hashval agent2)
			     in if i < j then true
				else if i > j then false
				     else leq (real agent1, real agent2)
			     end

(* use noTauOrigin because if you're using this fn you don't want taus to  *)
(* be labelled as resulting from synchronising on a: it'd be false. *)
   fun makeAgentFromNextSteps l =
     let
       fun mktrans action var =
	 makeAgent(Prefix([P.prefixFromAction action],makeAgent(Var (var,[]))))
       fun mkag [] = []
	 | mkag ((ac,l)::t) = (map (mktrans ac) l)@(mkag t)
       fun mksum [] = makeAgent(Nil)
	 | mksum [h] = h
	 | mksum l = makeAgent(WSum l)
     in mksum (mkag l)
     end

   fun makeAgentFromVar v = makeAgent(Var (v,[]))

(* Perdita this isn't right, it's just a placeholder *)
   fun usesValues a = case real a of
     Nil => false
   | DNil => false
   | Bottom => false
   | Var _ => false			(* Nope! Perdita*)
   | Prefix (l,a) => (List.foldr (fn (a,b) => (P.usesValues a) orelse b)
		      false l)
     orelse (usesValues a)
   | Delta (p,a) => (P.usesValues p) orelse usesValues a
   | Time (t,a) => usesValues a
   | WSum l => List.foldr (fn (a,b) => (usesValues a) orelse b) false l
   | SSum l => List.foldr (fn (a,b) => (usesValues a) orelse b) false l
   | Parallel l => List.foldr (fn (a,b) => (usesValues a) orelse b) false l
   | SMerge l => List.foldr (fn (a,b) => (usesValues (fst a)) orelse b) false l
   | Restrict (a,r) => usesValues a
   | Relabel (a,r) => usesValues a
   | Open (a,e) => true

(* Perdita the whole param agent scheme is daft and needs re^H^Hdesigned *)
(* Anyway, the param list is a list of FORMAL params, the agent is the body. *)
  type parameterisedAgent = (param list * agent)
  fun makeParameterisedAgent x = x	(* trivial constructor! *)

  val agtenv   : (parameterisedAgent E.env ref) = ref (E.empty())
  fun lookupAgent v = SOME(E.lookup (v, (!agtenv)))
    handle E.Unbound => NONE

(* Given an item (key, value) from the environment, make an appropriate *)
(* definition line that would produce such an entry. *)
   fun agentEnvItemString (v, (fp, ag)) =
(* Have a special paramstring for formal params. It would be easier if they *)
(* had separate types! They will... *)
     let fun paramString (ActParam a) = (A.mkstr a)^" : act"
	   | paramString (ActionSetParam (Variable v)) = (V.mkstr v)^" : set"
	   | paramString (AgentParam A) =
	     (case getVar A of
		SOME v => (V.mkstr v)^" : agent"
	      | NONE => raise PanicNoisily "Agent.str, agentEnvItemString1")
	   | paramString _ = raise PanicNoisily "Agent.str, agentEnvItemString"
	 fun paramsString [] = ""		(* no brackets for 0 params *)
	   | paramsString fp = "("^(Lib.mkstr paramString "," fp)^")"
     in "agent "^(V.mkstr v)^(paramsString fp)^" = "^(mkstr ag)^";"
     end
   fun printAgentEnv _ =
     let val items = E.listAlphabetical (!agtenv)
     in if null items then UI.chat "\n** No agents are defined **"
	else UI.print ("\n** Agents **\n"^
		       (Lib.mkstr agentEnvItemString "\n" items))
     end
   val _ = Registry.registerPrinter
     ("CCS Agent's agent environment printer", printAgentEnv)

(* may raise E.Unbound *)
   fun agentDefString v = agentEnvItemString (v, E.lookup (v, (!agtenv)))

   fun bindVarsToAgents l =
     let val needToReset = ref false
       fun bind (v,ag) = (if E.isBound (v, !agtenv) then needToReset := true
			  else ();
			    agtenv := E.bind (v,([],ag),!agtenv))
       val _ = map bind l
     in if !needToReset then Registry.resetTables() else ()
     end handle e => (Registry.resetTables(); raise e)

   fun forgetAgents _ = agtenv := (E.empty())
   val _ = Registry.registerForgetter
     ("CCS Agent's agent environment forgetter", forgetAgents)

   infix O

(************** Stuff about transition sets and agent sets ****************)
type transition = (A.act * agent)
type transitionSet = (A.act * agent list) list (* sorted lex by A.le, le *)
type agentSet = agent list		(* sorted by le *)

(* val getAction : transition -> A.act *)
val getAction = fst
(* val getAgent : transition -> agent *)
val getAgent = snd

fun listTransitionSet l = flatten (map (fn (a,d) => map (fn e => (a,e)) d) l)
fun listAgentSet l = l
val makeAgentSet = SL.sort le true
  
(* val actionsMatch : transitionSet * transitionSet -> bool *)
fun actionsMatch (s,t) = Lib.eq A.eq (map fst s, map fst t)

(* val pickAgent : agentSet -> agent * agentSet *)
fun pickAgent [] = raise Panic
  | pickAgent (h::t) = (h,t)

fun userPickAgent l =
  let val _ =  UI.message "Possible agents are:"
    val (pre, chosen, after) =
      UI.pickFromListC (fn _ => false) "Which agent? " mkstr l
  in (chosen, pre@after)
  end
  
(* val agentSetIsEmpty : agentSet -> bool *)
val agentSetIsEmpty = null

(* val derivatives : transitionSet * A.act -> agentSet *)
fun derivatives (t: transitionSet, a: A.act) : agentSet =
  snd (SL.retrieve fst A.le (a,t)) (* SL use OK since transition sets sorted *)
handle SL.Retrieve => []

(* val pickTransition : transitionSet -> transition * transitionSet *)
fun pickTransition [] = raise Panic
  | pickTransition ((a,l)::t) =
    let val next = (a, hd l)
      val rest = if null(tl l) then t else (a, tl l)::t
    in (next, rest)
    end
(* val transitionSetIsEmpty : transitionSet -> bool *)
val transitionSetIsEmpty = null
fun transitionString (act,ag) = "-- "^(A.mkstr act)^" --> "^(mkstr ag)

(********** End stuff about transition and agent sets ********************)  

   val relenv   : (literalRelabelling E.env ref) = ref (E.empty())
   fun bindRelabelling (X, S) =
     (if E.isBound(X, !relenv) then Registry.resetTables() else ();
	relenv := E.bind(X,(makeLiteralRelabelling S),!relenv))
   fun forgetRelabellings _ = relenv := E.empty()
   val _ = Registry.registerForgetter
     ("CCS Agent's relabelling environment forgetter", forgetRelabellings)
       
   fun relEnvItemString (v, r) =
     "relabel "^(V.mkstr v)^" = "^(literalRelabellingString r)^";"
   fun printRelabellingEnv _ =
     let val items = E.listAlphabetical (!relenv)
     in if null items then UI.chat "\n** No relabellings are defined **"
	else UI.print ("\n** Relabelling functions **\n"^
		       (Lib.mkstr relEnvItemString "\n" items))
     end
   val _ = Registry.registerPrinter
     ("CCS Agent's relabelling environment printer", printRelabellingEnv)
     
   (* may raise E.Unbound *)
   fun relabellingDefString v = relEnvItemString (v, E.lookup (v, (!relenv)))

(* transition-le: compare (action,agent) pairs so that if we sort with *)
(* this order we get aA aB bA bB etc. *)
(* ts on SMerge takes advantage of this particular order. *)
   val ts_le = Lib.lexicographicLe (A.le, le)

   val set_lookup = MaybeVar.dTRT (id, fn v => (A.actionSetEnvLookup v))
     
   fun undefinedComplaint v = "The free identifier "^(V.mkstr v)^" makes"^
     " it impossible to compute this result"
   fun lookup e = MaybeVar.dTRT (id, fn v => (E.lookup (v,e))
				 handle E.Unbound => raise Error
				   (undefinedComplaint v))
   fun rel_lookup x = lookup (!relenv) x
     
(* Give a literal set of ports which a portSet represents in global env     *)
(* More horrible than in might be because we don't actually have an env for *)
(* restrictions, just a general action set environment. Could change?       *)
(* Warning: this may do speed serious harm! *)
(* Perdita: better to have, underneath, separate environment, even if user  *)
(* doesn't see the difference? Yes, probably. *)
   val restrictionLookup =
     MaybeVar.dTRT (id, fn v => 
		    (A.portsOfActions (A.actionSetEnvLookup v)))
		     
(* Take a list of formal parameters, return list of variables standing for *)
(* agents. There is a better way of doing this! *)
   fun getAgentFPs [] = []
     | getAgentFPs ((AgentParam p)::pl) =
       (case getVar p of
	  SOME v => (v::(getAgentFPs pl))
	| NONE => raise PanicNoisily "Agent.str, getAgentFPs")
     | getAgentFPs (a::pl) = getAgentFPs pl

   fun act_fp [] = []
     | act_fp ((ActParam a)::pl) = (a::(act_fp pl))
     | act_fp (a::pl) = act_fp pl

(* ap : param list = actual parameters, fp : param list = formal parameters. *)
(* So we have lists of actual and formal parameters. We peel them off in    *)
(* pairs, and build up a triple of functions which you can think of as	    *)
(* being identity functions except that they map formal params to the	    *)
(* corresponding actual params.						    *)
(* The agent parser ensures that formal parameters are variable-like!!      *)
(* The whole thing is idiocy: not only telling the difference between agents *)
(* and sets, but telling the difference between actions and times.... *)
(* Thing is, any occurrence of a Time in the body of a param agent, where  *)
(* the time is represented by a formal param, will look to us like a Prefix.*)
(* Hence the A.act -> int type below. THE CWB NEEDS A TYPE SYSTEM!! Perdita! *)
(* Experimenting with slightly saner version for actionSets, for a start... *)
(* The formal parameter's opinion about whether a thing is a set or agent is *)
(* now reliable. It may still happen, though, that an ap is labelled wrongly *)
   (* Raise Match if actual and formal parameters don't match. *)
fun mksubst ap fp = 
  let fun zip [] [] s = s
    : (A.act -> int) * (A.act -> A.act) *
    (V.var -> actionSet) * (agent -> agent)
	| zip ((TimeParam a)::ap) ((ActParam f)::fp) (tim,act,actSet,agt) =
(* This is more dubious than the next case. Deciding that if x -> 1 then *)
(* 'x -> 1 also. But one could argue either for 'x being left alone (it has*)
(* type action, not time) or for this being an error. *)
          let val tim' =
	    fn z => if A.eq (f,z) orelse A.eq (f, A.inverse z) then a
		    else tim z
	  in zip ap fp (tim',act,actSet,agt)
	  end
	| zip ((ActParam a)::ap) ((ActParam f)::fp) (tim,act,actSet,agt) = 
(* Slight complication because if we map a -> b we also want to map 'a -> 'b *)
	  let val act' = 
	    fn z => if A.eq (f,z) then a
		    else if A.eq (f, A.inverse z) then A.inverse a
			 else act z
	  in zip ap fp (tim,act',actSet,agt)
	  end
	| zip ((ActionSetParam a)::ap)((ActionSetParam f)::fp)
	  (tim,act,actSet,agt) =
(* Now, if the formal param were a variable, we'd be even happier... *)
	  zip ap fp (tim,act,(fn z => if actionSetEq(f,Variable z) then a
				      else actSet z),agt)
(* if fp is ActionSetParam and ap is AgentParam, it's probably because   *)
(* of our attempt to be userfriendly. Try turning the AgentParam into  *)
(* an ActionSetParam and try again! *)
	| zip ((AgentParam v)::ap) (fps as ((ActionSetParam f)::fp))
	  (tim,act,actSet,agt) =
	  (case getVar v of
	     SOME x => zip ((ActionSetParam (Variable x))::ap)
	       fps (tim,act,actSet,agt)
	   | NONE => raise Match)	(* if the ap wasn't a variable, that *)
					(* can't be the explanation: it must *)
					(* be a bona fide user error. *)
(* and more importantly, because it may actually happen, vice versa! *)
	| zip ((ActionSetParam a)::ap) (fps as ((AgentParam v)::fp))
	  (tim,act,actSet,agt) =
	  (case a of
	     Variable av => 
	       zip (AgentParam (makeAgentFromVar av)::ap) fps
	       (tim,act,actSet,agt)
	   | _ => raise Match)
(* but in this case, we're now _sure_ it's an agent. phew. *)
	| zip ((AgentParam a)::ap) ((AgentParam f)::fp)
	  (tim,act,actSet,agt) =
	  zip ap fp (tim,act,actSet, (fn z => if eq(f,z) then a else agt z))
	| zip _ _ _ = raise Match;
  in
    zip ap fp ((fn t => ~1),(fn a => a),(fn a => Variable a),(fn a => a))
  end

(* Take an evaluation & prefix, return an action & new evaluation *)
(* Use a symbolic value that's not already mentioned in the evaluation *)
(* Current idea is that evaluation of output prefixes should happen on *)
(* the action: idea is that as we know more and more about values it  *)
(* happens, so that when we get to an output prefix it contains a real *)
(* value. We _implement_ this with an evaluation, but that's another *)
(* matter. Perdita? *)
   fun actionFromPrefix e p =
     let fun aFromP (a, NONE) = (a, e)
	   | aFromP (a, SOME x) =
	     let val var = Eval.newSymbolFor e
	       val newEval = Eval.update e (x,var)
	     in (A.changeValue a (SOME (Value.Symbolic var)), newEval)
	     end
     in aFromP (P.unmake p)
     end

fun dumbActionFromPrefix p =
  fst (actionFromPrefix (Eval.emptyEvaluation()) p)

(* Raise Match if there's a problem *)
(* Do not look up variables. *)
(* Decree: one pass lookup. Once we've looked up a formal param,  *)
(* we will not treat anything in the result as a formal parameter. *)
(* fpvars should be the formal agent params we may expect to meet, i.e. *)
(* the genuine domain of agts. Another thing that could be easier done! *)
fun apply fpvars (tims,acts,actSets,agts) =
      let
(* allow act[list]s to operate on port[list]s and prefixes by coercion! *)
(* Yes, things will go horribly wrong rather easily... Perdita! *)
	val ports  = A.beware acts
	fun prefixes p = P.prefixFromAction (acts (dumbActionFromPrefix p))
	fun prefixtims p = tims (dumbActionFromPrefix p)
	fun mapActs s = Literal (A.ActionSet.map (s, acts))
	fun mapPorts s = Literal (A.PortSet.map (s, ports))
	fun app2 Nil               = Nil 
	  | app2 DNil              = DNil
	  | app2 Bottom            = Bottom

	  | app2 (V as Var (v,[])) =  (* this is probably a parameter *)
	    if Lib.member V.eq (v,fpvars)
	      then real(agts (makeAgent V)) (* so apply the substitution *)
	    else V                   (* else it was a free variable *)
  
	  | app2 (Var (v,plist))   =  (* just apply the substitutions -- *)
(* a variable with a non-empty parameter list cannot be a formal param. *)
	    Var(v, map subst plist)

(* Problem case, because time and action formal params look the same. *)
	  | app2 (Prefix ([a],ag)) =
	    let val maybeTime = prefixtims a (* could a be a time fp? *)
	    in if maybeTime < 0 then Prefix([prefixes a], app ag) (* no *)
	       else Time(prefixtims a, app ag) (* yes *)
	    end

	  | app2 (Prefix (l,ag))   = 
	    Prefix(SL.sort P.le false (* keep prefix "list" sorted *)
		   (map (fn a => if (prefixtims a) < 0 then prefixes a
				 else raise Match) (* times not allowed *)
		    l),
		   app ag)

	  | app2 (Delta (a,ag))    = 
	    if (prefixtims a) < 0 then Delta(prefixes a, app ag)
	    else raise Match

	  | app2 (Time (t,ag))     = Time(t, app ag)
	  (* if we recognised it as Time, t can't be a formal time param! *)
	  | app2 (WSum agl)        = WSum(map app agl)
	  | app2 (SSum agl)        = SSum(map app agl)
	  | app2 (Parallel agl)    = Parallel(map app agl)
	  | app2 (SMerge agactl)   =
	    let val f = MaybeVar.dTRT (mapActs, actSets)
	    in SMerge (map (fn (ag,s) => (app ag, f s)) agactl)
	    end

(* if the restriction set is a formal param, substitute for it. If     *)
(* it's any other variable, leave it alone. *)
	  | app2 (Restrict (ag,r)) =
	    let fun fixV v = case actSets v of 
	      Variable x => Variable x (* do not recurse *)
	    | Literal s =>	(* Do not apply acts to the the elts *)
		Literal (A.portsOfActions s)
	    in Restrict (app ag, MaybeVar.dTRT (mapPorts, fixV) r)
	    end

(* Odd as it may seem, we can't parameterise on relabellings *)
(* But as with action sets, if the relabelling is given literally, then we *)
(* allow the actions in its elements to be considered as formal parameters *)
(* and substituted for. If it was given as a variable, we don't: we'd get  *)
(* accidental capture. (Pity we don't have parameterised relabellings??!)  *)
	  | app2 (Relabel (ag,r as Variable _)) = Relabel (app ag, r)
	  | app2 (Relabel (ag,Literal r))  =
	    real (relabel(app ag,
			  makeLiteralRelabelling
			  (map (fn (a,b) => (acts a, acts b))
			   (unmakeLiteralRelabelling r))))
	  | app2 (Open (ag,f)) = Open(app ag, f)

(* If the actual parameter to a param agent is one of our formal params, *)
(* it's instantiated to our actual param, so bindings to actual parameters *)
(* get "passed down". e.g. if A(V) =def B(V) then A(0) =def B(0) *)
(* We have our usual problem: if the param occurs in dom tims or dom actSets *)
(* we're in serious danger of missing it. Hack it...  *)
	and subst (ActParam a)   = 
	  if (tims a) < 0 then ActParam (acts a) else TimeParam (tims a)
(* Actually it *won't* be an ActionSetParam unless it's literal, but hey. *)
	  | subst (ActionSetParam a) =
	    ActionSetParam (MaybeVar.dTRT (mapActs, actSets) a)
	  | subst (TimeParam a)  = TimeParam (a) (* can't be from our FPs! *)
	  | subst (original as AgentParam a) = 
	    (case real a of
	       (V as Var(v,[])) => 
(* Is it *really* an AgentParam or is it an ActionSetParam? Let's try to see.*)
(* Let's leave it that if it could be both we'll assume it's an agent: *)
		 let val a' = agts a
		 in if eq(a,a') then (* it's not a formal AgentParam *)
		   (if actionSetEq (Variable v, actSets v) then original
(* it's not one of our formal ActionSetParams, either. *)
		    else ActionSetParam (actSets v))
		    else AgentParam a' (* it's an agent fp *)
		 end
	     | _ => AgentParam (app a)) (* it really clearly is an agent *)
	and app a = makeAgent(app2 (real a))
      in app
      end

(* Take a (variable, actual parameter *)
(* list) pair and return the agent which results from substituting the	    *)
(* actual for the formal parameters.                                        *)
(* Note that the agent may still have variables in it -- just not formal    *)
(* parameters. *)
exception Unbound of V.var
fun lookupapply (v,actualparameters) =
  let val (formalparameters, ag) = case lookupAgent v of
    SOME x => x
  | NONE => raise Error (undefinedComplaint v)
      val subs : (A.act -> int) * (A.act -> A.act)
	* (V.var -> actionSet) * (agent -> agent)
	= (mksubst actualparameters formalparameters) 
      val answer = if null formalparameters andalso null actualparameters
		     then ag (* don't mess with it, we're sure no mismatch *)
		   else (apply (getAgentFPs formalparameters) subs ag) 
  in
    ((* UI.debug *)
     (* 	  ("Lookupapply on "^(V.mkstr v)^" gave "^(mkstr answer)); *)
     answer)
  end handle Match => raise Error
    ("Use of "^(V.mkstr v)^" doesn't match its definition")

(* we check whether we've seen this variable with these parameters     *)
(* before. If so, we're definitely stuffed. If not, still check to see *)
(* whether we've seen this var with any params more than n times. If   *)
(* so, warn user that there may be bad recursion, get her to tell us   *)
(* whether to carry on. *)
   fun checkForBadRecursion ((v, paramList), seen, maxLookUp) =
     let
       val paramsSeen = E.lookup (v, seen) handle E.Unbound => []
       val newSeen = if Lib.member (Lib.eq parameq) (paramList, paramsSeen)
		       then raise Error
			 ("Non-well-founded recursion in "^(V.mkstr v))
		     else E.bind (v, (paramList::paramsSeen), seen)
       val seenManyTimes = ((length paramsSeen) > (!maxLookUp))
       fun askUser _ =
	 if UI.yOrN true
	   ("Variable "^(V.mkstr v)^
	    " has been looked up more than "^
	    (Int.toString (!maxLookUp))^
	    " times. \nThis could mean you have non-well-founded recursion \
\in the definition.\nGive up now?")
	   then raise Error ("Giving up on "^(V.mkstr v))
	 else maxLookUp := ((!maxLookUp) + (!maxLookUp))
(* could be more sophisticated, but for now, if they say keep going we *)
(* double the limit on times we can look up a var. *)
     in (if seenManyTimes then askUser() else (); newSeen)
     end
	
(*****************)
(*  transitions  *)
(*****************)
exception NotKnownHere
val knowledge = ref (HashTable.mkTable (hashval,eq) (1024,NotKnownHere))
  : (agent,(A.act * agent) list) HashTable.hash_table ref
val timeStepKnowledge = ref (HashTable.mkTable (hashval,eq)(1024,NotKnownHere))
  : (agent,agent option) HashTable.hash_table ref

val total = ref 0
val madenew = ref 0
fun forgetall _ = (total := 0; madenew := 0;
  knowledge := HashTable.mkTable (hashval,eq) (1024,NotKnownHere);
  timeStepKnowledge := HashTable.mkTable (hashval,eq) (1024,NotKnownHere))
val _ = Registry.registerTableResetter
  ("CCS Agent's knowledge and timestep knowledge", forgetall)
fun addknowledge agent nextsteps = HashTable.insert (!knowledge) (agent,nextsteps)
fun getknowledge agent = HashTable.find (!knowledge) (agent)
fun addTimeStep agent timeStep =
  HashTable.insert (!timeStepKnowledge) (agent,timeStep)
fun getTimeStep agent = HashTable.find (!timeStepKnowledge) (agent)

fun efficiencyInfo _ = List.foldr
  (fn (string1, string2) => string1^" "^string2)
   "" (map Int.toString (HashTable.bucketSizes (!knowledge)))

fun evaluationOf a = case real a of
  (Open (A,f)) => f
| _ => Eval.emptyEvaluation() 
	
(* Filter out of e any variables which aren't mentioned in A; pack up A with *)
(* whatever's left of e (if nothing, make it a closed agent). If A already *)
(* had an evaluation attached, update it with e. *)
(* This is the ONLY place an Open gets attached. Formalise? *)
fun pack (e, A) =
  let (* val _ = UI.debugFn (fn _ => "Packing "^(mkstr A)^"\nwith evaluation"^ *)
(* 			   (A.evaluationString e)) *)
    val (fullE, rawA) = case real A of
      Open (B,g) => (Eval.combineEvaluations (e,g), B)
    | _ => (e, A)
(* Grab the prefixes that appear syntactically. Only actually interested in *)
(* the expressions, and very naive. *)
    fun pIn Nil = []
      | pIn DNil = []
      | pIn Bottom = []
      | pIn (Var _) = []	(* vars must be closed *)
      | pIn (Prefix (l,A)) = l@(prefixesIn A)
      | pIn (Delta (a,A)) = a::(prefixesIn A)
      | pIn (Time (_,A)) = prefixesIn A
      | pIn (WSum l) = flatten (map prefixesIn l)
      | pIn (SSum l) = flatten (map prefixesIn l)
      | pIn (Parallel l) = flatten (map prefixesIn l)
    | pIn (SMerge l) = flatten (map (fn (A,_) => prefixesIn A) l)
      | pIn (Restrict (A,_)) = prefixesIn A
      | pIn (Relabel (A,_)) = prefixesIn A
      | pIn (Open (A,f)) = [] (* hmm? because shouldn't happen?*)
    and prefixesIn a = pIn (real a)
    val newEmaybe = Eval.filterEvaluation (* Perdita efficiency! *)
      (fullE, P.symbolsOf (prefixesIn rawA))
  in case newEmaybe of NONE => rawA
| SOME newE => makeAgent(Open (rawA, newE))
  end

(* may raise A.Invalid *)
fun constrain (A, c) = case real A of
  Open (A,f) => makeAgent (Open (A, Eval.constrainEvaluation (f,c)))
    | _ => A
      
(* everything in sight seems to return a list of (action,agent) pairs *)
(* taus resulting from communication are associated with the port on *)
(* which the communication happened: e.g. tau<a>, Tau(a). *)
fun transitions a =
  let exception Stopped
(*     val _ = UI.debug ("transitions from "^(mkstr a)) *)
(* timestep returns the agent reached after A.step, or raises Stopped if *)
(* A.step isn't allowed from here. *)
(* See if we already know. If not, find out. (This is not such a big win *)
(* as with ts, but it saves us doing unnecessary lookupapplies.) *)
    fun timestepIfNec agent =
      let val step = case getTimeStep agent of SOME s => s | NONE =>
	  let val calculated = (SOME (timestep agent)) handle Stopped => NONE
	  in addTimeStep agent calculated; calculated
	  end
      in case step of NONE => raise Stopped
                    | SOME a => a
      end

    and timestep2 Nil          = raise Stopped
      | timestep2 DNil         = makeAgent DNil
      | timestep2 Bottom       = raise Stopped
      | timestep2 (Prefix _)   = raise Stopped
      | timestep2 (Delta(a,A)) = makeAgent(Delta(a,A))
      | timestep2 (Time(t,A))  = if t=1 then A else makeAgent(Time(t-1,A))

      | timestep2 (Var (v,ap)) =
	(timestepIfNec (lookupapply (v,ap))
	 handle Unbound v => raise Error (undefinedComplaint v))
(* for WSum, end up with a (weak) choice between all the components that *)
(* were able to idle -- if a component can't idle, it's preempted. *)
      | timestep2 (WSum l)     =
	let val slist = SL.bigmerge le true (* SL use OK since singletons! *)
	  (map(fn a => [timestepIfNec a]
	       handle Stopped => []) l)
	in if null(slist) then raise Stopped
	   else if null(tl slist) then hd slist
		else makeAgent(WSum slist)
	end
(* for SSum, Parallel, SMerge, all the components must be able to idle if  *)
(* the whole agent is to *)
      | timestep2 (SSum l)     = makeAgent(SSum(map timestepIfNec l))
      | timestep2 (Parallel l) = makeAgent(Parallel(map timestepIfNec l))
      | timestep2 (SMerge l)   =
	makeAgent(SMerge(map (fn (x,s) => (timestepIfNec x,s)) l))
      | timestep2 (Restrict(A,restA)) =
	makeAgent(Restrict(timestepIfNec A,restA))
      | timestep2 (Relabel(A,relA))   =
	makeAgent(Relabel(timestepIfNec A,relA))
      | timestep2 (Open(A,f)) =
	makeAgent(Open (timestepIfNec A, f))
    and timestep a = timestep2 (real a)

(* mv is only used in expand below, which in turn is used once in ts *)
(* args are: components we've dealt with, the transitions from the  *)
(* current component, the components we haven't dealt with (including *)
(* the current component) *)
(* The result of mv is sorted by ts_le *)
(* if there aren't any components, there aren't any transitions *)
    fun mv (_,[],[]) = []
(* if there's only one component and it hasn't any transitions, ditto *)
      | mv (_,[],[_]) = []
(* if this component has no transitions, no more to be done with it,  *)
(* add it to collection of components we've done and keep going with rest *)
      | mv (left,[],(_,a)::(t as (l,_)::_)) =
	mv (left@[a],l,t)
(* this component does have some transitions, so do the real work here: *)
      | mv (left,(a as (ac,a'))::t,(right as (_::rt))) =
(* The result of comm is sorted. *)
	let fun comm (_,[],[])  = []
	      | comm (_,[],[_]) = []
	      | comm (chk,[],(_,a)::(t as (l,_)::_)) =
		comm(chk@[a],l,t)
	      | comm (chk,(b as (bc,b'))::u,(cright as _::ct)) =
(* if agent a -ac-> a' and b -bc-> b' can these actions synchronise? If so, *)
(* what is the result? If a value passes we have to take care of it. *)
		  (case A.inverses(ac,bc) of
		   NONE => comm(chk,u,cright) (* no synchronisation *)
		 | SOME (a'IsSender, resultant, receiverConstraint) =>
		     let val (newA, newB) =
		       case receiverConstraint of NONE => (a',b') (* no VP *)
		                                | SOME e =>
						 if a'IsSender
						   then (a', constrain(b',e))
						 else (constrain(a',e), b')
		     in SL.add ts_le true (* SL use OK by induction *)
		       ((resultant,
			 makeAgent
			 (Parallel(left@(newA::chk)@(newB::(map snd ct))))),
			comm(chk,u,cright))
		     end)
	      | comm _ = raise Panic (* shouldn't happen *)
(* comms is the tau<ac> transitions involving this component *)
	    val comms = if A.eq(ac,A.tau) orelse null(rt) then []
			else comm([],fst(hd rt),rt)
(* We can do ac as a non-communicating action *)
	    val thisLot =
	      SL.add ts_le true ((ac,makeAgent (* SL use OK by comms sorted *)
				  (Parallel(left@(a'::(map snd rt))))),
				 comms)
(* that was the list of ac-transitions, inc tau<ac>, involving current *)
(* component. *)
(* Now collate that with all the other relevant stuff: *)
	in
	  SL.merge ts_le true (thisLot, mv(left,t,right)) (* SL use OK... *)
(* ... since thisLot sorted and mv's output sorted by induction *)
	end
      | mv _ = raise Panic (* shouldn't happen *)

(* expand's job is to take a (componentTransitionList, component) list *)
(* and return the list of all transitions, including communications *)
(* The result of expand is sorted by ts_le (because of mv) *)
    fun expand  [] = []
      | expand (l as (l',_)::_) = mv([],l',l)

(* we want our own copy of the reference, because if we end up	       *)
(* increasing it we want that effect to be local to this calculation.  *)
   val maxLookUp = ref (UI.getMaxLookUp())

(* SORTING: tsifnec, ts, ts2 all produce output sorted by ts_le *)
(* chk is the collection of things (vars with params if any) we've     *)
(* seen, so that we can catch unguarded recursion. *)
(* See if we already know. If not, find out. *)
   fun tsifnec chk e agent = (total := !total + 1;
			      case getknowledge agent of SOME s => s | NONE =>
	let val calculated = ts chk e agent
	in madenew := !madenew + 1; addknowledge agent calculated; calculated
	end)

    and ts2 chk e Nil           = []
      | ts2 chk e DNil          = []
      | ts2 chk e Bottom        = []
      | ts2 chk e (Prefix([a],A)) =
	let val (newA, newE) = actionFromPrefix e a
	in [(newA,pack (newE,A))]
	end
(* It's very silly to do this if any output action mentions a data variable *)
(* bound by some input action! GIGO. Perdita, think about this some more? *)
(* remember the output must be sorted by ts_le! *)
      | ts2 chk e (Prefix(l,A)) =	(* keep prefix list sorted *)
	let fun list _ [] = []
	      | list l (h::t) =
		let val (newH, newE) = actionFromPrefix e h
		in SL.add ts_le true	(* SL use OK by induction *)
		  ((newH,pack (newE, makeAgent(Prefix(l@t,A)))),
		   (list (l@[h]) t))
		end
	in list [] l
	end
      | ts2 chk e (Delta(a,A))  =
	let val (newA, newE) = actionFromPrefix e a
	in [(newA,pack (newE,A))]
	end
      | ts2 chk e (Time(t,A))   = []

      | ts2 chk e (Var (x as (v,ap)))  =
(* Perdita assuming Var agents are closed, so eval must be irrelevant *)
(* bomb out if this looks like non-well-founded recursion: see         *)
(* checkForBadRecursion comments above for details.                    *)
	tsifnec (checkForBadRecursion (x, chk, maxLookUp)) e (lookupapply x)

      | ts2 chk e (WSum l) = SL.bigmerge ts_le true (* SL use OK by tsifnec*)
	(map (tsifnec chk e) l)
      | ts2 chk e (SSum l) = tsifnec chk e (makeAgent (WSum l))
(* Given parallel components, we get the successors of each and get a  *)
(* (successorlist, component) list, to which we apply expand. *)
(* NB expand's output is sorted *)
      | ts2 chk e (Parallel l)  = 
	(expand (map (fn a => ((tsifnec chk e a),a)) l))

(* Remember that an SMerge can do an a provided that some set mentions a, *)
(* and that every component whose set mentions a can do an a. If so, the  *)
(* a-derivative leaves alone any components whose set doesn't contain a,  *)
(* even if they could do a-transitions. For the components whose set does *)
(* contain a, an arbitrary a-derivative is the resulting component.       *)
      | ts2 chk e (SMerge mergeComps) =
	let
(* For a given action, see whether it is permitted. *)
(* If the action is a, find the possible new versions of component (P,S) *)
	  fun newVersions a (P,S,allPsTransitions) =
	    if A.ActionSet.member (set_lookup S, a) then
(* If we can do an a, we're allowed to do it any way we like. Options? *)
	      let fun f [] = []
		    | f ((b,P')::t) = if A.eq (a,b) then (P',S)::(f t)
				      else f t
	      in f allPsTransitions
	      end
	    else [(P,S)]	(* if action is a, we can't participate *)
(* Take a list of lists, return a list of "perpendicular" lists: *)
(* e.g., given [[l11,l12,l13],[l21,l22],[l31]], return some ordering of  *)
(* [[l11,l21,l31],[l11,l22,l31],[l12,l21,l31],[l12,l22,l31],[l13,...]... *)
(* Empty if any of the lists in the original list is empty, of course. *)
          exception NoEntries
(* This gets called on a list of length number of SMerge'd components; *)
(* that is, at least 2. Returns non-empty listlist, or raises exception *)
          fun perpendicular [] = raise PanicNoisily "AgentFuns, perpendicular"
	    | perpendicular [l] = map (fn x => [x]) l
	    | perpendicular ([]::t) = raise NoEntries
	    | perpendicular (h::t) = Lib.multiply (op::) h (perpendicular t)
(* For each merged component, find out what transitions it may have *)
	  val compTrs = map (fn (P,S) => (P,S,tsifnec chk e P)) mergeComps
	  fun transitionsVia a =	(* could eliminate the sort, but... *)
	    SL.sort ts_le true (map (fn L => (a,makeAgent(SMerge L)))
				(perpendicular (map (newVersions a) compTrs))
				handle NoEntries => [])
(* With our particular ts_le, actions being sorted will make result sorted. *)
(* If I've got everything the right way round :-) *)
	in List.foldr
	  (fn (a, rest) => (transitionsVia a)@rest)
	  []
(* sorted list of all actions that may conceivably be permitted *)
	  (A.ActionSet.unmake
	   (A.ActionSet.bigUnion
	    (map (fn el => set_lookup (snd el)) mergeComps)))
	end

      | ts2 chk e (Restrict(A,r)) =
	let fun rmac [] = []
	      | rmac ((ac,A)::t) =
		if forbids (restrictionLookup r) ac then rmac t
		else SL.add ts_le true	(* SL use OK by induction *)
		  ((ac,makeAgent(Restrict(A,r))),(rmac t))
	in rmac (tsifnec chk e A)
	end
      | ts2 chk e (Relabel(A,f)) =
	let val relA = (rel_lookup f)
	  fun rel (a,A') = (relabelAction relA a,relabel(A',relA))
	in SL.map ts_le true
	  (fn (a,A') => (relabelAction relA a,relabel(A',relA)))
	  (tsifnec chk e A)
	end
      | ts2 chk e (Open(A,f)) = ts chk f A (* e should be empty??? *)
   and ts chk e a = ts2 chk e (real a)
   val trans = tsifnec (E.empty()) (Eval.emptyEvaluation()) a
   val _ = UI.debugFn (fn _ => if SL.isSorted ts_le trans then "trans sane"
			       else raise PanicNoisily "Agent, transitions")
  in SL.add ts_le true ((A.step,timestepIfNec a),trans)	(* SL use OK,tsifnec *)
    handle Stopped => trans
  end

(* Here's a version of transitions that returns a transitionSet. Would like *)
(* to make this one the default and rewrite more efficiently. *)
fun transitions2 a = 
let val rawList = transitions a
  val _ = UI.debugFn
    (fn _ => if (SL.isSorted ts_le rawList) then "Transition list is sane"
	     else raise PanicNoisily "Agent, transitions2")
  fun chop current (action, agentlist) [] =
    rev ((action, rev agentlist)::current)
    | chop current (action, agentlist) ((h as (act, ag))::t) =
      if A.eq (action, act) then chop current (action, ag::agentlist) t
      else chop ((action, rev agentlist)::current) (act, [ag]) t
in case rawList of
  [] => []
| ((h as (act, ag))::t) => chop [] (act, [ag]) t
end


(* only here for PG's graph fns *)     
(**************)
(*  diverges  *)
(**************)
(* return a fn which given an agent returns true iff the agent defn *)
(* contains @ (undefined) at the top level.                         *)
   val diverges =
       let
(* we want our own copy of the reference, because if we end up	       *)
(* increasing it we want that effect to be local to this calculation.  *)
	 val maxLookUp = ref (UI.getMaxLookUp())
	 fun dv2 chk Nil = false
             | dv2 chk DNil = false
             | dv2 chk Bottom = true
             | dv2 chk (Prefix _) = false
             | dv2 chk (Delta _) = false
             | dv2 chk (Time _) = false
             | dv2 chk (Var (v,ap)) =
(* bomb out if this looks like non-well-founded recursion: see         *)
(* checkForBadRecursion comments above for details.                    *)
	       dv (checkForBadRecursion ((v, ap), chk, maxLookUp))
	       (lookupapply (v,ap))
             | dv2 chk (WSum l) = List.exists (dv chk) l
             | dv2 chk (SSum l) = List.exists (dv chk) l
             | dv2 chk (Parallel l) = List.exists (dv chk) l
             | dv2 chk (SMerge l) = List.exists (dv chk) (map fst l)
             | dv2 chk (Restrict(A,_)) = dv chk A
             | dv2 chk (Relabel(A,_)) = dv chk A
	     | dv2 chk (Open(A,_)) = dv chk A
	 and dv chk a = dv2 chk (real a)
       in dv (E.empty())
      end

(* only here for PG's graph fns *)
(*****************)
(*  prefix form  *)
(*****************)
(* This whole area is dodgy and not (much) used. Perdita, check or delete! *)
(* Give an agent strongly bisimilar to the original in the form a.P + b.Q .. *)
   fun prefixform agent =
     let val pf = map (fn (action,agent2) =>
		       if A.eq(action,A.step) then makeAgent(Time(1,agent2))
		       else makeAgent
			 (Prefix([P.prefixFromAction action],agent2)))
       (transitions agent)
	 val pff = if diverges agent then (makeAgent Bottom)::pf else pf
     in makeAgent(WSum pff)
     end

     
(*****************************************************************************)
(*                                                                           *)
(*  Recursive descent parser: see user documentation                         *)
(*                                                                           *)
(* eps is never allowed in an actlist, but                                   *)
(* tau is allowed in actlists used in PARAMs or PREFIXs. Depending on        *)
(* how the param is used, taus might or might not be OK in params:           *)
(* caveat user!                                                              *)
(*****************************************************************************)
(* Let's have a new lexer, so that we can reinitialise it without messing *)
(* up anything outside. In fact it uses the same token set as the global one *)
structure LexingAgent = Lexing(structure Lexer = CWBLex); 
local open LexingAgent in

(* Take a formalParams of things of known type plus a sorted list of unknown *)
(* NONE: not a fp. SOME NONE: fp of unknown type. SOME (SOME t): type t *)
   fun typeOf (fps, unspecified) v = case SmallVarDict.find (fps, v) of
     NONE => if SL.member V.le (v, unspecified)	(* SL use OK by precond *)
	       then SOME NONE else NONE
   | SOME t => SOME (SOME t)

   fun mkact s = A.mkact s		(* may raise Parse: will pass it up *)
(* This version takes information about any formal parameters of a param. *)
(* agent, so that we can complete type inference, etc. NB only the user can *)
(* bind a parameterised agent: the public interface doesn't allow it. So   *)
(* a wrapper mkstr with no type information is OK. *)
(* This version returns the (possibly updated) dictionary of fps and types *)
   fun mkagent2 typeInfo str =
     let
       val _ = initLexer str

       val (getParamType, checkParamType, getTypeInfo) =
	 case typeInfo of
	   NONE => ((fn _ => NONE), (fn _ => ()), (fn _ => NONE))
	 | (SOME (fps, unspecified)) =>	(* unspecified is sorted & stays so *)
	     let val fpsR = ref fps : formalParams ref
	       val unspecifiedR = ref unspecified : V.var list ref
	       fun getTypeInfo _ = SOME (!fpsR, !unspecifiedR)
	       fun getParamType v = typeOf (!fpsR, !unspecifiedR) v
	       fun checkParamType (v,t : paramType) = case getParamType v of
		 NONE => ()			(* it's not an fp, so fine *)
	       | SOME(NONE) =>		(* we didn't know, but now we do *)
		   (fpsR := SmallVarDict.insert (!fpsR, v, t);
		    unspecifiedR := SL.remove id V.le (* SL use OK by above *)
		    (v,!unspecifiedR)) 
	       | SOME(SOME tt) =>
		   if t = tt then () (* confirmed what we knew *)
		   else raise Parse ((V.mkstr v)^
				     " used both as "^(paramTypeString t)^
				     " and as "^(paramTypeString tt))
	     in (getParamType, checkParamType, getTypeInfo)
	     end

(* return the action corresponding to actionString, unless it falls in *)
(* the forbidden list, in which case raise Parse. *)
       fun forbid (forbidden, actionString, error) =
	 let val a = mkact actionString
	 in if Lib.member A.eq (a, forbidden) then
	   raise Parse(actionString^error)
	    else a
	 end
       val actionPrefixErrorString = " cannot be an action prefix"

       (* Given the string ac from an Actt, return for hackish reasons the *)
       (* strings forming the next prefix! Apply P.makePrefix to the result.*)
       fun getPrefix ac =
	 let
	   val tok = lexer()
	   val expression = if tok = Lbrack then SOME (toRbrack())
			    else (cache tok; NONE)
	 in (ac,expression)
	 end
       
       fun AGENT tok =
	 let val (A,newTok) = WEAKSUM tok
	 in if newTok=Plus then
	   let val (B,tok) = AGENT(lexer())
	   in case real B of
	     (WSum l)  => (makeAgent(WSum (A::l)),tok)
	   |    _      => (makeAgent(WSum [A,B]),tok)
	   end
	    else (A,newTok)
	 end

           and WEAKSUM s =
               let val (A,newTok) = STRONGSUM s
                in if newTok=SPlus then
                      let val (B,s) = WEAKSUM(lexer())
                       in case real B of
                          (SSum l)  => (makeAgent(SSum (A::l)),s)
                        |    _      => (makeAgent(SSum [A,B]),s)
                      end
                   else (A,newTok)
               end

           and STRONGSUM s =
               let val (A,tok) = PARALLEL s
                in if tok=VBar then
                      let val (B,s) = STRONGSUM(lexer())
                       in case real B of
                          (Parallel l)  => (makeAgent(Parallel (A::l)),s)
                        |        _      => (makeAgent(Parallel [A,B]),s)
                      end
                   else (A,tok)
               end

           and PARALLEL s =
               let val (A,tok) = PREFIX s
                in if tok=Colon then
                      let val (sort,tok) = SORT(lexer())
                       in if tok=Merge then
                             let val (l,s) = MERGE(lexer())
                              in (makeAgent(SMerge((A,sort)::l)),s)
                             end
                          else raise Parse("Expected "^tokstrExtra Merge^
                                           " but found "^tokstrExtra tok)
                      end
                   else (A,tok)
               end

           and SORT (Vart v) =
	     let val var = V.mkvar v
	       val _ = checkParamType (var, ActionSetParamType)
	     in (Variable var, lexer())
	     end
	   
             | SORT (Lset) =
               let val tok = lexer()
                in if tok=Rset
		     then (UI.chat
"Hmm... a component with empty sort can't do anything. D'you mean this?";
			   (Literal (A.ActionSet.make []),lexer()))
                   else let val (l,s) = ACTLIST (tok, [A.eps, A.tau],
						 " cannot be in the sort")
			in (Literal (A.ActionSet.make l),
			    check(Rset,s))
                        end
               end

             | SORT tok =
               raise Parse("Expected { or a variable after : but found "
                           ^tokstrExtra tok)

           and MERGE s =
               let val (A,tok) = PREFIX s
                   val (sort,tok2) = SORT(check(Colon,tok))
                in if tok2=Merge then
                      let val (l,tok3) = MERGE(lexer())
                       in ((A,sort)::l,tok3)
                      end
                   else ([(A,sort)],tok2)
               end

           and PREFIX (Actt ac) =
	     let
	       val a = P.makePrefix (getPrefix ac)
	       val (A,s) = PREFIX(check(Point,lexer()))
	     in (makeAgent(Prefix([a],A)),s)
	     end

	   | PREFIX (Prefixt p) =	(* see below *)
	     let
	       val a = P.makePrefix p
	       val (A,s) = PREFIX(check(Point,lexer()))
	     in (makeAgent(Prefix([a],A)),s)
	     end

(* the only way a BASIC POST can start with an Lbrack is if the BASIC *)
(* is actually an (AGENT) so we use this knowledge to avoid *)
(* backtracking after we've eaten the Lbrack. *)
             | PREFIX Lbrack =
               let val tok = lexer()
(* a little tricky. (a might be followed by ,... (i.e. the a was part *)
(* of a PREFIXLIST) or by ) (the silly user wrote a one-element action *)
(* list with brackets) or by . (the a is a prefix, the brackets are part of *)
(* an (AGENT) which in turn is a BASIC -- the PREFIX we're looking at *)
(* has the form BASIC POST, specifically (AGENT) POST *)
	       in case tok of Actt ac =>
		 let
		   val preA = getPrefix ac
		   val a = P.makePrefix preA
		   val nextTok = lexer()

(* if a PREFIX starts with (a,...q), it must be (a,...q).PREFIX *)
		 in case nextTok of Comma =>
		   let val (l,s) = PREFIXLIST (lexer())
		     val (A,newTok) = PREFIX(check(Point,check(Rbrack,s)))
		   in (makeAgent
		       (Prefix((SL.sort P.le false (a::l)),A)),newTok)
		   end

(* if a PREFIX starts with (a), it must be (a).PREFIX *)
		     | Rbrack =>
		   let val (A,newTok) = PREFIX(checkNext Point)
		   in (makeAgent(Prefix([a],A)),newTok)
		   end

(* if a PREFIX starts (a. it must be *)
(* BASIC POST where the BASIC must be ( AGENT ) and the AGENT starts *)
(* a. So we shove the . back on the stack, use AGENT and then POST !! *)
(* Value-passing persuaded me into an even more wierd hack: we start AGENT *)
(* off with this special token Prefixt (seen nowhere else) to save pushing *)
(* many tokens back onto the stack! *)
	             | Point =>
		   let val _ = cache Point (* :-) *)
		     val (A, newTok) = AGENT (Prefixt preA)
		   in POST(A, check (Rbrack, newTok))
		   end

		     | tok => raise Parse
			 ("Expected . or , or ), found "^tokstrExtra tok)
		 end
(* if we met something other than an action after the ( it's simple, *)
(* we're in the same situation as above (looking at (AGENT) POST) but *)
(* we found this out one token sooner. *)
               		 | _ =>
		 let val (A,s) = AGENT tok
		 in POST (A, check (Rbrack, s))
		 end
	       end

             | PREFIX (Timet t) =
               let val (A,s) = PREFIX(check(Point,lexer()))
                in (makeAgent(Time(t,A)),s)
               end

             | PREFIX Deltat =
               let val tok = lexer()
	       in (case tok of Actt ac =>
		     let val a = P.makePrefix (getPrefix ac)
			 val (A,s) = PREFIX(checkNext Point)
		     in (makeAgent(Delta(a,A)),s)
		     end

	                     | _ =>
		 let val _ = cache tok
		 in
		   POST(BASIC Deltat)
		 end)
               end

             | PREFIX s = POST(BASIC s)

           and BASIC (Nilt) = (makeAgent(Nil),lexer())

             | BASIC (Deltat) = (makeAgent(DNil),check(Nilt,lexer()))

             | BASIC (Bottomt) = (makeAgent(Bottom),lexer())

(* Idea is that a variable in this context really is an agent variable.  *)
(* Avoid ending up here if it's a variable used as AP to a param agent *)
             | BASIC (Vart v) =
	       (case lexer() of
		  Lbrack =>
		    let val (pl,s) = PARAMLIST(lexer())
		    in (makeAgent(Var(V.mkvar v,pl)),check(Rbrack,s))
		    end
		| s => let val var = V.mkvar v
			   fun reallyAgent _ = (makeAgent(Var(var,[])),s)
		       in (checkParamType (var, AgentParamType);
			   (makeAgent(Var(var,[])),s))
		       end)

             | BASIC (Lbrack) =
               let val(A,s) = AGENT(lexer())
                in (A,check(Rbrack,s))
               end

             | BASIC tok =
               raise Parse("Unexpected "^tokstrExtra tok)

           and PARAMLIST s =
	     let val (p,tok) = PARAM s
	     in if tok=Comma then
	       let val (pl,s) = PARAMLIST(lexer())
	       in (p::pl,s)
	       end
		else ([p],tok)
	     end

       and PARAM (token as Actt ac) =
	 let val a = forbid ([A.eps], ac, " cannot be a parameter")
	   val tok = lexer()
	 in if tok=Point then
(* oops, this is the beginning of an agent parameter, backtrack *)
	   let val _ = cache Point
	     val (A,s) = AGENT(token)
	   in (AgentParam A, s)
	   end
	    else (ActParam a,tok)
	 end

(* here need to be careful to distinguish between a time occurring as *)
(* a param in its own right and as the beginning of an agentparam *)
	 | PARAM (token as Timet t) =
	   let val tok = lexer()
	   in if tok=Point then
(* oops, this is the beginning of an agent parameter, backtrack *)
	     let val _ = cache Point
	       val (A,s) = AGENT(token)
	     in (AgentParam A, s)
	     end
	      else (TimeParam t,tok)
	   end

(* it's an action set, and we're being given it explicitly as a list *)
	 | PARAM Lset =
	   let val tok = lexer()
	   in if tok=Rset
		then (ActionSetParam (Literal (A.ActionSet.make [])),
		      lexer())
	      else let val (l,s) = ACTLIST (tok, [A.eps],
					    " cannot be in an action list")
		   in (ActionSetParam
		       (Literal (A.ActionSet.make l)),
		       check(Rset, s))
		   end
	   end

(* Mildly complicated. If a parameter starts with a variable and is a bare *)
(* variable, we want to make it the right kind of parameter if possible. *)
(* But the next token might be a Vart because, say, it's X + a.0, in which *)
(* case we want to use the case below. So let's have a look: *)
	 | PARAM (Vart v) =
	   let val nextTok = lexer()
	   in if (nextTok = Comma) orelse (nextTok = Rbrack) then
(* it's a bare variable *)
	     let val var = V.mkvar v
	       fun reallyAgent _ = (AgentParam (makeAgentFromVar var),nextTok)
	     in case getParamType var of
	       NONE => reallyAgent() (* it isn't a fp *)
	     | SOME(NONE) => reallyAgent() (* it is, but we don't know type *)
(* It may actually turn out to be an action set, but  *)
(* we'll handle that in a minute or in lookupapply. Hack hack! *)
	     | SOME (SOME AgentParamType) => reallyAgent()
	     | SOME (SOME ActionSetParamType) =>
		 (ActionSetParam (Variable var), nextTok)
	     | SOME _ => raise PanicNoisily "Agent.str, PARAM"
	     end
	      else			(* nextTok wasn't , or ) *)
		let val _ = cache nextTok;
		  val (A,s) = AGENT (Vart v)
		in (AgentParam A,s)
		end
	   end
		
	 | PARAM s = let val (A,s) = AGENT s
		     in (AgentParam A,s)
		     end

(* take a token, a list of things that shouldn't be in the list, and a *)
(* string to pass as an error message if such a thing should occur. *)
       and ACTLIST (Actt ac, forbidden, error) =
	 let val a = forbid (forbidden, ac, error)
	 in let val tok = lexer()
	    in if tok=Comma then
	      let val (l,s) = ACTLIST(lexer(), forbidden, error)
	      in (a::l,s)
	      end
	       else ([a],tok)
	    end
	 end

	 | ACTLIST (tok,_,_) =
	   raise Parse("Unexpected "^tokstrExtra tok)

       and PREFIXLIST (Actt ac) =
	 let val a = P.makePrefix (getPrefix ac)
	 in let val tok = lexer()
	    in if tok=Comma then
	      let val (l,s) = PREFIXLIST(lexer())
	      in (a::l,s)
	      end
	       else ([a],tok)
	    end
	 end

	 | PREFIXLIST tok =
	   raise Parse("Unexpected "^tokstrExtra tok)

(* POST takes the agent for which we're looking at a postamble, and *)
(* the first token of the possible postamble. *)
       and POST (A, Lsq) =	
	 (case lexer() of
	    Rsq => POST(A, lexer())(* ignore empty relabelling *)
	  | (Vart v) =>
	      POST(relabelWithVar(A,V.mkvar v), check(Rsq,lexer()))
	  | s =>
	      let val (l,s) = RELABELLIST s
	      in POST(relabel(A,(makeLiteralRelabelling l)),
		      check(Rsq,s))
	      end )

	 | POST (A, Rest) =
	   (case lexer() of (Actt ac) =>
	      let val a = forbid ([A.eps,A.tau], ac," cannot be restricted")
	      in POST(makeAgent(Restrict
				(A, Literal (A.portsOfActions
					     (A.ActionSet.make [a])))),
		      lexer())
	      end
        	   | (Vart v) =>
		       let val var = V.mkvar v
		       in (checkParamType (var, ActionSetParamType);
			   POST(makeAgent(Restrict(A,Variable var)),
				lexer()))
		       end
	           | Lset =>
		       (case lexer() of Rset =>
			  (UI.chat "Ignoring empty restriction";
			   POST(A, lexer()))
		     | s =>
			  let val (l,s) =
			    ACTLIST (s, [A.tau, A.eps],
				     " cannot be in the restriction set")
(* So everything in the list has a port *)
			    val portSet = A.portsOfActions (A.ActionSet.make l)
			  in POST(makeAgent
				  (Restrict (A,Literal portSet)),
				  check(Rset,s))
			  end )
		   | tok => raise Parse("Unexpected "^tokstrExtra tok) )

	 | POST x = x

       and RELABELLIST s =
	 let val (relab,tok) = RELABEL s
	 in if tok=Comma then
	   let val (l,s) = RELABELLIST(lexer())
	   in (relab::l,s)
	   end
	    else ([relab],tok)
	 end

       and RELABEL (Actt ac) =
	 let val tok = checkNext Repl
	 in case tok of
	   Actt ac' =>
	     let val a = forbid ([A.eps], ac, " cannot be a relabelling")
	       val b = forbid ([A.eps, A.tau], ac', " cannot be relabelled")
	     in ((a,b),lexer())
	     end
	       | _      => raise Parse("Unexpected "^tokstrExtra tok)
	 end

	 | RELABEL tok = raise Parse("Unexpected "^tokstrExtra tok)

       val (A, nextTok) = AGENT(lexer())

       fun checkParamTypes A = case getTypeInfo() of
	   NONE => (A, NONE)
	 | SOME (fps, []) => (A, SOME fps) (* all params are now typed *)
	 | SOME (fps, (h::t)) =>
	     if UI.interactive() then 
	       let val _ = UI.message
		 ("Couldn't infer type of "^(V.mkstr h)^". Please specify:")
		   val typeOfH = UI.pickFromList "Enter digit: "
		     (fn t => (paramTypeString t)^"\n")
		     [AgentParamType, ActionSetParamType]
	       in (checkParamType (h,typeOfH); (* record user's choice *)
		   mkagent2 (getTypeInfo()) str)
(* and go round again with more type info. We could have a new fn just to do*)
(* the necessary substitution, but why bother, what would it buy?           *)
	       end
	     else (* there's no user, report error (could have default?) *)
	       raise Parse ("Couldn't infer type of "^(V.mkstr h))
       val _ = UI.debug ("mkagent on "^str)

     in if nextTok=Eos then (checkParamTypes A)
	else raise Parse("Extra input")
     end				(* of mkagent2 *)

(* version for the public interface: no type information given or returned *)
   fun mkagent str = fst (mkagent2 NONE str)
     
(* Specify that v is a formal param with type NONE (not yet specified) or  *)
(* SOME t. Add it to fps in the latter case, else to unspecified. *)
(* Raise Parse if this is a duplicate fp. *)
(* Unspecified must be sorted and stays so *)
   fun addFP (fps, unspecified) (v, t) =
     case typeOf (fps, unspecified) v of
       NONE =>
	 (case t of
	    NONE => (fps, SL.add V.le true (v,unspecified)) (* SL use OK *)
	  | SOME tt => (SmallVarDict.insert (fps, v, tt), unspecified))
     | SOME _ => raise Parse("Can't have duplicate formal parameters!")
     
(* As well as the list of params (now just plain variables) *)
(* return a smallVarDict specifying the types of the formal parameters *)
(* where specified, plus a list of unspecified agent or set params *)
(* Caution: this is experimental and time/act are not treated same way! *)
   fun makeAgentParamList agentParamString = 
     let val _ = initLexer agentParamString

       fun readParamType _ = case lexer() of
	 Actt t => makeParamType t	(* types look like Actts *)
       | x => raise Parse ("Expected a parameter type but found "^
			   (tokstrExtra x))

       fun FPARAMLIST (fps, unspecified) s =
	 let val (v,t) = FPARAM s
	   val (newFPs, newUnspecified) = addFP (fps, unspecified) (v,t)
	 in case lexer() of
	   Comma =>
	     let val (l,info) = FPARAMLIST (newFPs, newUnspecified) (lexer())
	     in ((v::l), info)
	     end
	 | Eos => ([v],(newFPs, newUnspecified))
	 | s => raise Parse ("Extra input "^(tokstr s)^
			     " after formal parameter "^
			     (V.mkstr v)^" to the agent.")
	 end

(* Return V.var * paramType option, NONE if unspecified *)
	 and FPARAM (Vart s) =
	   let val tok = lexer()
	     val v = V.mkvar s
	   in case tok of
	     Colon => (v, SOME (readParamType()))
	   | _ => (cache(tok); (v, NONE)) 
	   end
(* Warning: This may actually turn out to be an action set param -- we *)
(* can't tell at this stage. The instantiation process will try to Do  *)
(* The Right Thing, but it's a bit of a hack. *)

(* Make formal action/time params look just like lower case vars, i.e *)
(* forbid 'a as well as tau, eps. *)
	   | FPARAM (Actt s) =
	   let val a = mkact s
(* allow the user to specify act, just for fun *)
	      val _ = case lexer() of
		Colon => (case readParamType() of
			    ActParamType => ()
			  | tt => raise Parse ("Formal parameter "^s^
	      " starts with lower case, \nso it must have type act. Sorry!"))
	      | tok => cache tok	(* pretend we didn't look! *)
	   in if A.isInput a = SOME true
		then (V.mkvar s, SOME ActParamType)
	      else raise Parse(s^" cannot be a formal parameter")
	   end
(* Warning: This may actually turn out to be a time param -- we *)
(* can't tell at this stage. The instantiation process will try to Do  *)
(* The Right Thing, but it's a bit of a hack. *)

	 | FPARAM (tok) =
	   raise Parse("Expected a parameter but found "^tokstrExtra tok)

       val _ = UI.debug ("makeAgentParamList on "^agentParamString)
       val answer = FPARAMLIST (noFormalParams(),[]) (lexer())
     in if lexer()=Eos then answer
	else raise Parse("[46]Extra input")
     end				(* of makeAgentParamList *)
end					(* local open LexingAgent in *)

(* CWB SKELETON *)
(* Stuff that was in AgentParser before. There's some near-duplication *)
(* with what's above: need to sort this out, Perdita. *)

open Lexing				(* the global one this time *)
   exception ActErr of string
   fun mkact s = A.mkact s		(* may raise Parse, will pass it up *)

(* This could be in Act -- but relabellings want to be here? Not sure. *)
(* Possibly Relabelling wants to be a structure in its own right.      *)
   (* list of pairs of actions, as for relabellings *)
   (* return the next token as well as a parameter list, since we had to *)
   (* grab it to see if it was a comma. *)
   fun ACTACTLIST (Actt ac) =
     let val a = mkact ac
     in
       if A.eq(a,A.eps) then raise ActErr ac
       else
	 let val tok = check (Repl, lexer())
	 in
	   case tok of Actt ac =>
	     let val b = mkact ac
	     in
	       if A.eq(b,A.eps) orelse A.eq(b,A.tau)
		 then raise ActErr ac
	       else let val tok = lexer()
		    in if tok=Comma
			 then let val (l,newTok) = ACTACTLIST(lexer())
			      in ((a,b)::l,newTok)
			      end
		       else ([(a,b)],tok)
		    end
	     end
	 | _ => raise Parse("[AP1]Expected an action but found "
			    ^(tokstrExtra tok))
	 end
     end
   
     | ACTACTLIST (tok) =
       raise Parse("[AP2]Expected an action but found "^tokstrExtra tok)
  

   fun readRelabelling _ = 
     let val tok = checkNext(Lsq)
     in if tok=Rsq then []
	else let val (l,tok) = (ACTACTLIST tok
				handle ActErr ac =>
				  raise Parse("[AP4]Invalid use of "^ac))
		 val _ = justCheck(Rsq,tok)
	     in l
	     end
     end

   fun readAgent _ = mkagent (getRest())
     
   fun readAgentPair _ =
     let val _ = justCheckNext Lbrack
       val A = toCommaWithBracketCount()
       val B = toRbrack()
     in (mkagent A,mkagent B)
     end
	   
   fun readNatAgent _ = 
     let val _ = justCheckNext(Lbrack)
       val t = readNat()
       val _ = justCheckNext Comma
       val A = toRbrack()
     in (t,mkagent A)
     end

   fun readActAgent _ =
     let val tok = checkNext Lbrack
     in case tok of
       Actt ac =>
	 let val a = mkact ac
	 in if A.eq(a,A.eps) then
	   raise Parse("[25M]"^ac^" is an invalid action here")
	    else
	      let val _ = justCheckNext Comma
		val A = toRbrack()
	      in (a,mkagent A)
	      end
	 end
     | _ => raise Parse("[26M]Expected an action but found "
			^tokstrExtra tok)
     end
	
(* expect some actions (at least one) followed by an agent, all comma sep. *)
   fun readActlistAgent epsAndTausAllowed =
     let val tok = checkNext Lbrack
     in case tok of
       Actt ac =>
	 let val aseq =
	   (A.ACTLIST2 epsAndTausAllowed tok (is Rbrack))
	   handle ActErr ac =>
	     raise Parse("[14M]Invalid use of "^ac)
	     val A = toRbrack()
	     val _ = if null aseq then
	       raise Parse
		 ("Expected some actions (and then an agent)")
		     else ()
	     val _ = if A = "" then
	       raise Parse
		 ("Expected an agent but found only actions")
		     else ()
	 in (aseq,mkagent A)
	 end
     | _ => raise Parse("[17M]Expected an action but found "
			^tokstrExtra tok)
     end
		   
   fun readVarAgent _ = 
     let val tok = checkNext(Lbrack)
     in case tok of
       Vart t =>
	 let val _ = justCheckNext Comma
	   val A = toRbrack()
	 in (V.mkvar t,mkagent A)
	 end
     | _ => raise Parse("[16M]Expected a Variable")
     end

   
(*****************************************************************************)
(* Some stuff transplanted from Interface.str, defunct. Some of this *)
(* may want to end up elsewhere; it's arguable either way.           *)
   fun printagents [] =  UI.print "None."
     | printagents l = UI.printListNumbered mkstr l

   val actseq = Lib.mkstr A.mkstr " "
   fun multiStrongDeriv (al, ag) = "--- "^(actseq al)^" ---> "^(mkstr ag)
   fun multiWeakDeriv (al, ag) = "=== "^(actseq al)^" ===> "^(mkstr ag)
   fun transitionString (a, ag) = "--- "^(A.mkstr a)^" ---> "^(mkstr ag)

   fun printListForAgent f [] = UI.print "None."
     | printListForAgent f l = (map (fn x => UI.print (f x)) l; ())
   val printdersseq = printListForAgent multiStrongDeriv
   val printexps = printListForAgent multiWeakDeriv
   val printders = printListForAgent transitionString
(*****************************************************************************)

   fun setmkstr mkstrelt l = "{"^(Lib.mkstr mkstrelt "," l)^"}"

   fun agent2whatever p f (_ : unit) =
     let val ag = readAgent()
     in UI.print (p (f ag))
     end

   val agent2agent = agent2whatever mkstr
   val agent2bool = agent2whatever (Bool.toString : bool -> string)
(* CWB SKELETON *)

(* CWB SKELETON *)
(* Some stuff that used to be in AgentCommands: *)
   fun agentCommand _ =
     let val X = readVar()
       val tok = lexer()
       fun bindAgent (X, (FP, info)) =
	 let val (A, completedInfo) = mkagent2 info (getRest())
	   val pl = case completedInfo of
	     NONE => []			(* unparameterised agent *)
	   | SOME d => 
	       let fun varToParam v =
		 (case (SmallVarDict.find (d,v)) of
		    SOME AgentParamType => AgentParam (makeAgentFromVar v)
		  | SOME ActionSetParamType => ActionSetParam (Variable v)
		  | SOME ActParamType => ActParam (A.mkact (V.mkstr v))
		  | NONE => raise PanicNoisily
			("Agent.str, agentCommand: "^(V.mkstr v)))
	       in map varToParam FP
	       end
	 in (if E.isBound(X, !(agtenv)) then Registry.resetTables() else ();
	       (agtenv) := E.bind(X,makeParameterisedAgent(pl,A),
				  !(agtenv)))
	 end
       fun printAgent(X) =
	 (UI.print (agentDefString X)
	  handle E.Unbound => UI.message((V.mkstr X)^" is unbound"))

     in case tok of
       Equals => bindAgent(X,([],NONE))
     | Lbrack =>
	 let val agentParamString = toRbrack()
	   val (plist, info) = makeAgentParamList agentParamString
	   val _ = justCheckNext Equals
	 in bindAgent(X,(plist,SOME info))
	 end
     | Eos => printAgent X
     | _ => raise Parse("[18M]Expected = or ( but found"
			^tokstrExtra tok) 
     end

   fun relabelCommand _ =     
     let val X = readVar()
       val tok = lexer()
     in case tok of
       Equals => bindRelabelling (X, readRelabelling())
(* that may raise Error, we let it go up. Better than Parse in this case? *)
     | Eos => (UI.print (relabellingDefString X)
	       handle E.Unbound => UI.message((V.mkstr X)^" is unbound"))
     | _ => raise Parse("[23M]Unexpected "^(tokstrExtra tok))
     end

   fun transitionsCommand _ = printders (transitions (readAgent()))
   val divergesCommand = agent2bool diverges
   val prefixformCommand = agent2agent prefixform
		     
   val transitionsDoc = 
(* CWBDOC: transitions *)
(* Automatically generated section *)
"transitions: list the (single-step) transitions of an agent \
\\n\
\\n  transitions A; \
\\n  \
\\n  Synonyms: tr\
\\n  See also: sim, derivatives, closure, obs, vs, random, init"
(* CWBDOC: transitions *)

   val agentDoc = 
(* CWBDOC: agent *)
(* Automatically generated section *)
"agent: change (or show) the definition of an agent identifier \
\\n\
\\n  agent X = A; \
\\n  binds agent A to identifier X\
\\n  agent X(FP) = A; \
\\n  binds a parameterised agent ((T)CCS only)\
\\n  agent X; \
\\n  prints the definition of X\
\\n\
\\n  An agent identifier must begin with an upper case letter.\
\\n  \
\\n  (T)CCS only:\
\\n  \
\\n  If P is a formal parameter, it is an error to use P(anything)\
\\n  in the body of the definition.\
\\n  \
\\n  If a formal parameter name starts with a lower case letter, it stands\
\\n  for an action. If it starts with an upper case letter, it stands for\
\\n  an agent or for an action set, depending on context.\
\\n  \
\\n  Synonyms: bi,pi"
(* CWBDOC: agent *)

   val divergesDoc = 
(* CWBDOC: diverges *)
(* Automatically generated section *)
"diverges: does the agent contain an unguarded occurrence of @? \
\\n\
\\n  diverges A; \
\\n  \
\\n\
\\n  Returns true iff there is an unguarded occurrence of bottom (@).\
\\n  Notice especially that an agent which can just do taus for ever does\
\\n  not diverge in this sense!\
\\n  \
\\n  Synonyms: div"
(* CWBDOC: diverges *)

   val prefixformDoc = 
(* CWBDOC: prefixform *)
(* Automatically generated section *)
"prefixform: print an agent in prefix form \
\\n\
\\n  prefixform A; \
\\n  \
\\n\
\\n  This produces an agent which is strongly bisimilar to A and which is a sum of\
\\n  prefixes, e.g. a.A + b.B + c.C.\
\\n  \
\\n  Warning: identifiers appearing in the definition of A may get replaced\
\\n  by their current definitions, so if you later change the definition of\
\\n  such an identifier, A may cease to be bisimilar to what prefixform\
\\n  returned. \
\\n  \
\\n  Synonyms: pf\
\\n  See also: normalform, sim, transitions"
(* CWBDOC: prefixform *)

   val relabelDoc = 
(* CWBDOC: relabel *)
(* Automatically generated section *)
"relabel: change (or show) the definition of a relabelling identifier \
\\n\
\\n  relabel R = [a/p,...]; \
\\n  binds a relabelling function\
\\n  relabel R; \
\\n  prints function bound to R\
\\n\
\\n  a/p means that p is relabelled to a. You cannot relabel tau. \
\\n  If p is relabelled to a, then 'p is also relabelled to 'a. You cannot\
\\n  define a relabelling function which violates this rule.\
\\n  "
(* CWBDOC: relabel *)     

val ccsActDoc =
(* CWBSYNTAX: act *)  
(* Automatically generated section *)
" ACT  a  tau  internal action \
\\n         n  name: an identifier beginning with a lower case letter \
\\n         'n  coname. This is an ASCIIfication of normal CCS's overbarred n. \
\\n         eps  empty observation, not allowed in agents (because it isn't really an action!) \
\\n"
(* CWBSYNTAX: act *)

val ccsAgentDoc =
(* CWBSYNTAX: agent *)  
(* Automatically generated section *)
" AGENT  A  0  deadlock (nil) \
\\n           a.A  action prefix \
\\n           A + A  (weak) choice \
\\n           A | A  parallel composition \
\\n           A \\ a  restriction of a single action \
\\n           A \\ S  restriction of a set \
\\n           A[R]  relabelling \
\\n           (A)  you can use brackets just as you'd expect \
\\n           X  agent variables begin with upper case \
\\n           @  divergence (for Walker-style divergence preorders etc.) \
\\n           $ 0  delayed nil (for TCCS) \
\\n           $ a.A  delayed action prefix (for TCCS) \
\\n           A ++ A  strong choice (for TCCS) \
\\n           A1 : S1 | | A2 : S2  synchronisation merge (CSP style) (S1 and S2 are action sets) \
\\n           X(P,...)  parameterised agent \
\\n\
\\n\
\\n  The order of precedence is as usual: Summation binds the weakest,\
\\n  followed by Strong Summation, Parallel Composition, Prefixing, and\
\\n  finally Restriction and Relabelling. These precedence rules can be\
\\n  overcome by using parentheses.\
\\n  "
(* CWBSYNTAX: agent *)

val ccsRelabelDoc =
(* CWBSYNTAX: relabel *)   
(* Automatically generated section *)
" RELABEL  R  [a/a,...]  relabelling function, given as a set of pairs \
\\n             V  relabelling variables begin with upper case \
\\n"
(* CWBSYNTAX: relabel *)

val ccsDoc =
(* CWBDOC: ccs *)
(* Automatically generated section *)
"ccs: show CCS syntax \
\\n\
\\n  ccs; \
\\n  show all CCS syntax\
\\n  ccs act; \
\\n  show syntax of CCS actions\
\\n  ccs agent; \
\\n  show syntax of CCS agents\
\\n  ccs relabel; \
\\n  show syntax of CCS relabelling functions\
\\n\
\\n  The formatting's not great, sorry: you'll find it more convenient to \
\\n  consult the Web page or the user manual.\
\\n  "
(* CWBDOC: ccs *)

fun ccsCommand _ =
  let val tok = lexer()
  in case tok of
    Eos => UI.message (ccsActDoc^"\n"^ccsAgentDoc^"\n"^ccsRelabelDoc)
  | (Actt a) => if a="act" then UI.message ccsActDoc
		else if a="agent" then UI.message ccsAgentDoc
		     else if a="relabel" then UI.message ccsRelabelDoc
			  else UI.message
			    "Valid arguments are act, agent, relabel"
  | _ => UI.error "Invalid argument"
  end

   val _ = UI.registerCommands PABasic processAlgebra
     [
      ("transitions", transitionsDoc, transitionsCommand),
      ("agent", agentDoc, agentCommand),
      ("diverges", divergesDoc, divergesCommand),
      ("prefixform", prefixformDoc, prefixformCommand),
      ("relabel", relabelDoc, relabelCommand),
      ("ccs", ccsDoc, ccsCommand)
      ]

   val _ = UI.registerAlias ("bi","agent")
   val _ = UI.registerAlias ("pi","agent")
   val _ = UI.registerAlias ("tr","transitions")
   val _ = UI.registerAlias ("div","diverges")
   val _ = UI.registerAlias ("pf","prefixform")
end