Iavor Diatchki
12967c47c3
Fix tests for Mac and Windows
2022-09-28 16:54:05 +03:00
Iavor Diatchki
29e71d1600
Merge branch 'master' into functors-merge
2022-09-28 15:18:05 +03:00
Iavor Diatchki
58a351c765
Update evaluator to account for TError of kind prop.
...
At the moment this kind of representes "False" so we need
to handle it. In the future, we probaly should:
* add an explicit `TFalse` to distinguish between malformed and False
* Eliminate obviously false guards when instantiating a funcotr
2022-09-28 15:17:39 +03:00
Iavor Diatchki
4f8bc653e0
Disallow foreign with the same name and in functors
...
Fixes #1442
2022-09-28 11:23:18 +03:00
Iavor S. Diatchki
94283f2531
Merge pull request #1443 from GaloisInc/T1441
...
Add support for literat Cryptol with RST
2022-09-28 11:03:41 +03:00
Iavor Diatchki
bed32f8081
TraverseNames for EPropGuards
2022-09-28 10:28:00 +03:00
Iavor Diatchki
e6acf4ecb7
Add info to the CHANGES files
2022-09-28 09:37:12 +03:00
Iavor Diatchki
38ee399ccd
Fixes and improvements based on code review
2022-09-27 23:34:45 +03:00
Iavor Diatchki
42b56f6e8b
Add support for literat Cryptol with RST
2022-09-27 22:41:13 +03:00
Iavor Diatchki
6fea305ada
Fix test
2022-09-27 12:32:34 +03:00
Iavor Diatchki
489ded4313
Fix tests
2022-09-27 11:46:08 +03:00
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
e9d581a707
Merge pull request #1438 from GaloisInc/T1394
...
Support FFI on Windows
2022-09-24 13:12:14 -04:00
Ryan Scott
045a0c6d34
CI: Update cabal.GHC-*.config files
...
We need to use `hgmp-0.1.2.1` as the minimum, as it includes a critical bugfix
for Windows. Let's put this in the `cabal.GHC-*.config` files to guarantee that
that happens.
2022-09-24 11:56:00 -04:00
Ryan Scott
84b29a3721
CI: Install diff, gcc, gmp, make on Windows before running tests
...
These are required to run some of the FFI tests.
2022-09-24 11:21:08 -04: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
b72a5d97bd
Don't try to get information for undefined names.
...
When we find an undefined name we record an error,
but we also generate a fake name, so that we can continue
processing and report other errors. It is important
that we don't try to use this fake name.
This commit corrects this behavior where we'd try to get
information about an undefined intrface submodule.
Fixes #1440
2022-09-24 15:37:35 +03:00
Iavor Diatchki
09b68e2ae1
Fix typos in comments
2022-09-24 15:34:35 +03:00
Iavor S. Diatchki
146934b9d3
Merge pull request #1432 from GaloisInc/ffi-integer
...
Support `Integer`, `Z`, and `Rational` in FFI
2022-09-23 18:44:07 +03:00
Iavor Diatchki
96fb52dc9c
Fix Mac OS test
2022-09-23 17:47:50 +03:00
Iavor Diatchki
c3f6181204
Add a couple of tests with Z
2022-09-23 17:13:14 +03:00
Iavor Diatchki
741959f918
Add gmp as en explicit dependency
2022-09-22 19:10:12 +03:00
Iavor Diatchki
e7a3f87858
Update FFI Section of Reference Manual to describe Integer/Rational/Z
2022-09-22 18:30:03 +03:00
Iavor Diatchki
4e75c38330
Modify generate-header to support Integer/Rational/Z
...
Add some tests
2022-09-22 17:15:04 +03:00
Iavor Diatchki
12f2bb086e
Merge branch 'master' into ffi-integer
2022-09-22 16:18:36 +03:00
Iavor Diatchki
cb43685abc
Just cosmeic tweaks
2022-09-22 16:17:22 +03:00
Iavor Diatchki
ddcc67b1cb
Resolve Has selectors for each nested module separately.
...
This fixes #1439
See the comment on the new function `selectorScope`
for details.
2022-09-22 15:59:54 +03:00
Iavor Diatchki
516ad74a28
Remove unused functoion
2022-09-22 08:47:02 +03:00
Iavor S. Diatchki
6ab24582e1
Merge pull request #1429 from GaloisInc/ffi-generate-headers
...
Generate C header files from `foreign` declarations
2022-09-19 09:51:29 +03:00
Ryan Scott
4367eee0d1
Make fromTo and friends return VWord when appropriate ( #1436 )
...
Previous, `fromTo` and related functions would always return a `VSeq`. If the
type happened to be a `Bit`, this would violate the internal invariant that
sequences of `Bit`s are always represented with `VWord`s, leading to the panics
observed in #1435 . This patch fixes the issue by using the `mkSeq` smart
constructor, which chooses between `VWord` and `VSeq` depending on the sequence
type.
Fixes #1435 .
2022-09-17 10:48:15 -04:00
Iavor Diatchki
d241e4945b
Restrict the names allowed in foreign declarations.
...
For now we allow alpha numeric characters and '_' which
should be fairly portable.
2022-09-14 18:37:34 +03:00
Iavor Diatchki
85c3f43840
Escape weird names (mostly quotes) in type parameters and record fields.
2022-09-14 18:21:26 +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
Iavor S. Diatchki
6fd1a115e3
Merge pull request #1416 from GaloisInc/ffi-aes-ni
...
AES-NI version of SuiteB module using FFI
2022-09-14 16:58:51 +03:00
Iavor S. Diatchki
51b765efd8
Merge pull request #1431 from GaloisInc/ffi-slides
...
Add FFI presentation slides
2022-09-14 16:40:17 +03:00
Iavor S. Diatchki
f8b5543946
Merge pull request #1380 from GaloisInc/conditional-constraints
...
Numeric Constraint Guards
2022-09-14 16:38:08 +03:00
Iavor Diatchki
2be867e19d
Report an error if we find unsupported constraints
2022-09-13 13:53:46 +03:00
Iavor Diatchki
61ad2527ed
Fix pretty printer for propguards
2022-09-13 13:44:22 +03:00
Iavor Diatchki
69719529d2
Merge branch 'master' into conditional-constraints
2022-09-13 13:16:44 +03:00
Iavor Diatchki
44685f09b0
Fix test
2022-09-12 18:42:10 +03:00
Iavor Diatchki
4ef8000c0e
Another test
2022-09-12 14:58:18 +03:00
Iavor Diatchki
3dc6c014f9
Clean up translation, and support for nested modules
2022-09-12 14:57:44 +03:00
Iavor Diatchki
16e7d4f751
Fixes to exhaustivness checking
2022-09-12 14:28:16 +03:00
Iavor Diatchki
4f82466a7f
Simplify type checking of constraint guards
2022-09-12 11:35:34 +03:00
Bretton
adfb760cad
FFI: Update ffi-type-errors test output
2022-09-10 13:09:27 -07:00
Bretton
8732bbee79
FFI: Add comments
2022-09-10 13:05:16 -07:00
Bretton
c5a8b234b6
FFI: Update error message with new types
2022-09-10 03:16:30 -07:00
Bretton
a372df22f9
FFI: Remove now supported types from error test
2022-09-10 03:12:00 -07:00
Bretton
f32a099dc9
FFI: Support Rational
2022-09-10 03:08:37 -07:00
Bretton
4c86ac633b
FFI: Support Z
2022-09-10 02:35:07 -07:00
