[CakeML-dev] ML mk_* function that instantiates argument term type

[Ramana Kumar]

I don't know any more automated way to do this than you found. You
could define a wrapper around mk_TypeId, like:

val TypeId_arg_ty = type_of TypeId |> type_of |> dom_rng |> #1
fun mki_TypeId x = mk_TypeId (cinst TypeId_arg_ty x)

On 16 January 2017 at 09:25, Yong Kiam <tanyongkiam at gmail.com> wrote:
> Hi dev,
>
> I'm repairing the translator on env_refactor where the id type is defined
> as:
>
> ... id = Short of 'n | Long of 'm => id
>
> The translator gets to a point where it constructs a term like ``Short foo:
> ('v,tvarN) id``
>
> However, it then tries to wrap it using mk_TypeId, where TypeId is a
> constructor for:
>
> ... tid_or_exn = TypeId of (modN,typeN) id | ...
>
> (tvarN,modN,typeN, are all abbrevs for string)
>
> but this fails because mk_TypeId does not instantiate 'v to modN.
>
> I found that I could get around this manually using TypeBasePure.cinst
> ``:(tvarN,tvarN) id`` , but is there a way that already automatically does
> this?
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>