Commit Graph

276 Commits

Author SHA1 Message Date
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
Edwin Brady
1f52530313 Implement 'impossible' 2019-06-02 21:21:07 +01:00
Edwin Brady
f5556a1a9d Add Core.Coverage
Little of the recently added bits are wired up yet, but it'll all start
coming together soon.
2019-06-02 20:03:41 +01:00
Edwin Brady
bdc38d438c Add CompileExpr 2019-06-02 17:54:55 +01:00
Edwin Brady
0fa61f7c4f Add compiler support files 2019-06-02 17:31:59 +01:00
Edwin Brady
5c2d78e893 More of the Idris machinery
ModTree and ProcessIdr
2019-06-02 17:24:39 +01:00
Edwin Brady
8302fb08a7 Bring in more bits of IDE mode 2019-06-02 15:38:39 +01:00
Edwin Brady
d6e637b2c5 Fix structural difference check in search
Now it successfully finds zipWith too
2019-06-02 15:16:54 +01:00
Edwin Brady
b41bd48970 Add MakeLemma 2019-06-02 14:41:21 +01:00
Edwin Brady
109dcf08f9 Add definition generation 2019-06-02 14:28:26 +01:00
Edwin Brady
af79e57ae2 Store number of locals in holes
This gives useful information for expression search, because we can add
lambdas while we're still building the environment, and start looking at
locals after that.
2019-06-02 01:23:01 +01:00
Edwin Brady
bf70aa07d2 First attempt at expression search
Not quite there yet because we're not saving all the information about
holes in TTCs but the basics work
2019-06-01 22:34:59 +01:00
Edwin Brady
ae28f1b1f2 Add CaseSplit
Adapted from Blodwen version
2019-06-01 19:05:02 +01:00
Edwin Brady
b1f7863830 Add Implementation and Interface
It turns out we need a new kind of map, mapping possibly ambiguous names
to values. This is what 'Context' does but we can only have one of them
because it resolves names to a position in an array and it'd be
confusing to have more than one index per name.
2019-06-01 18:13:19 +01:00
Edwin Brady
d82f6c5080 Add errors, REPLCommon now builds 2019-06-01 15:53:16 +01:00
Edwin Brady
2e2622c38b Add more of the high level stuff 2019-06-01 15:05:04 +01:00
Edwin Brady
a7d7785a0a Added Idris.Socket
In preparation for REPL and IDE mode
2019-06-01 14:13:28 +01:00
Edwin Brady
5bbab03e38 Added Idris.Desugar
Mostly adapted from Blodwen, also added necessary bits to the context
such as name directives and hiding.
2019-06-01 14:11:21 +01:00
Edwin Brady
67cbf05b4c Add parser for high level syntax
Almost entirely unchanged from Blodwen
2019-05-31 18:50:07 +01:00
Edwin Brady
a3bf2e3aa9 Start on the high level syntax
Copied and adapted Idris.Syntax from Blodwen, updated to cope with new
core.
2019-05-31 18:48:04 +01:00
Edwin Brady
a05c656d76 Record editing metadata and interface hashes 2019-05-31 11:42:11 +01:00
Edwin Brady
2b38ce0188 Add Metadata type
Metadata is now propagated through the elaborator, although we're not
using it yet
2019-05-31 05:52:54 +01:00
Edwin Brady
6c88bfec7a Elaborate 'with' blocks 2019-05-29 11:57:07 +01:00
Edwin Brady
a59a104230 Implement 'rewrite' expressions
Mostly direct from Blodwen (some minor modifications to deal with new
way of going into a new scope in the elaborator as well as the usual
bits dealing with name lookup and Glued terms)
2019-05-27 12:15:37 +01:00
Edwin Brady
7cc37d28b3 Add (dependent) record update
This is pretty much straight from Blodwen
2019-05-27 10:56:13 +01:00
Edwin Brady
22a5286ed9 Added record declarations
Also, since it could need it when building types, added auto implicit
binding (so no need for $ everywhere in the tests from now on...)
2019-05-26 23:51:20 +01:00
Edwin Brady
c4d7e18742 Extend unification so that Functors work
Need to identify invertible (or cancellable) holes so that we can unify
e.g. ?f Nat with List Nat and get f = List.
2019-05-26 18:41:48 +01:00
Edwin Brady
628a7bde0f Improve auto search to support interfaces
Parser now allows options on data types and functions, and elaborator
processes options so we can set up interfaces
2019-05-26 14:28:38 +01:00
Edwin Brady
3e3c224bcb Move some tests around
Add a 'search' category
2019-05-26 11:34:02 +01:00
Edwin Brady
18e0cabc26 Save hints to TTC files
And process them on loading. We record that hints need saving out when
adding them, and clear that list unless we happen to be reexporting the
thing we've just read (import public).
2019-05-25 23:31:47 +01:00
Edwin Brady
54d4d5a8ed Implement auto implicits 2019-05-25 22:13:38 +01:00
Edwin Brady
c65285a1f6 Check pattern variables don't unify with things
This is bad because it means a pattern variable isn't actually a
variable, but rather has a specific value!
2019-05-25 20:18:43 +01:00
Edwin Brady
6c7f13d128 Implement dot patterns
Like Idris 1, these are implicitly added on encountering a repeated name
or a non-constructor application. Unlike Idris 1 (and Blodwen) they are
checking by unification rather than matching (which means in particular
that function argument names can't be bound in dot patterns) which is
slightly less expressive, but better overall because matching is
potentially more error prone.
2019-05-25 18:39:21 +01:00
Edwin Brady
c75569c255 Implement laziness
Slight change of plan: instead of having special names, add Lazy, Inf,
Delay and Force and keywords and elaborate them specially.
Correspondingly, add DelayCase for case trees. Given that implicit
laziness is important, it seems better to do it this way than constantly
check whether the name we're working with is important.

This turns out to make implicit laziness much easier, because the
unifier can flag whether it had to go under a 'Delayed' to succeed, and
report that back to the elaborator which can then insert the necessary
coercion.
2019-05-22 19:42:43 +01:00
Edwin Brady
9f4ca9e67f Add pruneByType
This shortcuts ambiguity checking by only keeping the things which have
the target type. Given a set of ambiguous applications, the rules are:

- keep any which return the expected target type (a concrete match), or
  a polymorphic type (a possible match)
- if there are any concrete matches, drop any possible match which has
  the '%allow_overloads' flag set (in practice this will be interface
  methods, but other things can be flagged).
- if there ar eno matches, keep everything so that the error messages
  show everything that went wrong.
2019-05-21 12:11:55 +01:00
Edwin Brady
c2e1b85143 Let's not use exceptions for control flow... 2019-05-20 19:05:28 +01:00
Edwin Brady
6385cb6e0f A bit more on performance
Most notably, when elaborating deferring argument, if the hole
standing for the argument is still a hole, fill it in directly rather
than going via unification. This prevents some needless evaluation.
2019-05-20 18:41:08 +01:00
Edwin Brady
11a72dc953 Some small tweaks
These are attempts to allocate slightly less memory. They don't achieve
much, but also don't do any harm...
2019-05-20 13:36:32 +01:00
Edwin Brady
0ac539fdc2 Substitute a whole environment at once 2019-05-19 23:41:02 +01:00
Edwin Brady
871ca6603c Move options out of Core and into Defs
This is quite a performance win, because there's less thunking (and I
imagine more scope for inlining?)
2019-05-19 23:25:35 +01:00
Edwin Brady
f95205b8b9 Some small performances improvements
The biggest one being that logging wasn't taking the String as a lazy
argument!
2019-05-19 23:05:21 +01:00
Edwin Brady
d256dbf5ec Add a test for non linear LHS 2019-05-19 20:30:27 +01:00