Examine relationship between contexts and function definitions / calls

[phlegmaticprogrammer]

Currently a function is executed in the context of where it is defined. That is a problem:

    # Block A
    def 
      dest t =
        match t
          case '‹p› ∧ ‹q›' => (1, p, q)
          case '∃ X. ‹p› X ∧ ‹q› X' => (2, p, q)
          case '‹p› = ‹q›' => (3, p, q)
          case '∀ x. ‹p› x = ‹q› x' => (4, p, q)
          case _ => nil  

    # Block B
    let 'x : 𝒰'
    let 'y : ℙ'
    choose inf: 'inf' infinity

    # Block C
    assert dest inf == [1, '∅ ∈ inf', '∀ x ∈ inf. x ∪ {x} ∈ inf']
    assert dest infinity == [2, 'X ↦ ∅ ∈ X', 'X ↦ ∀ x ∈ X. x ∪ {x} ∈ X']
    assert dest 'x = x' == [3, 'x', 'x']
    assert dest '∀ q. q = x' == [4, 'y ↦ y', 'y ↦ x']
    assert dest '∀ q. q = y' == [4, 'x : ℙ ↦ x', 'x : ℙ ↦ y']
    assert dest '∃ q. q = x' == nil

Currently several of the assertions in Block C will not hold. After switching Block A with Block B, these assertions hold, though! This is because in the above the constant inf for example is not known in the context of dest, therefore terms containing inf will not be valid as parameters to dest.

The solution could be that all term literals in dest are handled with respect to the context where dest is defined, but the actual execution context of dest is passed by the call site.

[phlegmaticprogrammer]

Let's outline what seems to be a sensible strategy that could resolve both this issue as well as issue #18:

• functions are executed in the context of the calling site, not in the context of the definition site; this also makes more sense if in addition we allow calling functions in a way that modifies the context of the calling site, for example via a call statement
• term literals inside a function definition are interpreted in the context of the definition side, not the calling site
• term values should carry their context around with them in some form; for example, on the kernel level certified terms could be introduced (similar to what happens in the Isabelle kernel) and the kernel only operates on certified terms
• there should be some sort of certified term lifting; this kind of lifting does not need to change the term, but merely checks if the term can be transferred from one context into another or not. The simplest way of doing this is to just type check the term again in the new context. If instead we go the other route of doing the check via operating on the involved context, maybe we can even relax the annoying condition that all introduced constants must be fresh (obviously then lifting could change the term)?

[phlegmaticprogrammer]

I've opted for the simple fix: function calls are now always done by passing the context (dynamic context instead of lexical context).

This could lead to the situation where your term literals in a function definition mean something differently than what you intended them to mean, because the meaning of the calling site is assumed, and not the meaning at the site of the function definition. What could happen is that you refer to a constant c in term literal in a function defined in namespace A, then this function is called from namespace B which has its own constant c; 'c' is then parsed not as '\A\c', but as '\B\c'. To avoid that, you have to refer to the c in your literal via '\A\c', then no confusion can occur.

That seems to be not ideal. But the quick fix of having dynamic contexts with lexical contexts for parsing literals only fails, because there really is no such thing as lexical context, as the function body can introduce new constants as well, so you would have to take that into account as well. You possibly could do that, of course, so I might revisit this issue later.