git.iko.soy/Idris-dev
on fadeecd help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
7b8ce28Enable alternate names for shared librariesDavid Christiansen 2a17e4fFix scoping rules on lhs of with clauseEdwin Brady a807a34Remove the unused arg from lookup functionsDavid Christiansen 83b7ae5Tweak linearity checker to deal with overloaded names properlyEdwin Brady ab498e9Add syntax for language extensions and turn off type providers by defaultDavid Christiansen 161ef3dMerge remote-tracking branch 'upstream/master' into providersDavid Christiansen 9875894Merged upstream changesDavid Christiansen 228ffdbquiet mode: for editorsraichoo db5973bAdded rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v.Edwin Brady 8b96fc7Fix another unification problem (solving things which shouldn't be)Edwin Brady 3a80954%dynamic now works from IBC filesDavid Christiansen 5aa46adFix name shadowing error when checking for linear patternsEdwin Brady 3fc67a2Fix error with linearity checking in patternsEdwin Brady 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen dd5001fmake TT aware of Set -> Typeraichoo 7fefa89PSet -> PTyperaichoo 2c58ebaFix elaboration of higher order dependent function types Fixes issue #116Edwin Brady 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 430eab9Allow postulates in where/parameters blocksEdwin Brady a6f8de5Fix name shadowing bug in case/destructuring let Fixes issue #96Edwin Brady e7c9256Allow inference of Sets at REPLEdwin Brady 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady 17d2ceaFix for expansion of types in parameters blocksEdwin Brady 4ddbc65Fix bug in lifting of with clauses Need to make sure _ remains _ on lifting - stray variables were creeping in after 'match'.Edwin Brady 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