<*>= [D->] procedure emit_tokenized_closure_functions(pp, cons, b) pushtrace("TCLOS") every cl := subterms_matching(b, "Sclosure") do emit_tokenized_functions_of_closure(pp, cons, cons.name, cl) poptrace() return end
Definesemit_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) else 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))) return end
Definesclosure_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 Sguarded(1, 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 ofclo
(and placeholder) tocl.creation
and return width> return end
Definesemit_tokenized_closure_function
(links are to index).
<add creation ofclo
(and placeholder) tocl.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 put(cl.creation.alloc, if offset = 0 then literal(template_to_list("create-closure.t", "name", clo.ty, "clofun", clo.fun, "uses-pc", upc, "save", l)) else literal(template_to_list("create-closure-at.t", "name", clo.ty, "clofun", clo.fun, "uses-pc", upc, "save", l, "offset", offset))) <add placeholder forseq
tocl.creation.emit
>
This is really dreadful, but I don't have time to be clean.
<add placeholder forseq
tocl.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 ", seq.class.name)
<*>+= [<-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 end
Definesconditions_applying_to
(links are to index).
<*>+= [<-D] procedure free_variable_set(x) s := set() every insert(s, free_variables(x)) return s end
Definesfree_variable_set
(links are to index).