Mercurial Mercurial > hg > lexing / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys3/README.md
author Chengsong
Mon, 09 May 2022 17:24:26 +0100
changeset 513 ca7ca1f10f98
parent 496 f493a20feeb3
permissions -rw-r--r--
more isarfy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
495
f9cdc295ccf7 a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset 
     1
 
# POSIX Lexing with Bitcoded Regular Expressions
f9cdc295ccf7 a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset 
     2
 












f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




     3


Run the code with













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




     4














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




     5


```isabelle build -c -v -d . Posix```













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




     6









496






f493a20feeb3
updated to include the paper



Christian Urban <christian.urban@kcl.ac.uk>


parents: 
495

diff
changeset




     7


Generate the paper with













f493a20feeb3
updated to include the paper



Christian Urban <christian.urban@kcl.ac.uk>


parents: 
495

diff
changeset




     8














f493a20feeb3
updated to include the paper



Christian Urban <christian.urban@kcl.ac.uk>


parents: 
495

diff
changeset




     9


```isabelle build -c -v -d . Paper```













f493a20feeb3
updated to include the paper



Christian Urban <christian.urban@kcl.ac.uk>


parents: 
495

diff
changeset




    10









495






f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    11


Tested with Isabelle2021-1.













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    12














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    13














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    14


* RegLangs.thy (contains basic definitions for Regular Languages)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    15














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    16


* PosixSpec.thy (contains values and POSIX definitions)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    17














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    18


* Positions.thy (shows the equivalence of our POSIX spec and the definition by Okui & Suzuki)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    19














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    20


* PDerivs.thy (Partial Derivatives according to Antimirov, size bounds of pderivs)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    21














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    22


* Lexer.thy (first algorithm by Sulzmann & Lu without simplification)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    23














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    24


* LexerSimp.thy (correctness for simple-minded simplification rules)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    25














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    26


* Blexer.thy (second algorithm by Sulzmann & Lu without simplification)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    27














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    28


* BlexerSimp.thy (correctness for aggressive simplification rules)













f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    29














f9cdc295ccf7
a fresh directory with cleaned up code



Christian Urban <christian.urban@kcl.ac.uk>


parents: 

diff
changeset




    30


* Finite Bound Result: BasicIdentidies.thy, ClosedForms.thy, GeneralRegexBound, ClosedFormBounds.thy (Section 5 in the paper)














lexing