Token-based closures

The major difference is that we split disjuncts into individual sequents (tokens) and handle the sequents one by one.
<*>= [D->]
procedure emit_tokenized_closure_functions(pp, cons, b)
  every cl := subterms_matching(b, "Sclosure") do
    emit_tokenized_functions_of_closure(pp, cons,, cl) 
Defines emit_tokenized_closure_functions (links are to index).

We really ought to add a string type to the closure, so that we could give the name of the constructor when conditions aren't satisfied in the closure. As it is, I use the same error message for each constructor---otherwise they won't all use the same closure function!

To have some prayer of getting the PC right, I split creation into alloc and emit.

<*>+= [<-D->]
record closure_creation(alloc, emit)
procedure emit_tokenized_functions_of_closure(pp, cons, name, cl)
  local latevars, offset
  latevars := set()
  every insert(latevars, inputs_of(cons, "string").name)
  cl.creation := closure_creation([], [])
  offset := 0
  every s := !cl.disjunct.sequents & type(s) == "sequent" do {
    if subterms_matching(s, "Eforce") then # was member(latevars, free_variables(s)) 
      emit_tokenized_closure_function(pp, cons, name, cl, latevars, s, offset)
      put(cl.creation.emit, sequent_to_Stoken(s, offset))
    offset := cl.creation.emit[-1].offset + cl.creation.emit[-1].n
  cl.creation := Sstmts(put(cl.creation.alloc, Semit(cl.creation.emit)))
Defines closure_creation, emit_tokenized_functions_of_closure (links are to index).

Because a single sequent can have a placeholder of multiple sequents, we can't just continually add the last n to the offset. Ugh. This procedure comes from some very fast and loose inline expansion of disjunct_to_emission. There must be a more careful and intelligent way to do things.

I hack things to make the offset always look like zero in the closure body. This enables more sharing, but I have to compensate by adjusting the PC when I create the closure.

<*>+= [<-D->]
procedure emit_tokenized_closure_function(pp, cons, name, cl, latevars, seq, offset)
  local selections, selected, free, save, upc, clo, subst, body, lconds
  lconds := conditions_applying_to(\cl.conditions, seq) | &null
  if offset > 0 then {
    lconds := subst_for_pc(lconds, binop(the_global_pc, "-", offset))
    seq    := subst_for_pc(seq,    binop(the_global_pc, "-", offset))
  body := 
     super_simplify(Sif([Sguarded(lconds, Semit([sequent_to_Stoken(seq, 0)])),
        ### sequent_to_Stoken should be changed to include width conditions &c
                            Sfail("Conditions not satisfied for unnamed constructor"))
  p := hoist(pp, Elambda(sort(latevars), body), latevars)
  clo := p.e # is a closure
  clo := apply_subst(clo, p.sigma)
  free := set(); every insert(free, free_variables(clo))
  free := sort(free)
PPwrite(pp, "/****************")
PPxwrite(pp, "CLOSURE IS:$t $o", ppexpimage(clo), "$b")
PPwrite(pp, "****************/")
  <add creation of clo (and placeholder) to cl.creation and return width>
Defines emit_tokenized_closure_function (links are to index).

<add creation of clo (and placeholder) to cl.creation and return width>= (<-U)
l := []
every i := 1 to *clo.values do
  put(l, pretty(Gasgn(Eclosure_val(i),  clo.values[i])) || "$n")
every i := 1 to *clo.addresses do
  put(l, pretty(Gasgn(Eclosure_addr(i), clo.addresses[i])) || "$n")
upc := if subterms_matching(\lconds | seq, "Epc", "Epc_known") then 1
       else 0
  if offset = 0 then 
    literal(template_to_list("create-closure.t", "name", clo.ty, "clofun",, 
                             "uses-pc", upc, "save", l))
    literal(template_to_list("create-closure-at.t", "name", clo.ty, "clofun",, 
                             "uses-pc", upc, "save", l, "offset", offset)))
<add placeholder for seq to cl.creation.emit>

This is really dreadful, but I don't have time to be clean.

<add placeholder for seq to cl.creation.emit>= (<-U)
d := disjunct_to_emission(place_holder(disjunct([seq])), offset)
every put(cl.creation.emit, !d.x)

<complain if /seq.class.holder>=
if /seq.class.holder then
    error("No placeholder is defined for class ",
<*>+= [<-D->]
procedure conditions_applying_to(conds, seq)
  local applying
  applying := copy(conds)
  every c := !applying & f := free_variable_set(c) do
    if member(f, free_variables(seq)) then &null else delete(applying, c)
  return if *applying = 0 then &null else applying
Defines conditions_applying_to (links are to index).

<*>+= [<-D]
procedure free_variable_set(x)
  s := set()
  every insert(s, free_variables(x))
  return s
Defines free_variable_set (links are to index).