git.iko.soy/Idris-dev
on bba09bd help sign in
history ofsrc/Idris/Prover.hs
all commits
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 33bf2bdUnification tweakEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady baaba44Run-time forcing optimisationEdwin Brady 4ca34ffFix error recovery in replEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 2e9fcd4Remove semicolons in tutorialEdwin Brady 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady dcc09e0Fix metavariable naming in namespacesEdwin Brady