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

Local blocks in ml_progLib #595

Merged
merged 12 commits into from Jan 8, 2019

Conversation

Projects
None yet
2 participants
@talsewell
Copy link

talsewell commented Dec 30, 2018

This collection of patches adds local-block support to ml_progLib.

For this to be useful, this requires supporting a stack of open blocks, rather than the 1-2 available previously (global + one module). Nested modules are now supported and have been very very lightly tested. Along the way, the ML_code theorem shape had to change, and rather than trying to make sense of all the RATOR_CONVs and RAND_CONVs, I refactored the way that the relevant theorems are defined and applied.

Thomas Sewell added some commits Dec 22, 2018

Thomas Sewell
ml_progLib: support a stack of blocks.
Generalise from 1/2 open blocks in the ML_code constant to a list
of open blocks. Refactor the code for updating ML_code
in ml_progLib. Work in progress.
Thomas Sewell
alist_tree: bugfix: handle more cases in merge.
Not much thought has gone into the case where terms with prebuilt
representations are merged and then extended. It should now be
working in general, although the merge leads to the contents being
sorted again from scratch.
Thomas Sewell
ML_code multiple blocks: third bugfix
Handle init_env and empty_env better. It solves a lot of headaches
to hide init_env_def from EVAL, and have nsLookup operations on it
solve in the 'usual way' via pfun_eqs and nsLookup.
Thomas Sewell
Restore ML_code_env constant.
This was previously folded into the ML_code predicate, but doing so
requires computing environment merges when new blocks are opened,
which in hindsight might be expensive. Let's revert to the ML_code_env
constant and the use of merge_env of all open environments, which will
then be examined one at a time on each nsLookup.
Thomas Sewell
Tweak alist_treeLib again.
Fix a bug and generally refactor the bit about representing terms
which are merges/option-choices of terms with existing representations.
Thomas Sewell
Support for local blocks in ml_progLib.
Adds a new interface to ml_progLib for progressively defining a
'local .. in .. end' block via open_local_block, open_local_in_block
and then close_local_block.
Thomas Sewell
Permit nested modules in ml_translator.
The ml_translator code can now compute long names of arbitrary length,
permitting the use of constants/types/etc defined in nested modules.
This is tested in at least one simple case.
Thomas Sewell
Bugfix in EVAL setup in ml_progLib changes.
The v_thms were being constructed with the wrong flag and added to
the EVAL/computeLib set.
@talsewell

This comment has been minimized.

Copy link

talsewell commented Dec 30, 2018

Oops, closing this PR for now, there's a known failure, I haven't tracked down all the uses of ML_code, especially in characteristic.

@talsewell talsewell closed this Dec 30, 2018

@talsewell talsewell reopened this Dec 31, 2018

@talsewell talsewell closed this Dec 31, 2018

Thomas Sewell
Many compatibility fiddles for ML_code changes.
Lots of adventures in hunting down slight incompatibilities between
the translator and the basis. The basis theories now all build.

In particular:
  - ensure that 'env' objects are abbreviated without being normalised.
    + the definitions of write/write_cons/merge_env etc will eventually be
      added to the global compute set.
  - ensure that auto-names of _v constants are exactly as before.
    + basisFunctionsLib.trans uses part of a _v constant name to guess
      a v_thm name and overwrite the translator thm with a rewritten version.
  - delete chunks of various scripts that reimplement parts of ml_progLib
    e.g. doing ml_progLib.get_state by hand via rator/rator/rand.
  - add some more queries to ml_progLib/ml_translatorLib to delete yet more
    hand interventions from other theories.

@talsewell talsewell reopened this Jan 3, 2019

@talsewell

This comment has been minimized.

Copy link

talsewell commented Jan 3, 2019

I've fixed a few issues, let's find out what the regression test thinks.

@talsewell talsewell removed the test failing label Jan 3, 2019

Thomas Sewell
Fix manual eval_rel proof in monad translator.
Fix another instance where an 'eval_rel' goal is constructed by
repeat manipulation of an ML_code thm (whose form has changed)
rather than just fetching the state and env component.

The monad translator seems to be working now.

@xrchz xrchz merged commit f298b17 into master Jan 8, 2019

1 check was pending

cakeml-regression-test regression test in progress
Details

@xrchz xrchz deleted the local branch Jan 8, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment