edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-22 12:21:30 +03:00
Code Issues Projects Releases Wiki Activity
202 Commits 2 Branches 1 Tag 4.2 MiB
99dac56e1e
Commit Graph

187 Commits

Author SHA1 Message Date
Edwin Brady
99dac56e1e Make sure matches are not too specific 
i.e. if an argument has a polymorphic type, we shouldn't allow a
concrete type in its place
 2019-06-29 19:28:04 +01:00
Edwin Brady
cda87a9c16 Fix coverage checker issue 
Don't use the type of a scrutinee to restrict possible patterns, because
it might have been refined by a Rig0 argument that has a missing case.
Instead, generate all the possible cases and check that the generated
ones are impossible (there's no obvious change in performance)
 2019-06-29 16:41:26 +01:00
Edwin Brady
39836f3cd0 Fix instantiation in pattern unification 
There was an optimisation that wasn't valid, and it turns out it doesn't
have any useful effect anyway.
 2019-06-28 19:41:25 +01:00
Edwin Brady
9b44839c57 Add test for eta 2019-06-28 12:43:55 +01:00
Edwin Brady
e9a3167e2f Even more tests 
Small change needed to fix one - assume given implicits which are of the
form x@_ arise from types. It's a bit of a hack but I don't think
there's any need for anything more complicated.
 2019-06-27 20:19:00 +01:00
Edwin Brady
b0cad15c65 Refine dot pattern rules 
Only valid if unifying the pattern at the end doesn't solve any
metavariables. Also when elaborating applications of fromInteger etc to
constants on the LHS we need to be in expression mode, then reduce the
result later.
 2019-06-27 19:16:33 +01:00
Edwin Brady
211de419bb Fix environments for nested names 
This was a slight difference from Blodwen that wasn't accounted for -
there might be lets in the nested environment, so when building the
expanded application type, make sure we go under them
 2019-06-27 15:26:18 +01:00
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
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
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
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
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
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
Edwin Brady
ed43fd49b9 Save FC so that metadata works 2019-06-15 13:28:27 +01:00