git.iko.soy/Idris-dev
on decad94 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
c020e50javascript: split javascript and node targetraichoo d53fccfMerge pull request #180 from david-christiansen/completion-workEdwin Brady 053708aMerge pull request #176 from david-christiansen/completionEdwin Brady 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen 4ae0450Remove old code, tinker with section 4Edwin Brady e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 2a13be4Distinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon!Edwin Brady 265d9a4Improve elaboration efficiency by cutting down on excessive backtrackingEdwin Brady 57628ffMerge pull request #146 from raichoo/javascriptEdwin Brady 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady 12dcee5Merge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascriptIrene Knapp 06fffa3JavaScript stuff.Irene Knapp 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