Commit Graph

292 Commits

Author SHA1 Message Date
Iavor Diatchki
441e163856 Merge branch 'master' into functors-merge
# Conflicts:
#	docs/RefMan/_build/doctrees/BasicSyntax.doctree
#	docs/RefMan/_build/doctrees/BasicTypes.doctree
#	docs/RefMan/_build/doctrees/Expressions.doctree
#	docs/RefMan/_build/doctrees/FFI.doctree
#	docs/RefMan/_build/doctrees/Modules.doctree
#	docs/RefMan/_build/doctrees/OverloadedOperations.doctree
#	docs/RefMan/_build/doctrees/RefMan.doctree
#	docs/RefMan/_build/doctrees/TypeDeclarations.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/.buildinfo
#	docs/RefMan/_build/html/BasicSyntax.html
#	docs/RefMan/_build/html/BasicTypes.html
#	docs/RefMan/_build/html/Expressions.html
#	docs/RefMan/_build/html/FFI.html
#	docs/RefMan/_build/html/Modules.html
#	docs/RefMan/_build/html/OverloadedOperations.html
#	docs/RefMan/_build/html/RefMan.html
#	docs/RefMan/_build/html/TypeDeclarations.html
#	docs/RefMan/_build/html/_static/doctools.js
#	docs/RefMan/_build/html/_static/fonts/Lato-Bold.ttf
#	docs/RefMan/_build/html/_static/fonts/Lato-Regular.ttf
#	docs/RefMan/_build/html/_static/js/modernizr.min.js
#	docs/RefMan/_build/html/_static/searchtools.js
#	docs/RefMan/_build/html/searchindex.js
#	src/Cryptol/ModuleSystem.hs
#	src/Cryptol/ModuleSystem/Base.hs
#	src/Cryptol/ModuleSystem/InstantiateModule.hs
#	src/Cryptol/Parser/AST.hs
#	src/Cryptol/Parser/ParserUtils.hs
#	src/Cryptol/REPL/Command.hs
#	src/Cryptol/Transform/AddModParams.hs
#	src/Cryptol/Transform/Specialize.hs
#	src/Cryptol/TypeCheck/Infer.hs
#	src/Cryptol/TypeCheck/InferTypes.hs
#	src/Cryptol/Utils/Ident.hs
2022-09-27 11:43:16 +03:00
Ryan Scott
27ac8d9717 Support FFI on Windows
This patch:

* Adds the appropriate conditional logic to use the `Win32` library to
  dynamically load shared libraries on Windows.
* Tweaks some FFI-related test cases to make them work portably on Windows. I
  have left comments describing each of the non-obvious tweaks that I had to
  make.
* Updates the reference manual accordingly.

Fixes #1394.
2022-09-24 11:21:03 -04:00
Iavor Diatchki
12f2bb086e Merge branch 'master' into ffi-integer 2022-09-22 16:18:36 +03:00
Iavor Diatchki
5a4a3967fc Merge remote-tracking branch 'origin/master' into ffi-generate-headers
# Conflicts:
#	docs/RefMan/_build/doctrees/FFI.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/FFI.html
#	docs/RefMan/_build/html/searchindex.js
2022-09-14 17:18:30 +03:00
Bretton
daba20a03e FFI: Support Integer 2022-09-10 01:19:57 -07:00
Bretton
c22404ad6a Add :generate-foreign-header command 2022-09-07 20:54:48 -07:00
Henry Blanchette
9a4f48d0fb
Merge pull request #1424 from GaloisInc/master
Update to master
2022-08-31 09:56:49 -07:00
Bretton
09cf06a8e8 time command: bind result to it 2022-08-30 14:24:47 -07:00
Bretton
e4b4611711 Move Benchmark module to Cryptol.Utils 2022-08-29 22:56:04 -07:00
Bretton
8dafb86dc6 Add :time command 2022-08-29 10:44:59 -07:00
Henry Blanchette
57cb59a845 Merge branch 'master' into conditional-constraints 2022-08-13 14:20:41 -07:00
Iavor Diatchki
f77e5cc1c9 Merge remote-tracking branch 'origin/master' into functors-merge
# Conflicts:
#	cryptol-remote-api/src/CryptolServer/Exceptions.hs
#	cryptol.cabal
#	docs/RefMan/_build/doctrees/BasicSyntax.doctree
#	docs/RefMan/_build/doctrees/BasicTypes.doctree
#	docs/RefMan/_build/doctrees/Expressions.doctree
#	docs/RefMan/_build/doctrees/Modules.doctree
#	docs/RefMan/_build/doctrees/OverloadedOperations.doctree
#	docs/RefMan/_build/doctrees/RefMan.doctree
#	docs/RefMan/_build/doctrees/TypeDeclarations.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/Modules.html
#	docs/RefMan/_build/html/searchindex.js
#	src/Cryptol/ModuleSystem.hs
#	src/Cryptol/ModuleSystem/Base.hs
#	src/Cryptol/ModuleSystem/Env.hs
#	src/Cryptol/ModuleSystem/InstantiateModule.hs
#	src/Cryptol/ModuleSystem/Monad.hs
#	src/Cryptol/Parser/Token.hs
#	src/Cryptol/Transform/AddModParams.hs
#	src/Cryptol/TypeCheck/Error.hs
#	src/Cryptol/TypeCheck/Infer.hs
#	src/Cryptol/TypeCheck/InferTypes.hs
2022-08-12 17:50:56 +03:00
Bretton
36fcdb3a93 FFI: Use upstream libffi 2022-08-11 13:35:17 -07:00
Bretton
6b1210d37c FFI: Revert dynamic linking hacks for linux 2022-08-05 13:54:38 -07:00
Bretton
65cb428010 FFI: Copy libffi to bin 2022-08-04 13:56:17 -07:00
Bretton
3fb609db72 FFI: add ghc libffi for other cryptol executables 2022-08-03 17:45:59 -07:00
Bretton
7f904e0bfa FFI: copy libffi to dist/lib/ and cryptol/../lib 2022-08-03 16:55:51 -07:00
Bretton
1b36a13a59 FFI: Fix linker flags 2022-08-03 15:42:20 -07:00
Bretton
8d28f59f26 FFI: Try linking against ghc's libffi at runtime 2022-08-03 14:56:27 -07:00
Bretton
45dfcaac25 FFI: Add size polymorphism and improve type errors 2022-07-28 21:17:48 -07:00
Bretton
b8b53a1bf4 Add FFI for all integral types 2022-07-13 14:40:59 -07:00
Henry Blanchette
f3c2f58411 expandpropguards 2022-07-06 15:51:51 -07:00
Bretton
7bac9db242 Add cabal flag for FFI 2022-07-05 19:29:15 -07:00
Henry Blanchette
6000ce96d5 new module: Cryptol.Parser.PropGuards 2022-07-05 16:10:49 -07:00
Bretton
1e18568e17 Add basic FFI for concrete backend (unix only) 2022-06-28 15:51:59 -07:00
Iavor Diatchki
6ab14706af New module system 2022-06-13 15:56:15 -07:00
Ryan Scott
5698bcd3bb Update copyright year 2022-05-17 09:02:36 -04:00
Ryan Scott
8881547ee9 Bump version numbers after 2.13.0 release 2022-05-17 09:02:06 -04:00
Ryan Scott
1dd4311417 Fix -Wincomplete-uni-patterns warnings
GHC 9.2 now includes `-Wincomplete-uni-patterns` as a part of `-Wall`. As a
result, building Cryptol with GHC 9.2 uncovers some previously undetected
warnings.

Some warnings can be fixed by rewriting the code slightly. For example,
changing a use of `Data.List.groupBy` to `Data.List.NonEmpty.groupBy` avoids
the need for an incomplete match on `(_ : _)` on the value that `groupBy`
returns. (Since `Data.List.NonEmpty` was added to `base` in `4.9`, this also
requires bumping the lower version bounds on `base` slightly.)

Other warnings were fixed by explicitly adding fall-through `error` cases.
The resulting code is no less partial than before, but it avoids warnings and
should provide a more specific error in the event that the fall-through cases
are reached.

Yet another class of warnings are those caused by the use of irrefutable
patterns, such as the definition of `ar1 ~[x] = x` in
`Cryptol.TypeCheck.TypePat`. It's rather unfortunate that
`-Wincomplete-uni-patterns` warns about these
(see https://gitlab.haskell.org/ghc/ghc/-/issues/14800), as the only way to
avoid the warning would be to rewrite these functions to use refutable
patterns, thereby changing their strictness properties. I've decided to simply
disable `-Wincomplete-uni-patterns` in each module that uses irrefutable
patterns to avoid this issue. I've written also written a Note explaining the
reasoning and referenced it in the affected modules.
2022-05-04 13:14:55 -05:00
Ryan Scott
980e652303 Support building with GHC 9.2
This contains a variety of changes needed to make Cryptol compile with GHC 9.2:

* In GHC 9.2, enabling `UndecidableInstances` no longer implies
  enabling `FlexibleContexts` (see
  [here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.2?version_id=7e2ce63ba042c1934654c4316dc02028d8d3dd31#undecidableinstances-no-longer-implies-flexiblecontexts-in-instance-declarations)).
  As a result, I had to enable `FlexibleContexts` in
  `Cryptol.ModuleSystem.Name`.
* The `argo` submodule was bumped to bring in the changes from
  GaloisInc/argo#191, which allows it to build with GHC 9.2.
* The upper version bounds on `base`, `bytestring`, `lens`, `base-compat`, and
  `sbv` were raised to allow building them with GHC 9.2.
2022-05-04 13:14:51 -05:00
Ryan Scott
0035d0bcf4
Update what4 dependency to 1.3 (#1346)
Among other things, `what4-1.3` includes a bugfix that allows `what4` to
correctly invoke modern versions of Boolector.
2022-04-25 12:59:58 -04:00
Felix Yan
8bf48b275e
Allow sbv 8.17
Tested to build fine here.
2022-03-26 03:39:55 +08:00
Ryan Scott
1181076f1f Factor out compatibility shims into GHC.Num.Compat 2022-01-13 12:13:40 -05:00
Ryan Scott
644d33bf1f Merge branch 'master' into ghc9 2022-01-12 09:33:24 -05:00
Aaron Tomb
4e9c5b1650 Update copyright year 2021-10-05 10:16:16 -07:00
Aaron Tomb
f980545711 Bump version number after 2.12 release 2021-10-05 10:11:28 -07:00
Felix Yan
868ce2cff3
Allow sbv 8.16
Tested to build fine.
2021-08-19 10:40:04 +08:00
Rob Dockins
35bb83b80c Swap out pretty printer packages. We are now using prettyprinter.
This required a fair amount of fixup to the pretty-printing code,
as some of the primitives have semantics that differ in subtle ways
from the old package.  The output now is mostly the same as before,
although some improvements have been made here and there.

The one somewhat negative outcome of this change is that the
"line fill" algorithm in `prettyprinter` works a bit different
and makes choices about where to break lines that are arguably
less desirable than before. When laying out structures nested inside
sequences, it is more likely to break a line inside a substructure,
whereas the old algorithm prefered to break lines between elements
of the outer sequence.  There are also appear to be some minor
differences regarding how ribbon width is calculated.
2021-08-06 14:17:47 -07:00
Felix Yan
4526f5090e Allow sbv 8.15 (#1205) 2021-07-23 08:27:04 -07:00
Iavor Diatchki
816523df10 Fixes #1167
This requires newer version simple-smt, which supports calling back into
the program when the solver exits
2021-07-21 10:54:03 -07:00
Rob Dockins
889bfd6511 First take at GHC 9.* compatibility.
There's a lot here that can be cleaned up, and we need
some backward compatiblity layer, but this is just a first
try.

Something in the PrimeEC module is causing hard crashes
during the test suite, so I'll have to figure out what's
going on there.
2021-07-14 22:44:53 -07:00
Rob Dockins
3900c68619 Update build metadata to allow/require What4 1.2 2021-06-17 11:54:09 -07:00
Iavor Diatchki
7727197800 Split off tokens and new layout in a separate modules 2021-04-29 11:17:34 -07:00
robdockins
cd0748cc74
Merge pull request #1161 from felixonmars/patch-2
Allow sbv 8.14
2021-04-20 10:22:19 -07:00
Felix Yan
6d17c2e97b
Allow sbv 8.14
Tested to build fine here.
2021-04-14 03:33:21 +08:00
Rob Dockins
3f185449ee Move WordValue into a separate module. 2021-04-13 10:27:17 -07:00
Rob Dockins
3f710468e8 Break SeqMap out into a separate module 2021-04-13 10:27:17 -07:00
Rob Dockins
234437af06 Remove our dependency on the random package.
Instead, directly use the generators defined in `tf-random`.
This changes the generation algorithm for some types, so we
need to update the tests that depend on those concrete values.

Fixes #1102
2021-04-07 12:12:32 -07:00
robdockins
c2ef506902
Merge pull request #1139 from felixonmars/patch-2
Allow sbv 8.13
2021-04-06 10:15:20 -07:00
Iavor S. Diatchki
523a2dcd5b
Merge pull request #1048 from GaloisInc/nested-modules
Nested modules
2021-04-06 08:40:42 -07:00