Features -------- * structured verbosity * debug information * Use substitutions for meta dependencies (at least for printing). We'll need to remember the number (or names?) of dependency args. How to show that a meta variable cannot depend on a particular variable? * lazy evaluation * unify primitive and {-# BUILTIN #-} * with-clauses * allow module instantiation before top-level module(?) * abstract open (need to re-type check to make sure the abstraction is solid) * implement the CHIT-CHAT module system Fixes ----- [Parsing] * allow more things in postulates (infix, private, ..) * allow postulates in mutual * Check out lex/parse errors (what position and what input is reported). [Printing] * print names properly qualified (we want to be able to parse it back) * get precedences right for things that aren't visible at the top level (requires having the right scope during type checking) * print patterns in mixfix notation (AbstractToConcrete) [Scope] * scope checking yields impossible when things clash (doesn't scope checking check for name clashes when opening? it should.) * local modules can clash * handle clashing of concrete names (in abstractToConcrete) * check that fixity declarations correspond to actual definitions * change syntax for fixity declarations (infix is a bit strange for prefix and postfix operators) [Testing] * write better tests [Bugs] * emacs interface gets the metas in the wrong order for local definitions (?) * importing A after importing A.B causes a clash [Interaction] [Errors] * Remember/figure out range of previous binding in DuplicateBuiltinBinding. * wrong "When..." reported for f (g x) if g x is well-typed but of wrong type. * weird meta cannot depend on errors * ranges of constructors in patterns are wrong. (also in right-hand sides?) [Type checking] * When do we have to turn on abstractMode. When checking anything public? Not done at the moment. * change to named free variables and deBruijn bound variables (I'm not a number paper). [Imports] * handle clashing builtin things * create interface for top-level module (not so important) * allow the source to not exist if there is an interface file (what if it needs rebuilding? throw error) * insert pragmas to specialise interface parsers (if this is the problem) [Builtin] * check that bindings to list and bool binds to datatypes of the right shape [Misc] * Allow qualified names in BUILTIN pragma. Currently pragmas are parsed as plain strings, so a qualified name is interpreted as an unqualified name containing a dot. * check that the module name matches the file name. Also when importing the module name should be the one we're trying to import. * Allow modules to be called things like Prop and Set (?) * Move large parts of the Makefiles to mk/rules.mk (or something) Speculative ----------- * make scope checking aware of abstract? or maybe this is too much work Cleaning -------- * TypeChecking.Reduce - Explicit dictionaries (Kit)? see notes/kit * Split vim highlighting into a general highlighting module and the vim specific parts. Performance ----------- * Check what's taking time with new meta var/constraint handling * a lot of memory created by subst is never used * space leak in lexer (positions too lazy?) Done ---- * Split TypeChecking.Errors into TypeChecking.Pretty and TypeChecking.Errors * inductive families with pattern matching * build agda as a package to speed up loading into ghci * OpenTerm type to simplify deBruijn variable handling * Monad transformer for checking patterns. * pretty printing of operator applications * named implicit arguments, see notes/named-implicit * Use Data.ByteString (if ghc-6.6) for interface parsing (faster, but still quite slow) * optimized natural numbers, user view is still zero/suc. * allow reexporting of things using 'open Foo, public' * allow import and open before the top level module. * checking that underscores have been solved (only in batch mode) * syntax highlighting * proper make test (agda now exits with failure on error) * failing test (like in agdaLight) * throwing not-in-scope error rather than no parse for application wheneven possible * use interface files in scope checking * check for cyclic imports (we need to use interface files when scope checking) * removed list sugar (and made [ and ] valid in names) * create interface files when importing * allowing lambda-bound operators by always writing _+_ (hence making underscore in names carry semantics). * allow no type signatures for definitions of the form x = e * mix-fix operators * list sugar * handle absurd patterns * literal patterns * literals * built-in things * pragmas * move trace to environment * name suggestions in telescopes * forall x y z -> A = (x:_)(y:_)(z:_) -> A * cleaning up of TypeChecking.Monad.* * Context to abstract thinks that the types are valid in the entire context. * Hiding info on lambdas. * flag for printing all implicit arguments (handled in internal to abstract) * proof irrelevance * Prop <= Set * sort checking of datatypes check that all constructor arguments fit inside the datatype sort (rather than checking that the types of the constructor fit) * let-bindings (only x = e definitions) * insertion of hidden lambdas when appropriate * optimise * for an as-pattern x@p x should reduce to p during type checking * as-patterns * split TypeChecking.Monad.Context * better names for implicit args in lhs * replace explicit Hidden with Arg in Pi and App (and more?) * independent functions in Type * local functions * speed up normalise * getopts * When instantiating a module we should generate functions for the axioms and constructors and probably for everything else as well (reducing to the instantiated versions from the instantiated module). Together with monomorphic constructors. * Monomorphic constructors. * ? should not be a valid operator characted * actually check sorts * Get rid of distinction between hole and underscore. Instead keep a separate list of which metas are interaction points. * Blocked constructor in Terms and Types * insert hidden arguments in lhss * ranges in error messages * abstract info on constraints (TCEnv instead of Context) and interaction meta vars. vim: sts=2 sw=2 ts=80