[CakeML-dev] ML mk_* function that instantiates argument term type
Yong Kiam
tanyongkiam at gmail.com
Sun Jan 15 22:25:03 UTC 2017
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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170115/a1c56ee5/attachment.html>
More information about the Developers
mailing list