% -*- mode: Noweb; noweb-code-mode: sml-mode -*-

% l2h substitution lrtl \-RTL
% l2h macro module 1 <a href="#$1.html"><tt>#1.nw</tt></a>

\chapter{Recognizing RTLs with conditions}

\label{crecrtl-module}

This chapter implements the abstract RTL interface such that an
attribute is almost a recognizer for instructions.
The ``almost'' comes in because the actual recognizer for an
instruction depends on the recognizers for its operands, so what we
really have is a function that, given recognizers for operands,
produces recognizers for instructions.
@

\section{Introduction}

This implementation is currently incomplete, but here are the
interesting elements.
\begin{itemize}
\item
I represent a recognizer using types from the [[RtlPattern]] module.
This module is designed to be easy to compile into recognizers for
RTLs; we'll see if it actually works.
\item
Aside from transforming goo from one form to another, the primary job
of this module so far is to deal correctly with [[if]] as applied to
expressions and locations.
To help, I have resurrected the ancient [[Guard]] module from an old,
untyped version of the \lrtl\ translator.
\item
The big piece that's missing is the binding-time analysis that would
make it possible to distinguish compile-time guards from run-time
guards.
It's not clear whether this should be here or should be a
transformation on the [[RtlPattern]] stuff.
If I expect to unify this code with the creation code, keeping the
binding-time stuff here would be a good plan.
\end{itemize}
@
\section{Guard expressions}
I make patterns into expressions for purposes of computing guards.
I go to some effort to make negation fairly sophisticated; see the
\module{guard} module for the requirements of the interface.
This code should probably migrate to central ``RTL pattern
utilities,'' for which the most sensible place might be \module{patrew}.

To improve a performance bottleneck with conjoining a list,
I need a set to collect expressions.
Theoretically, this code should be with the RTL pattern utilities as well,
but that causes a circular dependency between the modules.
<<patguardexp.sml>>=
structure ExpSet = RtlPattern.ExpSet
structure PatternGuardExp : GUARD_EXP = struct
  structure P = RtlPattern
  type exp = P.exp

  val true'  = P.BOOL true
  val false' = P.BOOL false

  fun negate (P.BOOL b) = P.BOOL (not b)
    | negate (P.APP (("not", []), [e])) = e
    | negate (P.APP (("conjoin", []), l)) = P.APP (("disjoin", []), map negate l) 
    | negate (P.APP (("disjoin", []), l)) = P.APP (("conjoin", []), map negate l) 
    | negate (P.APP (("eq", ws), es)) = P.APP (("ne", ws), es)
    | negate (P.APP (("ne", ws), es)) = P.APP (("eq", ws), es)
    | negate (P.APP (("lt", ws), es)) = P.APP (("ge", ws), es)
    | negate (P.APP (("ge", ws), es)) = P.APP (("lt", ws), es)
    | negate (P.APP (("gt", ws), es)) = P.APP (("le", ws), es)
    | negate (P.APP (("le", ws), es)) = P.APP (("gt", ws), es)
    | negate e = P.APP (("not", []), [e])

  fun isTrue (P.BOOL b) = b
    | isTrue (P.APP (("not", []), [e])) = isFalse e
    | isTrue (P.APP (("conjoin", []), l)) = List.all    isTrue l
    | isTrue (P.APP (("disjoin", []), l)) = List.exists isTrue l
    | isTrue e = false
  and isFalse (P.BOOL b) = not b
    | isFalse (P.APP (("not", []), [e])) = isTrue e
    | isFalse (P.APP (("conjoin", []), l)) = List.exists isFalse l
    | isFalse (P.APP (("disjoin", []), l)) = List.all    isFalse l
    | isFalse e = false
    
  fun existsConjunction f (P.APP (("conjoin", []), l)) =
        List.exists (existsConjunction f) l
    | existsConjunction f e = f e

  fun filterConjunction conjoin f (P.APP (("conjoin", []), l)) =
        foldl conjoin true' (map (filterConjunction conjoin f) l)
    | filterConjunction conjoin f c = if f c then c else true'

  fun equalityIsContradicted (P.APP (("eq", _), [l , P.INT (n, w)]), q) =
        let fun ne n n' = IntInf.compare (n, n') <> EQUAL
            fun contradicts (P.APP (("eq", _), [l' , P.INT (n', w')])) =
                  w = w' andalso ne n n' andalso l = l'
              | contradicts _ = false
        in  existsConjunction contradicts q
        end
    | equalityIsContradicted _ = false

  fun simpleConjoin (p, q) = P.APP (("conjoin", []), [p, q])

  fun foldrConjunction f (e, answer) =
    case e
      of P.APP (("conjoin", []), l) => foldr (foldrConjunction f) answer l
       | e => f (e, answer)

  fun conjoinWithoutDuplicates (p, q) =
    foldrConjunction (fn (p, q) =>
                      if existsConjunction (fn q => q = p) q then q
                      else simpleConjoin (p, q))
    (p, q)

  (* this could probably all be tidied up very simply using relop stuff *)
  fun withConstantEquality p (l, n, w) q =
    let fun ne n n' = IntInf.compare (n, n') <> EQUAL
        fun eq n n' = IntInf.compare (n, n') =  EQUAL
        fun contradicts (P.APP (("eq", _), [l' , P.INT (n', w')])) =
              w = w' andalso ne n n' andalso l = l'
          | contradicts (P.APP (("ne", _), [l' , P.INT (n', w')])) =
              w = w' andalso eq n n' andalso l = l'
          | contradicts _ = false
        fun isImplied (P.APP (("ne", _), [l' , P.INT (n', w')])) =
              w = w' andalso l = l' andalso ne n n'
          | isImplied _ = false (* could do lt, gt, ge, le, etc, but no need yet *)
    in  if existsConjunction contradicts q then false'
        else simpleConjoin (p, filterConjunction conjoin (not o isImplied) q)
    end

  and conjoin (p, q) = 
    if isTrue p then q else if isTrue q then p
    else if isFalse p then p else if isFalse q then q
    else conjoinWithoutDuplicates (p, q)

  and conjoinLst [] = raise Empty
    | conjoinLst (es as e::_) =
        case List.find isFalse es of
            SOME e => e
          | NONE   =>
             (case List.filter (not o isTrue) es of
                  [] => e
                | es =>
                   let val conjunctSet =
                         foldl (foldrConjunction ExpSet.add') ExpSet.empty es
                   in  case ExpSet.listItems conjunctSet of
                           [c] => c
                         | cs  => P.APP (("conjoin", []), cs)
                   end)
end
@ 
I expose more than just the abstract RTL interface: also the guard
module and the [[recognizer]] type.
The [[debug]] function works around what would otherwise be a circular
dependency with [[RtlPattern]].
<<crecrtl.sig>>=
signature PATTERN_RTL = sig
  include ABSTRACT_RTL
  structure G  : GUARD where type Exp.exp = RtlPattern.exp
  <<recognizer type>>
  val debug : (recognizer -> PP.pretty) ref
  val splitBindings : 
    RtlPattern.exp * RtlPattern.rtl -> 
    RtlPattern.exp * RtlPattern.rtl * (string * RtlPattern.const * int option -> RtlPattern.exp)
      (* result should be an (int option -> RtlPattern.exp) StringMap.map? *)
end
@ 
Most of the recognizer is actually [[RtlPattern]]; here we just keep
track of which \emph{kind} of recognizer we have at any moment.
With expressions and locations, we have guards (grab explanation from
previous version---try Nov 1 2000).
With effects, we have converted some guards to creation-time
conditions.
The [[OPERAND]] variant keeps a pair: a name for this particular variable and the name
of the operand it stands for.
We need both because we may end up using different operand types for the different
fields in a structure operand.
<<recognizer type>>=
datatype recognizer
  = EFFECT  of (RtlPattern.exp * RtlPattern.rtl) list
  | EXP     of RtlPattern.exp G.with_guards
  | LOC     of RtlPattern.loc G.with_guards
  | TUPLE   of recognizer list
  | RECORD  of (string * recognizer) list
  | VECTOR  of recognizer list
  | OPERAND of (string * string)
@ 
The rest of the implementation is straightforward; the only tricky bit
is the [[attribute]] type, which enables us to inherit the attributes
of the operands in order to compute the attributes of an instance.
<<crecrtl.sml>>=

structure RtlRecognizer : PATTERN_RTL = struct
  structure P = RtlPattern
  structure PU = RtlPatternUtils
  structure G = GuardFun(PatternGuardExp)
  structure R = RtlOperators.Agg
  structure VI = VarInfo

  <<recognizer type>>

  type 'a recog = (string -> recognizer) -> 'a G.with_guards 

  type attribute = (string -> recognizer) -> recognizer

  type effect   = P.effect recog
  type loc      = P.loc recog
  type exp      = P.exp recog
  type cell     = (char * P.exp) recog
  type operator = P.operator

  type width = int

  type agg = width -> width -> cell -> loc

  exception Failure of string

  <<helpers>>
  <<operators>>
  <<expressions>>
  <<locations>>
  <<cells>>
  <<effects>>
  <<attributes>>
  <<binding split>>
end
@
These helper functions are intended to make the monad operations a
little more readable.
<<helpers>>=
fun gcase     x f = G.map f x
fun gcasepair p f = gcase (G.crossPair p) f
@ 
An operator is just a pair of name and widths.
<<operators>>=
fun rtlop name ws = (name, ws)
@
The \emph{raison d'\^etre} of this implementation is to exploit the
guard module to handle conditions.
<<expressions>>=
fun ifExp (c, t, f) rho = G.ifMap (c rho, t rho, f rho)

fun t rho = G.single G.Exp.true'
fun f rho = G.single G.Exp.false'
@ 
The other stuff requires suitable unit and map operations on the
guards monad.
<<expressions>>=
fun int w n rho = G.single (P.INT (n, w))

fun prLoc (P.LOCVAR s) = print ("Locvar: " ^ s)
  | prLoc (P.NAMEDLOCVAR (s,_)) = print ("NamedLocvar: " ^ s)
  | prLoc (P.UNSLICED (agg, w, w2, c, e)) =
     (print (Char.toString c ^ "["); prExp e; print "]")
  | prLoc (P.SLICED {width, argwidth, lsbwidth, lsb, arg}) =
     (print "Sliced (";
      prLoc arg;
      print ", ";
      prExp lsb;
      print ")\n")
and prExp (P.INT (i,w)) = print (IntInf.toString i)
  | prExp (P.BOOL b) = print (if b then "true" else "false")
  | prExp (P.FETCH (l,w)) = prLoc l
  | prExp (P.APP (oper,es)) =
      (print "("; print (#1 oper);
       app (fn e => (print " "; prExp e)) es;
       print ")")
  | prExp (P.EXPVAR (s,_,w)) = print s
  | prExp (P.IVAR s) = print ("I" ^ s)
  | prExp (P.NAMEDIVAR (s,t)) = print ("NI" ^ s ^ ":" ^ t)
fun fetch w l rho = gcase (l rho) (fn l => P.FETCH(l, w))

fun app (rator, args) rho = 
  let val aa = (applyall rho args)
      val cp = (G.crossProduct aa)
  in  gcase cp (fn args => RtlPatternRewrite.apply (rator, args)) 
  end
@ Helper [[applyall]] deals with the attribute inheritance.
<<helpers>>=
fun applyall x l = List.map (fn f => f x) l
@
There's a problem here with [[loc]]; without being able to look up a
cell, I don't know what sizes to pass to the identity aggregation.
<<locations>>=
val ifLoc = ifExp (* polymorphic *)

fun agg a n w cell rho = 
  G.map (fn (space, addr) => P.UNSLICED (a, n, w, space, addr)) (cell rho)
fun bigE x    = agg (R.USER "B") x
fun littleE x = agg (R.USER "L") x
fun loc x     = agg R.ID 99 99 x
fun sliceLoc {width=w, argwidth=aw, lsbwidth=lw} {lsb, arg} rho = 
  gcasepair (lsb rho, arg rho)
    (fn (lsb, arg) =>
           P.SLICED {width=w, argwidth=aw, lsbwidth=lw, lsb=lsb, arg=arg})
@
Nothing unusual here.
<<cells>>=
fun cell (c, e) rho = gcase (e rho) (fn e => (c, e))
@
Again, I exploit the [[Guard]] module.
I don't implement sequential composition; this module should be
wrapped in ``sequential to parallel'' if necessary.
<<effects>>=
fun guard (g, rtl) rho = G.metaGuard (g rho, rtl rho)

fun seq (ef1, ef2) = Impossible.unimp "sequential composition" 

fun par (ef1, ef2) rho = ef1 rho @ ef2 rho

fun store w (l, e) rho = gcasepair (l rho, e rho) (fn (l, e) => P.STORE (l, e, w))
fun kill l rho = gcase (l rho) P.KILL
fun skip rho = []
@
To compute attributes, we need to split guards.
The idea is that we split a guard into 

Attribute mapping is straightforward.
<<attributes>>=
val debug : (recognizer -> PP.pretty) ref =
  ref (fn _ => PP.TEXT "attribute debugger not installed")

fun rtl e : (RtlPattern.exp * RtlPattern.rtl) list = 
  let fun earlyGuard (_, SOME e) = SOME e
        | earlyGuard ({guard, value}, NONE) = findEarly guard
      val early = foldl earlyGuard NONE e
      fun cvt e = P.RTL (map (fn {guard, value} => (guard, value)) e)
      fun refineGuards g = G.dropFalse (map (refineGuard g) e)
  in  case early
        of NONE => [(G.Exp.true', cvt (G.dropFalse e))]
         | SOME early =>
             let fun given e = 
                   let fun addto (g, rtl) =
                         if impliedBy (e, g) then (g, rtl)
                         else if contradictedBy (e, g) then (G.Exp.false', rtl)
                                   (* not sure if this case is needed *)
                         else (G.Exp.conjoin (e, g), rtl)
                   in  map addto (rtl (refineGuards e))
                   end
             in  given early @ given (G.Exp.negate early)
             end
  end

structure Attribute = struct
  fun fromEffect e rho = EFFECT (rtl (e rho)) 
      (*  val _ = List.app print ["computed effect = ", PP.flatten (!debug a), "\n"]*)

  fun unEffect (EFFECT l) = 
        let fun unRtl (g, P.RTL l) =
              let val effects = map (fn (g, v) => {guard=g, value=v}) l
              in  G.dropFalse (G.guard (g, effects))
              end
        in  List.concat (map unRtl l)
        end
    | unEffect _ = Impossible.impossible "non-effect"
  fun toEffect a rho = unEffect (a rho)

  fun fromExp (e : exp) = (fn rho => EXP (e rho)) : attribute
  fun unExp (EXP e)         = e
    | unExp (OPERAND (n,t)) = G.single (P.NAMEDIVAR (n,t))
    | unExp a               = (*Impossible.impossible "non-exp"*)
       G.single (P.expvar ("this can't happen (non-exp " ^
                           PP.flatten (!debug a) ^ ")", P.BITS, NONE))
  fun toExp a rho = unExp (a rho)

  fun fromLoc (e : loc) = (fn rho => LOC (e rho)) : attribute
  fun unLoc (LOC l)         = l
    | unLoc (OPERAND (n,t)) = G.single (P.NAMEDLOCVAR (n,t))
    | unLoc _               = Impossible.impossible "non-loc"
  fun toLoc a rho = unLoc (a rho)
end
<<attributes>>=
fun tuple l rho = TUPLE (map (fn x => x rho) l)
fun tupleSelect k a rho =
  case a rho
    of TUPLE l => 
         (List.nth (l, k-1) handle Subscript =>
             Impossible.impossible ("subscript " ^ Int.toString k ^ " out of bounds " ^
                                    "on tuple of size " ^ Int.toString (length l)))
     | a => Impossible.impossible "Cannot tupleSelect from non-tuple"
     (*| a => a (* bogus *)*)
<<attributes>>=
fun record l rho = RECORD (map (fn (n, x) => (n, x rho)) l)
fun recordSelect n a rho =
  case a rho
    of RECORD l => 
         (case List.find (fn (n', x) => n = n') l
            of SOME (_, x) => x
             | NONE => Impossible.impossible "Record-type mismatch")
     | OPERAND (s,t) =>
         (* Perhaps there should be some sanity checking here -- the operand should be
            a record *)
         OPERAND (s, t ^ "_" ^ n)
     | a => Impossible.impossible "Cannot recordSelect from non-record"
     (*| a => a (* bogus *)*)
<<attributes>>=
fun vector l rho = VECTOR (map (fn x => x rho) l)
fun sub (v, i) rho = Impossible.unimp "vector subscript for recognizers"
@ 
We have to call [[rho v]] for the [[VI.INT]] case in order to make
proper use of the [[intpact]] part of the RTL-property signature.
<<attributes>>=
fun var (VI.INT {early}) v rho = rho v (*formerly EXP (G.single (P.EXPVAR v))*)
  | var (VI.LOC)         v rho = LOC (G.single (P.LOCVAR v))
  | var (VI.ATT s)       v rho = rho s
@ 
Dealing with the binding-time split is a bear.
Here's the general idea:
\begin{itemize}
\item
We get an RTL.
It's full of guards.
Each guard is a list of conjuncts.
Supposing we can evaluate one of the conjuncts at creation time, what has
to be true?
\item
We get a brand new RTL.
To each effect of the original RTL, one of three things happens:
\begin{itemize}
\item
The value of its guard is independent of the value of the original
conjunct.
The effect appears as is.
\item
The guard contains the original conjunct.
We keep the effect, but we simplify the guard by dropping the known
conjunct.
\item
The guard contains the negation of the original conjunct.
We drop the effect.
\end{itemize}
\end{itemize}
To deal with all this, we accumulate conjunct pairs.
@
A basic utility just visits every conjunct in a conjunction.
<<helpers>>=
fun foldConjunction f (e, answer) =
  case e
    of P.APP (("conjoin", []), l) => foldl (foldConjunction f) answer l
     | e => f (e, answer)
@
A conjunct is interesting only if it can be evaluated early.\footnote
{Things get worse.  If we have an early conjunct we can't express in
the source language, we've got big troubles.}
The [[extendOk]] is a flagrantly expedient hack.
The problem it solves is this: we will cheerfully do early
computations on immediate operands, e.g., to check condition codes.
This is almost certainly not what is wanted, but it's unclear what we
do want.
The right move is probably to accept only early guards that we know
how to deal with, e.g., simple equality and inequality.
But this hack may do for now.
<<helpers>>=
fun early extendOk (P.INT _) = true
  | early extendOk (P.BOOL _) = true
  | early extendOk (P.FETCH _) = false
  | early extendOk (P.APP (("sx", _), args)) =
      extendOk andalso List.all (early extendOk) args
  | early extendOk (P.APP (("zx", _), args)) =
      extendOk andalso List.all (early extendOk) args
  | early extendOk (P.APP (_, args)) = List.all (early extendOk) args
  | early extendOk (P.EXPVAR _) = true
  | early _ (P.IVAR _) = false (*Impossible.impossible "instance var in recognizer"*)
  | early _ (P.NAMEDIVAR _) = false 
fun hasfreevar (P.INT _) = false
  | hasfreevar (P.BOOL _) = false
  | hasfreevar (P.FETCH _) =
      Impossible.impossible "asked for free var of non-early guard"
  | hasfreevar (P.APP (_, args)) = List.exists hasfreevar args
  | hasfreevar (P.EXPVAR _) = true
  | hasfreevar (P.IVAR _) = false (*Impossible.impossible "instance var in recognizer"*)
  | hasfreevar (P.NAMEDIVAR _) = false
@
Here's where we accumulate early conjunct pairs.
<<helpers>>=
val early = early true (* was false *)
fun findEarly e =
  foldConjunction
    (fn (_, SOME early) => SOME early
      | (e, NONE) => if early e andalso hasfreevar e then SOME e else NONE)
    (e, NONE)
@
<<helpers>>=
fun relop cmp (n, n') = IntInf.compare (n, n') = cmp

fun interpret "eq" _ = P.BOOL o       relop EQUAL
  | interpret "ne" _ = P.BOOL o not o relop EQUAL
  | interpret "lt" _ = P.BOOL o       relop LESS
  | interpret "le" _ = P.BOOL o not o relop GREATER
  | interpret "gt" _ = P.BOOL o       relop GREATER
  | interpret "ge" _ = P.BOOL o not o relop LESS
  | interpret _    q = fn _ => q

fun mapConjuncts f q =
  foldConjunction (fn (e, answer) => G.Exp.conjoin (f e, answer)) (q, G.Exp.true')

fun refine (p as P.APP (("eq", _), [l, P.INT(n, w)])) =
      let fun subst (q as P.APP ((rator, _), [l', P.INT(n', w')])) =
                if w' = w andalso l' = l then
                  interpret rator q (n, n')
                else 
                  q
            | subst q = q  (* could still substitute in here *)
      in  mapConjuncts subst
      end
  | refine p =
      let val notp = G.Exp.negate p
          fun subst q = if p = q then G.Exp.true'
                        else if notp = q then G.Exp.false'
                        else q
      in  mapConjuncts subst
      end

fun refine (p as P.APP (("eq", _), [l, x as P.INT(n, w)])) =
      let fun subst (q as P.APP (rator, [l', y])) =
                if l' = l then RtlPatternRewrite.apply (rator, [x, y])
                else q
            | subst q = q  (* could still substitute in here *)
      in  mapConjuncts subst
      end
  | refine p =
      let val notp = G.Exp.negate p
          fun subst q = if p = q then G.Exp.true'
                        else if notp = q then G.Exp.false'
                        else q
      in  mapConjuncts subst
      end

fun refineGuard p {guard=g, value=v} = {guard=refine p g : G.Exp.exp, value=v}

<<helpers>>=
  fun existsConjunction f (P.APP (("conjoin", []), l)) =
        List.exists (existsConjunction f) l
    | existsConjunction f e = f e

fun impliedBy (P.APP (("ne", _), [l, P.INT (n, w)]), conj) =
      let fun implies (P.APP (("eq", _), [l', P.INT (n', w')])) =
                w' = w andalso l' = l andalso IntInf.compare (n, n') <> EQUAL
            | implies _ = false
      in  existsConjunction implies conj
      end
  | impliedBy _ = false            

fun contradictedBy (P.APP (("ne", _), [l, P.INT (n, w)]), conj) =
      let fun implies (P.APP (("eq", _), [l', P.INT (n', w')])) =
                w' = w andalso l' = l andalso IntInf.compare (n, n') = EQUAL
            | implies _ = false
      in  existsConjunction implies conj
      end
  | contradictedBy _ = false            
@ 
Before splitting RTLs, we replace operands that are only extended.
This allows us to recognize the correct operands provided they fit in
the right spots.
<<binding split>>=
fun expString e = PP.flatten (!debug (EXP (G.single e)))
<<satisfaction>>
fun splitBindings (guard, rtl) =
  rewriteExtensions (guard, rtl)

and rewriteExtensions (guard, rtl) =
  let val m = childMap (guard, rtl)
      fun addCondition (v, (_,    TOP), guard) = guard
        | addCondition (v, (NONE, _), guard)   =
             Impossible.impossible "rewriteExtensions: NONE should only appear with TOP"
        | addCondition (v, (SOME c, SX (n, w)), guard) =
            G.Exp.conjoin (guard, P.APP (("fits signed",   [n, w]), [P.EXPVAR (v, c, w)]))
        | addCondition (v, (SOME c, ZX (n, w)), guard) =
            G.Exp.conjoin (guard, P.APP (("fits unsigned", [n, w]), [P.EXPVAR (v, c, w)]))
      fun remove v = case StringMap.find (m, v)
                       of SOME (_, TOP) => false
                        | NONE => false
                        | _ => true
      fun addConditions (guard, rtl) = (StringMap.foldli addCondition guard m, rtl)
      val (guard, rtl) =
        if StringMap.exists (fn (_, TOP) => false | _ => true) m then
          addConditions (removeExtensions remove (guard, rtl))
        else
          (guard, rtl)
  in  applyUnconstrainedEqualities (guard, rtl)
  end
@ 
We want to know in what context each operand appears, i.e., what sort
of thing it is a child of. 
For our purposes, we're going to rewrite only those operands that are
consistently sign-extended or zero-extended; everything else is ignorable.
<<satisfaction>>=
datatype child_of = SX of int * int
                  | ZX of int * int
                  | TOP (* not SX or ZX, or inconsistently *)
<<support for removing extensions>>
@ 
We split only RTL things, and only if there is a condition on a
variable not free in a pattern.
To make things easy, we start with equality conditions.
<<binding split>>=
and applyUnconstrainedEqualities (guard, rtl) =
  let fun unconstrainedEquality (P.APP(("eq", [w]), [P.EXPVAR (x, c, _), v])) =
            if not (RtlPatternUtils.FreeIn.rtl x rtl) then SOME (x, c, v) else NONE
        | unconstrainedEquality _ = NONE
      fun findEq e =
        foldConjunction
        (fn (_, answer as SOME _) => answer
          | (e, NONE) => unconstrainedEquality e)
        (e, NONE)
  in  case findEq guard
        of SOME (x, c, v) => <<rewrite [[guard]] by [[x = v]] and split again>>
         | NONE => stripUnmentionedInequalities rtl guard
  end
<<rewrite [[guard]] by [[x = v]] and split again>>=
let fun replace (e as P.EXPVAR (x', c, w)) = if x' = x then v else e
      | replace e                          = e
    val guard = RtlPatternUtils.Subst.exp replace guard
    val (guard, rtl, bindings) = splitBindings (guard, rtl)
    fun rebind (x', c, w) = if x' = x then v else bindings (x', c, w)
in  (guard, rtl, rebind)
end
@ 
<<nofix help>>=
fun nofix guard =
let val ppg = !debug (EXP (G.single guard))
    val fl = PP.flatten
in  List.app print ["===== nothing to replace in guard ", fl ppg, "\n"];
    guard
end
<<emit debugging info>>=
let val ppg = !debug (EXP (G.single guard))
    val ppv = !debug (EXP (G.single v))
    val fl = PP.flatten
in  List.app print ["***** replacing ", x, " with ", fl ppv, " in guard ",
                    fl ppg, "\n"]
end
@ 
The idea is if something doesn't appear in the RTL, we choose a value
satisfying the guard.
The right and proper thing to do here is search the guard for free
variables that don't appear in the RTL.
We can then try to solve for reasonable values of those variables.
The search for a solution could be smart or could be a dumb sequential
search; either way, we could test a potential solution by seeing if
the guard simplifies to false. (This may be pushing it in the presence
of disjunction, or it may be perfectly OK---I haven't thought it
through.)
Once we solve, we rewrite the guard and continue.
<<satisfaction>>=
fun stripUnmentionedInequalities rtl guard =
  let fun unconstrainedInequality (P.APP(("ne", [w]), [P.EXPVAR (x, _, _), P.INT vw])) =
            if not (RtlPatternUtils.FreeIn.rtl x rtl) then SOME (x, vw) else NONE
        | unconstrainedInequality _ = NONE
      fun findNe e =
        foldConjunction
        (fn (_, answer as SOME _) => answer
          | (e, NONE) => unconstrainedInequality e)
        (e, NONE)
      fun strip guard =
        case findNe guard
          of SOME (x, (v, w)) => <<rewrite [[guard]] by choosing [[x]] $\ne$ [[v]] and strip again>>
           | NONE => boundOrSatisfying rtl guard
  in  strip guard
  end
<<rewrite [[guard]] by choosing [[x]] $\ne$ [[v]] and strip again>>=
let val v' =
      IntInf.fromInt (if IntInf.compare(v, IntInf.fromInt 0) = EQUAL then 1 else 0)
    fun replace (e as P.EXPVAR (x', c, w)) = if x' = x then P.INT (v', w) else e
      | replace e                          = e
    val guard = RtlPatternUtils.Subst.exp replace guard
    val (guard, rtl, bindings) = 
      if G.Exp.isFalse guard then
        Impossible.impossible ("could not find satisfying assignment for " ^ x)
      else
        strip guard 
    fun checkWidth w' = if getOpt(w', w) = w then ()
                        else Impossible.impossible "width mismatch in inequality"
fun checkWidth _ = ()
    fun rebind (x', c, w') = if x' = x then P.INT (v', w) before checkWidth w'
                             else bindings (x', c, w')
in  (guard, rtl, rebind)
end
@ 

I'm taking the cheap way out---which could also constitute a base
case.
Namely, if a variable is mentioned on the right but not on the left
(and also not in the guard), pick an arbitrary value---like zero.
<<satisfaction>>=
and boundOrSatisfying rtl guard =
  (guard, rtl,
   fn (name, c, width) => 
     if PU.FreeIn.rtl name rtl then
(*       P.INTVAR (name, getOpt(width, ReadSLED.SledSpec.defaultWidth))*)
       P.expvar (name, c, width)
     else
       if PU.FreeIn.exp name guard then
         P.expvar ("Bug in lrtl tools: must expunge unmentioned variable `" ^
                   name ^ "' from guard", c, NONE)
       else
         P.INT (IntInf.fromInt 0, getOpt(width, ReadSLED.SledSpec.defaultWidth))
  )
@ 
<<support for removing extensions>>=
fun childMap (guard, r) =
  let fun insert(m, x, const, context) =
        case StringMap.find (m, x)
          of NONE          => StringMap.insert(m, x, (const, context))
           | SOME (_, TOP) => m (* premature optimization *)
           | SOME (_, c')  =>
               if context = c' then m else StringMap.insert(m, x, (const, TOP))
      fun exp (P.INT _, m) = m
        | exp (P.BOOL _, m) = m
        | exp (P.FETCH (l, _), m) = loc (l, m)
        | exp (P.APP (("sx", [n, w]), [P.EXPVAR (x, c, _)]), m) =
            insert(m, x, SOME c, SX (n, w))
        | exp (P.APP (("zx", [n, w]), [P.EXPVAR (x, c, _)]), m) =
            insert(m, x, SOME c, ZX (n, w))
        | exp (P.APP (_, args), m) = foldl exp m args
        | exp (P.EXPVAR (x, c, _), m) = insert(m, x, SOME c, TOP)
        | exp (P.IVAR _, _) = Impossible.impossible "instance var in recognizer"
        | exp (P.NAMEDIVAR _, _) =
            Impossible.impossible "named instance var in recognizer"
      and loc (P.UNSLICED (_, _, _, _, e), m) = exp (e, m)
        | loc (P.SLICED {lsb, arg, ...}, m) = exp (lsb, loc (arg, m))
        | loc (P.LOCVAR x, m) = insert(m, x, NONE, TOP) (* might be wrong, but is safe *)
        | loc (P.NAMEDLOCVAR (x,_), m) = insert(m, x, NONE, TOP) (* might be wrong, but is safe *)
      fun effect (P.STORE (l, r, _), m) = exp (r, loc(l, m))
        | effect (P.KILL l, m) = loc(l, m)
      fun guarded ((g, e), m) = exp(g, effect (e, m))
      fun rtl (P.RTL l, m) = foldl guarded m l
  in  rtl (r, exp(guard, StringMap.empty))
  end
@ 
Now, we need to remove extensions.
<<support for removing extensions>>=
fun removeExtensions remove (guard, r) =
  let fun exp (e as P.INT _) = e
        | exp (e as P.BOOL _) = e
        | exp (P.FETCH (l, w)) = P.FETCH (loc l, w)
        | exp (e as P.APP (("sx", [n, w]), [P.EXPVAR (x, c, _)])) =
            if remove x then P.EXPVAR (x, c, w) else e
        | exp (e as P.APP (("zx", [n, w]), [P.EXPVAR (x, c, _)])) = 
            if remove x then P.EXPVAR (x, c, w) else e
        | exp (P.APP (f, args)) = P.APP (f, map exp args)
        | exp (e as P.EXPVAR x) = e
        | exp (P.IVAR _) = Impossible.impossible "instance var in recognizer"
        | exp (P.NAMEDIVAR _) = Impossible.impossible "named instance var in recognizer"
      and loc (P.UNSLICED (a, n, w, s, e)) = P.UNSLICED (a, n, w, s, exp e)
        | loc (P.SLICED {lsb, arg, argwidth=aw, lsbwidth=lw, width=w}) =
            P.SLICED {lsb=exp lsb, arg=loc arg, argwidth=aw, lsbwidth=lw, width=w}
        | loc (l as P.LOCVAR x) = l
        | loc (l as P.NAMEDLOCVAR x) = l
      fun effect (P.STORE (l, r, w)) = P.STORE (loc l, exp r, w)
        | effect (P.KILL l) = P.KILL (loc l)
      fun guarded (g, e) = (exp g, effect e)
      fun rtl (P.RTL l) = P.RTL (map guarded l)
  in  (exp guard, rtl r)
  end