git.iko.soy/Idris-dev
on aa8aefd help sign in
history ofsrc/Idris/Parser.hs
all commits
41f3d97Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstringBenjamin Saunders 1ffdfc0Parse case options as patterns, not expressions Fixes issue #147Edwin Brady b2cf967Allow class constraints in syntax definitionsEdwin Brady 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders 60dbc48Add %instance for explicit access to resolveTC tacticEdwin Brady 8d090c0A couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before doing any totality checkingEdwin Brady 0a70480Merge branch 'type' of https://github.com/raichoo/Idris-dev into raichoo-typeEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo 12f7a82Allow documentation comments for records.startling 7fefa89PSet -> PTyperaichoo cc716d7Make 'Type' the type of types instead of Sets ...after mailing list discussionEdwin Brady 441f51dpossible fixes for missing type signature in data declsraichoo ed85b4eerror messages with possible fixesraichoo f6451efword 8/16 primitive typesraichoo e23c029Allow type annotations on let tacticEdwin Brady 160eeddMerge pull request #101 from chetant/windowsEdwin Brady 51f3340Merge pull request #99 from raichoo/masterEdwin Brady fab5d73Adding support for Windows MingW32chetant b1cdd04Added postulate declarations postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time.Edwin Brady 2250085indent fixity error messageraichoo 5d33da2removed "user error" from error messagesraichoo 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