mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Make :m
work the same way as :l
More precisely, in both cases we unload all modules and then reload everything (this is what `:l` used to do, while `:m` only reloaded the current module). This fixes #668. There are opportunities to be smarter here: in particular when we reload modules, we do need to parse them so that we can find out what their dependencies are, and if needed to reload those. However, if none of the dependencies have changed, and we didn't change, then we could reuse the current module. This could be quite useful for modules that take a long time to load.
This commit is contained in:
parent
be408d7bfe
commit
372d2bf3aa
@ -70,7 +70,7 @@ loadModuleByPath path (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
|
||||
|
||||
-- | Load the given parsed module.
|
||||
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
|
||||
loadModuleByName n env = runModuleM env $ do
|
||||
loadModuleByName n (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
|
||||
unloadModule ((n ==) . lmName)
|
||||
(path,m') <- Base.loadModuleFrom (FromModule n)
|
||||
setFocusedModule (T.mName m')
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module issue290
|
||||
Loading module issue290bar
|
||||
Showing a specific instance of polymorphic result:
|
||||
|
@ -1,3 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T1::Main
|
||||
0x02
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T10::Main
|
||||
Symbols
|
||||
=======
|
||||
|
@ -1,3 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T11::A
|
||||
Loading module T11::Main
|
||||
|
@ -1,3 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T12::A
|
||||
Loading module T12::Main
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T13::A
|
||||
Loading module T13::B
|
||||
Loading module T13::Main
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T2::A
|
||||
Loading module T2::Main
|
||||
0x00
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T3::A
|
||||
|
||||
[error] Import of a non-instantiated parameterized module: T3::A
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T4::A
|
||||
Loading module T4::Main
|
||||
main : T
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T5::A
|
||||
Loading module T5::B
|
||||
Loading module T5::Main
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T5::A
|
||||
Loading module T5::B
|
||||
Loading module T5::Main
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T7::Main
|
||||
|
||||
Expression depends on definitions from a parameterized module:
|
||||
|
@ -1,3 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T8::Main
|
||||
f : {x : [8]} -> [8]
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T9::A
|
||||
Loading module T9::Main
|
||||
main : [16]
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Array
|
||||
Primitive Types
|
||||
===============
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Float
|
||||
Loading module FloatTests
|
||||
"-- Float Formatting-----------------------------------------------------------"
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module r03
|
||||
Satisfiable
|
||||
True
|
||||
|
Loading…
Reference in New Issue
Block a user