Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Functors iface tysyn #1459

Closed
wants to merge 70 commits into from
Closed

Functors iface tysyn #1459

wants to merge 70 commits into from

Conversation

yav
Copy link
Member

@yav yav commented Oct 25, 2022

No description provided.

yav and others added 30 commits June 13, 2022 15:56
When we resolve an undfined name we record error, but we continue
processing things, so that we can report multiple errors.  As a result
we need to generate some sort of fake "real" name for the undefined entity.

Previously we used to generate a fake local name, but that confused parts
of the code that expected certain things to always be defined at the top
level.  So now we generate a fake name in the Cryptol prelude instead.
Also, for the names of the imported instances now
use the location in the file to make them unique,
rather than a synthetic counter,
Still to do: modules and funcotrs
yav and others added 28 commits September 24, 2022 15:34
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
# 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
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
PR #1403 accidentally removed our build coverage for an older Ubuntu LTS
configuration. This patch adds in back and ensures that we don't accidentally
run the tests on this configuration.
# Conflicts:
#	src/Cryptol/TypeCheck/Sanity.hs
This is mostly for debugging.
When loaded an interface is treated like an empty functor.
Adding this capability would also be useful if we generalize
interfaces to allow for definitions, as discussed in #1457

This also fixes #1456
@yav yav marked this pull request as draft October 25, 2022 16:20
@yav yav closed this Oct 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants