git.iko.soy/Idris-dev
on e63fcef help sign in
history ofsrc/Idris/Prover.hs
all commits
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 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin 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 b8815e2added proof listraichoo 19495edCheck patterns are inaccessibleEdwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady 368fdf6Some playing around with widths to make everything look nicer.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan ab039f2Fix universe checking bugEdwin Brady e39254cAdded 'abandon' command in proof mode (Alternatively, :q)Edwin Brady 6682ebbPropagate solutions properlyEdwin Brady a3c6231:addproof knows about .lidr filesEdwin Brady