git.iko.soy/Idris-dev
on b63e9bb help sign in
history ofsrc/Idris/Parser.hs
all commits
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 3b13341Better error reporting for unresolved type classesEdwin Brady 7df6265Remove some needless bracketing from if...then...elseEdwin 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 f3ce933Some prelude shufflingEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady 201ade9Fixed accessibility bug; added some library functionsEdwin Brady 7f74f91Fix error handling again in replEdwin Brady 4ca34ffFix error recovery in replEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 8b1e498Change 'data' and where syntax so that they don't need '|' This breaks old code - instead ofEdwin Brady 2852e71Made do notation behave better when bracketedEdwin Brady 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 817c1a0Monad comprehension notationEdwin Brady 6196bbcAllow types on let in do blocksEdwin Brady e62b7eaPattern matching lambda, plus tutorial updateEdwin 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 dcc09e0Fix metavariable naming in namespacesEdwin Brady 2000a54Arbitrary length tuples (reducing to nested pairs)Edwin Brady d22364aOperator sectionsEdwin 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 00e21caAnother parser fix for withEdwin Brady c3427e8with parsing fixEdwin Brady 582afe1Added system module (getArgs, getEnv, exit)Edwin Brady 1fa2dfaMore concise 'with' syntax if patterns are repeated from previous lineEdwin Brady 0bc69fbAdded prelude.strings, made believe_me primitiveEdwin Brady dea8d48Added support for literate programming with bird tracks (use .lidr extension)Edwin Brady b645699Don't write .ibc on error; add new testEdwin 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 c997a48Hierarchical namespaces; reorganised prelude accordinglyEdwin Brady 57c8ed3Added 'module' keyword to declare default namespace. 'main' must be in namespace 'main'Edwin Brady 6bef4f9Overloading lists and syntactic sugarEdwin Brady fa5f1cdNamespacesEdwin Brady 94d888bParsing and elaboration of alternativesEdwin Brady 07f12f9Separate elaboration of declarations and termsEdwin Brady 01ceeadNamesEdwin Brady 03d7d5eAllow type labels on lambdasEdwin Brady dbc607cDecorating names for namespacesEdwin Brady bbaa193Better representation of namesEdwin Brady ae3ad10Apply fromInteger for negative numbersEdwin Brady 925648aAdd %include directiveEdwin Brady