git.iko.soy/Idris-dev
on 4ddbc65 help sign in
history ofsrc/Idris/Parser.hs
all commits
809c283Merge pull request #90 from raichoo/parserEdwin Brady bbe9dc1Minor fixes for inlining and integer literalsEdwin Brady 92f3139eof should close all open blocksraichoo 40ce0cabetter fixity error messageraichoo c9e0444show actual ParseError messageraichoo ff56693prevent different fixity declarationsraichoo a777c93Change 'abstract' rule for records Still have access to field names, but not constructor nameEdwin Brady 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady 6d7a6aaChange comment rules Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.Edwin Brady 319582eElaborate lhs of pattern clause properly in implicit argumentsEdwin Brady 29c67e9Pattern matching on strings, big integers and charactersEdwin Brady af66f25Added 'mutual' blocks Effect is to elaborate all types in the block before elaborating definitionsEdwin 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 671d39aFix name clashes between holes and bound variablesEdwin Brady 7438e0fDocument --warnpartial Behaviour fixed so that it doesn't report declared partial functionsEdwin 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 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady 7b2bf5eAdded "partial" keyword and "%default" directiveEdwin Brady 72c0156Added 'parameters' blocks Allows abstracting over parameters across a block of functions and data definitions. Effect is to add those parameters to *every* function, type and data constructor. Inside the block, no need to pass those parameters, outside they must be made explicit.Edwin 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 7cb5a60fix parsing for with-clauseraichoo a7adbdbFix cyclic universe checking bugEdwin Brady b74161fMinor parser fixes; added binary sampleEdwin Brady 4b1109esatisfy hlintraichoo 0306e49removed parsec compatibility layerraichoo 16027ddFix with parsing bugEdwin Brady 517acc1Namespace parsing improvements (for qualified operator names) thanks to Dirk UllrichEdwin Brady 3553b1dtiny tiny tiny typo fixMekeor Melire 2ec60c8Added binding form to syntax rules (and updated tutorial accordingly)Edwin Brady 0e997eeSyntax rules need to allow implicitsEdwin Brady ffc7b69First baby steps towards a new RTS (and towards removing epic dependency)Edwin Brady 3e3615aAllow explicit names on type class instances (for explicit resolution)Edwin Brady 46338e2Parsing restrictions for implicit argument typesEdwin Brady 2316dc9-i option added (thanks to Dirk Ullrich)Edwin Brady dcb9ca0Change meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.Edwin Brady 535d77bAdd --ibcsubdir option (thanks to Dirk Ullrich)Edwin Brady 6c08816More paper changesEdwin Brady dca8f9fNormalise types before applying forcingEdwin Brady 3ce7d92Better pruning of alternatives so that resolving is much fasterEdwin Brady 022e230Added backtick notation: e.g. x xsEdwin Brady a12ecc2Fix parser bug: whitespace now allowed at the top of modulesEdwin Brady 76ac83bParse rule for big integers is brokenEdwin Brady 463e62aSome type class bug fixesEdwin Brady 4bcfa68Tinker with specialisationEdwin Brady ed72247Try to get line numbers betterEdwin Brady 7142d7eTotality checker tweaksEdwin Brady 7fb7decImproved termination check (gets ackermann now, but still no mutual recursive definitions)Edwin Brady 68194ceFix export of record fieldsEdwin Brady 02501efChanged record update syntax... ...since {} is too overloaded now record { field = val } rec Also put records in their own namespaceEdwin Brady