git.iko.soy/Idris-dev
on dd09721 help sign in
history ofsrc/Idris/Prover.hs
all commits
b1d2553Respect accessibility in case tree elaboration.Matus Tejiscak f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen 7faf4e8Show argument names in :docDavid Raymond Christiansen b38bc03Add basic elaboration context tracking to unificationDavid Raymond Christiansen 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen bd744f1Propagate function name to tacticsEdwin Brady af0171eProver commands for evaluation and typechecking expressionsDavid Raymond Christiansen d95808eDon't give INTERNAL ERROR when abandoning a proofEdwin Brady da24632Render using console widthDavid Raymond Christiansen 94c4cf8Make prover respect showimplicits from IStateDavid Raymond Christiansen 5f0c449Colouring support in the proverDavid Raymond Christiansen 13f3c29Basic functioning with new pretty-printerDavid Raymond Christiansen d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 7604451Cache argument types for building case treesEdwin Brady 5000aebAdd a Cabal libraryBrian McKenna f18d79cRemove calls to "error". Fixes #607.David Christiansen 6b16b47Fix display of errors in proverDavid Christiansen 3c32b65Whitespace cleanup.George Leontiev f34f0afBetter display of metavariable types in :tEdwin Brady 57c8657Added column name to sourceAhmad Salim Al-Sibahi b5eee09Convert IO errors into erros in the Idris monadDavid Christiansen 63038b3Use the ErrorT failure functions and attempt to preserve error structureDavid Christiansen 267f34dChanged the way addproof works to indented-block style Allowed a larger range of expression to work with slices (improves on idris-lang/Idris-dev#524)Ahmad Salim Al-Sibahi 73bdc53Refactoring of parser to Trifecta, documenting and updating some items/fixing some issues.Ahmad Salim Al-Sibahi 81425d2Add skeleton of inlinerEdwin Brady 3fcbff5A little reorganisation of clauses elaboration To be more clear which case tree is whichEdwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin Brady fd9bd68Add '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.Edwin Brady 9b4b7dccleanupsHannes Mehnert 64afbf1send start/end proof mode messages from within proverHannes Mehnert 5242001support ideslave mode with proverHannes Mehnert 50086acabstract set-prompt into isetPrompt -- and use itHannes Mehnert d7c8e63define and use iputGoal instead of putStrLnHannes Mehnert 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 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 a807a34Remove the unused arg from lookup functionsDavid Christiansen 3fc67a2Fix error with linearity checking in patternsEdwin Brady a162bd4Check the type of a proof matches the type of the goal!Edwin Brady bdf07beManually track prover historyDavid Christiansen 66d8360Crude support for completion in proverDavid Christiansen 52203a3Complete tactic names in proverDavid Christiansen 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 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 f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady 2fb2445indent proof blocks by 2 spacesraichoo 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 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