Iavor Diatchki
662d6443a6
Comments, and describe a problem with the current algorithm
2022-02-28 16:18:04 -08:00
Iavor Diatchki
a5ce2c5d22
Start on the entry point interface to this functionality
2022-02-25 16:21:25 -08:00
Iavor Diatchki
4b1e78ec5c
New renamer loop to compute what's defined by a module
2022-02-25 16:09:43 -08:00
Iavor Diatchki
187a6a49c0
Make things build and a bit more progress with instances
2022-02-23 14:22:47 -08:00
Iavor Diatchki
d5ca0e772d
WIP
2022-02-22 16:18:00 -08:00
Iavor Diatchki
c1cd2317db
Just comments
2022-02-21 16:13:50 -08:00
Iavor Diatchki
eb26f5e4e4
Checkpoint: more on instantiating functors
2022-02-21 16:08:01 -08:00
Iavor Diatchki
c70aa21146
Thoughts on the algorithm for instantiating functors.
2022-02-16 16:07:13 -08:00
Iavor Diatchki
817f850ae7
Checkpoint
2022-02-16 11:34:15 -08:00
Iavor Diatchki
e41bc0f4f9
Checkpoint (buildable): changes related to functor instances
2022-02-16 11:34:15 -08:00
Iavor Diatchki
532854cf9a
Updates to Name
and OriginalName
...
We now keep enough information to be able to distinguish between
parameters from different `import signature A`
2022-02-16 11:34:15 -08:00
Iavor Diatchki
f8b687e94e
Fix the check for valid evaluation context.
2022-02-16 11:34:15 -08:00
Iavor Diatchki
7c4499072f
Change original names to support parameters
...
Parameters have empty module qualifiers. This enables us to create
proper display environments so that parameters can be qualified if needed.
2022-02-16 11:34:15 -08:00
Iavor Diatchki
2ca8581a3a
Group parameters by "signature import" and fix resolution of paramters at REPL
2022-02-16 11:34:15 -08:00
Iavor Diatchki
0bb5e64f21
Disallow importing uninstantiated functors
2022-02-16 11:34:15 -08:00
Iavor Diatchki
f2f53a62e8
Simplify top-level contsraints at the end of submodules
2022-02-16 11:34:15 -08:00
Iavor Diatchki
047029df3f
Don't add implicit imports for functors.
2022-02-16 11:34:15 -08:00
Iavor Diatchki
e3bcea5fe6
Split off help about named things into a separate module
2022-02-16 11:34:15 -08:00
Iavor Diatchki
2c212546f7
Fixes to checking signatures, and initial checking of module parameters
2022-02-16 11:34:15 -08:00
Iavor Diatchki
5d2ad31259
Add a function to conveniently enable printing of name uniques
2022-02-16 11:34:15 -08:00
Iavor Diatchki
7fd1326cf3
Checkpoint
2022-02-16 11:34:15 -08:00
Iavor Diatchki
e686922358
Small changes in prep for type checking
2022-02-16 11:34:15 -08:00
Iavor Diatchki
5c2c8fb8d8
Avoid incorrect warnings for unused parameters
2022-02-16 11:34:15 -08:00
Iavor Diatchki
26e2aef64a
Add better dependencies on top level constraints for types.
2022-02-16 11:34:15 -08:00
Iavor Diatchki
bd06555b40
A comment outlining what's happening with top-level constraints and type declarations
2022-02-16 11:34:15 -08:00
Iavor Diatchki
fe79bff3dd
Fix build
2022-02-16 11:34:15 -08:00
Iavor Diatchki
94dd15f91a
Change naming convention for module parameters
...
Also:
* Remove unused Renamer errors
* Do not repeat the same error many times
* Check that all module parameters have different names
2022-02-16 11:34:15 -08:00
Iavor Diatchki
6262568a12
Fix dependencies between functor-like things
...
XXX: The depending on constraints is still wrong
2022-02-16 11:34:15 -08:00
Iavor Diatchki
a74a762e08
Fix environment validation, simplify it, and check parameter validation
2022-02-16 11:34:15 -08:00
Iavor Diatchki
87c50d52c3
Split up NamingEnvironemnt into multiple modules and cleanup
2022-02-16 11:34:15 -08:00
Iavor Diatchki
48443946f2
Renaming of module parameters, and dump renamed info (debug)
2022-02-16 11:34:15 -08:00
Iavor Diatchki
25911522bd
Renaming module parameters, part 1
2022-02-16 11:34:15 -08:00
Iavor Diatchki
8b03ebc3cf
Text
2022-02-16 11:34:15 -08:00
Iavor Diatchki
a30cf2b0f2
A little more cleanup
2022-02-16 11:34:15 -08:00
Iavor Diatchki
a87d139679
Mostly comments and a few small tweaks.
2022-02-16 11:34:15 -08:00
Iavor Diatchki
613a66d15e
Adding signatures (checkpoint)
2022-02-16 11:34:15 -08:00
Iavor S. Diatchki
7748a619e9
Merge pull request #1323 from GaloisInc/T1321
...
T1321
2022-02-08 10:43:01 -08:00
Iavor S. Diatchki
335216ffe4
Merge pull request #1319 from GaloisInc/T1313
...
Make `:module` work more like `:load`.
2022-02-07 16:46:06 -08:00
Iavor Diatchki
a53b24b8a0
Fix paths in nested relative includes
...
Fixes #1321
2022-02-07 16:45:50 -08:00
Iavor Diatchki
2d1f2c1033
Fix windows tests, take 2
2022-02-07 14:56:20 -08:00
Iavor Diatchki
800f1e0cfe
Fix tests on windows (hopefully)
2022-02-07 11:15:49 -08:00
Iavor Diatchki
5a55e31585
Fix tests
2022-02-07 10:21:10 -08:00
Iavor Diatchki
24af7343d8
Make :module
work more like :load
.
...
Fixes #1313
2022-02-07 10:21:10 -08:00
Ryan Scott
413788c578
Merge pull request #1233 from GaloisInc/ghc9
...
GHC 9.*
2022-01-25 18:04:06 -05:00
Ryan Scott
3892615998
Address review comments
2022-01-25 17:03:03 -05:00
Ryan Scott
3b9eafbc91
CI: Update what4-solvers to use Z3 4.8.14
...
The previous `what4-solvers` snapshot used Z3 4.8.10, which is known to cause
severe performance regressions with the `negshift` regression test. See #1107 .
This updates to a more recent `what4-solvers` snapshot that uses Z3 4.8.14
instead, which is known to work more reliably with `negshift`.
2022-01-14 14:48:11 -05:00
Ryan Scott
09aaf1d82c
Make issue{066,093} resilient to different solvers' behavior
...
This adopts the same approach as in commit
3ea5e9e51c
:
use `:set show-examples=false` in the affected examples to avoid showing the
particular data that a solver picks for examples/counterexamples. Also avoid
printing the contents of `it` for similar reasons. I have verified that the
new output works across a wide range of Z3 versions.
Fixes #1280 .
2022-01-14 14:45:10 -05:00
Ryan Scott
3a204fc4aa
Make integerRecipMod return a Maybe instead of an unboxed sum
2022-01-13 15:35:41 -05:00
Ryan Scott
cb1cf652ae
Use test-lib-0.4
2022-01-13 15:12:57 -05:00
Ryan Scott
7030088e13
Ensure that there is at least one Windows build
2022-01-13 15:09:47 -05:00