Re: [isabelle] term_uncheck and abbreviation folding



Ah, I never noticed that translation, thanks for pointing this out, it
all makes sense now.

On Thu, Apr 24, 2014 at 2:58 PM, Dmitriy Traytel <traytel at in.tum.de> wrote:
> Hi Julian,
>
> Am 24.04.2014 07:01, schrieb Julian Brunner:
>
>> 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:
>>
>> 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:
>
> 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
>




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