git.iko.soy/Idris-dev
on 64fc043 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
f9678b7Remove priority ordering on function arguments Should no longer be necessary since unification is improved, and causes problems when it guesses wrong.Edwin Brady 1b6cc6aFix parameter block expansionEdwin Brady f50f006Expand backend control options and infrastructureBenjamin Saunders 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady 96f3b9eFix nested parameters blocksEdwin 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 264b67fMore restrictive automated addition of implicit arguments Only added automatically if they begin with a lower case letter, or appear in a using block. Apologies for breaking code: however, this catches a common class of error which causes confusing (but correct) typechecker behaviour.Edwin 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 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 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 49259a5Type class fix Chase parent class dependencies last (after looking for a directly defined instance)Edwin Brady 3c641aeAdded --dumpdefuns flagEdwin 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 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin Brady 72d4d96Starting unused argument analysisEdwin Brady 6d7c9bcCall graph changeEdwin Brady 0f957f6Add Proj operator to runtime version of TT Allows extracting arguments without checking constructor first which will make erasing unused values easier shortlyEdwin Brady f26b42fDeal with shadowing better in patterns Variable names in patterns should override global names, as long as they are not applied to anything. If the global name is desired (e.g. if it is the result of a dependency elsewhere, either use a _ or give the qualified version of the name)Edwin Brady 4ff3b25Added --dumpc flagEdwin Brady a7adbdbFix cyclic universe checking bugEdwin Brady 1e52324Added simple library packaging system Now used for the prelude (see lib/base.ipkg)Edwin Brady 7cdb0c0Removed Epic dependencyEdwin Brady e956ecaDon't lambda lift unused argumentsEdwin Brady 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