Using bound variables in quotations

[phlegmaticprogrammer]

Let's assume you want to programmatically construct a term like

'x ↦ x + ... + x'

for a given variable number n of occurrences of x on the right hand side of ↦. How would you do that by using actual terms and quotations, and not just by constructing the entire thing as a monolithic string which is then turned into a term?

If we could somehow access a bound variable from within a quotation, then we could program a function mkabs such that mkabs f returns a term of the form x ↦ ‹f @x› where @x is the notation we use to refer to the bound variable x from within the quotation. Then to solve above problem, we could define f for a given n via

def f x = 
  def 
    sum 1 = x
    sum m = `‹sum (m - 1)› + ‹x›`    
  sum n

[phlegmaticprogrammer]

I've slept over the problem, and I feel that it would be very difficult, maybe impossible, to have something like @x in ProofScript. On the other hand, it should be possible to improve ProofScript so that mkabs can be programmed in ProofScript. Given mkabs, the effect of being able to address bound variables in quotations can be easily simulated by higher order application and abstraction.

So why can't mkabs currently not be programmed in ProofScript? In short, because terms currently don't have contexts associated with them, unlike theorems, and because terms cannot be lifted between contexts.

Usually there are 2 types of terms in theorem provers: sealed terms, which have been established to be well-formed and well-typed, and unsealed terms. ProofScript currently only uses unsealed terms. Because well-formedness only makes sense relative to a context, sealed terms would always be accompanied by a context in ProofScript. The question now is: do we ever need unsealed terms? What problems would introducing sealed terms introduce?