| #
b48f79ea |
|
31-May-2019 |
Konrad Slind <konrad.slind@gmail.com> |
switched to Definition and Theorem syntax (partial). Added different signed integer encodings to Regexp_Type. (This encoding stuff is going to be moved elsewhere once some things settle.) Minor renamings.
|
| #
07c4ff31 |
|
03-Jun-2017 |
Konrad Slind <konrad.slind@gmail.com> |
reset permissions
|
| #
3842bf8b |
|
03-Jun-2017 |
Konrad Slind <konrad.slind@gmail.com> |
speed up some proofs, adjust to IntInf, and some re-org
|
| #
42865876 |
|
22-Feb-2017 |
Konrad Slind <konrad.slind@gmail.com> |
Added some code-gen targets (java and sml). Also ruthlessly got rid of whitespace. I don't know why it is so bad, but it is gone.
|
| #
35739ff0 |
|
31-Jan-2017 |
Konrad Slind <konrad.slind@gmail.com> |
Revised regexp package. Now based on charsets modelled with bool[256]. Some optimizations added, and some work on packed intervals also included.
|
| #
0d008291 |
|
23-Dec-2016 |
Konrad Slind <konrad.slind@gmail.com> |
Added a pretty printer and improved performance of Regexp_Match. Proof path not working at the moment.
|
| #
cf399097 |
|
19-Dec-2016 |
Konrad Slind <konrad.slind@gmail.com> |
fixed efficiency bug (in parse tree for disjoined replications like \w{1,20}
|
| #
06e46592 |
|
09-Jun-2016 |
Konrad Slind <konrad.slind@gmail.com> |
Theory of regular expressions, featuring derivative-based regexp compiler which can be applied in deduction mode, or in SML mode.
|