This is just confirming that Ramana is right. Record literals can easily include ARB by accident. It's best to use record updates. -- Magnus<br><div class="gmail_quote"><div dir="ltr">On Sun, 29 Jan 2017 at 21:06, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I'm forwarding this to the developers list. I think Magnus can confirm<br class="gmail_msg">
the canonical solution to this issue.<br class="gmail_msg">
<br class="gmail_msg">
I think the workaround is as you suggested: define and translate an<br class="gmail_msg">
initial record - you might have to use the locn constructor directly<br class="gmail_msg">
for that - and then only use explicit updates. The literal record<br class="gmail_msg">
syntax does produce an ARB, but record updates don't.<br class="gmail_msg">
<br class="gmail_msg">
On 30 January 2017 at 06:47, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com" class="gmail_msg" target="_blank">tanyongkiam@gmail.com</a>> wrote:<br class="gmail_msg">
> Hi all,<br class="gmail_msg">
><br class="gmail_msg">
> I'm fixing up the translation on env_refactor, and the lexer implementation<br class="gmail_msg">
> now runs into a weird bug in the translator (or maybe elsewhere):<br class="gmail_msg">
><br class="gmail_msg">
> I believe the issue boils down to:<br class="gmail_msg">
><br class="gmail_msg">
> find_term is_arb `` <| row := loc.row + 1; col := 1; offset := 0|>``<br class="gmail_msg">
><br class="gmail_msg">
> deciding that the term on the right actually has an ARB in it<br class="gmail_msg">
> (because internally, that record is represented as a series of updates)<br class="gmail_msg">
><br class="gmail_msg">
> e.g.:<br class="gmail_msg">
><br class="gmail_msg">
> val (l,r) = dest_comb `` <| row := 1; col := 1; offset := 0|>``<br class="gmail_msg">
><br class="gmail_msg">
> val l = ``row_fupd (K 1)``: term<br class="gmail_msg">
> val r = ``<|col := 1; offset := 0|>``: term<br class="gmail_msg">
><br class="gmail_msg">
> Is there a workaround for this? I guess defining some kind of default record<br class="gmail_msg">
> and re-writing that line in next_sym_alt_def would work, but that's not very<br class="gmail_msg">
> neat.<br class="gmail_msg">
<br class="gmail_msg">
_______________________________________________<br class="gmail_msg">
Developers mailing list<br class="gmail_msg">
<a href="mailto:Developers@cakeml.org" class="gmail_msg" target="_blank">Developers@cakeml.org</a><br class="gmail_msg">
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" class="gmail_msg" target="_blank">https://lists.cakeml.org/listinfo/developers</a><br class="gmail_msg">
</blockquote></div>