Simple expressions

<assoc.sml*>=
structure Assoc = struct
  datatype associativity = Left | Right | None
end
Defines Assoc (links are to index).

<rators-sig.sml*>=
signature RATORS = sig 
  type nullop
  type unop
  type binop
  type anyop
  val orders : { order'nullop : nullop Order.T
               , order'unop   : unop Order.T
               , order'binop  : binop Order.T
               , order'anyop  : anyop Order.T
               }
  type 'a image = 'a * PP.pretty list * int * Assoc.associativity -> PP.pretty
  val images : { nullimage : nullop image
               , unimage : unop image
               , binimage : binop image
               , anyimage : anyop image
               }
end
Defines RATORS (links are to index).

Expressions

We'll begin with expressions. We stratify expressions so that the solver and balancer can depend only on what they need to know about expressions, not on accidents of whatever expressions are used in a particular application. We always parameterize an expression type by a type variable 'a, which stands for ``all other kinds of expressions.'' 
<exp-sig.sml*>=
signature EXP = sig
  structure OLC : OLC
  structure Operators : RATORS
  open Operators
  <definition of exp type>
  val exists_var : (string -> bool) -> exp -> bool
  val gsubst     : (string -> exp) -> exp -> exp
  val order      : exp Order.T
  val image      : exp * int * Assoc.associativity -> PP.pretty
end
Defines EXP (links are to index).

<exp.sml*>=
functor Exp (structure OLC : OLC   Operators : RATORS) : EXP = struct
  structure OLC = OLC
  structure Operators = Operators
  open Operators
  <definition of exp type>
  val { order'nullop, order'unop, order'binop, order'anyop } = Operators.orders
  <definition of order'exp_element>
  <definitions of expression basics>
end

The Number structure defines numbers, which are used as constants in expressions and as coefficients in linear sums. Integers or reals would be good choices. I don't functorize with respect to Number because I'm afraid the compiler wouldn't be able to inline arithmetic. An expression could be a variable, constant, linear sum, or something else (represented by 'a). 

<definition of exp type>= (<-U <-U)
datatype exp_element
  = VAR     of string
  | NULLARY of nullop
  | UNARY   of unop  * exp_element olc
  | BINARY  of binop * exp_element olc * exp_element olc
  | NARY    of anyop * exp_element olc list
type exp = exp_element olc
Defines exp, exp_element (links are to index).

We can choose either integers or reals as numbers. 

<number.sml*>=
structure IntNumber = struct
  type number = int
  val zero      : number = 0
  val one       : number = 1
  val dividenum : number * number -> number = op div
  val mulnum    : number * number -> number = op *
end
structure RealNumber = struct
  type number = real
  val zero      : number = 0.0
  val one       : number = 1.0
  val dividenum : number * number -> number = op /
  val mulnum    : number * number -> number = op *
end
structure Number = IntNumber
Defines IntNumber, Number, RealNumber (links are to index).

Now, here's what we need from ordered linear combinations. Following [cite derman:simple], an ordered linear combination is either a constant term, or the linear sum of an ``other'' expression and another ordered linear combination. ``Other'' expressions must be ordered, and the first term in the ordered linear combination must precede all other terms in the ordering. 

<olc-sig.sml*>=
signature OLC = sig
  type number 
  sharing type number = Number.number
  datatype 'elem olc = CONST of number
                     | SUM of number * 'elem * 'elem olc 
                         (* invariant: coefficient is never zero *)

  val basics = 'a Order.T -> 

  (* constructors *)

  { mkconst : number -> 'a olc                     (* create k *)

  (* mutators *)

  , kadd    : 'a olc * number          -> 'a olc   (* olc + k *) 
  , eadd    : 'a olc * number * 'a     -> 'a olc   (* olc + k o *) 
  , add     : 'a olc * 'a olc          -> 'a olc   (* olc1 + olc2 *)
  , divide  : 'a olc * number          -> 'a olc   (* olc divided by k *)
  , mul     : 'a olc * number          -> 'a olc   (* olc * k *)

  , order   : 'a olc Order.T
  }
end
Defines OLC (links are to index).

OK, let's do some functions! Begin with the basics. 

<definitions of expression basics>= (<-U) [D->]

Here are the functions on expressions that we intend to export. (I let the compiler figure out the types.) 

<expfuns-sig.sml*>=
signature EXPFUNS = sig
  structure Exp : EXP
  type exp     sharing type exp    = Exp.exp
  type number  sharing type number = Number.number
  type olc     sharing type olc    = Exp.OLC.olc

  (* compare expressions *)
  val order   : exp Order.T

  (* arithmetic on olcs and expressions *)
  val add     : exp * number * exp -> exp    (* s1 + k * s2 *)
  val olcaddd : number * exp * number * exp -> exp    (* k1 * s1 + k2 * s2 *)
  val neg     : exp -> exp                           (* ~s *)
  val divide  : exp * number -> exp                  (* s / k *)
  val mul     : exp * number -> exp                  (* s * k *)

  (* tests for variables in expressions *)
  val exists_var  : (string -> bool) -> exp -> bool
  val forall_vars : (string -> bool) -> exp -> bool
  val is_free_in  : string * exp -> bool

  (* generic substitution for variables in expressions and olcs *)
  val gsubst      : (string -> exp) -> exp -> exp

  (* and substitution of a value for a particular variable *)
  val subst       : string * exp -> exp -> exp

  (* images *)
  val image    : exp -> PP.pretty
  val expimage : exp * int * Assoc.associativity -> PP.pretty

  val simplify : exp -> exp
end
Defines EXPFUNS (links are to index).

<expfuns.sml*>=
functor ExpFuns (Exp : EXP) : EXPFUNS = struct
  structure Exp = Exp
  open Exp.OLC
  open Exp
  open Number
  open Prec
  <exp functions>
  fun simplify e = e
end

Now, let us deal with arithmetic. First, adding olcs: 

<exp functions>= (<-U) [D->]
fun addsums(s1, k, s2) =   (* s1 + k * s2 *)
  let fun do_var(v::rest,   t) = do_var(rest, vadd(t, k * vcoeff(s2, v),   v))
        | do_var([],        t) = t
      fun do_oth(oth::rest, t) = do_oth(rest, oadd(t, k * ocoeff(s2, oth), oth))
        | do_oth([],        t) = t
      val (vs, es) = terms s2
  in  kadd(do_var(vs, do_oth(es, s1)), k * const s2)
  end
Defines addsums (links are to index).

and negating them: 

<exp functions>+= (<-U) [<-D->]
fun neg s = addsums(mkconst zero, ~one, s)
Defines neg (links are to index).

Adding an expression to a olc is a bit less tricky. 

<definitions of expression basics>+= (<-U) [<-D->]
fun addse(s, k, olc s2)    = addsums(s, k, s2)
  | addse(s, k, Const n)   = kadd(s, k * n)
  | addse(s, k, Var v)     = vadd(s, k, v)
  | addse(s, k, Other oth) = oadd(s, k, oth)
Defines addse (links are to index).

To convert an expression to a olc, we might add it to the zero olc. 

<exp functions>+= (<-U) [<-D->]
fun exp2sum (Sum s)     = s
  | exp2sum e           = addse(mkconst zero, one, e)
Defines exp2sum (links are to index).

The opposite conversion is messy; basically if the olc is a single term (constant, variable, or expression) we use that term, otherwise we apply Sum. 

<exp functions>+= (<-U) [<-D->]
fun olc2exp s =
  let val k = const s
  in  case terms s 
        of ([v], [])    => if k = zero andalso vcoeff(s, v)   = one then Var   v 
                           else olc s
         | ([],  [oth]) => if k = zero andalso ocoeff(s, oth) = one then Other oth 
                           else olc s
         | ([],  [])    => Const k
         | _            => olc s
  end
Defines olc2exp (links are to index).

Once we have the conversions, we can do orderity tests. 

<exp functions>+= (<-U) [<-D->]
fun olcs_eq(s1, s2) =
  const s1 = const s2 andalso
    let val (v1, o1) = terms s1
        val (v2, o2) = terms s2
    in  length v1 = length v2 andalso length o1 = length o2 andalso
      let
        nonfix o
        fun vtest(v::t) = vcoeff(s1, v) = vcoeff(s2, v) andalso vtest t
          | vtest nil   = true
        fun otest(o::t) = ocoeff(s1, o) = ocoeff(s2, o) andalso otest t
          | otest nil   = true
      in 
        vtest v1 andalso otest o1
      end
    end
Defines olcs_eq (links are to index).

Here's where we need the conversion, so we can make sure, e.g., that x = 0 + 1*x. 

<exp functions>+= (<-U) [<-D->]
fun order (e1, e2) =
  let fun eq(Sum s1,   olc s2  ) = olcs_eq(s1, s2)
        | eq(Const n1, Const n2) = n1 = n2
        | eq(Var v1,   Var v2  ) = v1 = v2
        | eq(Other o1, Other o2) = Other.order(o1, o2)
        | eq _                   = false
      fun unsum(Sum s) = olc2exp s
        | unsum e      = e      
  in  eq(unsum e1, unsum e2)
  end
Defines order (links are to index).

Next we need to get into testing and substitution over variables. First, exists: does any free variable in e satisfies a predicate p.? We must be passed a function that does the job for the Other case. 

<definitions of expression basics>+= (<-U) [<-D->]
<existence testing in olcs>
fun exists_var p =
  let fun ex(Var v)     = p v
        | ex(Const _)   = false
        | ex(Sum s)     = olc_exists_var p s
        | ex(Other oth) = exists_var' p oth
  in  ex
  end
Defines exists_var (links are to index).

To test a olc, we test all the variables and other things. 

<existence testing in olcs>= (<-U)
fun olc_exists_var p s =
  let fun test(p, h::t) = if p h then true else test(p, t)
        | test(p,   []) = false
      val (vs, os) = terms s
  in  test(p, vs) orelse test(exists_var' p, os)
  end
Defines olc_exists_var (links are to index).

Getting forall with the same transformation involves the usual DeMorgan stuff. 

<exp functions>+= (<-U) [<-D->]
fun forall_vars p e = not (exists_var (fn v => not(p v)) e)
Defines forall_vars (links are to index).

Testing for free variables is common: 

<exp functions>+= (<-U) [<-D->]
fun is_free_in(v, e) = exists_var (fn v' => v = v') e
Defines is_free_in (links are to index).

We define a way of substituting for variables using the substition function f, which maps variables to expressions. 

<definitions of expression basics>+= (<-U) [<-D]
<substitution in olcs>
fun gsubst f =
  let fun sub(Var v)          = f v
        | sub(e as (Const _)) = e
        | sub(Sum s)          = olc2exp(sum_gsubst f s)
        | sub(Other oth)      = gsubst' f oth
  in  sub
  end
Defines gsubst (links are to index).

Substitution in olcs involves creating a new olc from scratch, adding up all the substituted expressions. Using addse makes substitutions of olcs for variables come out right automagically. 

<substitution in olcs>= (<-U)
fun olc_gsubst f s = 
  let fun do_var(v::rest, t) = do_var(rest, addse(t, vcoeff(s, v), f v))
        | do_var([],      t) = t
      fun do_oth(e::rest, t) = do_oth(rest, addse(t, ocoeff(s, e), Other.subst f e))
        | do_oth([],      t) = t
      val (vs, os) = terms s
  in  do_var(vs, do_oth(os, mkconst (const s)))
  end
Defines olc_gsubst (links are to index).

Here's basic substitution (as opposed to generic substitution). 

<exp functions>+= (<-U) [<-D->]
fun subst    (v, vval) = gsubst     (fn v' => if v = v' then vval else Var v')
fun olc_subst(v, vval) = olc_gsubst (fn v' => if v = v' then vval else Var v')
Defines olc_subst, subst (links are to index).

Here's how we print expressions: 

<exp functions>+= (<-U) [<-D]
fun expimage(Var v,   precedence, associativity) = PP.Text v
  | expimage(Const c, precedence, associativity) = PP.Text (makestring c)
  | expimage(Other c, precedence, associativity) = 
                                        Other.image(c, precedence, associativity)
  | expimage(Sum s,   precedence, associativity) = 
       let <bind im to representation of olc s, eliding additive and multiplicative units>
       in  PP.List [PP.Indent 2, PP.Begin, im, PP.End, PP.Outdent]
       end
fun image e = expimage(e, 0, Assoc.Left)
Defines expimage, image (links are to index).

Show positive terms, then negative terms, with the constant term always last in its group. The internal function add adds the images of terms that pass an ok test (which will be positive or negative). 

<bind im to representation of olc s, eliding additive and multiplicative units>= (<-U)
val im =
  let <stuff to build up image of olc>
  in  <image of olc>
  end
Defines im (links are to index).

We're going to scan the olc left to right, but eventually build up the image right to left. As a result, there's a lot of reversing going on. raddterms captures the generic thing: if the term is ok (i.e., we want it to appear in this part of the image), then append the leading sign and the image of the term to whatever came before (backwards), and update the leading sign. Otherwise, proceed to the next term without touching the leading sign. This process updates both the leading sign and the accumulated terms, so that's what it returns. Both are reversed. 

<stuff to build up image of olc>= (<-U) [D->]
fun raddterms (image, ok, sign) =
  let fun add([],   (rleadingsign, previous)) = (rleadingsign, previous)
        | add(h::t, (rleadingsign, previous)) = 
            if ok h then
              add(t, ([PP.Text sign, PP.Optional],
                      rev (image h) @ rleadingsign @ previous))
            else
              add(t, (rleadingsign, previous))
  in  add
  end
Defines raddterms (links are to index).

Now some predicates. We use key x to stand for the coefficient of x, and we'll be printing positive and negative terms separately. 

<stuff to build up image of olc>+= (<-U) [<-D->]
fun pos key = fn x => key x > zero
fun neg key = fn x => key x < zero
Defines neg, pos (links are to index).

To get the image of a term, we print the absolute value of the coefficient, plus the image of the term itself---except we show no unit multiplications. 

<stuff to build up image of olc>+= (<-U) [<-D->]
fun img (img',key) x = 
  let val k = abs (key x)
  in  if k = Number.one then      
        img' x 
      else 
        PP.Text(makestring k^"*") :: img' x
  end
Defines img (links are to index).

Now, here's how we get images of other things: 

<stuff to build up image of olc>+= (<-U) [<-D->]
fun varimg x = [PP.Text x]
fun othimg x = [Other.image (x, precof "+", Assoc.Left)]
fun conimg k = [PP.Text (makestring (k:Number.number))]
Defines conimg, othimg, varimg (links are to index).

And how to get the coefficients: 

<stuff to build up image of olc>+= (<-U) [<-D->]
fun vkey v = vcoeff(s, v)
fun okey x = ocoeff(s, x)
fun kkey k = k
Defines kkey, okey, vkey (links are to index).

And we have three lists of terms: variables, others, constants: 

<stuff to build up image of olc>+= (<-U) [<-D->]
val (vs, os) = terms s
val ks       = [const s]
Defines ks (links are to index).

allterms puts together all the terms for either positive or negative, giving us a list of stuff in result. We can't pass in pos or neg directly, since parametric polymorphism isn't permissive enough. Instead we pass a Boolean and assign to ok', and let-polymorphism does the job. 

<stuff to build up image of olc>+= (<-U) [<-D]
fun allterms (postest, leadsign, midsign) = 
  let val ok' = if postest then pos else neg
      val (rleadingsign, im) =
        raddterms(img (conimg, kkey),  ok' kkey, midsign) (ks,  (* constant last *)
        raddterms(img (othimg, okey),  ok' okey, midsign) (os,  (* others middle *)
        raddterms(img (varimg, vkey),  ok' vkey, midsign) (vs,  (* vars first *)
            (rev leadsign, []))))
  in 
    rev im
  end
val result = allterms(true, [], "+") @ allterms(false, [PP.Text "-"], "-")
Defines allterms, result (links are to index).

And finally, our answer: 

<image of olc>= (<-U)
case result of []  => PP.Text "0"
             | [x] => x
             | l   => PP.List l

Implementing linear olcs

<OLC.sml*>=
structure OLC : OLC = struct
  type number = Number.number
  datatype 'elem olc = CONST of number
                     | SUM of number * 'elem * 'elem olc 
  open LibBase

  fun sum (k, x, y) = if k <> zero then SUM(k, x, y) else y

  fun basics exporder = 
    let val mkconst = CONST
      
        fun kadd (CONST k', k)  =  CONST (k + k')
          | kadd (SUM(k', x, y), k) = SUM(k', x, kadd(y, k))
        fun eadd (CONST k', e)  = SUM(one, e, CONST k')
          | eadd (SUM(k, x, y), e) = 
             (case exporder (e, x) 
                of Less  => SUM(one, e, SUM(k, x, y))
                 | Equal => sum(k + one, x, y)
                 | Greater => SUM(k, x, eadd(y, e)))
        fun add (CONST k,      CONST k')      = CONST (k + k')
          | add (SUM(k, x, y), CONST k')      = SUM(k, x,  kadd(y, k'))
          | add (CONST k,      SUM(k', x, y)) = SUM(k', x, kadd(y, k))
          | add (olc as SUM(k, x, y), olc' as SUM(k', x', y')) =
             (case exporder (x, x') 
                of Less    => SUM(k,    x,  add(y, olc'))
                 | Equal   => sum(k+k', x,  add(y, y'))
                 | Greater => SUM(k',   x', add(olc, y')))
        fun divide(CONST k, k') = Number.dividenum(k, k')
          | divide(SUM(k, x, y), k') = sum(Number.dividenum(k, k'), x, divide(y, k'))
        fun mul(CONST k, k') = Number.mulnum(k, k')
          | mul(SUM(k, x, y), k') = SUM(Number.mulnum(k, k'), x, mul(y, k'))
        val mul = fn(olc, k) => if k = zero then CONST zero else mul(olc, k)
         (* constant terms follow everything *)
        fun order(CONST k,      CONST k')      = Number.order (k, k')
          | order(SUM(k, x, y), CONST k')      = Less
          | order(CONST k,      SUM(k', x, y)) = Greater
          | order(olc as SUM(k, x, y), olc' as SUM(k', x', y')) =
             (case exporder (x, x') 
                of Less    => Number.order(k, zero)
                 | Equal   => if k = k' then order(y, y') else Number.order (k, k')
                 | Greater => Number.order(zero, k'))
  
    in  {mkconst=mkconst, kadd=kadd, eadd=eadd, add=add, 
         divide=divide, mul=mul, order=order}
    end
end
Defines OLC (links are to index).

Inequalities

<inequality.sml*>=
structure Inequality = struct
  datatype relop = EQ | NE | LT | LE | GT | GE
  type 'exp inequality = 'exp * relop * 'exp
  local
    fun im EQ = "="
      | im NE = "!="
      | im LT = "<"
      | im LE = "<="
      | im GT = ">"
      | im GE = ">="
    val Left = Assoc.Left
    open Prec
  in 
    fun eqnimage expimage (l, relop, r) = 
      PP.List [expimage(l, precof "=", Left), PP.Text (" "^im relop^" "), PP.Optional,
               expimage(r, precof "=", Left)]
  end
end
Defines Inequality (links are to index).

Operator precedence

<prec.sml*>=
structure Prec = struct
  local
    val ops = [("N", ["low"]),
               ("L", ["|", "pattern"]),
               ("L", [";"]),
               ("L", ["&", "sequent"]),
               ("R", [":="]),
               ("L", [","]),
               ("N", ["Sguarded"]),
               ("N", ["="]),
               ("L", ["ORB", "Eorb"]), 
               ("L", ["AND", "Eand"]),
               ("L", ["<", "<="]),
               ("L", ["+"]),
               ("N", ["Emod", "Ediv", "*"]),
               ("N", ["Eshift"]),
               ("N", ["NOT"]),
               ("L", ["Eslice", "Narrowu", "Narrows", "Widen", "."]),
               ("N", ["app"]),           (* function application *)
               ("N", ["high"])
       ]
    fun a "L" = Assoc.Left
      | a "R" = Assoc.Right
      | a "N" = Assoc.None
      | a _   = raise Impossible.Impossible "bad associativity in table"
    fun add_dict(dict, [],        level) = dict
      | add_dict(dict, (astring, ops)::rest, level) =
          foldl (fn (s, dict) => StringDict.insert(dict, s, (a astring, level))) 
                (add_dict(dict, rest, level+1))
                ops
    val precedence_dictionary = add_dict(StringDict.mkDict(), ops, 0) 
  in
    fun precof s =
       let val (_, p) = StringDict.find(precedence_dictionary, s)
       in  p
       end
       handle StringDict.NotFound => raise Impossible.Impossible ("precedence of " ^ s)
    fun assocof s =
       let val (a, _) = StringDict.find(precedence_dictionary, s)
       in  a
       end
       handle StringDict.NotFound => 
           raise Impossible.Impossible ("associativity of " ^ s)
    fun bracket(expimage, operator, prec, assoc) =
       let val e = if precof operator > prec orelse 
                      (precof operator = prec andalso assocof operator = assoc) then 
                     expimage
                   else
                     PP.List [ PP.Text "(", expimage, PP.Text ")"]
       in 
         PP.List [PP.Begin, e, PP.End]
       end
  end
end
Defines Prec (links are to index).

Narrow and widen, balancing

<narrow.sml>=
functor NarrowOther(Exp : EXP) : OTHER = struct
  open Prec
  structure Exp = Exp
  datatype t = Widen   of t Exp.exp * int
             | Narrows of t Exp.exp * int
  val rec 
      ex = Exp.exists_var' exists_var
  and exists_var = fn f =>
         let fun exists (Widen  (e, n)) = ex f e
               | exists (Narrows(e, n)) = ex f e
         in  exists
         end
  val rec
      gsub = Exp.gsubst' subst
      subst = fn f =>
         let fun gsubst (Widen  (e, n)) = Widen  (gsub f e, n)
               | gsubst (Narrows(e, n)) = Narrows(gsub f e, n)
         in  gsubst
         end
  val rec
      eq   = Exp.order' order
  and order = 
        fn (Widen  (e1, n1), Widen  (e2, n2)) => n1 = n2 andalso eq(e1, e2)
         | (Narrows(e1, n1), Narrows(e2, n2)) => n1 = n2 andalso eq(e1, e2)
         | _ => false
  val rec 
      img  = Exp.image' image
  and image = fn (e, prec, assoc) =>
        case e of
            Narrows(e, n) => 
              bracket(img(e, precof "Narrows", assoc) ^ "[" ^ makestring n ^ "!]",
                      "Narrows", prec, Assoc.Left)
          | Widen (e, n) =>
              bracket(img(e, precof "Widen",   assoc) ^ "!" ^ makestring n,
                      "Widen", prec, Assoc.Left)
end

<cycle.dot>=
digraph recursions {
  { rank=min "exists'" "order'" "image'" "subst'" }
  "exists'" -> "exists" -> olc_exists -> { "exists'" terms}
  exists -> "exists'"
  terms
  "image'" -> "image" -> { ocoeff "image'" }
  ocoeff -> "order'"

  "subst'" -> "subst" -> {sum2exp "subst'" olc_gsubst}
  olc_gsubst -> {addse ocoeff "subst'"}

  "order'" -> "order" -> {"order'" olcs_order olc2exp}
  olcs_order -> ocoeff

  addse -> {addsums oadd}
  oadd -> "order'"

  olc2exp -> ocoeff
  addsums -> oadd
}


<Order.sml*>=
structure Order = struct
  type 'a T = 'a * 'a -> LibBase.relation
end
Defines Order (links are to index).