# 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_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.
```
```<*>+= [<-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
"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_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).

```<*>+= [<-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).

```<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).

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

```<basic cases for simplification>= (<-U <-U)
"eqn"      : {<simplify equation>}
"pattern"  : {<simplify pattern>}
"disjunct" : {<simplify disjunct>}
"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]
}
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
```
```<*>+= [<-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)
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 ||:= (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 ||:= (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 ||
"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_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->]
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).

```<*>+= [<-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).

```<*>+= [<-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).