[isabelle-dev] type unification

[Dmitriy Traytel]

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 
>>>
>>>
>>