#
8d83067c |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from examples
|
#
85cc084b |
|
02-Nov-2017 |
Ramana Kumar <ramana@member.fsf.org> |
Remove zip_def in regexpTheory Closes #478 One potential issue is if computeLib/EVAL of ZIP is required to work for lists of different lengths -- listLib's compset does not support this (but easily could). I am guessing the regexp library does not need this though.
|
#
49f96a8a |
|
18-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix formal-languages/regular given 93036c73b4
|
#
74e33b78 |
|
11-Jul-2017 |
Konrad Slind <konrad.slind@gmail.com> |
Converted ML implementation of charsets to align with that used in HOL. Also replaced regexp2{c,java,sml} by a single regexp2dfa program.
|
#
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
|
#
393e1938 |
|
14-Feb-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix a regexp proof for experimental kernel Replay of 735f8b1, which was junked by cb8925df9d
|
#
7812c0e8 |
|
14-Feb-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove DOS \n and trailing w/space in regexpScript Replay of 5d0f97b, which was junked by cb8925df
|
#
cb8925df |
|
13-Feb-2017 |
Konrad Slind <konrad.slind@gmail.com> |
* Moved formalization of charsets to be word64#word64#word64#word64. This will support CakeML translation. However, the implementation of the SML regexp compiler in Regexp_Match still uses IntInf as the representation of charsets. It might be interesting to compare the two representations for efficiency, but that's future work. * Incorporated in-logic PEG parser for regexps (regexp_parserTheory). This was renamed from reSyntax to be in line with the existing naming scheme (pre-pending things with "regexp"). * Revised packed interval syntax \p{e_1 ... e_n} to get rid of superfluous commas between elements, and to incorporate support for padding.
|
#
e03cecc0 |
|
07-Feb-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Switch regular expressions in the logic to use charset64
|
#
735f8b1c |
|
01-Feb-2017 |
Michael Norrish <michael.norrish@nicta.com.au> |
Fix a regexp proof for experimental kernel Unfortunately this was a case where generated names differed from kernel to kernel.
|
#
5d0f97b9 |
|
01-Feb-2017 |
Michael Norrish <michael.norrish@nicta.com.au> |
Remove DOS \n and trailing w/space in regexpScript
|
#
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.
|
#
8e6c2f3a |
|
02-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix regexp theories for pat_assum rename
|
#
7e49980d |
|
23-Jun-2016 |
Michael Norrish <michael.norrish@nicta.com.au> |
Really fix names in regexpScript
|
#
75b34251 |
|
23-Jun-2016 |
Michael Norrish <michael.norrish@nicta.com.au> |
Be more explicit with variable names to fix expk breakage
|
#
e3d390e4 |
|
22-Jun-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix regexpScript's line-endings and trailing whitespace
|
#
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.
|