This project is based on the regular expresion matching programs described in the paper "A Play on Regular Expressions - Functional Pearl" by Fischer et al. Three of the implementations, namely the default matcher, marked regular expressions matcher, and cached marked regular expressions matcher. Each of the previous implementations was formally formalised and its correctness was proved using the theorm prover HOL4.
SML code was later synthesised from HOL4 EmitML, and an SML library was executed and tested from the extracted code.
- To run this project if you have
Emacs,HOL4andPolyMLinstalled. - Clone the project.
- Change the path in the Holmakefile wherever the directory HOL got installed.
- build it using
Holmake, it will take approximatly 5 seconds.real 0m5,850s user 0m5,094s sys 0m0,627s.
RegScript.sml: Contains regular expressions and their matchers.
reggenScript.sml: Contains the code required to extract the code.
reggenML.sml : Contains the code that got synthesised from HOL4 implementation to SML.
regLib.sml : The library of the generated code.
test.sml and Performance_test.sml : SML files for testing.
- To test the definitions and the theorms or to play with the proofs you can open the file
RegScript.smland test it in HOL mode of emacs. - Thesting the generated SML code and library should be in SML REPL mode of Emacs, two optional files are there:
a.
test.smlwhere you can test various regex and strings with your favourite matchers. b.Performance_test.smlthis file contains a function that generates all combinations of the a charachter list and test it against the four matchers.
Please check the project documentation to gain a better knowledge of what has been done and the steps followed.