RCS "$Id: GameCheck.str,v 1.84 1998/08/13 11:39:03 pxs Exp $";
(* Model checker based on Stirling games. *)
functor GameCheck ( structure Ag  : AGENT_WRAPPER;
		    structure L  : LOGIC2_PROTECTED;
		    sharing  Ag.A = L.M.A) : GAMECHECK =
struct
structure Ag = Ag
structure A = Ag.A
structure AgentHash = HashTable
open L

type index = (int Vector.vector)

(* ints are saying when this decision was added so we can tell when we  *)
(* may have invalidated it. 0 means never invalidate this one.          *)
(* a decision is Safe if it always applies: no need to check or keep index *)
datatype decision = Safe of int
(* index is the index where we added the decision, obviously *)
  | Unsafe of (int * index)

type config = Ag.agent * prop
(* type node represents an annotated node of the game graph, as known so far *)
(* Config uniquely determines node: see function makeNode below. *)
datatype node = DUMMY of
  (config *				(* where is this node? *)
   node list option *
   (* successors, if known? *)
(* WARNING: dependency: the A-decision list must be in sync with the *)
(* move node-list. Better way to do this? (O for mutually rec. datatypes.) *)
   (decision list * decision list) *	(* abelard, eloise: see defn above *)
   node list *			(* if A-choice with A-dec, what move *)
                                (* in the strategy justify A-decisions? *)
   (index * int * (bool ref * bool ref)) option
(* Is there an occurrence in playList? At what index? What count? *)
(* Has it been used as an assumption for abelard? for eloise? *)
   ) ref
type position = node * index

type 'a configTable = (prop, (Ag.agent, 'a) HashTable.hash_table)
  HashTable.hash_table
    
exception NotKnownHere  
fun getPropEntry l prop = (HashTable.lookup l prop)
  handle NotKnownHere => raise (PanicNoisily "GameCheck, getPropEntry")
  
fun setPropEntry l (key, value) = (HashTable.insert l (key,value); l)
fun noPropEntry _ = HashTable.mkTable (hashval, op =) (126,NotKnownHere)
val applyProp = HashTable.appi
val listPropEntries = HashTable.listItemsi
fun configString (agent, prop) = (Ag.mkstr agent)^"\n"^(L.printString prop)
  
fun getConfigEntry l (agent,prop) = HashTable.lookup (HashTable.lookup l prop)
  agent 

fun setConfigEntry l ((agent,prop), value) =
  let
(*     val _ = UI.debugFn (fn _ => "setConfigEntry for "^(configString (agent, prop))) *)
    val agentTable = (HashTable.lookup l prop)
    handle NotKnownHere =>
      let val emptyAgentTable = HashTable.mkTable (Ag.hashval, Ag.eq)
	(1024, NotKnownHere)
      in (setPropEntry l (prop, emptyAgentTable); emptyAgentTable)
      end
  in (AgentHash.insert agentTable (agent, value); value)
  end
fun noConfigEntry _ = noPropEntry()
fun deleteConfigEntry l (agent, prop) =
  ((* UI.debugFn (fn _ => "deleteConfigEntry for "^(configString (agent, prop))); *)
   (AgentHash.remove (getPropEntry l prop) agent))
  handle NotKnownHere => raise PanicNoisily
      "GameCheck, deleteConfigEntry"

fun configTableString eltStr t = 
  List.foldr
  (fn ((prop,agentTable),soFar) => soFar^
   "\n\nMoves from "^(L.printString prop)^"\n"^
   (List.foldr
    (fn ((agent, value),soFar2) => soFar2^"\n"^(Ag.mkstr agent)^" => \n"^
     (eltStr value))
     "" (AgentHash.listItems agentTable)))
   "" (listPropEntries t)

(* We replace fixpoints by their variables. Here's a fun that does that *)
fun variableize p =
  case real p of
    (Max (X,phi)) => makeProp(Var X)
  | (Min (X,phi)) => makeProp(Var X)
  | _ => p
  

(* Let's have a more concise description of a strategy. *)
(* Print it as we go because concatenating this string is slooooooooow *)
fun printStrategyString table =
  let val printIt = UI.print
    val _ = printIt
("We divide the reachable configurations according to proposition.\n"^
 "We omit positions from which there's only one legal move.")
    fun f (prop,agentTable) =
    let val l = AgentHash.listItems agentTable
      val start =
"\n=========================================================================\n"
^(L.printString prop)^"\n"
      fun whichOfTwoProps word (p,q) =
	let val (pv,qv) = (variableize p, variableize q)
	    fun separate (left, right) [] = (left, right)
	      | separate (left, right) ((agent, (_, prop))::t) =
		let val propv = variableize prop
		in if propv = pv then separate (agent::left, right) t
		   else if propv = qv then separate (left, agent::right) t
			else raise PanicNoisily "GameCheck, strategyString"
		end
	    val (takeLeft, takeRight) = separate ([],[]) l
	in if null takeLeft then
	  if null takeRight then ()
	  else printIt(start^"always take the right "^word)
	   else if null takeRight
		  then printIt(start^"always take the left "^word)
		else printIt
		  (start^"take the left "^word^" from these agents:\n\n"^
		   (Lib.mkstr Ag.mkstr "\n" takeLeft)^
		   "\n\nand take the right "^word^" from these agents:\n\n"^
		   (Lib.mkstr Ag.mkstr "\n" takeRight))
	end
(* Really, should filter out cases where there is only one valid successor, *)
(* but that's a bit harder. Worth doing? I dunno.   *)
      fun whichSuccessor _ =
	(printIt (start^"these agents may occur:");
	(map (fn (ag1, (ag2, _)) =>
	      printIt("\nfrom\n"^(Ag.mkstr ag1)^"\nmove to\n"^(Ag.mkstr ag2)))
	 l);
	 ())
    in case real prop of
      (And (p,q)) => whichOfTwoProps "conjunct" (p,q)
    | (Or (p,q)) => whichOfTwoProps "disjunct" (p,q)
    | (Nec (m,p)) => whichSuccessor()
    | (Pos (m,p)) => whichSuccessor()
    | _ => raise PanicNoisily "GameCheck, strategyString, not a choice point"
    end
  in (map (fn x => (f x)) (HashTable.listItemsi table); ())
  end

(* position and as-yet-unexplored successor nodes *)
type gameListItem = position * node list
fun init _ = ref (HashTable.mkTable (Ag.hashval, Ag.eq) (1024,NotKnownHere))
  : (Ag.agent, node) HashTable.hash_table ref

(************************** Players *****************************************)
(* Eloise (Player) is CPS' Player II. Abelard (Opponent) is Player I.       *)
(* Abandonned P/O, mostly(!) because it's too confusing with type player    *)
(****************************************************************************)
type player = bool
val eloise = true
val abelard = false
fun playerString b  = if b then "Eloise"
		      else "Abelard"
val (pString, oString) = (playerString eloise, playerString abelard)
val other = not				(* excessive? historic! *)

datatype mover = Referee | Player of player
  
(* When we go through a fixpoint we record the fact, so that at each fixpoint*)
(* we can quickly check whether it's a repeat, and who wins.                 *)
(* When we meet such a repeat won by PlayerA, later decisions for A will be  *)
(* vulnerable until/unless we backtrack through the fixpoint checking for A  *)
(* If we end up backtracking checking for B we need to recognise that these  *)
(* decisions are unusable. We use counters in the assumptions and decisions  *)
(* to recognise these ones. This also lets us not *actually* remove them.    *)
(* NB same reference, now! *)
val counts as (oCount, pCount) = let val r = ref 0 in (r, r) end
fun pairMember player = if player then snd else fst
(* Segments say which counts mean this decision is invalid. *)
(* Segments are non-overlapping, ordered from high to low.  *)
val invalidSegments as (invalidOSegments, invalidPSegments) =
  (ref []: (int * int) list ref, ref []:  (int * int) list ref)

fun segmentsString l = Lib.mkstr (fn (x,y) : int * int
				  => "["^(Int.toString x)^","
				  ^(Int.toString y)^"]") " " l
(* Record the fact that all decisions for player with numbers at least *)
(* leastInvalidNo and at most the current no are invalid.     *)
fun invalidate (leastInvalidNo, player) =
  let val selector = fn arghValueRestriction =>
    pairMember player arghValueRestriction
    val topR = selector counts
    val top = !topR
    val _ = UI.debugFn (fn _ =>
		     "Invalidating decisions for "^(playerString player)^
		     " from "^(Int.toString leastInvalidNo)^" to "^
		     (Int.toString top))
    val segments = selector invalidSegments
    fun addTo [] = [(top, leastInvalidNo)]
      | addTo ((seg as (high,low))::t) =
	if low > leastInvalidNo (* seg covered by [top,least...]*)
	  then addTo t	
	else if high < leastInvalidNo (* seg doesn't intersect with new bit *)
	       then (top, leastInvalidNo)::seg::t
	     else (top, low)::t		(* coalesce *)
  in (segments := addTo (!segments);
      UI.debugFn (fn _ => "New segments: "^(segmentsString (!segments)));
      inc topR) (* increment counter! *)
  end
  
fun isValid player no = if no = 0 then true else
  let val segments = !(pairMember player invalidSegments)
    fun f [] = true
      | f ((high,low)::t) = if high < no then true (* gone past no's place *)
			    else if low > no then f t else false
    val answer = f segments
    val _ = UI.debugFn (fn _ => let val s = if answer then " valid for "
					    else " invalid for "
				in (Int.toString no)^s^(playerString player)
				end)
  in answer
  end
  
val (TrueProp, FalseProp) = (makeProp True, makeProp False)

(* relevantSuccessors takes a modality and an agent and returns a list  *)
(* of the successor agents which "satisfy" the modality. That is, if   *)
(* the modality is a positive act list the state is reached via an *)
(* action in the list; if negative, by an action not in the list *)
fun relevantSuccessors (m, ag) = M.filter (m, (Ag.transitions ag))

(******************** MODEL-CHECKING FUNCTION ******************************)
fun modelCheck definitelyPlay (topLevelAgent, topLevelFormula) =
let
val counter = ref 0
val _ = (oCount := 0; pCount := 0; 
	invalidOSegments := []; invalidPSegments := [])
(* paranoia: let's avoid checking the debugging flag every time, it won't *)
(* change during model checking of one problem! *)
val debugFn = if UI.debuggingOn() then UI.debugFn else (fn _ => ())
		 
val _ = UI.chat "Examining proposition..."
(************************** Propositions ************************************)
(* Return the no of variables used, and info about the props bound in order *)
(* It's convenient to have maxVar around as well: arrays start from 0 *)
(* Also doublecheck that the variables are in the right order; they should be*)
val (noOfVars, maxVar, propsBound) =
  let val current = ref 0
    fun check i = if i = (!current) then inc current
		  else raise PanicNoisily "GameCheck, checkOrder"
    fun ex True = []
      | ex False = []
      | ex (Var v) = []
      | ex (And (p,q)) = (examine p)@(examine q)
      | ex (Or (p,q)) = (examine p)@(examine q)
      | ex (Nec (m,p)) = examine p
      | ex (Pos (m,p) )=  examine p
      | ex (phi as Max (v,p)) = (check v; (true,p))::(examine p)
      | ex (phi as Min(v,p)) = (check v; (false,p))::(examine p)
    and examine p = ex (real p)
	
    val boundList = examine topLevelFormula
  in (!current, (!current) - 1, boundList)
  end

val (max, body) =
  let val isMax = Array.fromList (map fst propsBound)
    val bodies = Array.fromList (map snd propsBound)
  in ((fn x => (Array.sub (isMax, x))
       handle General.Subscript => raise PanicNoisily "GameCheck, max"),
      (fn x => (Array.sub (bodies, x))
       handle General.Subscript => raise PanicNoisily "GameCheck, body"))
  end
  
(* A few handy array and vector fns, which assume things have size noOfVars *)
(* Apply a fn to the elements of an array, with index as key, in order. *)
fun applyToArray f i =
  let fun g k =
    if k > maxVar then ()
    else (f (k,Array.sub(i,k)); g (k+1))
  in g 0
  end handle General.Subscript => raise PanicNoisily "GameCheck, applyToArray"

(* Apply a fn to the elements of an array, with index as key, in order. *)
fun applyToVector f i =
  let fun g k =
    if k > maxVar then ()
    else (f (k,Vector.sub(i,k)); g (k+1))
  in g 0
  end handle General.Subscript => raise PanicNoisily "GameCheck, applyToVector"

fun arrayList a =
  let fun from k = if k > maxVar then []
		   else (Array.sub (a,k))::(from (k+1))
  in from 0
  end handle General.Subscript => raise PanicNoisily "GameCheck, arrayList"

(* is there an index s.t. f (index, a[index]) = true? *)
fun arrayExists f a =
  let fun from k = if k > maxVar then false
		   else if f(k,Array.sub (a,k)) then true else (from (k+1))
  in from 0
  end handle General.Subscript => raise PanicNoisily "GameCheck, arrayExists"

fun arrayString f a =
  let fun from k = if k>maxVar then ""
		   else (f (Array.sub (a,k)))^" "^(from (k+1))
  in "["^(from 0)^"]"
  end handle General.Subscript => raise PanicNoisily "GameCheck, arrayString"

fun vectorString f a =
  let fun from k = if k>maxVar then ""
		   else (f (Vector.sub (a,k)))^" "^(from (k+1))
  in "["^(from 0)^"]"
  end handle General.Subscript => raise PanicNoisily "GameCheck, vectorString"

(* Don't include Max or Min, since they don't appear in the game *)
(* In add, below, we rely on the fact that if X = sigma X.phi, *)
(* phi must occur before X! *)
(* A subformula (non-Var) may occur several times: consider this a bug? *)
fun subformulae z =
  case real z of
      True => [TrueProp]
    | False => [FalseProp]
    | (Var v) => []
    | (And (p,q)) => z::((subformulae p)@(subformulae q))
    | (Or (p,q)) =>  z::((subformulae p)@(subformulae q))  
    | (Max (Y,q)) => (subformulae q)@[makeProp(Var Y)]
    | (Min (Y,q)) => (subformulae q)@[makeProp(Var Y)]
    | (Nec (Y,q)) => z::(subformulae q)
    | (Pos (Y,q)) => z::(subformulae q)

val subformsWithDuplication = subformulae topLevelFormula (* just for add *)
val subforms = SL.sort le true subformsWithDuplication (* for everywhere *)
  
(* We need to know, for each subformula phi, whether a given var X may occur*)
(* in a loop X -> phi -> X where X is the winning variable: that is, is X   *)
(* active in phi? *)
val activeVarInfo = ref (noPropEntry()) :
  (prop, bool Array.array) HashTable.hash_table ref
fun getActiveVars prop = getPropEntry (!activeVarInfo) prop

fun free z = case real z of
    True => []
  | False => []
  | (Var v) => [v]
  | (Or (p,q)) => (free p)@(free q)
  | (And (p,q)) => (free p)@(free q)
  | (Nec (Y,q)) => free q
  | (Pos (Y,q)) => free q
  | (Max (Y,q)) => filter (fn X => not (X=Y)) (free q)
  | (Min (Y,q)) => filter (fn X => not (X=Y)) (free q)

(* Take a prop and list of its free vars. For each var, say X = sigma X.phi,*)
(* look up which vars are active in that phi. Which had better be known!*)
fun add (prop, l) = 
  let
    val a = Array.array (noOfVars, false)
(* We have to be careful not to look up formulae we don't store active info *)
(* for, or to get into a loop *)
    val earlierProps =
      let val bodies = map body l
	fun bodystar p =
	  if Lib.member (op =) (p, [TrueProp, FalseProp, prop]) then NONE
	  else case real p of (Max (Y,q)) => bodystar q
                 	| (Min (Y,q)) => bodystar q
			| _ => SOME p
      in List.foldr (fn (p,ll) => case (bodystar p) of NONE => ll | SOME x => x::ll)
	 [] bodies
      end
    val arrays = map getActiveVars earlierProps
    fun updateIfNec (k,_) =
      (if Lib.member (op =) (k,l) (* k free in prop, so active *)
	 orelse List.exists (fn x => Array.sub (x,k)) arrays
(* k was active in body of some var which is free in prop, so active in prop *)
	 then Array.update (a,k,true)	
       else ())
  in (applyToArray updateIfNec a;
      activeVarInfo := setPropEntry (!activeVarInfo) (prop, a))
  end
  
val _ = map (fn p => add (p, free p)) subformsWithDuplication
(* Now activeVarInfo really does record what we think it does! *)

(* If no subformula has both min and max variables active in it, then it *)
(* is always safe to use a decision: there is no need to store or compare *)
(* indexes with decisions. So see whether that's the case. *)
val nonAlternating = not (List.exists
  (fn (_,a) =>
   let fun activeMax (i,active) = active andalso (max i)
     fun activeMin (i, active) = active andalso (not (max i))
   in (arrayExists activeMax a) andalso (arrayExists activeMin a)
   end)
  (listPropEntries (!activeVarInfo)))

val _ = 
  let fun active [] = ""
	| active ((prop,activeVars)::t) = (L.printString prop)^" "^
	  (arrayString Bool.toString activeVars)^"\n"^(active t)
      val s = if nonAlternating then " not" else ""
  in debugFn (fn _ =>
    ("The formula is"^s^" alternating\n"^
     (active (listPropEntries (!activeVarInfo)))))
  end 

(* Just for fun, as an experiment, let's try playing with the order in which *)
(* we explore con/disjuncts. Maybe it's a good idea to explore things with *)
(* no or insignificant active variables first? *)
(* POSTPONED: maybe try this later. *)
(*************************** Indexes*****************************************)
(* An index stores in the ith slot, i.e. against the variable i, the number *)
(* of times X has been                                                      *) 
(* unfolded since any "earlier" variable was unfolded.                      *)
(****************************************************************************)
fun indexString i = vectorString Int.toString i

(* Initially put 0 against all variables. *)
val initindex = Vector.tabulate (noOfVars, (fn _ => 0))

fun applyToIndex f i = applyToVector f (i)

fun indexSub (i,j) = (Vector.sub (i, j))
  handle General.Subscript => raise PanicNoisily "GameCheck, indexSub"
    
(* find Y, increase its index, zero everything to its right. *)
(* We need a new copy, hence the tabulate call. *)
fun update Y j =
  let val i = j
    fun newEntry k =
      if k < Y then Vector.sub (i, k)
      else if k > Y then 0
	   else Vector.sub (i,Y) + 1
  in Vector.tabulate (noOfVars, newEntry)
  end handle General.Subscript => raise PanicNoisily "GameCheck, update"

(* index -> index -> player -> bool array -> boolean *)
(* compatindex says whether it is safe to reuse a decision for  player b *)
(* which was stored at index old, to avoid exploring from index new *)
fun compatindex new old b safe =
  let fun examine k =
    if k > maxVar then true		(* new and old were identical *)
    else let val newVal = Vector.sub(new,k)
	     val oldVal = Vector.sub(old,k)
	 in if newVal = oldVal then examine (k+1)
	    else if Array.sub(safe,k) then true
		 else if newVal > oldVal then b = max k
		      else not (b = max k)
	 end
      val answer = examine 0
      val _ = debugFn
	(fn _ => ((indexString new)^" "^(indexString old)^" "^(playerString b)^
		  " "^(if answer then " compatible" else " incompatible")))
  in answer
  end handle General.Subscript => raise PanicNoisily "GameCheck, compatindex"

(* If we have a repeat section with indexes from and to, who wins? The owner *)
(* of the leading difference, i.e. eloise iff most sig. var where to > from *)
(* is maximal. *)
fun winsOn from to =
  let val _ = debugFn
    (fn _ => "Comparing "^(indexString from)^" with "^(indexString to))
      fun g k =
	if k > maxVar then raise (PanicNoisily
				  "GameCheck, winsOn")
	else if Vector.sub (to, k) > Vector.sub (from, k) then max k
	     else g (k+1)
  in g 0
  end handle General.Subscript => raise PanicNoisily "GameCheck, winsOn(2)"
      

(***************** Stuff about things we know or assume **********************)
val nodeStore = List.foldr (fn (x,l) => setPropEntry l (x, init()))
   (noPropEntry()) subforms

(***************** Functions for manipulating nodes **************************)
fun getRef (DUMMY i) = i
fun getConfig n = let val i = getRef n
			    val (x,_,_,_,_) = !i
			in x
			end
fun getAgent n = let val i = getRef n
		     val ((x,_),_,_,_,_) = !i
		 in x
		 end
fun getProp n = let val i = getRef n
		     val ((_,x),_,_,_,_) = !i
		 in x
		 end
fun getNextMove n = let val i = getRef n
			val (_,_,_,x,_) = !i
		    in x
		    end
fun getDecisionInfo n = let val i = getRef n
			    val (_,_,x,_,_) = !i
			in x
			end
fun setDecisionInfo (n, d) = let val i = getRef n
				 val (x,y,_,z,a) = !i
			     in i := (x,y,d,z,a)
			     end
fun getSuccessors n = let val i = getRef n
			  val (_,x,_,_,_) = !i
		      in x
		      end
fun setSuccessors (n, l) = let val i = getRef n
			       val (x,_,y,z,a) = !i
			   in i := (x,l,y,z,a)
			   end
			
fun pushNextMove (node, next) =
  let val i = getRef node
    val (x,y,z,w,a) = !i
  in i := (x,y,z,next::w,a)
  end

fun popNextMove node =
  let val i = getRef node
    val (x,y,z,w,a) = !i
  in case w of
    [] => raise PanicNoisily "GameCheck, popNextMove"
  | (h::t) => i := (x,y,z,t,a)
  end
  
fun getOccurrence n = let val i = getRef n
			  val (_,_,_,_,x) = !i
		      in x
		      end

fun setOccurrence (n, info) =
  let val i = getRef n
    val (x,y,z,a,_) = !i
  in i := (x,y,z,a,info)
  end

  
(* Notice that an effect of the way we do this is that it's OK to compare *)
(* nodes using = *)
fun makeNode (agent, rawProp) =
  let
(* Since we now have to store some decision against True and False, may as *)
(* well be correct!! *)
    val (dec,prop) = case real rawProp of
      True => (([], [Safe 0]), rawProp)
    | False => (([Safe 0], []), rawProp)
    | _ => (([], []), variableize rawProp)
    val agentTable = !(getPropEntry nodeStore prop )
  in
    case HashTable.find agentTable agent of
      NONE => let val nodeRef = DUMMY (ref ((agent,prop),NONE, dec, [],NONE))
	      in (AgentHash.insert agentTable (agent, nodeRef); nodeRef)
	      end
    | SOME(x) => x
  end

(*****************************************************************************)
(* given a node, whose turn is it next? *)
fun whoseTurnNext node =
  let (* Given a prop, whose turn is it next? (Silly q in some cases!)*)
    fun wTurnNext True = Player(abelard)
      | wTurnNext False = Player(eloise)
      | wTurnNext (And _) = Player(abelard)
      | wTurnNext (Or _) = Player(eloise)
      | wTurnNext (Nec _) = Player(abelard)
      | wTurnNext (Pos _) = Player(eloise)
      | wTurnNext (Var _) = Referee
      | wTurnNext (Min _) = Referee
      | wTurnNext (Max _) = Referee
  in wTurnNext (real (getProp node))
  end

fun nodesConfigString n = configString (getConfig n)
fun positionString (node, index) =
  nodesConfigString node^"\n"^(indexString index)

fun forgottenString player j = if isValid player j then "" else "FORGOTTEN "
fun decisionItemStringValid p (Safe j) =
    (forgottenString p j)^"Safe "
  | decisionItemStringValid p (Unsafe (j,l)) =
    (forgottenString p j)^"Unsafe:"^(indexString l)
fun decisionStringValid (a, e) =
   "Abelard: \n"^(Lib.mkstr (decisionItemStringValid abelard) " " a)^"\n"^
   "Eloise: \n"^(Lib.mkstr (decisionItemStringValid eloise) " " e)^"\n"

fun infoString node =
  let val config = nodesConfigString node
    fun f [] = ""
      | f (h::t) = (nodesConfigString h)^" "^(f t)
    val next = f (getNextMove node)
    val decisions = decisionStringValid (getDecisionInfo node)
  in
    "\nRecorded config: \n"^config^
    "\nRecorded next move: \n"^next^
    "\nRecorded decision: \n"^decisions
  end


(* From a choice point, return SOME(node to try next, rest) or NONE if there *)
(* are no possible next nodes. *)
(* If there is a move recorded in the strategy, we try that first, because *)
(* it's the most likely to be right (because of our pessimistic reuse).    *)
fun next node =
  let val (ag,prop) = getConfig node
    fun n (And(p,q)) = [makeNode(ag, p),makeNode(ag,q)]
      | n (Or(p,q)) = [makeNode(ag, p),makeNode(ag,q)]
      | n (Nec(m,p)) = map (fn x => makeNode(x,p))
	(relevantSuccessors (m, ag))
      | n (Pos(m,p)) = map (fn x => makeNode(x,p))
	(relevantSuccessors (m, ag))
      | n  _ = raise PanicNoisily "GameCheck, next"
    val allChoices = case getSuccessors node of
      SOME l => l
    | NONE => let val calculated = n (real prop)
	      in (setSuccessors (node, SOME calculated); calculated)
	      end
  in case getNextMove node of
    [] => (case allChoices of 
	[] => NONE 
      | (h::t) => SOME(h,t))
  | (iNode::t) => SOME(iNode, filter (fn j => not (iNode=j)) allChoices)
  end

(* We keep stacks of decisions (and corresponding next moves). Ones other *)
(* than the head are never needed, but may become the head later. *)
(* In fact, there are circumstances where we can discard some decisions, *)
(* saving space -- think about this more, Perdita. *)
val (addKnowledge, getKnowledge) =
  if nonAlternating then
(* There's no alternation in the formula, so we don't need to store indexes *)
    let fun addKnowledge ((position as (node : node, index : index)), b, m) =
      let val _ = (debugFn
	    (fn _ => ("Adding simple decision for "^(playerString b)^
		      " at "^
		      (positionString position))))
	val (oldAbD, oldElD) = getDecisionInfo node
	val d = if b then (oldAbD, (Safe(!pCount))::oldElD)
		else ((Safe(!oCount))::oldAbD, oldElD)
	val _ = case m of NONE => () | (SOME next) => pushNextMove (node, next)
      in setDecisionInfo (node, d)
      end
(* call lookAtEloise only if there is no extant abelard decision. *)
	fun lookAtEloise (node, [], w) = NONE
	  | lookAtEloise (node, ((Safe j)::t), w) =
	    if isValid eloise j then SOME(eloise)
	    else (setDecisionInfo (node, ([], t));
		  (if w = Player(eloise) then popNextMove(node) else ());
		     lookAtEloise (node, t, w))
	  | lookAtEloise (node, ((Unsafe _)::t), w) =
	    raise PanicNoisily "GameCheck, lookAtEloise (safe)"
	fun lookAtAbelard (node, ([],d), w) = lookAtEloise (node, d, w)
	  | lookAtAbelard (node, (((Safe j)::t), d), w) =
	    if isValid abelard j then SOME(abelard)
	    else (setDecisionInfo (node, (t, d));
		  (if w = Player(abelard) then popNextMove(node) else ());
		  lookAtAbelard (node, (t, d), w))
	  | lookAtAbelard (node, (((Unsafe _)::t),d), w) =
	    raise PanicNoisily "GameCheck, lookAtAbelard (safe)"
	fun getKnowledge (node, index) =
	  lookAtAbelard (node, getDecisionInfo node, whoseTurnNext node)
    in (addKnowledge, getKnowledge)
    end
else
  let
(* Return an array to say for each variable whether, if we have indexes *)
(* whose leading difference is that variable, it's always safe to reuse *)
(* a decision for player there -- i.e. there is no "real alternation". *)
    fun safetyInfo phi player =
      let val other = other player
	val active = getActiveVars phi
(* If k is not active in phi, a leading difference of k is safe *)
	val safe = Array.tabulate (noOfVars,
				   (fn k => not(Array.sub (active, k))))
(* If there is no variable less significant than k and belonging to the *)
(* other player which is active in phi, leading diff at k is safe *)
	fun noOppVar k =
	  let fun g i =
	    if i > maxVar then true (* we got to end without finding problem *)
	    else if (max i = other) andalso (Array.sub (active, i)) then false
		 else g (i+1)	(* i wasn't a problem, keep looking *)
	  in g k  (* vars more significant than leading diff don't matter *)
	  end
	fun f (k,_) = if (noOppVar k) then Array.update (safe, k, true)
		      else ()
	val _ = applyToArray f safe	(* now safe is correct *)
	val alwaysSafe = not(arrayExists (fn (_,x) => not x) safe)
	val _ = debugFn (fn _ =>
("Safety information for "^L.printString phi^" and "^(playerString player)^
 "\nAlways safe: "^
 (Bool.toString alwaysSafe)^" Safety array: "^(arrayString Bool.toString safe)))
      in (alwaysSafe, safe)
      end
    fun init x = (safetyInfo x abelard,safetyInfo x eloise)
    val safetyKnowledge = List.foldr (fn (x,l) => setPropEntry l (x, init x))
      (noPropEntry()) subforms 
    fun getSafetyInfo node = getPropEntry safetyKnowledge (getProp node) 
    fun oValid (i,_) = isValid abelard i
    fun pValid (i,_) = isValid eloise i
    fun addKnowledge ((position as (node, index)), b, m) =
      let val _ = debugFn
	(fn _ => ("Adding decision for "^(playerString b)^" at "^
		  (positionString position)))
	  val selector = fn arghValueRestriction =>
	    pairMember b arghValueRestriction
	  val (safeForB,_) = selector (getSafetyInfo node)
	  val (abDec, elDec) = getDecisionInfo node
	  val count = selector counts
	  val newBDecisionInfo = if safeForB then Safe (!count)
				 else Unsafe (!count, index)
	  val newDecisionInfo = if b then (abDec, newBDecisionInfo::elDec)
				else ((newBDecisionInfo::abDec), elDec)
	  val _ = case m of
	    NONE => ()
	  | (SOME next) => pushNextMove (node, next)
      in setDecisionInfo (node, newDecisionInfo)
      end
    fun canUse (node, index) i player =
      let val (always, safe) = pairMember player (getSafetyInfo node)
      in always orelse (compatindex index i player safe)
      end
(* Answer two questions: does this decision apply here, and do we need to *)
(* forget it? Return boolean (use it) * new decisions. *)
(* p is the player we want a decision for, w is the chooser at this node. *)
    fun lookAt (position as (node, index)) p w [] = (false, [])
      | lookAt (position as (node, index)) p w (d as ((Safe j)::t)) =
	if isValid p j then (true, d)
	else ((if w = Player(p) then popNextMove(node) else ());
	      lookAt position p w t)
      | lookAt (position as (node, index)) p w (d as ((Unsafe (j,i))::t)) =
	if isValid p j then
	  if canUse position i p then (true, d)
	  else (false, d)
	(* if we can't use this, then for sure we can't use anything earlier*)
	else ((if w = Player(p) then popNextMove(node) else ());
	      lookAt position p w t)

    fun getKnowledge (position as (node, index)) =
      let val decs as (abDec, elDec) = getDecisionInfo node
	val chooser = whoseTurnNext node
	val (canUseAb, newAbDec) = lookAt position abelard chooser abDec
	val (answer, newDecs) =
	  if canUseAb then (SOME(abelard), (newAbDec, elDec))
	  else
	    let val (canUseEl, newElDec) = lookAt position eloise chooser elDec
	    in (if canUseEl then SOME(eloise) else NONE, (newAbDec, newElDec))
	    end
      in (if decs = newDecs then () else setDecisionInfo (node, newDecs);
	    answer)
      end
  in (addKnowledge, getKnowledge)
  end

(* Return player option to say whether one or other player wins by repeat. *)
fun getWinsByRepeat (position as (node, index)) =
  case getOccurrence node of
    NONE => NONE
  | SOME (i, c, (aUse, eUse)) =>
      let val winner = winsOn i index
	  val select = pairMember winner
	  val use = select (aUse, eUse)
	  val _ =  use := true
      in SOME(winner)
      end
	
(* we're backtracking for winner: if anything used assumptions *)
(* about the other player, we should mark anything that might have done so   *)
(* invalid. *)
(* index only passed for sanity checking *)
fun backtrackingThrough ((node, index), winner) =
  let val (i,c,use) = case getOccurrence node of
(* If we're backtracking through it we played through it earlier! *)
      NONE => raise PanicNoisily "GameCheck, backtrackingThrough (empty)"
    | (SOME h) => h
      val _ = if i = index then () else
	raise PanicNoisily "GameCheck, backtrackingThrough2"
      val _ = setOccurrence (node, NONE) (* this occ no longer above us *)
    fun maybeInvalidate p u =
      if !u then invalidate (c, p) else ()
    val loser = other winner
  in maybeInvalidate loser (pairMember loser use)
  end

fun addOccurrence (position as (node, index)) =
(* remember oCount = pCount *)
  setOccurrence (node, SOME (index, (!oCount), (ref false, ref false)))
  
fun inform b gameList reason =
  debugFn (fn _ => 
	   "Checking for "^(playerString b)^
	   " on gamelist of length "^
	   (Int.toString (length gameList))^
	   " because "^reason)

(* Could make use of the nextMove slot to store this: good or bad?? *)
fun unwind (node, index) =
  let val (agent, prop) = getConfig node
    val X = case real prop of
      Var X => X
    | _ => raise PanicNoisily "GameCheck, unwind"
  in (makeNode(agent, (body X)), (update X index))
  end

datatype interactive = Yes | No
(************************** Playing *****************************************)
(* Order of checking for decision and occurrence: it's easy but tedious to  *)
(* show that if you have a decision for A and elsewhere a repeat of the     *)
(* same configuration, then if the decision is applicable at the bottom and *)
(* not at the top of the repeat (i.e. there is both an applicable decision  *)
(* and an occurrence at the bottom) then A wins on that repeat. That is, we *)
(* may safely check for the decision first: if it's there it gives the same *)
(* answer as we would get from using the occurrence. Phew!                  *)
fun win interacting fns (position as (node, index)) glist =
  let val (getKnowledge, next, nextRef, print, inform) = fns
    val _ = inc counter
    val _ = inc oCount		(* = pCount *)
    val _ = print (node, (!counter))
    val (backtrack, keepPlaying) = (check interacting fns, win interacting fns)
  in case getKnowledge position of
    SOME(winner) => backtrack winner glist node
  | NONE => 
(* Is this a repeat? If so, see who wins on it, record that we're making *)
(* this assumption, and backtrack for that winner. Otherwise just record *)
(* that we've seen this config, and keep playing. *)
      (case  getWinsByRepeat (node, index) of
	 SOME(winner) =>
	   (inform (winner, "of a repeat");
	    backtrack winner glist node)
       | NONE =>
	   (debugFn (fn _ =>
		     ((Int.toString (!counter))^
		      " Exploring "^
		      (positionString position)));
	    (case whoseTurnNext node of
	       Referee => (addOccurrence position;
			   nextRef();
			   keepPlaying
			   (unwind (node, index))
			   ((position,[])::glist))
	     | (Player chooser) =>
		 (case next node of
		    NONE =>
(* the player whose turn it is has no moves, so the other player wins. *)
		      let val winner = other chooser
		      in (inform (winner, "there are no moves for loser");
			  backtrack winner glist node)
		      end
(* explore some option *)
		  | SOME(h,t) =>
		      (addOccurrence position;
		       keepPlaying (h, index)
		       ((position, t)::glist))))))
  end


(* check Someone gamelist assumes that Someone has just won a game whose *)
(* ghost is recorded in gamelist, and checks whether this win extends to *)
(* a winning strategy: i.e. could Someone have coped with all the choices *)
(* the other player could have made? Someone's win may depend on assumptions*)
(* which will get discharged or invalidated as we go  *)
(* The node whereWeCameFrom allows us to update the strategy once we know *)
(* which move was successful, as we do here (provisionally). *)
and check No fns winner gameList whereWeCameFrom =
  let
    val _ = debugFn (fn _ => "Check with: "^(playerString winner))
    val play = win No fns
(* The things we must do whenever we decide it's OK to keep backtracking: *)
    fun keepBacktracking (position as (node, index), maybeMove, glist) =
      (backtrackingThrough ((node, index), winner);
       (* invalidate ass. if nec. etc. *)
       addKnowledge (position, winner, maybeMove);
     (* record the decision *)
     chk glist node)			(* keep going *)
    
    and chk [] whence = winner 
      | chk (((position as (node, index)), unexplored)::glist) whence =
	case whoseTurnNext node of
	  Referee => keepBacktracking (position, NONE, glist)
	| (Player chooser) => 
	    if winner = chooser then
(* the choice was made by the player who eventually won the game, so no need *)
(* to examine alternative choices *)
	      keepBacktracking (position, (SOME whence), glist)
	    else
(* could the other have chosen differently? *)
	      (case unexplored of
		 [] => keepBacktracking (position, NONE, glist)
	       | (n::l) =>
		   (debugFn (fn _ =>
			     ("Branching at "^(positionString position)));
		    play (n, index) ((position, l)::glist)))
  in chk gameList whereWeCameFrom
  end
(* Version to use when we're playing interactively: *)
(* backtrack simply to remove occurrences, in case we play again. *)
  | check Yes fns winner gameList whereWeCameFrom =
    let fun chk [] = true
	  | chk (((position as (node, index)), unexplored)::glist) =
	    (backtrackingThrough ((node, index), winner);
	     chk glist)
    in chk gameList
    end
  
fun showSize _ = UI.chat
  ("Total number of nodes visited (counting repetitions) "^
   (Int.toString (!counter)))

val winner = (UI.chat ("There are "^(Int.toString (length subforms))^
			" relevant subformulae.\nPlaying...");
	      (win No (getKnowledge, next,
		       noOp, noOp,	(* no printing *)
		       (fn (r,reason) => UI.debugFn (fn _ => "Got "^
						     (playerString r)^
						     " because "^reason)))
	       (makeNode(topLevelAgent, topLevelFormula),initindex) []))

  handle Interrupt => (showSize();
		       raise Interrupt)
val _ = showSize()    
  
val (winnerString, loserString) = (playerString winner,
				   playerString (not winner))
val _ = UI.print (Bool.toString winner)

fun interact winner =
  let
    fun getKnowledgeI (node, index) =
      case real (getProp node) of
	True => SOME(eloise)
      | False => SOME(abelard)
      | _ => NONE
    fun nextRef _ =
      (UI.message "The referee unwinds the fixpoint.";
       UI.hitReturnToContinue())
    fun nextI node =
      let val mover = whoseTurnNext node
      in case mover of
	Referee =>
	  (UI.message "The referee unwinds the fixpoint.";
	   UI.hitReturnToContinue();
	   next node)
      | Player p =>
	  if p = winner then
	    (UI.message ("CWB's turn (playing "^(playerString winner)^")");
	     UI.hitReturnToContinue();
	     next node)
	  else (UI.message ("Your turn (playing "^
			    (playerString (other winner))^")");
		case getSuccessors node of
		  NONE => raise PanicNoisily "GameCheck, interact"
		| SOME [] => NONE
		| SOME l => let val (befor, chosen, after) =
		    UI.pickFromListC (fn _ => false) "Which move? "
		    (fn x => "\n"^(nodesConfigString x)^"\n")
		    l
			    in SOME(chosen,befor@after)
			    end)
      end
    fun printI (node,c) =
      UI.message ((Int.toString c)^": Current position:\n"^
		  nodesConfigString node)
    fun informI (wonHere, reason) =
      if winner = wonHere then
	UI.message ("The CWB (playing "^(playerString winner)^
		    ") won, because "^reason)
      else raise PanicNoisily ("GameCheck, informI2: CWB lost!")
      
    val willPlay = if definitelyPlay then ref true else
      if UI.userHatesGames() then ref false else
	ref (UI.yOrN false
	     "Would you like to play (and lose!) a game against the CWB?")
  in while (!willPlay) do
    (UI.message ("The CWB will choose "^winnerString^
		 "'s moves.\nYou can choose "^loserString^"'s.");
     counter := 0;
     (win Yes (getKnowledgeI, nextI, nextRef, printI, informI)
      (makeNode(topLevelAgent, topLevelFormula),initindex) []);
     willPlay := UI.yOrN false "Another game?")
  end

val _ = if UI.interactive() then interact(winner) else ()
  
in
  winner
end

end