git.iko.soy/Idris-dev
on ef93607 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
5ce8ee7Fix shadowing bug with dependent pair bindingsEdwin Brady 6dc5ea2Fix name shadowing in whereEdwin Brady 0aca9f2New module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging around when building packages, and has required some fixes to imports in the library.Edwin Brady ecb42f0Resolve names/expand implicits inside refl Fixes #447Edwin Brady 48d1105Added 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of automated proof by reflection.Edwin Brady 6f88ecdAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.Edwin Brady c0ff0e8Fix type class index propagation bug ...which lead to implicit arguments not being spotted. Fixes #402Edwin Brady 9b4b7dccleanupsHannes Mehnert 50086acabstract set-prompt into isetPrompt -- and use itHannes Mehnert d7c8e63define and use iputGoal instead of putStrLnHannes Mehnert 7fc4865Allow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.Edwin Brady 7b6448eOptimization level selectionBenjamin Saunders f149970Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of hostBenjamin Saunders be36353Merge pull request #362 from david-christiansen/cmdline-execEdwin Brady 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 db18c51Add scriptsDavid Christiansen f885274Fix ordering of auto-implicits with 'using' 'using' arguments always now appear before fully implicit arguments, rather than the order we happen to find them in. TODO: Better would be to sort according to which ones we know depend on each other...Edwin Brady eacfe5cAdded backend target specification to %lib, %link and %include directivesJan Bessai 5b2f091Allow type class constraints in 'using' clauses e.g. if a using block is given asEdwin Brady d6d5634be more precise when to emit a warning (still a workaround - fix involves to not parse the string)Hannes Mehnert 9505a71cleanups, rename List to SexpList to disambiguateHannes Mehnert f608369Merge pull request #312 from hannesm/ideslaveEdwin Brady 99a8a66Check that explicitly given implicit args unify with inferred versions Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked.Edwin Brady 674c8b8IdeSlave mode improvements: - introduce iResult and iFail to report success and failure of a REPLcommand - send warnings for occuring warnings during parsing / typechecking - introduce ideslaveProcess function, which guards process with iResult/iFail (and does not support all operations) - revert commit which removed IState from ideslaveStart/ideslave functionsHannes Mehnert 2253212send prompt over the wire - also minor refactoringHannes Mehnert c96561bdon't use a field in IOption and a field in IState, only one of themHannes Mehnert 4118b79implement outputmode in IState, which either prints it raw or sexpressions (for ideslave support)Hannes Mehnert e0783efinitial ideslaveHannes Mehnert 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