Commit Graph

421 Commits

Author SHA1 Message Date
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
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