* Limitations:
Does not work in combination parameterized modules, as I am
about to redo how that works.
* General refeactorings:
* Namespaces:
- We have an explicit type for namespaces, see `Cryptol.Util.Ident`
- Display environments should now be aware of the namespace of the
name being displayed.
* Renamer:
- Factor out the renamer monad and error type into separate modules
- All name resultion is done through a single function `resolveName`
- The renamer now computes the dependencies between declarations,
orders things in dependency order, and checks for bad recursion.
* Typechecker: Redo checking of declarations (both top-level and local).
Previously we used a sort of CPS to add things in scope. Now we use
a state monad and add things to the state. We assume that the renamer
has been run, which means that declarations are ordered in dependency
order, and things have unique name, so we don't need to worry about
scoping too much.
* Change specific to nested modules:
- We have a new namespace for module names
- The interface file of a module contains the interfaces for nested modules
- Most of the changes related to nested modules in the renamer are
in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename`
- There is some trickiness when resolving module names when importing
submodules (seed `processOpen` and `openLoop`)
- There are some changes to the representation of modules in the typechecked
syntax, in particular:
- During type-checking we "flatten" nested module declarations into
a single big declaration. Hopefully, this means that passes after
the type checker don't need to worry about nested modules
- There is a new field containing the interfaces of the nested modules,
this is needed so that when we import the module we know we have the
nested structure
- Declarations in functor/parameterzied modules do not appear in the
flattened list of declarations. Instead thouse modules are collected
in a separate field, and the plan is that they would be used from
there when we implmenet functor instantiation.
This allows us to express enumerations with exclusive upper bounds.
In contrast with the `Literal` constraint, `LiteralLessThan n a`
express that `a` contains all the literals strictly less than `n`,
and explicitly allows `n` to be `inf` for unbounded types like
`Integer` and `Rational`.
It is possible to define `Literal n a` as
`(fin n, LiteralLessThan (n+1) a)` instead of leaving it primitve.
However, this makes infered types and error messages worse, IMO.
As it stands, the typechecker has no real knowledge of the connection
between `Literal` and `LiteralLessThan`.
We now reject situations where the user writes a type application
on a term that is not an identifier, and we correctly unwind
and reapply tuple and field selectors.
Fixes#962Fixes#1045Fixes#1050
to a kind-checking error. This at least provides actionable
feedback about where the error occurs.
We should also improve the parser post-processing pass to
handle these situations better, but this at least removes
the panic.
This allows us to attach information to `EFun` nodes that describe
which named function the lambda belongs to, and which arguments
it handles. This information is filled in by the `NoPat` pass
as it desugars multi-argument functions into a sequence of lambdas
and is used during typechecking to produce error messages.
There is an odd potential for the renamer to get things wrong here.
If a named function has an argument that shadows it's own name,
the renamer may incorrectly resolve the name in a function description
for later arguments. The resulting error message will then point to
the wrong name (although it will be in the vicinity...). It's hard
to fix this without folding the NoPat pass into the renamer (which
we should also do, but it's a nontrivial refactoring).
Multi-argument functions are now desuguared into nested lambdas
in the `NoPat` phase instead of during typechecking. This gives
more sensible results when the same variable is shadowed in the argument
list. In particular, extra "where" bindings that are added for pattern
desugaring now have a scope that is outside patterns and variables
occuring further to the right.
Some programs that used to produce "overlapping symbols" errors are
now accepted with a shadowing warning instead.
The main downside of this refactoring is that the `checkFun` operation
no longer has access to function name or argument numbers for definitions,
as all functions have become single-argument lambdas by typechecking time.
This can be fixed by recording this information in the AST during the
NoPat desugaring instead.
The name binding structure that results from multi-parameter
functions with repeated names, and the interaction with pattern
desugaring is currently very counterintuitive. See issue #567 for
more discussion.
