git.iko.soy/Idris-dev
on fa526e4 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
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 3448469Add "equiv" tactic "equiv t" asserts that the current goal has a type equivalent (by conversion) to tEdwin Brady 7b6448eOptimization level selectionBenjamin Saunders f149970Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of hostBenjamin Saunders 14ee023Skeleton of stub-generating LLVM codegenBenjamin 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 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 db18c51Add scriptsDavid Christiansen 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 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 425c97achanged defaultOpts to use field names for assignmentjoe9 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 6d01828put ideslave_counter into IStateHannes Mehnert 1b65f6ause process in ideslave loopHannes Mehnert e0783efinitial ideslaveHannes Mehnert 700759fCache missing cases found by totality checker, for display Now :missing works correctly (fixes issue #210) Also, remove a large chunk of unused code in coverage checker.Edwin Brady 8af32d4squash potential space leaks by using strict foldlraichoo 2a17e4fFix scoping rules on lhs of with clauseEdwin Brady d1e450fPrint Nats as numeralsAndy Morris bc8d3adRepl prints listy things with sugarAndy Morris a807a34Remove the unused arg from lookup functionsDavid Christiansen ea6bb9aMerge branch 'ImprovedReflection' of https://github.com/JanBessai/Idris-dev into JanBessai-ImprovedReflectionEdwin Brady c1a4eacFull TT reflection and reificationJan Bessai 75e0141add command to change current directoryHannes Mehnert ab498e9Add syntax for language extensions and turn off type providers by defaultDavid Christiansen 161ef3dMerge remote-tracking branch 'upstream/master' into providersDavid Christiansen d81e2edAdd clauses to declared and defined.Sam T 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 3a80954%dynamic now works from IBC filesDavid Christiansen 3262127Dynamically load C libraries in REPLDavid Christiansen 0f49abcAdded first steps in type providersDavid Christiansen 306a451Reformat existing comments for Haddock and add Haddock commentsDavid 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 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