Elaboration of Structures fails for nested theory domains

[Jazzpirate]

A minimal example that breaks:

theory NestedTest : ur:?LF = A : type ❙ a : A ❙ ❚

theory Outer : ur:?LF = include ?NestedTest ❙

theory Inner : ur:?LF =
    b : A ❘ = a ❙
❚

❚

theory NestedTest2 : ur:?LF = structure inner : ?Outer/Inner = b @ c ❙ ❚ include ?NestedTest ❙ test : A ⟶ type ❙ test2 : test a ❙ claim : test c ❘ = test2 ❙ // works iff a = c ❙ ❚

[florian-rabe]

It's not specified yet how to handle structures or includes whose domains are nested theories.

Your example should not be well-typed at all. The structure inner would need a morphism Outer -> NestedTest2 in order to see Outer/Inner at all. How to provide that morphism is an open design question.

[Jazzpirate]

@florian-rabe that's unrelated. You can replace the include of ?NestedTest by an include of ?Outer, put it above the structure, giving you the morphism you want and it will still fail. The problem is that Elaboration attempts to apply the structure-morphism to a, which is not part of the flattened version of ?Inner.

[florian-rabe]

Even with that include present, the behavior is not specified.

The behavior you expect in this case is reasonable, but an implementation has never been attempted.

[Jazzpirate]

Is there an alternative behavior one might expect or can I get working then? :D

[florian-rabe]

The structure inner needs to know a morphism m:Outer->NestedTest2 (possibly the identity morphism).

There are two main options to provide it:

• The domain of inner is m(Inner), i.e., a new theory is materialized in which all constants from Outer are replaced according to m.
• The body of inner includes a morphism that maps the constants from Inner in the usual way.

In both cases, if m is the identity, it could be inferred, and that is an easy special case to get going quickly. Probably, when the structure is checked/elaborated, we could add an include of the identity morphism from Outer->NestedTest2 to it.

If the involved theories take parameters, special care is needed to get the details right.

[Jazzpirate]

Ok. So to get the details wrt nested theories as right as possible:

1. You said "Your example should not be well-typed at all." - I don't see why. Currently nested theories are treated like any other theories, right? They have an MPath, are instances of DeclaredTheory and can be gotten by the controller. Is this behavior wrong?
2. If they are to be treated specially, is there a way to identify a DeclaredTheory/MPath as a nested theory? Can I safely assume that a theory is nested if it's name has more than one LNStep?

[florian-rabe]

They're special in the sense that they only make sense inside their parent theory. So to use them outside the parent theory, a morphism is needed.

A module is nested iff its local name has more than one step.

[Jazzpirate]

1.: Yeah, so that seems to be missing in the current implementation. The backend treats them just like any other theory.

2. : Perfect :)

[Jazzpirate]

Suggestion: I'll add checks to the structure checker (and ModelsOf) such that whenever a structure (including plain includes) to a nested theory occurs, an implicit morphism needs to exist?

[Jazzpirate]

fixed with 62b17f9f97fcbcc107332dc1d5d3f6038bfd334b

[florian-rabe]

This is one of those "not even wrong" kind of changes.

Without specifying what is supposed to happen, it is impossible to judge if this change makes things better or worse.

It's plausible that the most desirable specification will include the now-produced behavior as a special case. It's also possible that the changes made were exactly the right ones to create that behavior.

But we don't know that until we specify the semantics of importing nested theories.

[Jazzpirate]

I understand completely. This was my train of thought, we can maybe use that as a starting point to think about this in more depth:

• MMTStructureChecker: I suppose this one is not controversial - it merely makes sure that a nested theory ?S/T is "visible" via an implicit morphism.
• The reason why I changed TheoryExp.metas is because
  • it seemed minimally invasive in terms of actual code changes
  • symbols visible via a meta-theory already behave exactly as we want the symbols visible via the parent theory of a nested theory when it comes to structure elaboration, so I did not have to change the library, the elaborator and/or structures
  • I strongly suspect that in all other situations in which theory expressions related to nested theories occur (i.e. when TheoryExp.metas would be called), we want to treat the visible symbols in the exact same way as in the special case of structures. At least in all cases that I could think of it's the behaviour I'd expect, but I/we should probably think about that more carefully.