summaryrefslogtreecommitdiff
path: root/lib/lexing/headers.ml
diff options
context:
space:
mode:
authorfilip <“filip.rabiega@gmail.com”>2025-04-22 18:38:38 +0200
committerfilip <“filip.rabiega@gmail.com”>2025-04-22 18:59:19 +0200
commit2e893fd0df7dae8c4ae843d4a23acb098dd97aff (patch)
tree1f4a50da28d2e6ef04b2fc2b663790b42352f2ca /lib/lexing/headers.ml
parentaf76b11278204c25428c4f95ef51d4aa8f2a1e0e (diff)
downloadchadprover-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.ml23
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 *)
+}