GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-22 11:27:44 +03:00
Code Issues Projects Releases Wiki Activity
3,439 Commits 65 Branches 28 Tags 83 MiB
3698ed08a3
Commit Graph

3439 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Matthew Yacavone
098c046a43 add case for lengthFromThenTo to to_type 2021-12-21 15:44:37 -08:00
Matthew Yacavone
aef1edd7d2 actually finish Cryptol props, add missing case to test_basics.py 2021-12-21 15:40:49 -08:00
Matthew Yacavone
fbb50dbdd5 add section headers 2021-12-21 15:03:52 -08:00
Matthew Yacavone
d726646506 add remaining props, lengthFromThenTo, unit to cryptoltypes.py 2021-12-21 14:57:48 -08:00
Iavor S. Diatchki
08cd609c4c
Merge pull request #1301 from GaloisInc/T1299 
T1299
 2021-12-20 21:56:20 +02:00
Iavor Diatchki
92e3174b2f Fix loop in TC 
The issue is that we use a think to represent dictionaries for selectors,
and we can't extract position information from the thunk, as it will
force it.  Instead, we compute the location from the source expression
instead.
 2021-12-20 20:49:02 +02:00
Iavor Diatchki
d9057100f9 Improve locations of error messages. 
Fixes #1299
 2021-12-20 10:44:33 +02:00
Iavor Diatchki
009f400a44 Use the same location for property as we do for normal declarations. 2021-12-20 10:41:29 +02:00
Matthew Yacavone
234324f381 add more docstrings to cryptoltypes, check types in CryptolApplication 2021-12-10 16:28:43 -08:00
Matthew Yacavone
16e35f689a use @dataclass, add missing __str__ methods in cryptoltypes 2021-12-10 16:02:22 -08:00
Matthew Yacavone
07c689a699
Merge pull request #1312 from GaloisInc/rpc/clean-cryptoltypes-1 
[RPC] Clean up `to_cryptol` interface in cryptoltypes.py
 2021-12-10 19:01:54 -05:00
Matthew Yacavone
6628bcd36d update CHANGELOG 2021-12-10 14:57:06 -08:00
Matthew Yacavone
554f53124d add docstring to to_cryptol, remove eval_numeric 2021-12-10 14:45:36 -08:00
Matthew Yacavone
565a48a2c7 add deprecation errors to CryptolType.from_python and .convert 2021-12-10 14:41:21 -08:00
Andrew Kent
cec87706e5
bump argo submodule (#1300) 2021-12-10 11:26:26 -08:00
Andrew Kent
c332ad987f
chore: bump cryptol client python deps (#1306) 
* chore: bump cryptol client python deps

* bump argo-client (and in turn, urllib3)

Co-authored-by: Matthew Yacavone <matthew@yacavone.net>
 2021-12-10 11:24:12 -08:00
Matthew Yacavone
780c572858 allow bytearrays in BV.from_bytes 2021-12-09 14:29:38 -08:00
Matthew Yacavone
faa4e78504 clean up interface for converting to JSON in cryptoltypes 2021-12-09 14:04:15 -08:00
Andrew Kent
490e046b07
fix what4-abc solver in python client, add more SMT tests (#1311) 
* fix what4-abc solver in python client, add more SMT tests (include more solvers)
 2021-12-09 11:17:19 -08:00
robdockins
435bb81e52
Merge pull request #1303 from GaloisInc/primitive-scanl 
Primitive scanl
 2021-12-07 15:00:24 -08:00
Rob Dockins
7b3121f0b6 Make sure to memoize the sequence map inside the scanl primitive. 
This speeds up concrete computation and preserves sharing for
symbolic computation.
 2021-12-07 13:46:43 -08:00
Rob Dockins
928cc98768 Add a test comparing the reference implemntations of foldl, 
`scanl` and `iterate` to their primitive implementations.
 2021-12-07 11:56:46 -08:00
Rob Dockins
22af290eae Update test output 2021-12-07 11:56:46 -08:00
Rob Dockins
41613ade02 Tweak the type signature for scanl and scanr. 
It is convenient for Coq extraction for the constant 1 factor
to be on the left of the addition symbol.
 2021-12-07 11:56:46 -08:00
Rob Dockins
253a7f26ab Add reference implementations for foldl and scanl and iterate 2021-12-07 11:56:34 -08:00
Rob Dockins
849a79c9bc Reimplement the updates, updatesEnd and iterate functions 
in the prelude to use `foldr` or `scanl`.

This leaves `sortBy` as the only remaining operation in the Cryptol
prelude defined directly by recursion.
 2021-12-06 14:33:18 -08:00
Rob Dockins
750ce5f00a Make scanl into a primitive. This puts it on similar footing as foldl. 2021-12-06 14:33:18 -08:00
Ryan Scott
ebb1dd152f
cryptol-remote-api: Allow building with aeson-2.0.* (#1308) 
This introduces some CPP, unfortunately, but this probably necessary to
continue allowing `cryptol-remote-api` to be buildable with old versions of
`aeson` until the ecosystem catches up with `aeson-2.0.*`.
 2021-11-30 09:05:30 -05:00
Matthew Yacavone
abb41f5b4e
Merge pull request #1307 from GaloisInc/rpc/quoted-cryptol 
[RPC] f-string-like Cryptol quasiquotation
 2021-11-29 17:07:30 -05:00
Matthew Yacavone
aebde831d1 use __to_cryptol_str__ instead of __str__, add type to __to_cryptol__ 2021-11-29 12:35:34 -08:00
Matthew Yacavone
6555352351 docs changes from @RyanGlScott 2021-11-29 11:24:24 -08:00
robdockins
4ad896172c
Merge pull request #1302 from GaloisInc/mergeSort-Prelude 
A take at updating Cryptol's sort function from insertion sort to merge sort
 2021-11-29 09:43:55 -08:00
Matthew Yacavone
1867938921 add check to CryptolCode's __call__ 2021-11-26 13:57:18 -08:00
Matthew Yacavone
36fac34c61 handle CryptolApplication in cry_f, fix parens in to_cryptol_str 2021-11-26 13:10:46 -08:00
Matthew Yacavone
f6c3e6b251 keep __all__ alphabetical 2021-11-24 14:35:44 -08:00
Matthew Yacavone
3c28a03c7e add proper handling of conversions and format specs to cry_f 2021-11-24 14:29:39 -08:00
Matthew Yacavone
e2c01db7e2 pull out implementation of cry_f/eval_f 2021-11-24 13:18:58 -08:00
Matthew Yacavone
bbc327cd8c improve docs for cry_f 2021-11-24 12:46:47 -08:00
Rob Dockins
b9d76689e3 Update changelog regarding sortBy 2021-11-24 10:40:07 -08:00
Matthew Yacavone
f46dfa5937 update CHANGELOG 2021-11-19 17:06:10 -08:00
Matthew Yacavone
c9c8be587c add f-string-like quasiquoting for cryptol 2021-11-19 16:53:55 -08:00
Andrew Kent
cffdcdd049
rpc v2.12 release details fixes (i.e., cabal, changelogs, etc) (#1305) 
* rpc v2.12 release details fixes (i.e., cabal, changelogs, etc)

* bump rpc server/client to dev version
 2021-11-19 11:54:07 -08:00
Sean Weaver
b62960034b Updating issues and regression tests to work w/ latest prelude 2021-11-18 12:36:26 -05:00
Sean Weaver
3fabe4a21f selected the first merge option 2021-11-12 22:00:13 -05:00
Sean Weaver
c064d408dc Updating private scoping 2021-11-06 10:11:55 -04:00
Sean Weaver
2375055403 A take at updating Cryptol's sort function from insertion sort to merge sort. This implementation is much more computationally efficient. 2021-11-04 16:25:39 -04:00
Iavor Diatchki
8b97cf4a8a Fix typo 2021-10-18 11:47:16 -07:00
Iavor Diatchki
6bb573eef3 Add the basic Cryptol classes 2021-10-18 10:21:33 -07:00
Iavor Diatchki
c03a590c34 Fix the URL 2021-10-18 09:49:38 -07:00
Iavor Diatchki
638525fd64 Disable jekyll, as it ignores files starting with _ 2021-10-18 09:47:08 -07:00