-
Notifications
You must be signed in to change notification settings - Fork 3
/
TODO
42 lines (36 loc) · 1.61 KB
/
TODO
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
Short term things to do:
* Either String better rhan Monad m?
* Fix naming bug --- terms of form t1 -> t2 automatically give t1 the
name X, which can clash. Particularly a problem in data type declarations.
* Current naive proof state representation is far too slow. Come up
with something better.
* Keep track of level in proof state.
* Keep track of binding level in context, and check at point of use.
* Allow dump of global context to disk, for fast reloading.
* Syntax for equality.
* Elimination with a motive.
* Unit tests - at least check nat.tt, vect.tt, JM equality,
primitives, simple staging, compiler.
* More readable high level language for function definition. Really
just has to use tactic engine to translate simple case expressions into
D-case calls.
* Separate API into several files for clarity.
* Allow call <fn args> _ in raw terms; i.e. allow the typechecker to
spot recursive calls, rather than needing a tactic to do so.
* Finish compiler by:
- Finding a method of exporting primitive types
- Implement compilation of D-Case
Things which could be done to the library, in no particular order
(other than the order I thought of them in...):
* A higher level dependently typed language might be useful (e.g. like
Coq's language). If not useful, at least fun :).
* Namespace management.
* Some useful error messages from the Parsec parsers would be nice.
* Proper type universes, of some form.
* Generate DRec and DNoConfusion as well as DElim/DCase.
* Build in Sigma types? (At least a nicer syntax?)
* Infix operators, especially = would be nice.
Tactics:
* Injectivity.
* Discriminate.
* Inversion.