Re: [isabelle] term_uncheck and abbreviation folding

Hi Julian,

Am 24.04.2014 07:01, schrieb Julian Brunner:

I've run into a situation where the last uncheck phase returns
abbreviations folded differently than what's shown in the final
output. An example:

   let fun out l x = let val _ = writeln (l ^ ": " ^ (@{make_string} x)) in x end
   in Context.theory_map (Syntax_Phases.term_uncheck 100 "test" (fn _
=> map (out "uncheck"))) end

ML {* Syntax_Phases.print_checks @{context} *}

term "surj f"
term "~ surj f"

Thet print_checks command shows that the 'test' uncheck phase is the
last one to happen. The first term command displays "uncheck: Const
("Fun.surj", "('b ⇒ 'a) ⇒ HOL.bool") $ Free ("f", "'b ⇒ 'a")", showing
that the surj abbreviation was successfully folded by the last uncheck
phase that wasn't 'test'. The second term command, however, outputs
"uncheck: Const ("HOL.not_equal", "'a Set.set ⇒ 'a Set.set ⇒
HOL.bool") $ (Const ("Set.range", "('b ⇒ 'a) ⇒ 'a Set.set") $ Free
("f", "'b ⇒ 'a")) $ Const ("Set.UNIV", "'a Set.set")". It appears that
instead of folding the surj abbreviation, it decided to fold the
not_equal abbreviation, which then prevented it from folding surj. Of
course, that's just guesswork on my part. What remains is that
something does successfully fold the surj abbreviation, as the final
result in the output panel is "~ surj f", but that transformation
appears to happen after the last uncheck phase.

So my questions are:

1. Is this the way it's intended to work?
2. If it is, is there any way to do transformations (like
check/uncheck) on the final terms as they appear in the output?
3. As an aside, which abbreviation takes priority when there a
conflict as in the case of surj? I haven't been able to find anything
about it in the reference manual.
I assume, abbreviations are resolved in a first-come-first-served manner w.r.t. to the used traversal of the term (looks like top-down when considering your example).

The output is still "¬ surj f" because of the explicit print translation in Fun.thy:

"¬ CONST surj f" <= "CONST range f ≠ CONST UNIV"

Such print/parse translation happen before/after the check/uncheck phases (cf. isar-ref Sect. 7.5 Syntax transformations).


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