Commit Graph

13 Commits

Author SHA1 Message Date
William J. Bowman
b853d49b31
Fixed some tactic docs; tests that print to stdout 2015-10-03 03:55:22 -04:00
William J. Bowman
1fd96f0140
Proof read sartactics. closes #17 2015-09-25 13:54:42 -04:00
William J. Bowman
9055662a5d
Exported some convenience features 2015-09-23 16:22:05 -04:00
William J. Bowman
aa4b0ccf82
Started documenting the tactics library 2015-09-23 00:11:21 -04:00
William J. Bowman
fae24ab496
Styles tweaks
* Types now start with a Capital letter, because.
* Boolean expression no longer start with the letter b.
2015-09-22 23:32:02 -04:00
William J. Bowman
41b40fea2b
Commented out things that cause package to fail
Lots of tests and examples cause the package to fail to build. These
have been commented out until they can be fixed.
2015-09-22 15:32:54 -04:00
William J. Bowman
0f5026aee0
Fixed typo 2015-09-16 19:54:16 -04:00
William J. Bowman
23c1b56065
Knocked off a bunch of TODOs
* Removed some TODOs that were already completed
* Added cur-match, to abstract the common (syntax-parse (cur-expand syn) ...)
  pattern
2015-09-15 18:53:53 -04:00
William J. Bowman
3ce14c3871
Refactored core
Moved all curnel code into curnel/, and split the two kernel modules
into separate files. Now the trusted core and the module/#lang stuff are
in separate files. The #lang is now reprovided by "cur.rkt", which
should also provide core agnostic sugar.
2015-09-15 18:02:36 -04:00
William J. Bowman
31603bf109
Cleaned up tactic base system
* Various style fixes
* Standardize the proof state interface/naming a little.
* Reorganized base.rkt; now easier to read
* Fixed some mismatch code/documentation
* Renamed "basic" to "standard"; basic was too close to base, and not
  really helpful.
2015-09-15 16:02:53 -04:00
William J. Bowman
13d3016c85
Fixed order in which tactic scripts are printed 2015-09-13 18:57:01 -04:00
William J. Bowman
1bb886cfbb
Introduced Sartactics!
* Added the Sartactics library, provides a sassy wrapper around the basic
  tactics.
* Added prefix-in, although it probably only works for macros
* Better syntax for define-tactic
2015-09-11 17:20:53 -04:00
William J. Bowman
f2278696b5
Refactored tactics
Refactored tactics and corrected several bugs with how tactics, modules, and environments play together.
2015-09-11 15:11:06 -04:00