git.iko.soy/Idris-dev
on 031ffb4 help sign in
history ofsrc/Idris/Parser.hs
all commits
9c11754Added %unifyLog construct For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the traceEdwin Brady ce7e45bEXPERIMENTAL: Syntax for applying functions by expected type "t <== f" applies a function f to arguments in such a way that it returns something of type t. The <== is a placeholder syntax until someone comes up with something better. (Alternative: t by f, but that uses up a new keyword)Edwin Brady c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady 894db6fMerge pull request #340 from JanBessai/BackendTargetSpecificationEdwin Brady eacfe5cAdded backend target specification to %lib, %link and %include directivesJan Bessai f2f0e07Default to Integer instead of Int, and adjust fromInteger accordinglyBenjamin Saunders 5b2f091Allow type class constraints in 'using' clauses e.g. if a using block is given asEdwin Brady 943b653Merge branch 'MixingImplicitArgs' of https://github.com/JanBessai/Idris-dev into JanBessai-MixingImplicitArgsEdwin Brady a0308f1Parser improvement to allow mixing of implicit and non implicit ArgumentsJan Bessai 8af32d4squash potential space leaks by using strict foldlraichoo 7b8ce28Enable alternate names for shared librariesDavid Christiansen 071b834Move parsing of comprehensions Fixes issue #178Edwin Brady 200475fMerge pull request #276 from david-christiansen/lookupsEdwin Brady a807a34Remove the unused arg from lookup functionsDavid Christiansen 03f962aDisallow laziness annotations below top level (since they don't work there) Handles issue #263Edwin Brady 34506e9Hack to parse big integer constants without overflow But we still need fromInteger to do the right thingEdwin Brady 477820aParsing for Big Integer constants fixedJan Bessai c1a4eacFull TT reflection and reificationJan Bessai 81865b4Remove type class argument restriction in parserEdwin Brady 7308d26Remove type class argument restriction in parserEdwin Brady ab498e9Add syntax for language extensions and turn off type providers by defaultDavid Christiansen 161ef3dMerge remote-tracking branch 'upstream/master' into providersDavid Christiansen 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 3a80954%dynamic now works from IBC filesDavid Christiansen 04267d6Top-level directive for dynamic linkingDavid Christiansen 0f49abcAdded first steps in type providersDavid Christiansen 6e732f9Added %provide directive to parserDavid Christiansen 0b58ae0Missing case in Idris.ParserMichael Thompson a5ea29fMerge pull request #203 from david-christiansen/haddockEdwin Brady 422521fTweak syntax rules to deal with consecutive non-terminals betterEdwin Brady 22c355aDocumentation comment additionsDavid Christiansen 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 82a4e9bFix for line numbers on type signaturesEdwin Brady 4c5b1bdMerge branch 'master' into bitstringBenjamin Saunders 1eed9c2Merge pull request #181 from raichoo/masterEdwin Brady 37ed162load command should ignore trailing whitespacesraichoo e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 41f3d97Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstringBenjamin Saunders 1ffdfc0Parse case options as patterns, not expressions Fixes issue #147Edwin Brady b2cf967Allow class constraints in syntax definitionsEdwin Brady 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders 60dbc48Add %instance for explicit access to resolveTC tacticEdwin Brady 8d090c0A couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before doing any totality checkingEdwin Brady 0a70480Merge branch 'type' of https://github.com/raichoo/Idris-dev into raichoo-typeEdwin Brady dd5001fmake TT aware of Set -> Typeraichoo 12f7a82Allow documentation comments for records.startling 7fefa89PSet -> PTyperaichoo cc716d7Make 'Type' the type of types instead of Sets ...after mailing list discussionEdwin Brady 441f51dpossible fixes for missing type signature in data declsraichoo