git.iko.soy/Idris-dev
on 83fdb4d help sign in
history ofsrc/Core/TT.hs
all commits
f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady 9e58e28Type safe message passing concurrencyEdwin Brady 895b323Allow forward declaration of data structures To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sectionsEdwin Brady 9affb75Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possibleEdwin Brady b894841Improve some error messagesEdwin Brady 5a6299bUnification fix Specifically to stop it filling in things which are given by the programmer (caused by a bug replacing nullary constructors with terms!)Edwin Brady 0f957f6Add Proj operator to runtime version of TT Allows extracting arguments without checking constructor first which will make erasing unused values easier shortlyEdwin Brady bb76c6cMore aggressive simplification; fix case generation bugEdwin Brady dde7fc3Report error for missing type declarationEdwin Brady 23ab26fSpeed improvements when code contains type errors Identify "unrecoverable" unification failures so that type checking doesn't continue to search all the alternative overloadings and orderings.Edwin Brady 7c75851Test file for new VM, hook up parserEdwin Brady 59d07f7Quicker resolution of overloaded names By checking the name's type against the goal type rather than fully checking.Edwin Brady 6554c7dTowards primitives in new VMEdwin Brady 6cb70bcFix for simple function applicationsEdwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady 19495edCheck patterns are inaccessibleEdwin Brady 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