diff options
author | filip <“filip.rabiega@gmail.com”> | 2025-04-22 18:38:38 +0200 |
---|---|---|
committer | filip <“filip.rabiega@gmail.com”> | 2025-04-22 18:59:19 +0200 |
commit | 2e893fd0df7dae8c4ae843d4a23acb098dd97aff (patch) | |
tree | 1f4a50da28d2e6ef04b2fc2b663790b42352f2ca /lib/lexing/headers.ml | |
parent | af76b11278204c25428c4f95ef51d4aa8f2a1e0e (diff) | |
download | chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.tar.gz chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.tar.bz2 chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.zip |
added a functional parser
Diffstat (limited to 'lib/lexing/headers.ml')
-rw-r--r-- | lib/lexing/headers.ml | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/lib/lexing/headers.ml b/lib/lexing/headers.ml new file mode 100644 index 0000000..2452eec --- /dev/null +++ b/lib/lexing/headers.ml @@ -0,0 +1,23 @@ +(* Types for lexing *) + +open Types + +(* Exceptions to aid control flow for lexer *) +exception Not_In_Alphabet of char +exception No_Transition of int * char + +(* Tagged Deterministice Finite Automaton *) +type tdfa = { + alphabet : char list; + start_state: int; + register_init : tok; (* initial contents of the single register for this TDFA *) + delta : int * char -> int * (tok -> tok) +} + +(* Description of a possible state that the TDFA could be in *) +type tdfa_state = { + state_id : int; (* current state *) + register : tok; (* contents of register *) + tokens : tok list; (* tokens emitted so far *) + to_parse : char list; (* characters left to parse *) +} |