git.iko.soy/Idris-dev
on 08797ae help sign in
history ofsrc/Core/TT.hs
all commits
5602ea7A small cleanup after missing some stray ends in the diff.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan 9a54230Started adding pretty printing capabilities for core data types to improve rendering of proof state.Dominic Mulligan 00d7c69Work towards making {static} arguments and specialisation work properlyEdwin Brady 392c225Check definitions structurally as well as by name in conversionEdwin Brady 21c3a30Give up type class resolution soonerEdwin Brady 3b13341Better error reporting for unresolved type classesEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady 38732d8Heuristic for picking best error message when overloaded alternatives all failEdwin Brady 02881b1Implemented forcing optimisation Constructor arguments which are inferrable from the indices in the constructor type are erased both at compile-time and run-timeEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady dcc09e0Fix metavariable naming in namespacesEdwin Brady 8ea902dAdded %hide and %freeze directivesEdwin Brady 0bc69fbAdded prelude.strings, made believe_me primitiveEdwin Brady dea8d48Added support for literate programming with bird tracks (use .lidr extension)Edwin Brady dccbc43Generate bytecode so that files don't need to be rechecked every time they're loadedEdwin Brady 8f77986Added some serialisationEdwin Brady 9f65713Fix name parsing for nested namespacesEdwin Brady fa5f1cdNamespacesEdwin Brady 8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady ada02deTinker with universe constraintsEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady bbaa193Better representation of namesEdwin Brady e20f401No holes allowedEdwin Brady 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady 814ebdaMake sure patterns are in dependency orderEdwin Brady 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 7b1336bFixed naming problem in type checking of applicationEdwin Brady 3bdfa26Added [static] annotations (which do nothing yet) and state to evaluatorEdwin Brady 6757c47Added case analysis on types, but only when enabled with --typecase (since it breaks parametricity)Edwin Brady 5fbca2aFix with so that clauses are checked for matches against top level defnEdwin Brady 5e92c70When collecting implicit args in wheres, ignore names bound in above scopeEdwin Brady bf368abFirst attempt at with ruleEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady 868409aSmall bug fixesEdwin Brady 083fc70Added 'where' clauses in pattern matchesEdwin Brady a2a5141Allow interleaving of explicit and implicit arguments in top level typesEdwin Brady a805f47Added constants and some primitive operationsEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin Brady 22b4dc4Lots of improvements in elaborating and evaluatingEdwin Brady c637850Pattern matcher, evaluation of 2+2 now worksEdwin Brady 17e22afFeed a type to the elaborator for the RHS of a pattern. Also, change type of pattern bindersEdwin Brady 1b6709fPretty printing data declarationsEdwin Brady a8768afParser now fills in implicit argumentsEdwin Brady