[CakeML-dev] Workaround ARB in record definition

[Ramana Kumar]

I'm forwarding this to the developers list. I think Magnus can confirm
the canonical solution to this issue.

I think the workaround is as you suggested: define and translate an
initial record - you might have to use the locn constructor directly
for that - and then only use explicit updates. The literal record
syntax does produce an ARB, but record updates don't.

On 30 January 2017 at 06:47, Yong Kiam <tanyongkiam at gmail.com> wrote:
> Hi all,
>
> I'm fixing up the translation on env_refactor, and the lexer implementation
> now runs into a weird bug in the translator (or maybe elsewhere):
>
> I believe the issue boils down to:
>
> find_term is_arb `` <| row := loc.row + 1; col := 1; offset := 0|>``
>
> deciding that the term on the right actually has an ARB in it
> (because internally, that record is represented as a series of updates)
>
> e.g.:
>
> val (l,r) = dest_comb `` <| row := 1; col := 1; offset := 0|>``
>
> val l = ``row_fupd (K 1)``: term
> val r = ``<|col := 1; offset := 0|>``: term
>
> Is there a workaround for this? I guess defining some kind of default record
> and re-writing that line in next_sym_alt_def would work, but that's not very
> neat.