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



On 28/11/2018 09:09, Peter Lammich wrote:
> 
>> 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.
>>
> 
> 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.

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
theory Scratch
  imports Main
begin

ML \<open>
  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;
\<close>

syntax "_Tag" :: "logic" ("\<^tag>")

parse_translation \<open>
  [(\<^syntax_const>\<open>_Tag\<close>, fn ctxt => fn _ => 
    mark_term (Syntax.read_term ctxt "hd"))]
\<close>


definition hd where "hd = 1"

term hd  \<comment> \<open>\<open>Scratch.hd\<close>\<close>
term \<open>\<^tag>\<close>  \<comment> \<open>\<open>Scratch.hd\<close>\<close>
term \<open>\<lambda>hd. \<^tag>\<close>  \<comment> \<open>\<open>\<lambda>hda. Scratch.hd\<close>\<close>


experiment
begin
definition hd where "hd = 1"

term hd  \<comment> \<open>\<open>local.hd\<close>\<close>
term \<open>\<^tag>\<close>  \<comment> \<open>\<open>local.hd\<close>\<close>
term \<open>\<lambda>hdd. \<^tag>\<close>  \<comment> \<open>\<open>\<lambda>hda. local.hd\<close>\<close>

end

end


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