git.iko.soy/Idris-dev
on adbe613 help sign in
history ofsrc/Idris/Parser.hs
all commits
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 4cd20b3Record update syntax { field = val } is a function which updates the field. So { field = val } rec update the field in record 'rec'. (This is backwards from Haskell, firstly because the other way round would conflict with implicit argument syntax, and secondly because it means record updates can be partially applied)Edwin Brady 3c42704Record projectionEdwin Brady 98be75cAdded (experimentally) auto implicit argumentsEdwin Brady de6bb41Added 'total' keyword and positivity checkEdwin Brady dc3f0f9added dsl blocksEdwin 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 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