Email Gateway (Aug 22 2022 at 18:48): 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
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
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.
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
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: Nov 21 2024 at 12:39 UTC