git.iko.soy/Idris-dev
on de6bb41 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
de6bb41Added 'total' keyword and positivity checkEdwin Brady ae4be75Well founded recursion checkEdwin Brady dc3f0f9added dsl blocksEdwin Brady 6807cf4Unreachable case warningEdwin Brady 247b20cSome minor fiddlingEdwin Brady e39254cAdded 'abandon' command in proof mode (Alternatively, :q)Edwin Brady eec2b83Fix syntax macro bugEdwin Brady 3b36802Record syntax (but no magic yet...)Edwin Brady 1d76cd3Fix checked vs inferred bugEdwin Brady 566616cFixed bug: global names should not override 'using' namesEdwin Brady 95ff97cFix bug: checking names are not local before adding implicits and resolving namespacesEdwin Brady 991c229Better match checkingEdwin Brady 558d226Update elaborator for application of local variablesEdwin Brady 33bf2bdUnification tweakEdwin Brady 6e699c7Add Transform module; make implicit args lazyEdwin 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 3f18d02Record data type infoEdwin Brady 42ca063:d to display elaborated pattern definitionEdwin Brady baaba44Run-time forcing optimisationEdwin 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 19f1e3aCompatibility with old ghcEdwin Brady 969e573Checking elaborated term and inferred term matchEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady a33b4c2Avoid adding duplicate information to .ibc => quicker load timeEdwin Brady 7f74f91Fix error handling again in replEdwin Brady b20f2f8Tinker with compiler interfaceEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 b0f47e1Made braces optional (at the expense of 'with' now needing the expression to be tested in brackets) do notation doesn't quite behave right - the first token after the do block must be at a lower level of indentation, which means putting it in brackets is awkward.Edwin Brady bd61594Removed need for terminating ; A declaration is now considered terminated on encountering a token in the same column as the declaration began - or on encountering a semicolon. Libraries and some tests updated.Edwin Brady 6196bbcAllow types on let in do blocksEdwin Brady 947c2b3Fix bug in generation of case functionsEdwin 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 7932e28Added idiom bracketsEdwin Brady 16708a9More flexibility using overloading functions in patternsEdwin Brady 85e91efAdded '%access' directive and updated libsEdwin Brady 9265e7cAdded 'public', 'abstract' and 'private' modifiers 'public' means export everything (name and definition) 'abstract' means export just the name 'private' means export nothing for data types and classes, 'abstract' means export the type/class name but not the members.Edwin Brady 8ea902dAdded %hide and %freeze directivesEdwin Brady 88f6bf1Fix obscure where naming bugEdwin Brady 00e21caAnother parser fix for withEdwin Brady c3427e8with parsing fixEdwin Brady d7df489Fixed a 'with' bug; added char and span for StringsEdwin Brady 582afe1Added system module (getArgs, getEnv, exit)Edwin Brady 1fa2dfaMore concise 'with' syntax if patterns are repeated from previous lineEdwin Brady 11d4feeSome file handlingEdwin Brady 87946abShow user chosen names rather than machine onesEdwin 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 60c4ef9Added 'impossible' keywordEdwin Brady 3b5e50cAdded universe constraint checker and --typeintype command line optionEdwin Brady