[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

Dmitriy Traytel traytel at in.tum.de
Mon Nov 24 09:03:26 CET 2014 

Cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e

Dmitriy

On 23.11.2014 21:20, Christian Sternagel wrote:
> *Moved from isabelle-users*
>
> Thanks for the crucial hint Dmitriy!
>
> Coming back to the original issue of Andreas, some explanation might 
> be in order.
>
> What we did until now in adhoc_overloading.ML (more precisely, the 
> function "insert_variants") was to check for a given constant "c" of 
> type "T" whether there is a registered variant "v" whose type unifies 
> with "T". If so, "v" was inserted (but with all type-annotations 
> "flattened" to "dummyT"). After that we just hoped that type-inference 
> would do the trick. Apparently this worked quite well in many 
> situations (or maybe there are just not that many users of 
> "adhoc_overloading" ;)).
>
> Be that as it may. In Andreas' example this "flattening" of types 
> leads to somewhat unexpected results. Funnily (or maybe it was to be 
> expected but I don't know the details) everything worked out in 
> top-level thoeries. Somehow types are more polymorphic there (even 
> though HOL is not polymorphic at all ;)). With notepad and a fixed 
> type "'b" the problem occurred (and I guess the same would happen with 
> locales).
>
> (I'm not sure whether the TYPE_MATCH exception, which is not raised 
> inside adhoc_overloading.ML but caused by its result, is the best 
> problem-indicator for users here. Maybe there is also space for 
> improvement elsewhere. Comments?)
>
> Anyway, attached is the following series of patches (to be applied in 
> this order):
>
> delete - fixes a typo
> drop_semicolons - drops semicolons
> inst_unifier - uses the obtained unifier to instantiate the type of "v"
> tune - misc tuning
>
> With those applied (the important one is "inst_unifier") 
> "insert_variants" does the following. For a given constant "c" of type 
> "T", check whether there is a variant "v" of type T' such that T and 
> T' unify. If so, apply the obtained type-unifier to "v" and insert the 
> result instead of "c".
>
> I hope this resolves your problem Andreas.
>
> I tested the change on one of my local files that make heavy use of 
> adhoc overloading. Maybe someone could have a look, push the changes 
> to a test server, and push them to the main repo if everything is fine?
>
> cheers
>
> chris
>
> On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:
>> Hi Christian,
>>
>> just a few weeks ago, I learned that Envir.subst_term_types is indeed
>> the wrong function when substituting with a unifier (instead it is
>> intended for matchers).
>>
>> The right functions for unifiers in envir.ML are the ones prefixed with
>> "norm".
>>
>> Hope that helps,
>> Dmitriy
>>
>> On 22.11.2014 21:02, Christian Sternagel wrote:
>>> I'm currently a bit confused by the result of "Sign.typ_unify" (or
>>> rather the result of applying the corresponding "unifier"). So maybe
>>> the problem stems from my ignorance w.r.t. to its intended result.
>>>
>>> After applying the attached "debug" patch for the following
>>>
>>>   consts pure :: "'a ⇒ 'b"
>>>
>>>   definition pure_stream :: "'a ⇒ 'a stream"
>>>   where "pure_stream = sconst"
>>>
>>>   adhoc_overloading pure pure_stream
>>>
>>>   consts ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream"
>>> (infixl "◇" 70)
>>>   consts S_stream :: "(('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c) stream"
>>>
>>>   declare [[show_variants]]
>>>
>>>   term "pure id :: ('b ⇒ 'b) stream"
>>>
>>> we obtain the output
>>>
>>> oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
>>> variant type: ?'a ⇒ ?'a stream
>>> ("unifier:",
>>>  {(("'a", 0), (["HOL.type"], "??'a ⇒ ??'a")),
>>>    (("?'a", 0),
>>>      (["HOL.type"],
>>>       "'b"))}) (line 165 of
>>> "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
>>> ("candidate term:",
>>>  Const ("Scratch.pure_stream",
>>>         "?'a
>>>          ⇒ ?'a Stream.stream")) (line 167 of
>>> "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
>>> ("after unification:",
>>>  Const ("Scratch.pure_stream",
>>>         "(??'a ⇒ ??'a)
>>>          ⇒ (??'a
>>>              ⇒ ??'a) Stream.stream")) (line 168 of
>>> "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
>>> "pure_stream id"
>>>   :: "('a ⇒ 'a) stream"
>>>
>>> The result of unification is a bit surprising to me, since the
>>> obtained "unifier" seems to claim that
>>>
>>>   ('b => 'b) => ('b => 'b) stream
>>>
>>> and
>>>
>>>   (??'a => ??'a) => (??'a => ??'a) stream
>>>
>>> are equal. What am I missing here? Maybe Envir.subst_term_types is not
>>> the way to apply the typenv obtained by typ_unify? (In this special
>>> case, if I would call subst_term_types twice with the same typenv, the
>>> result would be as I expected.)
>>>
>>> cheers
>>>
>>> chris
>>>
>>> Btw: the "delete" patch (which is to be applied before "debug") fixes
>>> a typo in the description of "no_adhoc_overloading". It is entirely
>>> unrelated to the issue at hand, but maybe somebody could apply it 
>>> anyway.
>>>
>>> On 11/21/2014 07:31 PM, Christian Sternagel wrote:
>>>> Dear Andreas,
>>>>
>>>> Thanks for the report, I'll have a look. First an immediate 
>>>> observation:
>>>>
>>>> When adding the following to Scratch.thy
>>>>
>>>> declare [[show_variants]]
>>>>
>>>> notepad
>>>> begin
>>>>    fix f :: "('b ⇒ 'b ⇒ 'a) stream"
>>>>    and x :: "'b stream"
>>>>    term "pure id :: ('b => 'b) stream"
>>>>
>>>> the first "term" results in
>>>>
>>>> "pure_stream id"
>>>>    :: "('c ⇒ 'c) stream"
>>>>
>>>> while the second results in
>>>>
>>>> "pure_stream id"
>>>>    :: "('b ⇒ 'b) stream"
>>>>
>>>> So it is not surprising that the first causes problems while matching.
>>>> Why, however "'c" is produced instead of "'b" is not immediately clear
>>>> to me. I'll investigate.
>>>>
>>>> cheers
>>>>
>>>> chris
>>>>
>>>> On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
>>>>> Dear experts on adhoc overloading,
>>>>>
>>>>> When I want to instantiate variables in a theorem using the attribute
>>>>> "of", sometimes the exception TYPE_MATCH gets raised. This seems
>>>>> strange
>>>>> to me because I would expect that adhoc_overloading either complains
>>>>> about not being able to uniquely resolve an overloaded constant or
>>>>> exchanges the constant in the AST.
>>>>>
>>>>> By adding more type annotations, I have so far been able to 
>>>>> circumvent
>>>>> the exception, but there seems to be a check missing. Attached you 
>>>>> find
>>>>> a small example.
>>>>>
>>>>> Best,
>>>>> Andreas
>>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141124/1d89d723/attachment-0002.html>

More information about the isabelle-dev mailing list