CakeML / CakeML/cakeml

Translating mutually recursive datatypes produces a bunch of warnings

Open
#1,461 0 comments 0 reactions 0 assignees View on GitHub
translator
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

Doing
```
Datatype:
a = A b ;
b = B a | C num
End
```
and then calling
```
val _ = register_type ``:a``;
```
produces a bunch of warnings.
As far as I can remember these warnings are indeed that the equality thm not being proved.
Even if it's spurious it needs redesign anyway to remove the exception driven control flow.
In the case of the warning being invalid it's probably mk_EqualityType_thm succeeding once and failing for the rest of the cases.
I believe the fix should probably be replacing this bit below
https://github.com/CakeML/cakeml/blob/87d99d1e72e3234bc6e16faef6f46a69d0de292e/translator/ml_translatorLib.sml#L1611-L1612
with some call to a `mk_EqualityType_thms` which is `mk_EqualityType_thm` refactored. You can't really separate the equality proof anyway and do it one by one.

Stuff to do to ensure this is fixed (assuming equality thms aren't being proved) .
Add a translation of a function that calls equality of the mutually recursive type to the ml_translator_testScript. Note it's just extending this bit

https://github.com/CakeML/cakeml/blob/87d99d1e72e3234bc6e16faef6f46a69d0de292e/translator/ml_translator_testScript.sml#L14-L28
NB: also can be used to check if the warnings are spurious.

Also right now ml_translator_testScript already spews out these warnings if I can remember correctly. It doesn't translate a function which calls equality for the mutrec datatype though.

Note I haven't looked at the translator deeply in sometime but I recall this issue and was planning to fix it but ran out of cycles.

Contributor guide

No contributing guide indexed for this repository

Research direction

Start with the mutually recursive datatype example and the existing warnings in translator/ml_translator_testScript.sml, extending its datatype tests with a function that calls equality. Then inspect translator/ml_translatorLib.sml around lines 1611–1612 and mk_EqualityType_thm. Done means the equality proofs and translation succeed without spurious warnings or exception-driven failures.

Written by the indexing model from the issue text.

Assessment

Domain
compilers, testing
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Active
Clarity
Mostly clear
Newbie friendliness
45/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.