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
Edwin Brady
ed43fd49b9
Save FC so that metadata works
2019-06-15 13:28:27 +01:00
Edwin Brady
a7bf075c94
Get GlobalHint flag right
...
'True' means a default hint, which is only used if all else fails (and
is only really intended to get default Integer)
2019-06-15 12:42:35 +01:00
Edwin Brady
c121910298
Add 'base' libraries
2019-06-15 11:54:22 +01:00
Edwin Brady
46c29c2ee4
Tweak rules for usableLocal in search
...
Needs to be allowed to search for things indexed by pattern variables,
which are not really holes in the same sense, or it might not find
things in types.
(Aside: we're currently implicitly binding failed searches in types,
which is, I think, wrong... better to report the failure)
2019-06-14 19:00:16 +01:00
Edwin Brady
8f386011b1
Defer erasure/run-time case trees
...
Don't build these until we've completed the whole clause (that is, don't
do it if we're inside a case block) because we might need to collect
more information to complete checking the case block. e.g. there may be
constraints inside the case block that are resolved outside.
2019-06-14 18:35:31 +01:00
Edwin Brady
2f7aa69f41
Remove AppInfo
...
It's just in the way, we don't use it for anything, and everything we
might get out of it we're already getting out of the type. Revisit later
if it turns out to be worth it.
2019-06-13 19:33:10 +01:00
Edwin Brady
2c1c86639a
Update makefiles and paths
...
We can now build and install the prelude, and hello world has
successfully compiled to chez
2019-06-13 16:53:16 +01:00
Edwin Brady
772b098de0
The Prelude type checks!
2019-06-13 13:23:21 +01:00
Edwin Brady
2374f23320
Add default alternatives
2019-06-11 13:52:49 +01:00
Edwin Brady
07229bdb5e
Add first Idris2 tests
2019-06-11 11:54:47 +01:00
Edwin Brady
94cc2a0d4c
Store type search hints separately
...
If we store them on the type constructor, we're required to have the
construction available, which might not be the case when reloading ttcs,
because we load and process modules *before* things they import.
2019-06-10 16:11:32 +01:00
Edwin Brady
803867006b
Add some missing files!
2019-06-09 23:14:27 +01:00
Edwin Brady
5a3aa3b13c
Some fixes for as patterns, add them implicitly
...
Much of the effort in renaming is to make types of holes display more
nicely!
2019-06-09 23:12:11 +01:00
Edwin Brady
146c301f6c
Change main program to be Idris2
...
With the --yaffle flag, you get the old behaviour which is to invoke the
checker for the core theory (and all the tests are updated appropriately
for this).
2019-06-09 11:58:29 +01:00
Edwin Brady
9d2067e9a8
Add command line option to invoke yaffle
2019-06-08 11:02:50 +01:00
Edwin Brady
c6a7050d39
Added Idris.Main
2019-06-07 11:29:29 +01:00
Edwin Brady
2afad1f13c
Add package files
2019-06-07 11:14:45 +01:00
Edwin Brady
b9e67db95d
Add REPL
2019-06-07 11:08:21 +01:00
Edwin Brady
c420082a43
Add Scheme back ends from Blodwen
2019-06-06 18:33:50 +01:00
Edwin Brady
8132378b04
Add Compiler.Common
...
This is generic compiler infrastructure (mainly finding all the names
used from a root expression)
2019-06-06 18:13:25 +01:00
Edwin Brady
18221f8f2d
Add inlining for CExps
2019-06-06 09:51:30 +01:00
Edwin Brady
169a958105
Compiling to CExp
2019-06-05 21:25:03 +01:00
Edwin Brady
bf67f5c87c
Record mutual type definitions
...
Also add some tests for totality checker
2019-06-05 17:28:55 +01:00
Edwin Brady
95cc48eeb6
Add termination checking
...
Still to do: mutual data definitions and proper testing
2019-06-05 15:59:35 +01:00
Edwin Brady
2c6202879e
Calculate missing cases via coverage checker
2019-06-02 23:43:21 +01:00
