git.iko.soy/Idris-dev
on ccc0f67 help sign in
history ofsrc/Main.hs
all commits
7c75851Test file for new VM, hook up parserEdwin Brady 168278eHook up new output; deal with exact callsEdwin Brady 109b291Different approach to bytecodeEdwin Brady 38a9365More towards the new compilerEdwin Brady ffc7b69First baby steps towards a new RTS (and towards removing epic dependency)Edwin Brady e1c7b0fAdd "--errorcontext" flag, and :set and :unset in the REPL. :set errorcontext will cause unification errors to also dump the current context.Edwin Brady 2316dc9-i option added (thanks to Dirk Ullrich)Edwin Brady 535d77bAdd --ibcsubdir option (thanks to Dirk Ullrich)Edwin Brady a3c6231:addproof knows about .lidr filesEdwin 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 7f74f91Fix error handling again in replEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 c783299Add --help and --version optionsEdwin Brady e2d0099File handling in preludeEdwin Brady dea8d48Added support for literate programming with bird tracks (use .lidr extension)Edwin Brady b645699Don't write .ibc on error; add new testEdwin Brady 3b5e50cAdded universe constraint checker and --typeintype command line optionEdwin Brady d496a9c:e now reloads the edited fileEdwin Brady d676ca6Added -o option, and :exec and :t at the REPLEdwin Brady 5528447Not really mini any more...Edwin Brady 22546bc:r and :e at the REPL.Edwin Brady 6757c47Added case analysis on types, but only when enabled with --typecase (since it breaks parametricity)Edwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady 796fa25BannerEdwin Brady 20bf4d7Added lib/ and preludeEdwin Brady ca6a5e1import statementEdwin Brady 083fc70Added 'where' clauses in pattern matchesEdwin Brady de89a04Add ElabInfo to pass through elaboratorEdwin Brady a805f47Added constants and some primitive operationsEdwin Brady 9fe3473Added using blocksEdwin Brady c637850Pattern matcher, evaluation of 2+2 now worksEdwin Brady 54c8a04Checking pattern match clausesEdwin Brady 06a81c9Elaborating types and data declarationsEdwin Brady 8e8d57aCollect all pattern clauses for a functionEdwin Brady 1b6709fPretty printing data declarationsEdwin Brady 2050102Pretty printer for PTermEdwin Brady a8768afParser now fills in implicit argumentsEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady 50d24ecStart of a REPL and main program with argument processingEdwin 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 44d62c7Better if unification substitutes rather than let bindsEdwin Brady cc0dc09Added elaborate; a language for composing primitive tactics.Edwin Brady 867f092Changed evaluatorEdwin Brady 6923ac1Started theorem prover and tacticsEdwin Brady 205fcefSome proof state, some showing of termsEdwin Brady dc0c198First lot of source files and paperEdwin Brady