Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Inaccessible constant when trying to parse ter...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:48):

From: Peter Lammich <lammich@in.tum.de>
Hi,

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-
case fails.

Thanks in advance for any help or hints (being completely lost here),
  Peter


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.
  *)

term ‹\<^tag>›
  (* Fine *)

  locale foo begin
    definition hd where "hd = 1"

    term ‹\<^tag>›
    (* Fine *)
  end

  experiment
  begin
    definition hd where "hd = 1"

    ML_val ‹Syntax.read_term @{context} "hd"›
    (* Fine *)

    term ‹\<^tag>›
    (* Inaccessible constant: "Scratch.experiment8356112.hd" *)
  end

view this post on Zulip Email Gateway (Aug 22 2022 at 18:48):

From: Makarius <makarius@sketis.net>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 18:48):

From: Peter Lammich <lammich@in.tum.de>
Hi Makarius,

thanks for the quick answer, at least I'm starting to understand what
is going on there now.

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.)

I am implementing a parser for some custom syntax.
It takes a string (and position), and constructs 
a fully-typed Isabelle term. E.g.

parse "x=5" --> "define ''x'' (5::int)" :: term

where "define" is a constant that is "hardcoded" into the parser, i.e.,
it uses @{const_name define}.

I extended this to reflect Isabelle constants into the custom syntax,
e.g.

definition "f = ..."

parse @{context} "f(5)" --> "f (5::int)" :: term

where f is whatever Isabelle would make of term "f" in @{context}. I'm
using Syntax.read_term for this.

Up to this point, I believe (hope), everything is well-defined.

Now I want to embed the custom syntax into Isabelle's term syntax using
an antiquotation. Following the example for strings from
Cartouche_Examples, I did it via a parse_translation, causing the
semantic type mismatch that you pointed out.

I see that there is an ambiguity in what I want to achieve, e.g., in

term ‹λf. \<^tag>‹ f(5) ››

it is no longer clear to what "f" refers. However, for my application,
both resolutions (f refers to "f" in the context in which whole term is
parsed OR f refers to the bound variable) would work, but I don't know
how to achieve any of these.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:49):

From: Makarius <makarius@sketis.net>
I have studied the sources of
$ISABELLE_HOME/src/Pure/Syntax/syntax_phases.ML a bit: the subsequent
mark_term function should protect a given term reasonably well from
subsequent syntax processing:

fun mark_term (Const (c, T)) = Const (Lexicon.mark_const c, T)
| mark_term (Free (x, T)) = Const (Lexicon.mark_fixed x, T)
| mark_term (t $ u) = mark_term t $ mark_term u
| mark_term (Abs (x, T, b)) = Abs (x, T, mark_term b)
| mark_term a = a;

Included is the full example, even with some abstractions.

Makarius
Scratch.thy

view this post on Zulip Email Gateway (Aug 22 2022 at 18:49):

From: Peter Lammich <lammich@in.tum.de>
Thanks a lot,

I built it into my parser, and it works like a charm!


Last updated: Mar 29 2024 at 12:28 UTC