Expressions and Equations

Expressions describe all the value manipulations performed by the toolkit. They include not only manipulations that can be expressed using the input expression language, but also manipulations that are generated internally, including slicing, narrowing, sign extension, division, and modulus. A special normal form is used to represent sums of terms with constant coefficients. The integer 1 may also be used as a term; it is multiplied by a coefficient to represent a constant term, if any. This normal form is represented as an Icon table in which the keys are the terms and the values are the coefficients. For example, the expression 10*x + 4 is represented by the Icon table mapping "x" to 10 and 1 to 4.

These expressions are used both in equation solving and to compute the values of fields. I give definitions in terms of Modula-3. x and y are expressions; n and lo are integer constants. 

<*>= [D->]
record Eorb(x, y)                       # Word.Or(x, y)
record Eand(x, y)                       # x AND y               -- short-circuit Boolean
record Eslice(x, lo, n)                 # Word.Extract(x, lo, width)
record Eshift(x, n)                     # Word.Shift(x, n)
record Enarrowu(x, n)                   # narrow to n bits, unsigned, with check
record Enarrows(x, n)                   # narrow to n bits,   signed, with check
record Ewiden(x, n)                     # sign-extend low n bits
record Ediv(x, n)                       # x DIV y
record Emod(x, n)                       # x MOD y
record Efitsu(x, n)                     # unsigned value x fits in n bits
record Efitss(x, n)                     # signed value x fits in n bits
record Epatlabel(l)                     # reference to patlabel l
record Eforce(x)                        # force relocatable x to an integer
record Eforceable(x)                    # true iff relocatable x has known address
record Epc()                            # start of pattern match or token emission
record Epc_known()                      # predicate needed in encoding
record Sstmts(x)                        # sequence of statements
record Enot(x)                          # NOT x
record Enosimp(x)                       # x, but suppress simplification
record Semit(x)                         # emit list of Stoken
record Stoken(x, n, offset)             # emit x with width n (offset from beginning)
                                        #       (offset >= 0 always)
record Einstance(cons, argt)            # cons applied to arguments in table argt
record Einstance_input(x, cons, name)   # input name from instance x of constructor cons
record Einstance_tagged(x, cons, uid)   # true iff instance x tagged as constructor cons
record Ebinding_instance(name, type, vart) # binding instance of constructor-typed input
                                           # vart is table used to find fresh vars
record Sif(arms)                        # list of Sguarded
record Sguarded(guard, x)               # if guard then x (in Sif)
record Sepsilon()                       # empty statement
record Efail(msg)                       # result of selecting from the wrong constructor
record Eapp(f, args)                    # function application
record Eclosure_loc()                   # location of a relocation closure
record Eclosure_addr(n)                 # relocatable address in a relocation closure
record Eclosure_val(n)                  # value in a relocation closure
Defines Eand, Eapp, Ebinding_instance, Eclosure_addr, Eclosure_loc, Eclosure_val, Ediv, Efail, Efitss, Efitsu, Eforce, Eforceable, Einstance, Einstance_input, Einstance_tagged, Emod, Enarrows, Enarrowu, Enosimp, Enot, Eorb, Epatlabel, Epc, Epc_known, Eshift, Eslice, Ewiden, Semit, Sepsilon, Sguarded, Sif, Sstmts, Stoken (links are to index).

<argument descriptions>=
expargs x y arms guard left right args.
special simplify Einstance Stagcase Enosimp Sif.
special hoist Epc Epc_known Eorb Sguarded Sepsilon Sfail Stoken Eforce.

The following types officially represent values: 

<*>+= [<-D->]
procedure exptypes()
  suspend "string" | "integer" | "table" | "Eorb" | "Eslice" | "Eshift" | "Enarrowu" |
          "Enarrows" | "Ewiden" | "Ediv" | "Emod" | "Einstance_input" | "Einstance" |
          "Ebinding_instance" | "Eapp" | "Eclosure_loc" | "Eclosure_addr" |
          "Eclosure_val"
end
Defines exptypes (links are to index).

An equation asserts that two expressions are equal. In this code, I extend the term to cover what is more normally called an ``inequality''---a pair of expressions related by one of the usual relational operators. 

<*>+= [<-D->]
record eqn(left, op, right)             # equality or inequality
Defines eqn (links are to index).

Searching for subterms and free variables

subterms_matching(e, ty) suspends all subterms of e that have type ty. 
<*>+= [<-D->]
procedure subterms_matching_f(e, types[])
  return if type(e) == !types then e
end

procedure subterms_matching(e, types[])
  suspend do_expwalk(e, subterms_matching_f, types)
end
Defines subterms_matching, subterms_matching_f (links are to index).

Finding free variables is a common enough case of subterms_matching that I define a special procedure for it: 

<*>+= [<-D->]
procedure free_variables_f(e)
  return if type(e) == "string" then e
end

procedure free_variables(e)
  suspend expwalk(e, free_variables_f)
end
Defines free_variables, free_variables_f (links are to index).

Testing for equality

This is a conservative test. 
<*>+= [<-D->]
procedure exps_eq(e1, e2)
  if e1 === e2 then return e2
  e1 := untableexp(e1)
  e2 := untableexp(e2)
  return case type(e1) == type(e2) of {
    <cases for exps_eq>
  }
end
Defines exps_eq (links are to index).

<cases for exps_eq>= (<-U) [D->]
"pattern"      : fail
"disjunct"     : fail
"adisjunct"    : fail
"sequent"      : fail
"patlabel"     : e1 === e2
"latent_patlabel" : e1 === e2  ## ???
"dots_sequent" : fail
"constraint"   : fail
"fieldbinding" : fail
"field"        : e1 === e2
"absolute_field" : exps_eq(e1.field, e2.field) & e1.offset = e2.offset

<cases for exps_eq>+= (<-U) [<-D->]
"list"         : if *e1 ~= *e2 then fail
                 else {
                   every i := 1 to *e1 do if not exps_eq(e1[i], e2[i]) then fail
                   e1
                 }
"eqn"          : <equations e1 and e2 are the same>

<cases for exps_eq>+= (<-U) [<-D->]
"table"        : { if *e1 ~= *e2 then fail
                   every k1 := key(e1) do
                     if k2 := key(e2) & e2[k2] = e1[k1] & exps_eq(k1, k2) then &null 
                     else fail
                   e2
                 }

<cases for exps_eq>+= (<-U) [<-D->]
"set"          : { if *e1 ~= *e2 then fail
                   s := set()
                   every x := !e1 do
                     if exps_eq(x, y := !e2)
                       then insert(s, y)
                     else
                       fail
                   *s = *e2          
                  }

<cases for exps_eq>+= (<-U) [<-D->]
"Eorb" | "Eand" : exps_eq(e1.x, e2.x) & exps_eq(e1.y, e2.y)
"Eslice" : e1.lo = e2.lo & e1.n = e2.n & exps_eq(e1.x, e2.x)
"Eshift" | "Enarrowu" | "Enarrows" | "Ewiden" | "Ediv" | "Emod" |
"Efitsu" | "Efitss" : e1.n = e2.n & exps_eq(e1.x, e2.x)
"Epatlabel" : e1.l === e2.l
"Eforce" | "Eforceable" | "Enot" | "Enosimp" | "Sstmts" | "Semit" : exps_eq(e1.x, e2.x)
"Epc" | "Epc_known" : true
"Stoken" : e1.offset = e1.offset & e1.n = e2.n & exps_eq(e1.x, e2.x)
"Einstance_input"  : e1.cons === e2.cons & e1.name == e2.name & exps_eq(e1.x, e2.x)
"Einstance_tagged" : e1.cons === e2.cons & e1.uid = e2.uid & exps_eq(e1.x, e2.x)
"Einstance"        : impossible("escaping Einstance")
"Ebinding_instance": impossible("escaping Ebinding_instance")

<cases for exps_eq>+= (<-U) [<-D->]
"Sif" | "Sguarded" | "Stagcase" : fail

<cases for exps_eq>+= (<-U) [<-D->]
"Glines"    : fail
"Gresynch"  : fail
"Gblock"    : fail
"Gdecl"     : fail
"Gcase"     : fail
"Gcasearm"  : fail
"Ginrange"  : fail
"Gsetname"  : fail
"Gnomatch"  : fail
"Gasgn"     : fail
"Tunsigned" : fail
"Gcomment"  : fail
"Gcommented" : e1.comment == e2.comment & exps_eq(e1.e, e2.e)

<cases for exps_eq>+= (<-U) [<-D->]
"string"  : e1 == e2
"integer" : e1 = e2

<cases for exps_eq>+= (<-U) [<-D->]
"Eapp" : fail

<cases for exps_eq>+= (<-U) [<-D]
"Eclosure_loc" : e1
"Eclosure_addr" : e1.n = e2.n
"Eclosure_val" : e1.n = e2.n

For matching equations, we have a plethora of possibilities. The first line is an optimization. For the second line, we test both for the same relation and ``opposite'' relations. Note that equality is its own opposite, so a=b is equivalent to a'=b' if either a-b=a'-b' or a-b=b'-a'. Similarly for simple inequality. 

<equations e1 and e2 are the same>= (<-U)
(e1.op == e2.op, exps_eq(e1.left, e2.left), exps_eq(e1.right, e2.right)) |
(d1 := subtract(e1.left, e1.right), 
  (e1.op == e2.op, 
   exps_eq(d1, subtract(e2.left, e2.right))) |
  (e1.op == opposite_op(e2.op),
   exps_eq(d1, subtract(e2.right, e2.left))))

<*>+= [<-D->]
procedure opposite_op(op)
  return case op of { 
    "<"  : ">"
    "<=" : ">="
    ">"  : "<"
    ">=" : "<="
    "="  : "="
    "!=" : "!="
  }
end
Defines opposite_op (links are to index).

<*>+= [<-D->]
procedure untableexp(e)
  local result
  if type(e) == "table" then {
    every k := key(e) & e[k] = 0 do 
      delete(e, k)
    case *e of {
      0: return 0
      1: { k := key(e)
           if k === 1 then return e[k]
           else if e[k] = 1 then return k
         }
     }
  }
  return e
end
Defines untableexp (links are to index).

Substitution

I have two forms: single value for variable and values for variables in table. 
<*>+= [<-D->]
procedure subst_f(e, var, value)
  if type(e) === "string" then return if var == e then value else e
end

procedure subst(e, var, value)
  return if var === value then e        # optimization
         else do_gsubst(e, subst_f, [var, value])
end
Defines subst, subst_f (links are to index).

If all is not null, all the free variables in the expression must be bound by the table. 

<*>+= [<-D->]
procedure subst_tab_f(e, tbl, all)
  return if type(e) == "string" then
           \tbl[e] | if \all then 
                       error("variable ", image(e)," is unbound in table ", 
                                                   envimage(tbl, "substitions"))
                     else 
                       e
end

procedure subst_tab(e, tbl, all)
  return do_gsubst(e, subst_tab_f, [tbl, all])
end
Defines subst_tab, subst_tab_f (links are to index).

Sometimes we just want to substitute for all elements of any table, even if they aren't just strings. 

<*>+= [<-D->]
procedure subst_table_elements_f(e, tbl)
  return \tbl[e]
end
procedure subst_table_elements(e, tbl)
  return do_gsubst(e, subst_table_elements_f, [tbl])
end
Defines subst_table_elements, subst_table_elements_f (links are to index).

<*>+= [<-D->]
procedure subst_for_pc_f(e, val)
  return if e === the_global_pc then val
end

procedure subst_for_pc(e, val)
  return do_gsubst(e, subst_for_pc_f, [val])
end
Defines subst_for_pc, subst_for_pc_f (links are to index).

Sometimes the values in a table are expressions. 

<*>+= [<-D->]
procedure subst_values_in_table(t, var, value)
  return do_gsubst_values_in_table(t, subst_f, [var, value])
end

procedure subst_tab_values_in_table(t, var, value)
  return do_gsubst_values_in_table(t, subst_tab_f, [var, value])
end

procedure do_gsubst_values_in_table(t, f, closure)
  n := 0
  u := table()
  every k := key(t) & x := do_gsubst(t[k], f, closure) do {
    u[k] := x
    if x ~=== t[k] then n +:= 1
  }
  return if n > 0 then u else t
end
Defines do_gsubst_values_in_table, subst_tab_values_in_table, subst_values_in_table (links are to index).

The solver needs destructive substitution when e is a table or an equation. Fortuitously, we can use the same code for dsubst and dsubst_tab. 

<*>+= [<-D->]
procedure dsubst(e, var, value)
  return destructive_subst(e, var, value, subst)
end
procedure dsubst_tab(e, tbl, all)
  return destructive_subst(e, tbl, all, subst_tab)
end
Defines dsubst, dsubst_tab (links are to index).

<*>+= [<-D->]
procedure destructive_subst(e, a2, a3, substitute)
  if type(e) == "eqn" then {
    e.left  := destructive_subst(term2table(e.left),  a2, a3, substitute)
    e.right := destructive_subst(term2table(e.right), a2, a3, substitute)
  } else {
    m := copy(e)
    every k := key(m) & mm := m[k] & kk := substitute(k, a2, a3) do {
      e[k] -:= mm
      if type(kk) ~== "table" then
        e[kk] +:= mm
      else 
        every v := key(kk) do e[v] +:= kk[v] * mm
    }
    every k := key(e) & e[k] = 0 do delete(e, k)
  }
  return e
end
Defines destructive_subst (links are to index).

Simplification

I discovered late in the day that there need to be two kinds of simplification. Basically, some of the simplifying rules reduce the strength of operations, and after strength reduction the solver can't always invert the results. On the other hand, there are situations in which one simply can't do without simplification, as when it eliminates an unsolvable disjunct (see bug #2). A tentative fix is to designate some simplification rules as <super rewrite rules>, and to use them only on expressions that won't be further transformed. They are used in super_simplify only.

simplify is not functional; it may mutate its argument. 

<*>+= [<-D->]
procedure simplify(e)
  local left, right
  return case type(e) of {
    $define simfun simplify
      <basic cases for simplification>
      <cases generated from rewrite rules>
    $undef simfun
    default : e
  }
end
Defines simplify (links are to index).

I need an empty chunk for bootstrapping. 

<cases generated from rewrite rules>= (<-U)

<*>+= [<-D->]
procedure super_simplify(e)
  local left, right
  return case type(e) of {
    $define simfun super_simplify
      <basic cases for simplification>
      <cases generated from super rewrite rules>
    $undef simfun
    default : e
  }
end
Defines super_simplify (links are to index).

I need an empty chunk for bootstrapping. 

<cases generated from super rewrite rules>= (<-U)


<basic cases for simplification>= (<-U <-U)
"eqn"      : {<simplify equation>}
"pattern"  : {<simplify pattern>}
"disjunct" : {<simplify disjunct>}
"adisjunct": {<simplify adisjunct>}
"sequent"  : if (l := simfun(e.constraints)) === e.constraints then e
             else sequent(l, e.class)
"patlabel"     : e
"dots_sequent" : e
"constraint"   : e
"fieldbinding" : if (x := simfun(e.code)) === e.code then e 
                 else fieldbinding(e.field, x)
"absolute_field" : 
  if simfun === super_simplify then
    afieldexp(e)
  else
    e
"set"   : {<simplify set of conditions>}
"table" : {<simplify table>}
"list"  : {l := maplist(simfun, e); if lists_match(e, l) then e else l}
"integer" | "string" : e
"Einstance" : {<simplify instance's argument table>}
"Stagcase"  : {<simplify tag case's arm table>}
"Sif"   : {<simplify if statement>}
"Enosimp" : e       # suppresses simplification
"Gcommented" : if (ee := simfun(e.e)) === e.e then e else Gcommented(ee, e.comment)
"Gcomment" : e

Simplification of a disjunct could fail, implying that the disjunct's condition is always false. 

<simplify pattern>= (<-U)
l := []; every put(l, simfun(!e.disjuncts))
if lists_match(l, e.disjuncts) then e else pattern(l, e.name)

<simplify disjunct>= (<-U)
c := simfun(e.conditions)
if member(\c, 0) then fail
else {
  l := []; every put(l, vanishing_latent_patlabel ~=== simfun(!e.sequents))
  if lists_match(l, e.sequents) then l := e.sequents
  if ss := !l & type(ss) == "sequent" &
     cc := !ss.constraints & type(cc) == "constraint" & cc.lo >= cc.hi 
  then
    fail # this disjunct can't match -- eliminate it
  if c === e.conditions & l === e.sequents then e else disjunct(l, e.name, c)
}

<simplify adisjunct>= (<-U)
c := simfun(e.conditions)
if member(\c, 0) then fail
else {
  l := simfun(e.aconstraints)
  if cc := !l & type(cc) == "constraint" & cc.lo >= cc.hi then
    fail # this disjunct can't match -- eliminate it
  if c === e.conditions & l === e.aconstraints then e ### & a === e.answers then e 
  else adisjunct(l, e.name, c, e.length, e.patlabelbindings) ### , a)
}

<simplify set of conditions>= (<-U)
s := set()
every x := simfun(!e) do {
  if type(x) == "eqn" then {
    if      x.op == "="  & x.left === x.right then x := 1
    else if x.op == "!=" & x.left === x.right then x := 0
  }
  insert(s, x) 
}
delete(s, 1)
return if member(s, 0) then set([0])
       else if sets_match(e, s) then e
       else if *s = 0 then &null
       else s       

<simplify instance's argument table>= (<-U)
every k := key(e.argt) do e.argt[k] := simfun(e.argt[k])
e

<simplify tag case's arm table>= (<-U)
every k := key(e.arms) do e.arms[k] := simfun(e.arms[k])
e

<simplify table>= (<-U)
m := copy(e)
every k := key(e) do {
  m[k] -:= e[k]
  add_to_table(m, simfun(k), e[k])
}
every k := key(m) & m[k] = 0 do delete(m, k)
if *m > 1 then
  return if tables_match(m, e) then e else m
else
  return if !m = 1 then key(m) else if key(m) === 1 then !m else m

<simplify equation>= (<-U)
l := simfun(e.left)
r := simfun(e.right)
if exps_eq(l, r) then 
  if e.left === 0 & e.right === 0 then e
  else eqn(0, e.op, 0) 
else if simfun === super_simplify & # not safe for decoding! see bugs{nnn}
        ( (type(l) == "Enarrows", type(r) == "Eslice",   r.lo = 0) |
          (type(l) == "Eslice",   type(r) == "Enarrows", l.lo = 0) ) & 
        l.n = r.n & exps_eq(l.x, r.x)
     then
       simfun(Efitss(l.x, l.n))
else 
  if e.left === l & e.right === r then e
  else eqn(l, e.op, r)

<simplify if statement>= (<-U)
a := simp_arms(e.arms, simfun)
if *a = 0 then Sepsilon()
else if *a = 1 & guard_always_satisfied(a[1].guard) then a[1].x
else if a === (e.arms) then e
else Sif(a)

<*>+= [<-D->]
procedure simp_arms(earms, simfun)
  local arms
  l := []
  arms := copy(earms)
  while a := get(arms) & g := simfun(a.guard) do
    if guard_always_satisfied(g) then { # always take this arm
      c := simfun(a.x)
      put(l, if exps_eq(g, a.guard) & exps_eq(c, a.x) then a else Sguarded(g, c))
      return if lists_match(l, earms) then earms else l
    } else if not case type(g) of {
      "integer" : g = 0
      "set"     : member(g, 0)
    } then { # sometimes take this arm
      c := simfun(a.x)
      put(l, if exps_eq(g, a.guard) & exps_eq(c, a.x) then a else Sguarded(g, c))
    } 
  return if lists_match(l, earms) then earms else l
end
Defines simp_arms (links are to index).

<*>+= [<-D->]
procedure guard_always_satisfied(g)
  return case type(g) of {
      "integer" : g = 1
      "set"     : *g = 0
      "null"    : &null
  } 
end
Defines guard_always_satisfied (links are to index).

<rewrite rules>= [D->]
Eorb(0, x) -> x
Eorb(x, 0) -> x
Eorb(N, M) -> ior(N, M)
Eorb(Eorb(x, N), M) -> Eorb(x, ior(N, M))
Eorb(N, x) -> Eorb(x, N)
Eand(1, x) -> x
Eand(0, _) -> 0
Eand(x, 1) -> x
Eand(_, 0) -> 0
Eand(x, y) ->
  if type(x) == "set" & *x = 0 then y
  else if type(x) == "set" & *y = 0 then x
  else e
Eslice(N, lo, n) -> iand(ishift(N, -lo), 2^n-1)

<super rewrite rules>= [D->]
Eslice(Eshift(x, n), m, k) -> 
  if m - n >= 0 then Eslice(x, m-n, k)
  else Eslice(Eshift(x, n-m), 0, k)
Eslice(y as Enarrowu(x, n), 0, m) -> if n <= m then y else e
Eslice(y as Enarrows(x, n), 0, m) -> if n <= m then y else e
Eslice(Eslice(x, l1, n1), l2, n2) -> 
  if l2 >= n1 then 0 else Eslice(x, l1+l2, if n2 < n1-l2 then n2 else n1-l2)
Eslice(y as Einstance_input(x, c, name), 0, n) ->
  if ipt := inputs_of(c) & ipt.name == name & case type(ipt.meaning) of {
    "field" : fwidth(ipt.meaning) <= n
  } then y else e
Eslice(x, 0, n) -> if n = wordsize then x else e

<rewrite rules>+= [<-D->]
Eshift(x, 0) -> x
Eshift(N, n) -> ishift(N, n)
Enarrowu(N, n) -> if 0 <= N < 2^n then N else Efail(expimage(e))

<super rewrite rules>+= [<-D->]
Enarrowu(y as Eslice(x, lo, n), m) -> if n <= m then y else e
Enarrowu(x, M) -> if M >= wordsize then x else e

<rewrite rules>+= [<-D->]
Ewiden(N, n) -> 
  if (iand(N,2^(n-1)) = 0) then iand(N,2^n-1) 
  else ior(iand(2^wordsize-1,icom(2^n-1)),N)
Enarrows(N, n) -> 
  if -(2^(n-1)) <= N < 2^(n-1) then iand(N,2^n-1) else Efail(expimage(e))

<super rewrite rules>+= [<-D->]
Ewiden(x, n) -> if n = wordsize then x else e
Enarrows(y as Eslice(x, lo, n), m) -> if n < m then y else e

<rewrite rules>+= [<-D->]
Enarrows(Ewiden(x, n), m) -> if n = m then x else e
Enarrows(y as Enarrows(x, n), m) -> if n = m then y else e

Note we can't rewrite Ewiden(Enarrows(x, N), N) as x because there's no way to pick up Efitss(x, N). Ugh. 

<super rewrite rules>+= [<-D->]
Enarrows(x, M) -> if M >= wordsize then x else e
Ediv(N, M) -> if N > 0 then N / M else (N - M + 1) / M  # force toward - infinity

<super rewrite rules>+= [<-D->]
Ediv(x, N) -> simfun(Eshift(x, - exactlog2(N))) | e

<rewrite rules>+= [<-D->]
Emod(N, M) -> {x := integer(N % M); while x < 0 do x +:= M; x}

<super rewrite rules>+= [<-D]
Emod(x, N) ->
  if x := strip_const_multiple_N(x, N) then
    simfun(Eslice(x, 0, exactlog2(N))) | Emod(x, N)
  else
    simfun(Eslice(x, 0, exactlog2(N))) | e

This procedure helps optimize the constant term out of modulus expressions. 

<*>+= [<-D->]
procedure strip_const_multiple_N(x, N) 
  local y
  if type(x) == "table" & x[1] ~= 0 & x[1] % N = 0 then {
    y := copy(x)
    y[1] := 0
    return y
  }
end
Defines strip_const_multiple_N (links are to index).

<rewrite rules>+= [<-D->]
Efitsu(N, m) -> if 0 <= N < 2^m then 1 else 0
Efitsu(Enarrowu(x, n), m)   -> if n <= m then 1 else e
Efitsu(Enarrows(x, n), m)   -> if n <= m then 1 else e
Efitsu(Eslice(x, lo, n), m) -> if n <= m then 1 else e
Efitsu(y as Einstance_input(_, _, _), m) -> 
  if known_to_fit(input_fitsu, y, &null, m) then 1 else e
Efitsu(Eshift(x, n), m)     -> simfun(Efitsu(x, m-n))
Efitsu(x, M) -> if M >= wordsize then 1 else e
Efitss(N, m) -> if -(2^(m-1)) <= N < 2^(m-1) then 1 else 0
Efitss(Enarrowu(x, n), m)   -> if n < m then 1 else e
Efitss(Enarrows(x, n), m)   -> if n < m then 1 else e
Efitss(Eslice(x, lo, n), m) -> if n < m then 1 else e
Efitss(Ewiden(Eslice(x, lo, n), m), mm) -> 
  if n = m <= mm then 1 
  else if lo > 0 then simfun(Efitss(Ewiden(Eslice(x, 0, n+lo), m+lo), mm+lo))
  else e
Efitss(y as Einstance_input(_, _, _), m) -> 
  if known_to_fit(input_fitss, y, &null, m) then 1 else e
Efitss(Eshift(x, n), m)     -> simfun(Efitss(x, m-n))
Efitss(x, M) -> if M >= wordsize then 1 else e
Eforce(x as Eforce(_)) -> x
Eforce(N) -> N
Eforceable(N) -> 1
Enot(N) -> if N = 0 then 1 else 0
Enot(Enot(x)) -> x

See eliminate_instances for an explanation of why the transformations below are no longer implemented as rewrite rules. 

<former rewrite rules now implemented by eliminate_instances>=
Einstance_tagged(Einstance(c, a), c2, uid) -> if c === c2 then 1 else 0
Einstance_input(Einstance(c, a), c2, name) -> if c === c2 then a[name] 
                                              else Efail(expimage(e))
Einstance_tagged(Ewildcard(_), _, _) -> 1
Einstance_input(Ewildcard(iname), c, fname) ->
   Ewildcard(iname || "." || c.name || "." || fname)
latent_patlabel(Einstance(_, _)) -> vanishing_latent_patlabel
latent_patlabel(Ewildcard(nam)) -> patlabel(nam, nam)

<rewrite rules>+= [<-D]
Sstmts(l) -> case *l of { 0 : Sepsilon(); 1: l[1]; default : e }

<*>+= [<-D->]
procedure exactlog2(n)
  local log
  log := 0
  while 2^log < n do log +:= 1
  if n = 2^log then return log else fail
end
Defines exactlog2 (links are to index).

Imaging

expimage prints a readable form of an expression. It is used only for diagnostic purposes; a separate procedure is used to produce C (or Modula-3) code that implements an expression. 
<*>+= [<-D->]
procedure expimage(e, pp, precedence, associativity)
  local leadingsign, prefix
  static nopp
  initial {<initialize prec and assoc>
           <initialize nopp>}
  /pp := nopp
  /precedence := 0
  /associativity := "L"
  return case type(e) of {
    <cases for expimage>
    default    : (proc(type(e) || "image") | image)(e)
  }
end
Defines expimage (links are to index).

expimage can optionally use a prettyprinter, but by default it uses none. 

<*>+= [<-D->]
record ppspec(be, en, in, ou, nl, on, cn) # { } t b m o c
Defines ppspec (links are to index).

<initialize nopp>= (<-U)
nopp := ppspec("", "", "", "", "", "", "")

<*>+= [<-D->]
procedure ppexpimage(e)
  static pp
  initial pp := ppspec("${", "$}", "$t", "$b", "$n", "$o", "$c")
  return expimage(e, pp)
end
Defines ppexpimage (links are to index).

<cases for expimage>= (<-U) [D->]
"arm" : pp.in || "| @" || e.file || ":" || e.line || ": " || pp.be ||
        expimage(e.pattern, pp) || pp.en || " => " || pp.cn || expimage(e.code, pp) ||
        pp.ou 

<cases for expimage>+= (<-U) [<-D->]
"pattern"  : if *e.disjuncts > 0 then {
               s := commaseparate(maplist3(expimage, e.disjuncts, pp, prec["|"]),
                                  " " || pp.cn || "| ")
               bracket(s, pp, "|", precedence) ### || ("[[" || \e.name || "]]" | "")
             } else "<NOMATCH>"

<cases for expimage>+= (<-U) [<-D->]
"disjunct" : { s := "(" || (if \e.name then e.name else "?noname?") || ") " 
               s ||:= if *\e.conditions > 0 then
                      "{" || pp.be || expimage(e.conditions, pp) || pp.en || "} => " ||
                      pp.in || pp.cn
                    else ""
               s ||:= if *e.sequents = 0 then "epsilon"
                      else { 
                        prefix := ""
                        every i := 1 to *e.sequents do {
                          s ||:= prefix || expimage(e.sequents[i], pp, prec[";"])
                          prefix := 
                            (if type(e.sequents[i]) == ("patlabel"|"latent_patlabel") 
                             then ": " 
                             else "; ") || pp.on
                        }
                      }
               s ||:= if *\e.conditions > 0 then pp.ou else ""
               bracket(s, pp, ";", precedence) ### || ("[" || \e.name || "]" | "")
             }

<cases for expimage>+= (<-U) [<-D->]
"adisjunct" : {  s := "(" || (if \e.name then e.name else "?noname?") || ") " 
                 s ||:= if \e.patlabelbindings then {
                  "[" || pp.in || pp.be || bindingimage(e.patlabelbindings, pp) || 
                         pp.en || pp.ou || "] " || pp.cn
                } else ""
                s ||:= if *\e.conditions > 0 then
                      "{" || pp.be || expimage(e.conditions, pp) || pp.en || "} => " ||
                      pp.in || pp.cn
                    else ""
               s ||:= "LENGTH = " || expimage(e.length) || ", "
               s ||:= if *e.aconstraints = 0 then "<MATCH>"
                      else commaseparate(maplist3(expimage, e.aconstraints, pp, prec["&"]),
                                      " & " || pp.on)
               s ||:= if *\e.conditions > 0 then pp.ou else ""
###               if *\e.answers > 0 then {
###                 l := []
###                 every k := key(e.answers) do
###                   put(l, k || " = " || expimage(e.answers[k], pp, prec["="]))
###                 s ||:= pp.in || pp.on || "{" || pp.in || pp.be ||
###                     commaseparate(l, ", " || pp.cn) || pp.en || pp.ou || "}" || pp.ou
###               }               
               bracket(s, pp, "&", precedence)
             }

<*>+= [<-D->]
procedure bindingimage(t, pp)
  local sep, id
  sep := ""
  s := ""
  every id := key(t) do {
    s ||:= sep || pp.be || id || " -> " || expimage(t[id], pp) || pp.en
    sep := ", " || pp.on
  }
  return s
end
Defines bindingimage (links are to index).

<cases for expimage>+= (<-U) [<-D->]
"sequent"  : { s := if *e.constraints = 0 then "some " || e.class.name
                    else commaseparate(maplist3(expimage, e.constraints, pp, prec["&"]),
                                       " & " || pp.on)
               pp.be || bracket(s, pp, "&", precedence) || pp.en
             }
"patlabel"        : \e.name | e.original_name || "#" || image(e)[17:-3] ||
                    ("@" || \e.offset | "") || ":"
"latent_patlabel" : "(?" || expimage(e.instance, pp, prec[","]) || ":)"
"dots_sequent"    : "..."
"constraint"      : bracket(stringininterval(expimage(e.field, pp, prec["="]), 
                                             e.lo, e.hi), pp, "=", precedence)
"fieldbinding"    : { s := expimage(e.field) || " = " || expimage(e.code, pp,prec["="])
                      bracket(s, pp, "=", precedence)
                    }
"field"  : e.name
"absolute_field" : "{" || expimage(e.field) || " at " || e.offset || "}"

<cases for expimage>+= (<-U) [<-D->]
"binding_instance" : expimage(e.val) || " : " || expimage(e.type)
"constype" : "constructor-type " || e.name

<cases for expimage>+= (<-U) [<-D->]
"list"     : commaseparate(maplist3(expimage, e, pp, prec[","]), ", " || pp.on)
"set"      : commaseparate(maplist3(expimage, sort(e), pp, prec[","]), ", " || pp.on)
"eqn"      : bracket(expimage(e.left, pp, prec["="]) || " " || e.op || " " || pp.on || 
                     expimage(e.right, pp, prec["="]), pp, "=", precedence)
"table"    : {                      # standard normal form
    <make s represent table e, but elide additive and multiplicative units>
    pp.in || pp.be || s || pp.en || pp.ou
  }
"string"   : e
"literal"  : image(e.s)
"integer"  : string(e)
"null"     : image(e)

The old version printed in any old order, but the new version prints positive terms first, then negative terms, with the constant term last in its group. 

<make s represent table e, but elide additive and multiplicative units>= (<-U)
{
  s := ""; leadingsign := ""
  <add positive terms to s>
  leadingsign := " - " || pp.on
  <add negative terms to s>
  s := if s == "" then "0" else bracket(s, pp, "+", precedence)
}

<add positive terms to s>= (<-U)
every e[k := 1 ~=== key(e)] > 0 do {
    s ||:= leadingsign 
    s ||:= (1 ~= abs(e[k])) || "*"    # print coefficient if not 1
    s ||:= expimage(k, pp, prec["+"])
    leadingsign := " + " || pp.on
}
if e[1] > 0 then s ||:= leadingsign || string(e[1])

<add negative terms to s>= (<-U)
every e[k := 1 ~=== key(e)] < 0 do {
    s ||:= leadingsign 
    s ||:= (1 ~= abs(e[k])) || "*"    # print coefficient if not 1
    s ||:= expimage(k, pp, prec["+"])
}
if e[1] < 0 then s ||:= leadingsign || string(-e[1])


<old make s represent table e, but elide additive and multiplicative units>=
{
  # print constant term if nonzero
  if e[1] ~= 0 then { s := string(e[1]) ; leadingsign := " + " || pp.on }
  else s := leadingsign := ""
  # print every nonconstant term k
  every k := 1 ~=== key(e) do {
      s ||:= if e[k] < 0 then " - " else leadingsign
      leadingsign := " + " || pp.on
      s ||:= (1 ~= abs(e[k])) || "*"    # print coefficient if not 1
      s ||:= expimage(k, pp, prec["+"])
  }
  s := if s == "" then "0" else bracket(s, pp, "+", precedence)
}

<cases for expimage>+= (<-U) [<-D->]
"Eorb"     : { s := expimage(e.x, pp, prec["Eorb"], "L")
               t := expimage(e.y, pp, prec["Eorb"], "R")
               bracket(s || " ORB " || pp.on || t, pp, "Eorb", precedence)
             }
"Eand"     : { s := expimage(e.x, pp, prec["Eand"], "L")
               t := expimage(e.y, pp, prec["Eand"], "R")
               bracket(s || " AND " || t, pp, "Eand", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Eslice"   : { s := expimage(e.x, pp, prec["Eslice"]) 
               s ||:= "[" || e.lo || ":" || (e.lo + e.n - 1) || "]"
               bracket(s, pp, "Eslice", precedence)
             }
"Eshift"   : { s := expimage(e.x, pp, prec["Eshift"]) 
               s ||:= if e.n < 0 then (" >> " || -e.n) else (" << " || e.n)
               bracket(s, pp, "Eshift", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Enarrowu" : { s := expimage(e.x, pp, prec["Enarrowu"]) 
               s ||:= "[" || e.n || "]"
               bracket(s, pp, "Enarrowu", precedence)
             }
"Enarrows" : { s := expimage(e.x, pp, prec["Enarrows"]) 
               s ||:= "[" || e.n || "!]"
               bracket(s, pp, "Enarrows", precedence)
             }
"Ewiden"   : { s := expimage(e.x, pp, prec["Ewiden"]) 
               s ||:= "!" || e.n
               bracket(s, pp, "Ewiden", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Ediv"     : { s := expimage(e.x, pp, prec["Ediv"]) 
               s ||:= " DIV " || e.n
               bracket(s, pp, "Ediv", precedence)
             }
"Emod"     : { s := expimage(e.x, pp, prec["Emod"]) 
               s ||:= " MOD " || e.n
               bracket(s, pp, "Emod", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Semit"    : commaseparate(maplist3(expimage, e.x, pp, prec[","]), ";" || pp.cn)
"Stoken"   : { s := "EMIT@" || e.offset || "(" || pp.in || 
                    expimage(e.x, pp, prec[","]) || ", " || 
                    pp.on || e.n || ")" || pp.ou
               bracket(pp.cn || s, pp, "app", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Efitsu"   : { s := "FITSU(" || expimage(e.x, pp, prec[","]) || ", " || pp.on || e.n||")"
               bracket(s, pp, "app", precedence)
             }
"Efitss"   : { s := "FITSS(" || expimage(e.x, pp, prec[","]) || ", " || pp.on ||e.n ||")"
               bracket(s, pp, "app", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Epatlabel" : "LOCATION_OF(" || expimage(e.l, pp, prec[","]) || ")" 

<cases for expimage>+= (<-U) [<-D->]
"Eforce"   : { s := "FORCE(" || expimage(e.x, pp, prec[","]) || ")"
               bracket(s, pp, "app", precedence)
             }
"Eforceable":{ s := "FORCEABLE(" || expimage(e.x, pp, prec[","]) || ")"
               bracket(s, pp, "app", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Epc"       : "FORCE(<program counter>)"
"Epc_known" :" FORCEABLE(<program counter>)"

<cases for expimage>+= (<-U) [<-D->]
"Enot"      : { s := "NOT " || expimage(e.x, pp, prec["NOT"])
                bracket(s, pp, "NOT", precedence)
              }

<cases for expimage>+= (<-U) [<-D->]
"Enosimp"   : expimage(e.x, pp, precedence, associativity)

<cases for expimage>+= (<-U) [<-D->]
"Sstmts"    : pp.in || pp.be || "{ " || pp.cn || 
              commaseparate(maplist3(expimage, e.x, pp), "; " || pp.cn) ||
              pp.ou || pp.cn || " }" || pp.en

<cases for expimage>+= (<-U) [<-D->]
"Einstance" : { l := []; 
                every i := inputs_of(e.cons) do
                  put(l, expimage(e.argt[i.name], pp))
                s := e.cons.name || "(" || commaseparate(l, ", " || pp.on) || ")"
                bracket(s, pp, "app", precedence)
              }
"Einstance_input" : { 
               s := expimage(e.x, pp, prec["."]) || "." || e.cons.name || "." || e.name
               bracket(s, pp, ".", precedence)
             }
"Einstance_tagged" : { 
               s := expimage(e.x, pp, prec["="]) || " IS " || e.cons.name 
               bracket(s, pp, "=", precedence)
             }
"Ebinding_instance" : e.name || " : " || e.type.name

<cases for expimage>+= (<-U) [<-D->]
"Sif"      : { s := pp.cn || "if"
               every s ||:= 
                 pp.cn || ":: " || pp.in || expimage(!e.arms, pp, prec["low"]) || pp.ou
               bracket(s || " " || pp.cn || "fi", pp, "app", precedence)
             }
"Sguarded" : { s := expimage(e.guard, pp, prec["Sguarded"]) || " -> " || 
                    pp.in || pp.be || pp.cn ||
                    expimage(e.x,     pp, prec["Sguarded"]) ||
                    pp.en || pp.ou
               bracket(s, pp, "Sguarded", precedence)
             }

<cases for expimage>+= (<-U) [<-D->]
"Stagcase" : { s := "CASE " || expimage(e.x, pp) || " OF "
              every c := kept_constructors(e.type) do
                s ||:= pp.nl || "| " || c.name || " => " || pp.in || pp.in || pp.be ||
                          pp.cn || expimage(e.arms[c], pp) || pp.en || pp.ou || pp.ou 
              pp.be || pp.cn || s || pp.nl || "END (* " || expimage(e.x, pp) ||
                  " *)" || pp.en || pp.on
            }

<cases for expimage>+= (<-U) [<-D->]
"Sfail"    : { s := "FAIL(" || image(if *pp.nl > 0 then escape_dollars(e.fmt) else e.fmt)
               every a := e.a1 | e.a2 | e.a3 do 
                 s ||:= ", " || pp.on || expimage(\a, pp, prec[","])
               s := pp.in || pp.be || s || ")" || pp.en || pp.ou
               bracket(s, pp, "app", precedence)
             }
"Sepsilon" : "/* skip */"

<cases for expimage>+= (<-U) [<-D->]
"Efail"    : "[BAD EXP: " || e.msg || "]"

<cases for expimage>+= (<-U) [<-D->]
"Glines"    : commaseparate(maplist2(expimage, e.x, pp), "\n")
"Gresynch"  : "#line " || e.line  || " " || image(\e.file | "generated-code")
"Gblock"    : { s := "{ " || pp.be || pp.in || pp.cn
                every s ||:= expimage(!e.decls, pp) || "; " || pp.nl
                every s ||:= expimage(!e.stmts, pp) || "; " || pp.cn
                s || pp.ou || pp.cn || "}" || pp.en
              }
"Gdecl"     : { s := pp.be || expimage(e.type, pp) || " " || e.name 
                s ||:= " = " || pp.in || pp.cn || expimage(\e.init, pp) || pp.ou
                s || pp.en
              }

<cases for expimage>+= (<-U) [<-D->]
"Gcase"     : { s := "CASE " || expimage(e.x, pp) || " OF "
                every s ||:= expimage(!e.arms, pp)
                pp.be || pp.cn || s || pp.nl || "END (* CASE " || expimage(e.x, pp) ||
                  " *)" || pp.en || pp.on
               }
"Gcasearm"  : { s := pp.nl || "| " || pp.in
                every i := 1 to *e.tags by 2 do {
                  if i > 1 then s ||:= ", " || pp.on
                  s ||:= if e.tags[i] + 1 = e.tags[i+1] then e.tags[i] 
                         else e.tags[i] || ".." || (e.tags[i+1]-1)
                } 
                s ||:= " => "  || pp.in || pp.cn || expimage(e.x, pp)
                pp.be || s || pp.ou || pp.ou || pp.en
              }
"Ginrange"  : bracket(pp.in || e.lo || " <= " || pp.on || 
                         expimage(e.x, pp, prec["<="]) || " < " || e.hi, 
                      pp, "<", precedence)
"Gcomment"  : "(* COMMENT : " || e.s || " *)"
"Gcommented" : expimage(e.e, pp)

<cases for expimage>+= (<-U) [<-D->]
"Gasgn"     : bracket(e.lhs || " := " || expimage(e.x, pp, prec[":="]), 
                      pp, ":=", precedence)
"Gsetname"  : e.lhs || " := " || image(e.name)
"Gnomatch"  : "<NO MATCH>"
"Tunsigned" : { s := "unsigned"
                s ||:= " /* " || \e.width || " bits */"
                s
              }

<cases for expimage>+= (<-U) [<-D->]
"Eapp" : image(e.f) || "(" || pp.in || expimage(e.args, pp, prec[","]) || pp.ou || ")"

<cases for expimage>+= (<-U) [<-D]
"Eclosure" : "CLOSURE(" || pp.in || pp.be || pp.cn || 
               "type = " || e.ty || ", " || pp.cn || 
               "fun = " ||  e.fun || ", " || pp.cn || 
               "header = " ||  e.headertype || ", " || pp.cn || 
               "values = {" || expimage(e.values) || "}, " || pp.cn || 
               "addresses = {" || expimage(e.addresses) || "}" || pp.en || pp.ou || ")"
"Elambda" : pp.be || "(FN " || commaseparate(e.formals) || " => " || pp.in || pp.on ||
               expimage(e.body, pp, prec[","]) || ")" || pp.ou || pp.en
"Eclosure_loc"  : "CL->loc"
"Eclosure_addr" : "CL->a" || e.n
"Eclosure_val"  : "CL->v" || e.n

<*>+= [<-D->]
global prec, assoc
procedure bracket(s, pp, op, p, a)
  /a := "L"
  return pp.be || (if prec[op] > p | (prec[op] = p & assoc[p] == a) then s
                   else "(" || s || ")") || pp.en
end
Defines assoc, bracket, prec (links are to index).

<initialize prec and assoc>= (<-U)
ops := ["N", ["low"],
        "L", ["|", "pattern"],
        "L", [";"],
        "L", ["&", "sequent", "patlabel"],
        "R", [":="],
        "L", [","],
        "N", ["Sguarded"],
        "N", ["="],
        "L", ["ORB", "Eorb"], 
        "L", ["AND", "Eand"],
        "L", ["<", "<="],
        "L", ["+"],
        "N", ["Emod", "Ediv", "*"],
        "N", ["Eshift"],
        "N", ["NOT"],
        "L", ["Eslice", "Enarrowu", "Enarrows", "Ewiden", "."],
        "N", ["app"],           # function application
        "N", ["high"]
       ]
prec := table([])  # missed lookups break arithmetic comparisons
assoc := table()
every i := 1 to *ops by 2 do {
  every prec[!ops[i+1]] := i
  assoc[i] := ops[i]
}


<*>+= [<-D->]
procedure escape_dollars(s)
  r := ""
  s ? {
    while r ||:= tab(upto('$')) do { ="$"; r ||:= "$$" }
    return r || tab(0)
  }
end
Defines escape_dollars (links are to index).

Semantic functions

binop implements the semantics of binary operators. It modifies its inputs and returns e1, so it should be used only during parsing. 
<*>+= [<-D->]
procedure binop(e1, op, e2) 
  e1 := term2table(e1)
  e2 := term2table(e2)
  case op of {
    "+" : every v := key(e2) do e1[v] +:= e2[v]
    "-" : every v := key(e2) do e1[v] -:= e2[v]
    "*" : if n2 := constant(e2) then {
              every !e1 *:= n2
          } else if n1 := constant(e1) then {
              every !e2 *:= n1
              e1 := e2
          } else error("multiplication must be by constants only")
    "/" : error("division is not permitted in this language")
  }
  return e1
end
Defines binop (links are to index).

<*>+= [<-D->]
procedure term2table(x)
  return case type(x) of {
    "table"   : x
    "integer" : 1(e := table(0), e[1] := x)
    default   : 1(e := table(0), e[x] := 1)
  }
end
Defines term2table (links are to index).

addconst is nondestructive. 

<*>+= [<-D->]
procedure addconst(e, n)
  if n = 0 then return e
  if type(e) == "table" then
    t := copy(e)
  else {
    t := table(0)
    if type(t) == "integer" then t[1] := e else t[e] := 1
  }
  t[1] +:= n
  return t
end
Defines addconst (links are to index).

It is necessary to identify a constant in normal form. 

<*>+= [<-D->]
procedure constant(e)
  if type(c := untable(e)) == "integer" then return c
end
Defines constant (links are to index).

<*>+= [<-D->]
procedure untable(e)
  return if type(e) ~== "table" then e else {
    n := 0
    every k := key(e) & e[k] ~= 0 do n +:= 1
    case n of {
      0       : 0
      1       : if k := key(e) & e[k] = 1 then k 
                else if e[1] ~= 0 then e[1]
                else e
      default : e
    }
  } 
end
Defines untable (links are to index).

Creation

mkslice is used only to create slices from actual specifications, in which the bit numbering could change. 
<*>+= [<-D->]
procedure mkslice(x, lo, hi)
  local n # size of range
  if lo < 0 then error("Can't take negative bit slice!!")
  if hi <= lo then error(expimage(x), "[", lo, ":", hi - 1, "] has no bits!")
  if hi > bitsizeof(x) then
    error(if type(f := symtab[x]) == "field" then "Field " || f.name 
          else "Host machine", 
             " has only ", bitsizeof(x), " bits")
  bit_numbering_used := 1
  <if needed, flip lo and hi>
  return Eslice(x, lo, hi - lo)
end
Defines mkslice (links are to index).

<if needed, flip lo and hi>= (<-U)
if /bit_zero_is_lsb then {
  lo := bitsizeof(x) - hi
  hi := bitsizeof(x) - lo
}

<*>+= [<-D->]
procedure bitsizeof(f)
  return case type(symtab[f]) of {
      "field" : fwidth(symtab[f])
      default : wordsize
    }
end
Defines bitsizeof (links are to index).

<*>+= [<-D->]
procedure fwidth(f)
  return f.hi - f.lo
end
Defines fwidth (links are to index).

<*>+= [<-D->]
procedure mkshift(x, n)
  return if n = 0 then x else 
         ishift(\simp & constant(x), n) | Eshift(x, n)
end
Defines mkshift (links are to index).

<*>+= [<-D->]
record bogus(e) # ditch invalid field name complaint
Defines bogus (links are to index).

flatten is used to flatten the argument lists of binary associative operators like Eorb and Eand. 

<*>+= [<-D->]
procedure flatten(e, ty, l)
  /l := []
  return if type(e) == ty then 
    flatten(e.x, ty, flatten(e.y, ty, l))
  else
    push(l, e)
end
Defines flatten (links are to index).

Unflatten takes the list and the operator and turns it back into a tree. 

<*>+= [<-D]
procedure unflatten(l, rator, zero)
  if *l = 0 then return zero
  else {
    x := l[1]
    every x := rator(x, l[2 to *l])
  }
  return x
end
Defines unflatten (links are to index).