Edwin Brady
d053a18977
Set fresh name counter on loading Main ttc
...
Make sure this is the counter from the right namespace, or we might get
name clashes at the REPL
2019-06-27 14:47:47 +01:00
Edwin Brady
0d01257ede
Set fresh name counter on loading Main ttc
...
Make sure this is the counter from the right namespace, or we might get
name clashes at the REPL
2019-06-27 13:42:49 +01:00
Edwin Brady
ce78abaaef
Build and save references for metavars too
...
This wasn't necessary before, since we always inlined, but since we can
now postpone things longer and don't always inline until much later, we
need to know what names everything refers to earlier.
2019-06-27 09:01:59 +01:00
Edwin Brady
2cd81a9eb0
More tests moved over...
2019-06-25 21:50:48 +01:00
Edwin Brady
3eda2494bf
Add error message tests
2019-06-25 21:46:28 +01:00
Edwin Brady
7b504e7a9e
More Chez tests
2019-06-25 21:27:46 +01:00
Edwin Brady
69199639cf
Fix Nat hack
...
And add chez scheme section to tests, with one initial test
2019-06-25 14:05:54 +01:00
Edwin Brady
bf64f843aa
A bit more totality checking polish
...
Need to check for 'assert_total' in getRefs, and get Inf and Lazy the
right way around!
2019-06-25 12:57:49 +01:00
Edwin Brady
0b4f4ec46d
Fix naming issue in totality checker
...
Also added a new test
2019-06-25 10:26:14 +01:00
Edwin Brady
5caa277cbe
Fix some totality issues, add tests
...
These are related to the change in naming and metavariables, mostly
2019-06-25 00:42:52 +01:00
Edwin Brady
e68b9134e7
Calculate parameter positions in types
2019-06-24 19:31:25 +01:00
Edwin Brady
fb7190b337
Add first batch of totality checking tests
2019-06-24 18:14:07 +01:00
Edwin Brady
b1acceb870
Add a simple lazy Inf test
2019-06-24 18:08:32 +01:00
Edwin Brady
32583d608d
More interface tests
...
and a small fix for the generation of method types which was okay for
Blodwen, but not here
2019-06-24 18:04:43 +01:00
Edwin Brady
e9514f3c22
Add first interface tests
2019-06-24 17:36:55 +01:00
Edwin Brady
e6292acdf0
Finish adding interactive tests from Blodwen
...
This involved implementing the 'TryWithImplicits' hack for allowing
unbound implicits in types with case blocks
2019-06-24 16:23:32 +01:00
Edwin Brady
1e2fcb8ccd
Fix small error is as patterns
...
Also added new interactive test
2019-06-24 15:30:36 +01:00
Edwin Brady
7a47c9ae0c
Add a couple of interactive tests
2019-06-24 15:16:49 +01:00
Edwin Brady
881426e62a
Add initial CONTRIBUTING.md
2019-06-24 15:06:27 +01:00
Edwin Brady
18f269bbef
Add some notes
...
Mostly copied from Blodwen and brought up to date (more or less).
2019-06-24 13:05:19 +01:00
Edwin Brady
af9dc69c61
Add record tests from Blodwen
2019-06-24 12:44:34 +01:00
Edwin Brady
aebb8ddfde
Need to update full names in metadata
...
We need to do this as we're building, not just on saving, because we
might immediately use it when searching for full definitions.
2019-06-24 09:51:02 +01:00
Edwin Brady
0a15c2cda1
Pay attention to visibility of names
...
Name lookup and search should ignore names which aren't visible (that
is, private names in another namespace)
2019-06-24 00:57:22 +01:00
Edwin Brady
67a43e0000
Check names are visible/public
2019-06-24 00:12:58 +01:00
Edwin Brady
40ea548a65
Cache whether a local is let bound, if we can
...
Since lookup up a binding can be expensive in a big environment, and we
only need to reduce it if it turns out to be a let, caching it can be a
noticeable win
2019-06-23 23:12:27 +01:00
Edwin Brady
9c902de5d1
Fix case tree compiler for coverage checking
...
We can't refine by a name in Rig0 because we can't assume it covers all
possibilities, so only refine by them at the end, at which point we
check that there's only one case left (otherwise we have to match on it,
which is not allowed for an erased thing)
2019-06-23 20:36:06 +01:00
Edwin Brady
9350122e1b
filterM was quadratic time. Oops!
...
Some care is still needed with ! notation because it lifts out of the
branches in if blocks and it really shouldn't...
2019-06-23 16:04:32 +01:00
Edwin Brady
1a333a481b
Process name directives from TTC
2019-06-23 12:52:37 +01:00
Edwin Brady
f77ef8154b
No longer any need for NameRefs
2019-06-22 22:36:15 +01:00
Edwin Brady
2df399a03c
Save definitions as Binary
...
Then on reloading, only decode the Binary when it's first looked up.
This is a huge win on loading because it's decoding the binary blob that
costs, rather than loading it!
2019-06-22 20:40:16 +01:00
Edwin Brady
7ba57cfc64
Store names in full in ttc
...
and resolve on reloading. This saves the time for loading the name map,
which can start to get big if there's lots of imports.
2019-06-22 16:09:43 +01:00
Edwin Brady
c3a4360ee9
Add missing ipkg
2019-06-19 18:50:46 +01:00
Edwin Brady
02c2358093
Add missing Makefile
2019-06-19 18:49:53 +01:00
Edwin Brady
60837bd599
Add interface HasNames
...
This allows conversion between structures with explicit names vs
resolved names
2019-06-19 00:59:55 +01:00
Edwin Brady
c21918e1f5
Add TTC interface Binary
...
This will let us decode things later, so we're not required to decode
Binary data immediately on loading from a TTC
2019-06-18 22:02:52 +01:00
Edwin Brady
070869f387
Add EmptyFC as a constructor
...
This way we don't have to keep rebuilding it every time when decoding
Terms from binary
2019-06-18 21:03:20 +01:00
Edwin Brady
76e2bd30e6
Slightly simpler binary writing
...
Easier just to have one chunk, starting pretty big, and grow it and copy
content if necessary
2019-06-18 18:10:24 +01:00
Edwin Brady
318a6eeab9
Add arguments to NForce
...
If it gets stuck, it could have a stack of arguments and we can't just
throw them away!
2019-06-18 09:42:00 +01:00
Edwin Brady
ed2d88b87e
Unelaboration of case blocks
...
This was identifying the old blodwen style name, also we need to store
patterns in ibcs after all if we want to see the unelaborated block
contents
2019-06-17 14:08:07 +01:00
Edwin Brady
2cdfac47b0
Look for case splits under As patterns
2019-06-17 13:46:54 +01:00
Edwin Brady
f1becb4ae0
Fix 'last chance' auto search
...
Need to record the solution as well as find it! Too much copying from
Blodwen without thinking here :)
2019-06-17 12:35:42 +01:00
Edwin Brady
6a72508e80
Eliminate cycles in auto search
...
This is important for, e.g. interfaces with parent constraints, so we
don't keep looping making the constraint bigger
2019-06-17 09:50:05 +01:00
Edwin Brady
8bc46c3438
Remove spurious assignment!
...
Left over from before pruneByType was implemented. Oops!
2019-06-16 23:23:57 +01:00
Edwin Brady
f5a5d01274
Turn lets to lambdas in hole environments
...
This works better when lifting lemmas, and ensures that the type of
everything will be shown and not normalised away
2019-06-16 23:10:32 +01:00
Edwin Brady
620ad8e706
Find linear bindings needs to know about As
2019-06-16 21:33:59 +01:00
Edwin Brady
ecb5cb1e40
Don't keep running delayed elaborators
...
Also fix a bug where the elaborator state wasn't updated on completing
the delayed elaborator, which could cause issues with implicitly bound
names in particular.
2019-06-16 20:48:31 +01:00
Edwin Brady
8d6b990157
No need to evaluate in 'instantiate'
...
Types are generated from the environment, and we only want to know how
many arguments there are
2019-06-16 15:24:52 +01:00
Edwin Brady
4bc87b4c72
Some TTC/Delay fixes
...
Need to run delayed elaborators before binding implicits, since there
might be some inside the delayed elaborator. Also reorganise TTC
implementations so they're all in one place.
2019-06-16 13:47:20 +01:00
Edwin Brady
dcae2c3386
Only write out names which are actually used
...
Rather than all the metavariables ever created, just the ones which end
up in terms (e.g. after inlining)
2019-06-15 18:28:41 +01:00
Edwin Brady
1be12c7f72
Block reduction of private/export names
2019-06-15 16:10:01 +01:00
