Email Gateway (Aug 19 2022 at 14:10): Email Gateway (Aug 19 2022 at 14:10):From: Julian Brunner <julianbrunner@gmail.com>
Hello,
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:
setup
{*
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:
If it is, is there any way to do transformations (like
check/uncheck) on the final terms as they appear in the output?
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.
Thanks in advance,
Julian
Email Gateway (Aug 19 2022 at 14:10):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Julian,
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:
translations
"¬ 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).
Dmitriy
Email Gateway (Aug 19 2022 at 14:11):From: Julian Brunner <julianbrunner@gmail.com>
Ah, I never noticed that translation, thanks for pointing this out, it
all makes sense now.
Last updated: Nov 21 2024 at 12:39 UTC