Features -------- * remembering the last thing in scope when computation gets stuck * 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 (or call by value?) * unify primitive and {-# BUILTIN #-} * allow module instantiation before top-level module(?) * abstract open (need to re-type check to make sure the abstraction is solid) * extend positivity check to handle function calls * mutual modules * more liberal builtin bindings (Nat as a special case of a general sequence) User interface -------------- * Highlighting fixity declarations and all module names. * Point warping for record fields. * locally nameless representation Fixes ----- [Errors] * DeclarationException when missing a type signature [Parsing] * allow more things in postulates (infix, private, ..) * allow fixity declarations for record fields (where?) * allow postulates in mutual * Check out lex/parse errors (what position and what input is reported). * Enable parsing of non-trivial literate files (see examples/syntax/highlighting/Test.lagda). [Serialisation] [Printing] * print patterns in mixfix notation (AbstractToConcrete) * meta variables are printed with their lambda lifted types [Scope] * check that fixity declarations correspond to actual definitions * change syntax for fixity declarations (infix is a bit strange for prefix and postfix operators) [Evaluation] * literal patterns are considered neutral when deciding if a match is No or DontKnow example funny : (A : Set) -> A -> D A -> .. funny .Nat zero nat funny .String "foo" string Here funny String "foo" string doesn't reduce because we DontKnow that "foo" doesn't match zero. [Type checking] * implicit function spaces and records interact badly with meta variables solution: postpone type checking problems - postpone checking of lambda against blocked types - postpone checking of applications where the function has a blocked type - postpone checking of records against blocked types [Testing] * write better tests [Bugs] * The Emacs interface meta variable treatment leads to problems with the syntax highlighting/point warping. Fix this by doing most work on the Haskell side, using the syntax tree, instead of mucking around with regular expressions on the Emacs side. Currently there are two known bugs: 1) _All_ question marks are treated as meta variables. 2) After a question mark has been converted into {! !} the point warping does not work (the offsets into the file have changed). * importing A after importing A.B causes a clash * Too many open files * Evaluation of _==_ loops on something like this: open module Eq = Equivalence (Eq'{ℂ}{A}{B}) renaming (_==_ to _=='_) f == g = .. ==' .. * There's a bug in the import chasing where a module can be imported before it's type checked. I.e. an old version of the module is stored in an interface file of a different module and we can't see that it's not up-do-date. I think this is what happens in the polydep example if everything is up-to-date except TYPE.agda. [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. * ranges of constructors in patterns are wrong. (also in right-hand sides?) * give sensible message for too few arguments to constructor in pattern [Type checking] * When do we have to turn on abstractMode. When checking anything public? Not done at the moment. [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) [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 ---- * pattern coverage * with-clauses * better algorithm for pattern matching on inductive families * structured verbosity * records * implemented the CHIT-CHAT module system * polymorphic constructors at run-time (at least at conversion checking) * 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