Commit Graph

3911 Commits

Author SHA1 Message Date
Iavor Diatchki
77fd64f8ec 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/basic.css
#	docs/RefMan/_build/html/_static/css/badge_only.css
#	docs/RefMan/_build/html/_static/css/theme.css
#	docs/RefMan/_build/html/_static/doctools.js
#	docs/RefMan/_build/html/_static/jquery.js
#	docs/RefMan/_build/html/_static/js/theme.js
#	docs/RefMan/_build/html/_static/searchtools.js
#	docs/RefMan/_build/html/_static/underscore.js
#	docs/RefMan/_build/html/genindex.html
#	docs/RefMan/_build/html/search.html
#	docs/RefMan/_build/html/searchindex.js
2023-05-25 11:38:40 -07:00
Iavor Diatchki
ed0d3fbb1e Add a function to compute a mapping from original names to names from an interface.
This is a setp toward #1522
2023-05-24 16:59:29 -07:00
Iavor Diatchki
614898f8d2 Refactor to avoid using eiter, and preserve a bit more context 2023-05-24 16:58:21 -07:00
Iavor Diatchki
141fe3a02e Remove repeated extension 2023-05-24 16:57:49 -07:00
Iavor Diatchki
f7d6a1453b Remove some warnings 2023-05-24 15:50:08 -07:00
Iavor S. Diatchki
db557b462b
Merge pull request #1521 from GaloisInc/instance-doc
Document the classes that inhabit the various overloading classes.
2023-05-24 15:37:22 -07:00
Iavor Diatchki
90585dc073 Make a note to update the docs if someone makes changes to the class instances 2023-05-24 13:09:31 -07:00
Iavor Diatchki
9addbc6365 Revert breaking change.
The PrimMap is not actually so much a about primitives, as it is
about "wired-in" names (i.e., built in names the Cryptol needs to
refer to)
2023-05-24 10:27:18 -07:00
Iavor Diatchki
de334589aa Make the remote-api build 2023-05-23 16:42:30 -07:00
Iavor Diatchki
31da6cb366 Restrict PrimMap to only refer to actual primtives.
Previously it would contain everything in the prelude.
Mostly this was not a problem because the usual use case for this is
to find out the names of actual primitives, so having more in the mapping
is not a problem.  However, this accuracy is inconveninet, if you
want to quickly look what's actually a primitive
2023-05-23 15:43:09 -07:00
Iavor Diatchki
08783625c1 Document the classes that inhabit the various overloading classes. 2023-05-23 11:23:36 -07:00
dependabot[bot]
758509447b
Bump requests from 2.28.2 to 2.31.0 in /cryptol-remote-api/python (#1520)
Bumps [requests](https://github.com/psf/requests) from 2.28.2 to 2.31.0.
- [Release notes](https://github.com/psf/requests/releases)
- [Changelog](https://github.com/psf/requests/blob/main/HISTORY.md)
- [Commits](https://github.com/psf/requests/compare/v2.28.2...v2.31.0)

---
updated-dependencies:
- dependency-name: requests
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2023-05-23 09:19:05 -04:00
Iavor Diatchki
64d58002f4 Merge branch 'master' into functors-merge 2023-05-15 10:16:41 -07:00
Ryan Scott
5eff6e530c
Python: Use poetry.core.masonry.api as build-backend (#1519)
This is motivated by a desire to switch away from `setuptools`, which has some
unfortunate interactions with static analysis tools.

This also bumps the `argo` submodule to bring in the changes from
https://github.com/GaloisInc/argo/pull/197, which applies similar changes.
2023-05-09 19:35:37 -04:00
Ryan Scott
ea2531f9e8
Merge pull request #1518 from GaloisInc/upgrade-poetry
CI: Upgrade Poetry and Python version
2023-05-08 17:25:45 -04:00
Ryan Scott
3080facea3 CI: Consistently use Python 3.11 2023-05-08 16:08:04 -04:00
Ryan Scott
1bae398b38 CI: Upgrade Poetry version
The version we were previously using (1.1.6) is affected by this bug, causing
invocations of Poetry to fail:
https://github.com/ionrock/cachecontrol/issues/292
2023-05-08 16:08:02 -04:00
Iavor Diatchki
5dafbe4020 Merge branch 'master' into functors-merge
# Conflicts:
#	src/Cryptol/ModuleSystem/NamingEnv.hs
2023-05-05 13:42:57 -07:00
Iavor Diatchki
1543bed522 Fix name export, to just put the module name the "module" field 2023-05-05 11:47:15 -07:00
Felix Yan
d4221b7e24
Correct a typo in NamingEnv.hs (#1516) 2023-05-03 07:06:09 -04:00
Iavor Diatchki
abbece3287 Merge branch 'master' into functors-merge
# Conflicts:
#	cryptol-remote-api/src/CryptolServer/Names.hs
2023-04-25 16:44:11 -07:00
Matthew Yacavone
d5a4463fae
Merge pull request #1512 from GaloisInc/better_names_cmd
Add more info to `names()` in Python API
2023-04-20 16:18:24 -04:00
Matthew Yacavone
ff0967abc7 add types to names(), etc. in Python, convert argument types to JSON in API 2023-04-20 15:16:34 -04:00
Iavor Diatchki
396b02bb35 Add a PP instance to PrimIdent 2023-04-20 11:25:46 -07:00
Matthew Yacavone
76f1db6ac5 remove Maybe Bool pattern in 'visible names' JSON, tweak docs 2023-04-13 18:30:18 -04:00
Matthew Yacavone
e8fc8f343d update Cryptol.rst with 'visible names' change 2023-04-13 13:54:53 -04:00
Matthew Yacavone
5a655ea287 tweak test_names.py 2023-04-13 13:19:14 -04:00
Matthew Yacavone
cf23e6f702 add test_names.py, fix docs, update CHANGELOG 2023-04-13 12:58:41 -04:00
Matthew Yacavone
ab4857440a handle parameters in names() instead of hanging 2023-04-12 17:00:12 -04:00
Matthew Yacavone
bd96bd5caa add property_names command 2023-04-12 13:28:12 -04:00
Matthew Yacavone
47a77612aa add remaining info from IfaceDecl to names command 2023-04-12 13:26:57 -04:00
Iavor Diatchki
05412e99a1 Things that depend on newtype constructors should depend on the newtypes
Fixes #1511
2023-03-29 10:51:10 -07:00
Iavor Diatchki
cb551e4718 Fix typos in comments 2023-03-29 10:50:37 -07:00
Iavor Diatchki
0289fbfbc1 Add a test for #1510 2023-03-28 14:37:56 -07:00
Iavor Diatchki
cbd87a8a9c Fix more tests 2023-03-28 14:32:00 -07:00
Iavor Diatchki
70a1592de6 Fix test 2023-03-28 13:55:07 -07:00
Iavor Diatchki
4c269e8722 Apply substitution to nested functors as well
Fixes #1510
2023-03-28 11:33:10 -07:00
Iavor Diatchki
f49261f26b Print nested functors also 2023-03-28 11:32:12 -07:00
Iavor S. Diatchki
3c5f6ff3a0
Merge pull request #1509 from GaloisInc/functors-merge-doc-cleanup
Functors merge doc cleanup
2023-03-24 11:11:07 -07:00
Ian Sweet
24a708b929 bring up to date with functors-merge 2023-03-24 12:16:40 -04:00
Iavor Diatchki
c9bdd5de3f Merge branch 'master' into functors-merge
# Conflicts:
#	CHANGES.md
2023-03-24 09:09:32 -07:00
Iavor Diatchki
8a43ba678d Add a test 2023-03-23 15:47:29 -07:00
Iavor Diatchki
0d271bcb36 Some code to print a full newypt declaration 2023-03-23 15:41:30 -07:00
Iavor Diatchki
7f078c37a3 Apply substitution to embedded newtype definition as well
Fixes #812
2023-03-23 15:40:45 -07:00
Iavor Diatchki
ba30b60267 Unused extensions 2023-03-23 15:39:41 -07:00
Iavor Diatchki
b669a61611 Remove id application that does nothing 2023-03-23 15:06:49 -07:00
Iavor Diatchki
ca0310ff58 Use standard definition 2023-03-23 15:05:45 -07:00
Ian Sweet
6ee9220a53 cryptol module docs: tightened some writing, fixed some typos, and introduced the term 'functor' as it was used without definition. 2023-03-23 11:05:11 -04:00
Ryan Scott
9382d52754
cryptol-remote-api: Restore the ability to build with vector-0.12.* (#1506)
The downstream `saw-remote-api` library doesn't quite support `vector-0.13.*`
yet, but GaloisInc/cryptol#1499 accidentally restricted `cryptol-remote-api`'s
build plan to only allow `vector-0.13.*`. This restores the ability to build
`cryptol-remote-api` with `vector-0.12.*` for `saw-remote-api`'s sake.
2023-03-13 14:02:26 -04:00
Ryan Scott
c941eddc23
Merge pull request #1504 from GaloisInc/T1503
Add CVC5 support
2023-03-06 16:57:12 -05:00