git.iko.soy/Idris-dev
on 012b595 help sign in
012b595Gratuitous interpreter extension to exercise the elaborator moreEdwin Brady f97602bmore interpreter testingEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin Brady 739e0b5Some error handlingEdwin Brady 22b4dc4Lots of improvements in elaborating and evaluatingEdwin Brady c637850Pattern matcher, evaluation of 2+2 now worksEdwin Brady 17e22afFeed a type to the elaborator for the RHS of a pattern. Also, change type of pattern bindersEdwin Brady 54c8a04Checking pattern match clausesEdwin Brady 7a30f10Maybe if I add liftCatch locally things will work on 6.12Edwin Brady be2b9bcAdd ElabDeclsEdwin Brady 174e696Don't crash on error, keep goingEdwin Brady 06a81c9Elaborating types and data declarationsEdwin Brady efd11bbOopsEdwin Brady 8e8d57aCollect all pattern clauses for a functionEdwin Brady 1b6709fPretty printing data declarationsEdwin Brady 2050102Pretty printer for PTermEdwin Brady f85d1f0:ttshellEdwin Brady a8768afParser now fills in implicit argumentsEdwin Brady 596e9aaFunctor for PTerm/PDeclEdwin Brady 2eb5b52Pattern clause parserEdwin Brady 82585e7Some ghc 6.12 compatibilityEdwin Brady 64b7cfdParsing high level data declarationsEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady 50d24ecStart of a REPL and main program with argument processingEdwin Brady 6414924Reserved wordsEdwin Brady 70ac28dChange fixity declarationsEdwin Brady aa85339Builds on ubuntu haskell platformEdwin Brady 554c395Made a start on the high level languageEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady ac25f15Changed contexts to Data.MapEdwin Brady 575b043Make sure apply doesn't solve holes automatically that the user wants to solve themselvesEdwin Brady 3501adbChanged way of building pattern match termsEdwin Brady c966457Just use proof state as TStateEdwin Brady edfe9c6Added pattern arguments; bug fixesEdwin Brady ee3dbaaChange tactic names: fill for unify_fill and exact for fillEdwin Brady 5dadd08QED now rechecks the term, instead of just finalise. *bites fingernails*Edwin Brady 44d62c7Better if unification substitutes rather than let bindsEdwin Brady 89ffe9bUndo tacticEdwin Brady ffd5e72arg tactic; unification tweakEdwin Brady 07f3b19Add patvar tactic; fix apply to deal with names properlyEdwin Brady 12f9368apply and prepare_apply elaborationsEdwin Brady 546e9f5A gadget or twoEdwin Brady 5ee3376make Elab a state monad for ease of EDSL programmingEdwin Brady cc0dc09Added elaborate; a language for composing primitive tactics.Edwin Brady cbc60ebUnification, and unify tacticEdwin Brady 77be0d0Simple parser for data typesEdwin Brady 6a6a048No mucking about with de Bruijn indices in proof constructionEdwin Brady 1921eacSome tidying; compute; printEdwin Brady 9c6ea4aFixing evaluator bugsEdwin Brady