Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Cryptol/pr1136 #200

Closed
wants to merge 9 commits into from
Closed

Cryptol/pr1136 #200

wants to merge 9 commits into from

Conversation

robdockins
Copy link
Contributor

Changes to track Cryptol PRs GaloisInc/cryptol#1048 and GaloisInc/cryptol#1136

Overlaps somewhat with #197, maybe it makes sense to rebase them together.

Brian Huffman and others added 9 commits April 7, 2021 17:25
Change the type of `EqTrue` to be in `Prop`.  Fix a bug in the
`scTypeOf` code that prevented it from treating `Prop` as impredicative.
This is mostly changes in the renamer related to nested
modules (PR #1084), but also a few changes related to
value representations (PR #1136).
@robdockins
Copy link
Contributor Author

@yav, following this update, one of the SAW integration tests is failing with the following message:

[19:38:02.144] Cryptol error:
[error]
    Overlapping symbols defined:
    (at Cryptol:844:11--844:17, Cryptol::update)
    (at cryptol-spec/mul_java.cry:7:1--7:7, mul_java::update)

I think this should probably be a shadowing warning instead. If I just load up the module in the Cryptol REPL, it works, so I think maybe I messed up something subtle here in the CryptolEnv module. Any ideas what might be the problem?

-- Resolve names
let nameEnv = nameEnv1 `MR.shadowing` getNamingEnv env
(rdecls :: [P.TopDecl T.Name]) <- MM.interactive (MB.rename interactiveName nameEnv (traverse MR.rename topdecls))
(_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@robdockins I am not really sure, but perhaps there is a problem here. Note that in the old code the naming environment in which we do the resolving already has the names added to it, while in the new one it does not...

Otoh, I don't understand why the old code was doing that in the first place, and what you've replaced it with makes sense to me, so perhaps the problem is not here.

To be more help, I should probably just check out the code and run it, ping me on the chat if that'd be useful.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wondered about this code too, but I think it's unrelated, actually. I think this code is for dealing with declarations appearing inside the {{ ... }} delimiters in SAWScript. The code for importing modules is further above, and is barely changed.

@robdockins
Copy link
Contributor Author

I think the Cryptol issue holding this up has been resolved, I plan to migrate this into the corresponding saw-script PR GaloisInc/saw-script#1191

@robdockins
Copy link
Contributor Author

These changes are now folded into GaloisInc/saw-script#1191

@robdockins robdockins closed this Apr 27, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants