summaryrefslogtreecommitdiff
path: root/lib/lexing/utils.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/utils.ml
parentaf76b11278204c25428c4f95ef51d4aa8f2a1e0e (diff)
downloadchadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.tar.gz
chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.tar.bz2
chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.zip
added a functional parser
Diffstat (limited to 'lib/lexing/utils.ml')
-rw-r--r--lib/lexing/utils.ml36
1 files changed, 36 insertions, 0 deletions
diff --git a/lib/lexing/utils.ml b/lib/lexing/utils.ml
new file mode 100644
index 0000000..aa218f5
--- /dev/null
+++ b/lib/lexing/utils.ml
@@ -0,0 +1,36 @@
+open Types
+open Headers
+
+(* Function for stepping through a TDFA computation *)
+let step (automaton : tdfa) (state : tdfa_state) : tdfa_state =
+ match state.to_parse with
+ | [] -> state
+ | c :: cs ->
+ try
+ let next_state_id, f = automaton.delta (state.state_id, c) in
+ let next_tok = f state.register in
+ {
+ state_id = next_state_id;
+ register = next_tok;
+ tokens = state.tokens;
+ to_parse = cs
+ }
+ with (No_Transition (_, c)) ->
+ let token_to_add = state.register in
+ let next_state_id, f = automaton.delta (0, c) in
+ let next_tok = f SKIP in
+ {
+ state_id = next_state_id;
+ register = next_tok;
+ tokens = if token_to_add <> SKIP then token_to_add :: state.tokens else state.tokens;
+ to_parse = cs
+ }
+
+(* Driver to perform a TDFA computation *)
+let rec driver (automaton : tdfa) (state: tdfa_state) : tok list =
+ if
+ state.to_parse = []
+ then
+ List.rev (state.register :: state.tokens) (* ensure that final tag is emitted *)
+ else
+ driver automaton (step automaton state)