New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplifier loop with arith_ss #473

Closed
bacam opened this Issue Oct 9, 2017 · 1 comment

Comments

Projects
None yet
2 participants
@bacam
Contributor

bacam commented Oct 9, 2017

The simplifier can loop on a simple expression containing dimindex when using arith_ss:

---------------------------------------------------------------------
       HOL-4 [Kananaskis 11 (stdknl, built Thu Oct 05 13:10:20 2017)]

       For introductory HOL help, type: help "hol";
       To exit type <Control>-D
---------------------------------------------------------------------
[Use-ing configuration file /home/bcampbe2/.hol-config.sml]
> load "wordsTheory";
val it = (): unit
> SIMP_CONV arith_ss [] ``n + dimindex (:'a) + dimindex (:'b) - 1``;
Exception- Interrupt raised

The problem appears to be that part of the simpset in src/num/arith/src/numSimps.sml uses a term comparison function that ignores types, and the two appearances of dimindex differ only in their types. Changing the comparison to Term.compare appears to work, but I don't know if there's some reason for using the particular ordering that's in numSimps.

@mn200

This comment has been minimized.

Show comment
Hide comment
@mn200

mn200 Oct 9, 2017

Member

Thanks for the bug report! I think you're right that we can simply replace the poor comparison in numSimps.

Member

mn200 commented Oct 9, 2017

Thanks for the bug report! I think you're right that we can simply replace the poor comparison in numSimps.

@mn200 mn200 closed this in eccf4fe Oct 11, 2017

xrchz added a commit to CakeML/cakeml that referenced this issue Oct 12, 2017

Remove unnecessary AC ADD_COMM ADD_ASSOC
Not only unnecessary, but after HOL-Theorem-Prover/HOL#473 was sending the simplifier into a loop.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment