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

[Yong Kiam]

Thanks! Before you replied, I ended up just making it do (inst [``:'m`` |->
``:tvarN``]) since it seemed like the type variable that appears is always
'm. I think your method is more portable.

I was actually confused in my initial question because I thought the
displayed 'm was 'v. i.e. that the choice of type variable could be
dependent on context where the term was constructed (hence needing
something like cinst instead of a fixed inst on a type var).

On Sun, Jan 15, 2017 at 10:23 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170116/b13a6dd6/attachment.html>