[isabelle-dev] type unification

[Christian Sternagel]

You are right. Thanks for the clarification! - chris

On 07/11/2013 04:19 PM, Dmitriy Traytel wrote:
> If you are planing to localize the thing, you'll have to take the
> context into account. I guess you don't want to generalize over fixed
> type variables (as your solution does).
>
> locale A =
> fixes a :: 'a
> begin
>
> ML {*
>    val T1 = @{term a} |> singleton (Variable.polymorphic @{context}) |>
> fastype_of
>    val T2 = @{term a} |> (fastype_of #> Term.map_type_tfree (TVar o
> apfst (rpair 0)))
> *}
>
> end
>
> Dmitriy
>
> Am 11.07.2013 09:01, schrieb Christian Sternagel:
>> Dear Dimitriy,
>>
>> thanks that does the trick. However, after having a look at the
>> implementation of Variable.polymorphic, I'm wondering whether it isn't
>> overkill in my case. What about
>>
>>   fastype_of #> Term.map_type_tfrees (TVar o apfst (rpair 0))
>>
>> as alternative?
>>
>> Since I'm manually "naming" schematic type variables apart before
>> unification anyway, shouldn't that also work (without ever using a ctxt)?
>>
>> cheers
>>
>> chris
>>
>> On 07/11/2013 02:57 PM, Dmitriy Traytel wrote:
>>> Hi Chris,
>>>
>>> I think Variable.polymorphic is what you want to use before using
>>> fastype_of.
>>>
>>> Dmitriy
>>>
>>> Am 11.07.2013 05:12, schrieb Christian Sternagel:
>>>> Dear list,
>>>>
>>>> what is the proper way of obtaining a type from a term, in case I want
>>>> to give it as argument to Sign.typ_unify (of Sign.typ_match for that
>>>> matter)?
>>>>
>>>> My question arises as follows. In adhoc_overloading.ML previously
>>>> Sign.the_const_type was used to obtain the type of a constant. The
>>>> result is a type with schematic type variables. Now that I want to use
>>>> terms instead of constants (as strings) I replaced Sign.the_const_type
>>>> by fastype_of, but this yields a type with fixed type variables and
>>>> thus unification may fail. So once again: What is the proper way of
>>>> getting a "schematic" type from a term?
>>>>
>>>> cheers
>>>>
>>>> chris
>>>>
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>>
>>>>
>>>
>