Re: [isabelle] add_assoc, add.assoc and reflection



On Mon, 20 Apr 2015, Walther Neuper wrote:

Looking at

   val ctxt = Proof_Context.init_global @{theory Main};
   Syntax.read_term ctxt "add_assoc"
      (* = Free ("add_assoc", "'a"): term *)
   Syntax.read_term ctxt "add.assoc"
      (* ERROR: Undefined constant: "add.assoc"*)

is my assumption right, that the latter is considered outer syntax only?
In other words: The latter is NOT considered to become a valid term (i.e. inner syntax) within some context ?

If both questions are answered "yes", then this question comes up: How comes that the designers of Isabelle are sure, that theorem names never shall occur in functions defined within Isabelle's function package (where function definitions are terms, i.e. belong to inner syntax) ?

Isabelle is not Coq or PVS. There is not just one big lambda calculus to assimilate everything, but we have arbitrarily nested languages and syntaxes.

Name spaces are strictly separate for each "kind" of things. The syntax is usually done in a way that the distinction of kinds is clear from how the text is written. E.g. fact expressions refer to attributes and theorems in a certain way, and cannot be mistaken as terms, for example.

The main exception to the syntactic distinction of kinds is the inner term language: consts, frees, bounds can all look the same in the syntax, but are later distinguished by their scope.


The main meta-problem on this thread might be actually an expectation of something complicated, but the situation is quite plain and simple. And after decades of reforms of the system implementation it should all work out smoothly, including arbitrary nesting of languages.

If you want do implement something like that yourself, you can take the "rail" language for syntax diagrams as an example (see ~~/src/Pure/Tools/rail.ML). It has the advantage that it is rather small, and has no connection to logic or lambda calculus to get confused. There is also a fair amount of IDE support just from the few canonical things done in that module; e.g. see uses of @{rail} in ~~/src/Doc/.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.