Commit Graph

3454 Commits

Author SHA1 Message Date
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