Re: [isabelle] Inaccessible constant when trying to parse term from cartouche in experiment



On 27/11/2018 19:00, Peter Lammich wrote:
> 
> I'm trying to parse a term that I read from a cartouche, which is
> contained in another term. For that, I Syntax.read_term the content of
> the cartouche inside a parse_translation. However, inside an experiment
> environment, this will yield "inaccessible constant" errors. What is
> going wrong here?
> I attached a boiled-down example, with my test-cases. The last test-
> 
> -----------------
> 
>   syntax "_Tag" :: "logic" ("\<^tag>")
> 
>   parse_translation ‹
>     [(@{syntax_const "_Tag"}, fn ctxt => fn _ => 
>       Syntax.read_term ctxt "hd"
>     )]
>   ›
> 
>   (* In my real example, the "hd" is a string parsed from 
>     a cartouche argument. I have to interpret this string as a term 
>     in the context where the outer 
>     term, containing the cartouche, appears.
>   *)

parse_translation operates on certain parse trees that happen to re-use
datatype term, but are quite different from what you get from
Syntax.read_term.

In other words, this is a semantic type-error. You cannot place a
fully-typed term into the concrete syntax tree and expect it to survive
the subsequent stages of processing the input.


Just the usual questions: What are you trying to achieve? What is the
application behind it? (It might help to construct further
counter-examples to this approach.)


	Makarius




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