Skip to content

support submodules in cryptol_load #2593

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.

Sign up for GitHub

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

Draft
wants to merge 26 commits into
base: master
Choose a base branch
from
Draft

support submodules in cryptol_load #2593

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
0af7c4e
refactor: new function loadAndTranslateModule, extracted from importM…
mtullsen Sep 16, 2025
5a4d568
comments and whitespace
mtullsen Sep 18, 2025
2cf2812
refactor: move code for generating CryptolModule into mkCryptolModule
mtullsen Sep 18, 2025
6949e21
refactors
mtullsen Sep 18, 2025
04717fa
improve fail message
mtullsen Sep 18, 2025
910f9ff
comments.
mtullsen Sep 18, 2025
50826d5
refactor: fold loadAndTranslateModule
mtullsen Sep 18, 2025
6693057
comments, refactors
mtullsen Sep 18, 2025
4bffbdd
refactor: make names more consistent
mtullsen Sep 18, 2025
a45b92b
improve comments
mtullsen Sep 19, 2025
7c3d477
comments, refactors (re-ordering, folding locatedUnknown, new mkImport)
mtullsen Sep 19, 2025
86878b2
refactor (with dead code, thus no compile), in prep for ...
mtullsen Sep 20, 2025
11cdf18
generalize the internals of "CryptolModule" (as seen on command-line)…
mtullsen Sep 21, 2025
72406e0
refactors, comments, whitespace
mtullsen Sep 24, 2025
1abc038
revert (misguided) c923c717b
mtullsen Sep 24, 2025
873ee63
comments: move/improve; change whitespace/identing
mtullsen Sep 24, 2025
5341ca9
refactor: re-plumb to get more arguments to `extractDefFromExtCryptol…
mtullsen Sep 24, 2025
c7a3f80
finish "generalize the internals of "CryptolModule" by finishing extr…
mtullsen Sep 24, 2025
9d16944
comments
mtullsen Sep 25, 2025
9d5136e
plumb ?fileReader down.
mtullsen Sep 25, 2025
9701212
refactor mkCryptolModule (inline internals and simplify)
mtullsen Sep 27, 2025
dbd44c5
wibble to improve messages (info and error)
mtullsen Sep 27, 2025
95e7bea
refactor
mtullsen Sep 28, 2025
b875080
Improve how we show a ECM_LoadedModule to the user.
mtullsen Sep 28, 2025
e90ffff
comments
mtullsen Sep 28, 2025
93fd2d8
new tests
mtullsen Sep 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion crux-mir-comp/src/Mir/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -238,7 +238,7 @@ loadCryptolFunc col sig modulePath name = do
let ?fileReader = BS.readFile
ce <- liftIO (readIORef (mirCryEnv mirState))
let modName = Cry.textToModName modulePath
ce' <- liftIO $ SAW.importModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing
ce' <- liftIO $ SAW.importCryptolModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing
liftIO (writeIORef (mirCryEnv mirState) ce')
-- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath)
-- tt <- liftIO $ SAW.extractDefFromCryptolModule m (Text.unpack name)
Expand Down
Loading
Loading