Skip to content
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

Manage state as in SAWScript #10

Open
david-christiansen opened this issue Jul 22, 2019 · 1 comment
Open

Manage state as in SAWScript #10

david-christiansen opened this issue Jul 22, 2019 · 1 comment
Labels
Low-Hanging Fruit Good first task to meet the code SAW Related to SAW API in particular

Comments

@david-christiansen
Copy link
Contributor

SAWScript contains an ambient state that includes things like the currently-loaded Cryptol modules. In a prior iteration of this API, the intention was to abolish this implicit state and provide all information explicitly in each call. However, this made it more difficult to share code with SAWScript, and it was unclear that the extra expressive power was actually useful.

This should be disentangled.

The SAWScript state is maintained here:

, _sawTopLevelRO :: TopLevelRO
, _sawTopLevelRW :: TopLevelRW

The most important code to change is in the SAWServer.CryptolSetup module. It should be replaced by code that updates the implicit state rather than saving a Cryptol setup value into the environment. See e.g.

cryptolSetupLoadFile :: CryptolSetupLoadFileParams -> Method SAWState OK
cryptolSetupLoadFile (CryptolSetupLoadFileParams fileName) =
cryptolSetupMethod $
\cenv ->
do sc <- biSharedContext . view sawBIC <$> getState
let qual = Nothing -- TODO add field to params
let importSpec = Nothing -- TODO add field to params
cenv' <- liftIO $ CEnv.importModule sc cenv (Left fileName) qual importSpec
return (cenv', OK)
.

@david-christiansen david-christiansen added Low-Hanging Fruit Good first task to meet the code SAW Related to SAW API in particular labels Jul 22, 2019
@david-christiansen
Copy link
Contributor Author

@atomb I think you made this happen late last year, right?

@atomb atomb added this to the June Bugs milestone May 7, 2020
@atomb atomb removed this from the June Bugs 2020 milestone Jan 4, 2021
@atomb atomb removed their assignment Oct 19, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Low-Hanging Fruit Good first task to meet the code SAW Related to SAW API in particular
Projects
None yet
Development

No branches or pull requests

2 participants