Iavor Diatchki
a0b43eef33
Add another test
2022-06-10 15:38:34 -07:00
Iavor Diatchki
9f8d711638
Add some documentation about the module system
2022-06-10 15:38:25 -07:00
Iavor Diatchki
87e51efbe6
Fix up the manual so that sections works properly
2022-06-10 11:41:21 -07:00
Iavor Diatchki
64ba445019
Add a separate notation for imposing constraints on multiple module parameters
2022-06-10 10:44:00 -07:00
Iavor Diatchki
381612d4f1
Solve generated goals for signatures
2022-06-10 09:18:55 -07:00
Iavor Diatchki
ca17f7f6df
Treat parameter groups specially if they contain only constraints
2022-06-09 15:46:09 -07:00
Iavor Diatchki
7e3d65090c
Fixup module system tests
2022-06-09 14:21:19 -07:00
Iavor Diatchki
75f19382b6
Don't warn for unused type parameters
2022-06-09 14:20:23 -07:00
Iavor Diatchki
1d5a0f0a79
Funky comment for quick recommenting
2022-06-09 14:20:08 -07:00
Iavor Diatchki
da30b1c71a
Report unused warnings for nested modules
2022-06-09 14:15:07 -07:00
Iavor Diatchki
ff7117462b
Better error location
2022-06-09 13:54:54 -07:00
Iavor Diatchki
4c5c13c1b1
Comments
2022-06-09 13:54:47 -07:00
Iavor Diatchki
c179d419d9
Only consider public names when instantiating a module
2022-06-09 11:05:00 -07:00
Iavor Diatchki
1cfe50850b
Merge public and private in interfaces. One may consult IfaceNames to determine what's public
2022-06-09 10:56:37 -07:00
Iavor Diatchki
2a8391d02e
Rewrite with unless for convenince while debuging (unless is imported)
2022-06-09 10:55:11 -07:00
Iavor Diatchki
be27abb84d
Report errors if things that shouldn't have parameters do (syntactically)
...
We do this here, because we have no good way to represent such things
anyway, so we might as well report an error.
2022-06-09 10:36:13 -07:00
Iavor Diatchki
0c1b2743fd
Remove backtick names, except for reproting an error in the parser
2022-06-08 16:55:25 -07:00
Iavor Diatchki
fdac77622d
Normalize module names when comparing for correct file name
2022-06-08 16:46:32 -07:00
Iavor Diatchki
331dee48b1
Make anonymous module parameters and interface modules work
2022-06-08 16:08:37 -07:00
Iavor Diatchki
743c689a10
Add a test for a type-level interface module
2022-06-08 13:42:00 -07:00
Iavor Diatchki
af0af83f8d
Don't warn on interfaces that only declare types.
2022-06-08 13:41:47 -07:00
Iavor Diatchki
cdbd9b309f
Fix more tests
2022-06-08 11:21:56 -07:00
Iavor Diatchki
308e346069
Fix tests, rename some uses for "signature" to "interface" but not all
2022-06-08 11:01:37 -07:00
Iavor Diatchki
5f816c8ef5
Checkpoint: functional top-level signatures?
2022-06-08 10:26:21 -07:00
Iavor Diatchki
e08548dff0
Pass in top level signatures to the type checker
2022-06-07 11:44:18 -07:00
Iavor Diatchki
52a907f9b4
Now TC gets module full module parameters, rather then exploding them by name
2022-06-07 11:13:14 -07:00
Iavor Diatchki
16f6a95efd
Add a field to keep track of loaded signatures.
2022-06-07 11:01:08 -07:00
Iavor Diatchki
1020f76fbe
Move module parameters datatype from Interface to the typechecker
2022-06-07 10:43:09 -07:00
Iavor Diatchki
2c8cfd2499
Renamings and comments
2022-06-07 10:05:57 -07:00
Iavor Diatchki
6a1f12e42c
Remove OldStyleParameters, which were unused
2022-06-07 09:53:31 -07:00
Iavor Diatchki
07ca544268
Some more tests
2022-06-06 17:27:41 -07:00
Iavor Diatchki
1b42bb5e6a
Better error
2022-06-06 17:27:30 -07:00
Iavor Diatchki
f426edca1c
Fix tests that should be passing
2022-06-06 17:02:41 -07:00
Iavor Diatchki
5c4b74b7a9
Remove accidentally committed debug lines
2022-06-06 16:58:02 -07:00
Iavor Diatchki
5578437e2c
Checkpoing: make signatures into a special kind of module.
...
Still need to refactor interfaces to account for top-level signatures
2022-06-06 14:46:54 -07:00
Iavor Diatchki
4ce271db02
Don't allow functors to import signatures defined in them
2022-06-03 11:16:33 -07:00
Iavor Diatchki
ce42b14fa7
Fix the mapping from nested modules to original names
2022-06-03 10:41:44 -07:00
Iavor Diatchki
c9d9f2c676
Just a comment
2022-06-02 17:08:17 -07:00
Iavor Diatchki
e774861966
Top-level instatiations.
2022-06-02 16:18:24 -07:00
Iavor Diatchki
6bd2ab6bc8
Make imported signatures work
2022-06-02 14:38:14 -07:00
Iavor Diatchki
a56b6ef08e
Implement anonymous modules for nested modules.
...
This doesn't work for top-level modules, as we need to figure out a
way to name the anonymous module in that case.
2022-06-01 16:22:34 -07:00
Iavor Diatchki
791d97a448
Checkpoint: refactoring in prep for supporting anonymous modules in instances
2022-06-01 15:52:41 -07:00
Iavor Diatchki
e681c322e9
Remove backtick imports
2022-06-01 14:33:29 -07:00
Iavor Diatchki
403f9db9ec
Treat top-level parameter declarations as declaring and importing a signature
...
Also some more tests
2022-06-01 14:22:54 -07:00
Iavor Diatchki
ecce7457c9
Add some tests
2022-06-01 11:05:59 -07:00
Iavor Diatchki
b7c8ad2e47
Add location and don't check goals twice
2022-06-01 11:05:47 -07:00
Iavor Diatchki
ea17f0ad9c
Remove debug stuff
2022-06-01 11:04:11 -07:00
Iavor Diatchki
948e4d37cc
Switch back to representing module type paramters as type variables.
...
This works better with our existing solver, as the solver doesn't really
know how to deal with assumptions on abstract types.
This commit also adds the top-level constraints from the functor, which
we'd forgotten previously.
This reverts commit bfc1633378
2022-06-01 10:39:39 -07:00
Iavor Diatchki
6585d344d9
Don't panic if simplification changes the predicate to true or and.
2022-06-01 09:24:59 -07:00
Iavor Diatchki
2ec12a4c05
Partially functional module system. Still some bugs to fix.
2022-05-31 16:50:38 -07:00
