git.iko.soy/Idris-dev
on 78fb1db help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
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 eec2b83Fix syntax macro bugEdwin Brady 3b36802Record syntax (but no magic yet...)Edwin Brady 1d76cd3Fix checked vs inferred bugEdwin Brady 566616cFixed bug: global names should not override 'using' namesEdwin Brady 95ff97cFix bug: checking names are not local before adding implicits and resolving namespacesEdwin Brady 991c229Better match checkingEdwin Brady 558d226Update elaborator for application of local variablesEdwin Brady 33bf2bdUnification tweakEdwin Brady 6e699c7Add Transform module; make implicit args lazyEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady 3f18d02Record data type infoEdwin Brady 42ca063:d to display elaborated pattern definitionEdwin Brady baaba44Run-time forcing optimisationEdwin 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 19f1e3aCompatibility with old ghcEdwin Brady 969e573Checking elaborated term and inferred term matchEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady