git.iko.soy/Idris-dev
on f03a655 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
848a597Lift syntax tree, main monad and pretty printing out of AbsSyntaxEdwin Brady 2ec60c8Added binding form to syntax rules (and updated tutorial accordingly)Edwin Brady 168278eHook up new output; deal with exact callsEdwin Brady 0887715Output C file (not finished...)Edwin Brady 782d0f7put toSC in the right placeEdwin Brady 6554c7dTowards primitives in new VMEdwin Brady 38a9365More towards the new compilerEdwin Brady ffc7b69First baby steps towards a new RTS (and towards removing epic dependency)Edwin Brady ec631d7Fix default arguments in pattern contextEdwin Brady 1f95bebFix a tactic implicit bug when argument given explicitlyEdwin Brady 3e3615aAllow explicit names on type class instances (for explicit resolution)Edwin Brady 46338e2Parsing restrictions for implicit argument typesEdwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady 01dc619New way of generating default definitionsEdwin Brady 2316dc9-i option added (thanks to Dirk Ullrich)Edwin Brady 489ea6fPass pattern variable names to match compilerEdwin 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 b01a78eQuick hack at :info for exploring type classesEdwin Brady 535d77bAdd --ibcsubdir option (thanks to Dirk Ullrich)Edwin Brady 455ae60Attempt to resolve type classes before applicationEdwin Brady 368fdf6Some playing around with widths to make everything look nicer.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan d254ce1Started adding pretty-printing capabilities for core datatypes to improve rendering of proof state.Dominic Mulligan 1c2098aAdded infinite list syntax [1..], [1,3,...] etc (But it doesn't work at the REPL yet because that doesn't respect 'lazy' annotations properly)Edwin Brady 97e28f7Export tactic-implicit arguments properlyEdwin Brady 0432a70Check that methods are part of a class when defining instancesEdwin Brady 463e62aSome type class bug fixesEdwin Brady 4bcfa68Tinker with specialisationEdwin Brady 00d7c69Work towards making {static} arguments and specialisation work properlyEdwin Brady 58bcd1eBetter type class resolutionEdwin Brady ed72247Try to get line numbers betterEdwin Brady c7a3b59Coverage checker tweakEdwin Brady f49cd3bPass options on functions in typeclasses through to instancesEdwin Brady 9864c25Add :total commandEdwin Brady 7142d7eTotality checker tweaksEdwin Brady b1e95cbFix coverage checkerEdwin Brady 7fb7decImproved termination check (gets ackermann now, but still no mutual recursive definitions)Edwin Brady 978479b(Try again...) Fixed some case statement bugsEdwin Brady 21c3a30Give up type class resolution soonerEdwin Brady 02501efChanged record update syntax... ...since {} is too overloaded now record { field = val } rec Also put records in their own namespaceEdwin Brady 3a4a26bBetter dealing with names in patternsEdwin Brady 98be75cAdded (experimentally) auto implicit argumentsEdwin Brady 6dcf4c3Build a call graph and only compile things which are usedEdwin Brady 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