See now http://isabelle.in.tum.de/reports/Isabelle/rev/7f990b3d5189 which seems to do the job. There a still dark corners wrt. to base sort inference which maybe one day will lift its ugly head but for the moment it is OK.
Florian
On 10.09.2014 10:35, Florian Haftmann wrote:
> Hi Clemens,
>
>> This is what I expected. Type inference of locale expressions is
> inherently heuristic and probably you are hitting this. (This could be
> verified further with a stack trace). For more background, see also
> this earlier message:
> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-February/003821.html
>
> thanks for that hint.
>
> The problem the class target faces is to determine the so called base
> sort of the class specification, i.e. the sort that is inferred for the
> type parameter 'a from the import *and* the fixes/assumes as given by
> the user. For this I cannot fix 'a in the first place.
>
> I think I can circumvent this problem by adding a suitable plugin to the
> term/type check phase. Let's see…
>
> Best,
> Florian
>
>>
>> Clemens
>>
>>
>> On 05 September, 2014 20:12 CEST, Florian Haftmann
>> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>>
>>>> Is this a regression in the type inference of locale expressions, or has
>>>> it always (i.e. since 2009) been like this?
>>>
>>> Using the attached retrofitted theory, the same behaviour occurs:
>>>
>>>> $ /opt/Isabelle2009/Isabelle2009/bin/isabelle tty
>>>>> val it = () : unit
>>>> val commit = fn : unit -> bool
>>>> Welcome to Isabelle/HOL (Isabelle2009: April 2009)
>>>>> theory Foo imports Class_Clash begin
>>>> Loading theory "Class_Clash"
>>>> parameters
>>>> f :: "'a => 'a => 'a"
>>>> constants
>>>> F :: "'a => 'a => 'a"
>>>> parameters
>>>> f :: "'a => 'a => 'a"
>>>> constants
>>>> F :: "'a => 'a => 'a"
>>>> "plus"
>>>> :: "'a => 'a => 'a"
>>>> "inf"
>>>> :: "'b => 'b => 'b"
>>>> "plus"
>>>> :: "'a => 'a => 'a"
>>>> "inf"
>>>> :: "'a => 'a => 'a"
>>>> "plus"
>>>> :: "'a => 'a => 'a"
>>>> "inf"
>>>> :: "'a => 'a => 'a"
>>>> *** Type unification failed
>>>> *** Type error in application: Incompatible operand type
>>>> ***
>>>> *** Operator: op = inf :: ('b => 'b => 'b) => bool
>>>> *** Operand: plus :: 'a => 'a => 'a
>>>> ***
>>>> *** At command "locale" (line 64 of
>>>> "/data/tum/drawer/thy/Class_Clash.thy").
>>>>> Error - Database is not opened for writing.
>>>>> val it = () : unit
>>>
>>> There is strong evidence that it has always been like this.
>>>
>>> Shall I just chance my luck and dive into the sources?
>>>
>>> Cheers,
>>> Florian
>>>
>>>
>>>>
>>>> On 04 September, 2014 09:21 CEST, Florian Haftmann
>>>> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>>>>
>>>>> At d6a2e3567f95, I am currently analysing a problem with type inference
>>>>> in locale expressions: when leaving types implicit, imported parameters
>>>>> are given disjoint types despite they could be unified, and are so if
>>>>> given explicit type annotations. The problem occurs if the imported
>>>>> locales themselves have dependencies on other locales containing a
>>>>> definition.
>>>>>
>>>>> The reason why this is really annyoing is that it breaks certain class>>
>>>>> specifications to typecheck and currently effectively prevents me from>>
>>>>> adding such a simple thing as product over lists.
>>>>>
>>>>> See attached theory for quite minimal examples.
>>>>>
>>>>> I will have to investigate this further.
>>>>>
>>>>> Florian
>>>>>
>>>>> --
>>>>>
>>>>> PGP available:
>>>>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-...@in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>>
>>>
>>> --
>>>
>>> PGP available:
>>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>
>>
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
