git.iko.soy/Idris-dev
on 0fef623 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
8d83f38Abstract matched terms from goal type in with clauses (like 'magic with' in Agda)Edwin Brady dd5001fmake TT aware of Set -> Typeraichoo 7fefa89PSet -> PTyperaichoo e4da568Take more care when expanding names in nested parameter blocksEdwin Brady 2c58ebaFix elaboration of higher order dependent function types Fixes issue #116Edwin Brady e3d393cAdded the ability to dump bytecode to a fileDaniel Waterworth c10146bLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call.Edwin Brady f833918(Experimental) Create deferred definitions by applicationEdwin Brady e23c029Allow type annotations on let tacticEdwin Brady 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 0c33cf1fixed bug in showImpraichoo 40ce0cabetter fixity error messageraichoo f50f006Expand backend control options and infrastructureBenjamin Saunders 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 8464bc4Add field for documentation comments in abstract syntaxEdwin 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 7438e0fDocument --warnpartial Behaviour fixed so that it doesn't report declared partial functionsEdwin Brady 665676bAdded :l and :m commands to REPLEdwin Brady 15fc297Merge branch 'master' of https://github.com/edwinb/Idris-devJason Dagit a41fe5bUse strict StateTJason Dagit 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 54ad219Add size change termination Now deals with recursive functions (still only simple structural size changes spotted, however)Edwin Brady ebb75fbCalculate size change graphsEdwin Brady d27925cMerge branch 'master' of https://github.com/raichoo/Idris-devEdwin Brady 30e4ed8Added simple productivity checker for coinductive definitions Recursive calls must be an argument to a coinductive constructorEdwin Brady 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady 997a982Added --total and --partial command line optionsEdwin Brady 7b2bf5eAdded "partial" keyword and "%default" directiveEdwin Brady f2af303:addproof now adds most recent proof if no argument given Consistent with old behaviour, and with tutorialEdwin 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 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 dde7fc3Report error for missing type declarationEdwin Brady 1e52324Added simple library packaging system Now used for the prelude (see lib/base.ipkg)Edwin Brady 7580119Added --libdir optionEdwin Brady 16a6c95Set up for adding new compiler back ends more easilyEdwin Brady ef1d7baMerge pull request #48 from raichoo/masterEdwin Brady 7cdb0c0Removed Epic dependencyEdwin Brady b642db5Almost working new back endEdwin Brady 7f2d76cenhanced proof handelingraichoo b8815e2added proof listraichoo 7c75851Test file for new VM, hook up parserEdwin Brady 848a597Lift syntax tree, main monad and pretty printing out of AbsSyntaxEdwin Brady