2025-09-28 22:01:44 +01:00
|
|
|
structure Nfa =
|
|
|
|
|
struct
|
|
|
|
|
datatype regex =
|
2025-10-01 10:48:45 +01:00
|
|
|
CHAR_LITERAL of char
|
|
|
|
|
| CONCAT of regex list
|
|
|
|
|
| ALTERNATION of regex list
|
|
|
|
|
| ZERO_OR_ONE of regex
|
|
|
|
|
| ZERO_OR_MORE of regex
|
|
|
|
|
| ONE_OR_MORE of regex
|
|
|
|
|
| GROUP of regex
|
|
|
|
|
| WILDCARD
|
2025-09-29 00:46:05 +01:00
|
|
|
|
2025-09-29 08:33:10 +01:00
|
|
|
structure ParseNfa =
|
|
|
|
|
struct
|
2025-09-29 13:34:55 +01:00
|
|
|
(* parsing through precedence climbing algorithm. *)
|
2025-09-29 00:46:05 +01:00
|
|
|
|
2025-09-30 14:25:45 +01:00
|
|
|
datatype action =
|
|
|
|
|
TRY_NEXT_NODE_WITHOUT_CONSUMING_CHR
|
|
|
|
|
|
2025-09-29 08:33:10 +01:00
|
|
|
val groupLevel = 1
|
|
|
|
|
val postfixLevel = 2
|
|
|
|
|
val concatLevel = 3
|
|
|
|
|
val altLevel = 4
|
2025-09-29 01:06:15 +01:00
|
|
|
|
2025-09-29 08:33:10 +01:00
|
|
|
local
|
|
|
|
|
fun loop (pos, str, openParens, closeParens) =
|
|
|
|
|
if pos = String.size str then
|
2025-09-29 13:34:55 +01:00
|
|
|
NONE
|
2025-09-29 08:33:10 +01:00
|
|
|
else
|
|
|
|
|
case String.sub (str, pos) of
|
|
|
|
|
#"(" => loop (pos + 1, str, openParens + 1, closeParens)
|
|
|
|
|
| #")" =>
|
2025-09-29 13:34:55 +01:00
|
|
|
if closeParens + 1 = openParens then SOME pos
|
2025-09-29 08:33:10 +01:00
|
|
|
else loop (pos + 1, str, openParens, closeParens + 1)
|
|
|
|
|
| _ => loop (pos + 1, str, openParens, closeParens)
|
|
|
|
|
in
|
|
|
|
|
fun getRightParenIdx (pos, str) = loop (pos, str, 1, 0)
|
|
|
|
|
end
|
2025-09-29 00:46:05 +01:00
|
|
|
|
2025-09-29 13:34:55 +01:00
|
|
|
fun climb (pos, str, lhs, level) : (int * regex) option =
|
2025-09-29 00:46:05 +01:00
|
|
|
if pos = String.size str then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
2025-09-29 00:46:05 +01:00
|
|
|
else
|
2025-09-29 08:33:10 +01:00
|
|
|
case String.sub (str, pos) of
|
2025-09-29 13:34:55 +01:00
|
|
|
#")" => SOME (pos + 1, lhs)
|
2025-09-29 08:33:10 +01:00
|
|
|
| #"(" =>
|
|
|
|
|
if level < groupLevel then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
2025-09-29 08:33:10 +01:00
|
|
|
else
|
2025-09-29 13:34:55 +01:00
|
|
|
(case getRightParenIdx (pos + 1, str) of
|
|
|
|
|
SOME groupEndIdx =>
|
|
|
|
|
let
|
|
|
|
|
val substr = String.substring
|
|
|
|
|
(str, pos + 1, groupEndIdx - pos - 1)
|
|
|
|
|
in
|
|
|
|
|
(case parse substr of
|
|
|
|
|
SOME rhs =>
|
|
|
|
|
let
|
2025-10-01 10:48:45 +01:00
|
|
|
val rhs = GROUP rhs
|
|
|
|
|
val result = CONCAT [lhs, rhs]
|
2025-09-29 13:34:55 +01:00
|
|
|
in
|
|
|
|
|
climb (groupEndIdx + 1, str, result, groupLevel)
|
|
|
|
|
end
|
|
|
|
|
| NONE => NONE)
|
|
|
|
|
end
|
|
|
|
|
| NONE => NONE)
|
2025-09-29 08:33:10 +01:00
|
|
|
| #"|" =>
|
|
|
|
|
if level < altLevel then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
|
|
|
|
else if pos + 1 < String.size str then
|
2025-09-29 08:33:10 +01:00
|
|
|
let
|
|
|
|
|
val chr = String.sub (str, pos + 1)
|
2025-10-01 10:48:45 +01:00
|
|
|
val chr = CHAR_LITERAL chr
|
2025-09-29 08:33:10 +01:00
|
|
|
in
|
2025-09-29 13:34:55 +01:00
|
|
|
case climb (pos + 2, str, chr, altLevel) of
|
|
|
|
|
SOME (pos, rhs) =>
|
|
|
|
|
let
|
|
|
|
|
val result =
|
|
|
|
|
case rhs of
|
2025-10-01 10:48:45 +01:00
|
|
|
ALTERNATION lst => ALTERNATION (lhs :: lst)
|
|
|
|
|
| _ => ALTERNATION [lhs, rhs]
|
2025-09-29 13:34:55 +01:00
|
|
|
in
|
|
|
|
|
SOME (pos, result)
|
|
|
|
|
end
|
|
|
|
|
| NONE => NONE
|
2025-09-29 08:33:10 +01:00
|
|
|
end
|
2025-09-29 13:34:55 +01:00
|
|
|
else
|
|
|
|
|
NONE
|
2025-09-29 08:33:10 +01:00
|
|
|
| #"?" =>
|
|
|
|
|
if level < postfixLevel then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
2025-09-29 08:33:10 +01:00
|
|
|
else
|
2025-10-01 10:48:45 +01:00
|
|
|
let val lhs = ZERO_OR_ONE lhs
|
2025-09-29 08:33:10 +01:00
|
|
|
in climb (pos + 1, str, lhs, postfixLevel)
|
|
|
|
|
end
|
|
|
|
|
| #"*" =>
|
|
|
|
|
if level < postfixLevel then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
2025-09-29 08:33:10 +01:00
|
|
|
else
|
2025-10-01 10:48:45 +01:00
|
|
|
let val lhs = ZERO_OR_MORE lhs
|
2025-09-29 08:33:10 +01:00
|
|
|
in climb (pos + 1, str, lhs, postfixLevel)
|
|
|
|
|
end
|
|
|
|
|
| #"+" =>
|
|
|
|
|
if level < postfixLevel then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
2025-09-29 08:33:10 +01:00
|
|
|
else
|
2025-10-01 10:48:45 +01:00
|
|
|
let val lhs = ONE_OR_MORE lhs
|
2025-09-29 08:33:10 +01:00
|
|
|
in climb (pos + 1, str, lhs, postfixLevel)
|
|
|
|
|
end
|
|
|
|
|
| chr =>
|
|
|
|
|
if level < concatLevel then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME (pos, lhs)
|
2025-09-29 08:33:10 +01:00
|
|
|
else
|
2025-09-30 14:05:39 +01:00
|
|
|
let
|
|
|
|
|
val currentState =
|
2025-10-01 10:48:45 +01:00
|
|
|
if chr = #"." then WILDCARD else CHAR_LITERAL chr
|
2025-09-30 14:05:39 +01:00
|
|
|
in
|
|
|
|
|
case climb (pos + 1, str, currentState, concatLevel) of
|
|
|
|
|
SOME (pos, rhs) =>
|
|
|
|
|
let
|
|
|
|
|
val result =
|
|
|
|
|
case rhs of
|
2025-10-01 10:48:45 +01:00
|
|
|
CONCAT lst => CONCAT (lhs :: lst)
|
|
|
|
|
| _ => CONCAT [lhs, rhs]
|
2025-09-30 14:05:39 +01:00
|
|
|
in
|
|
|
|
|
SOME (pos, result)
|
|
|
|
|
end
|
|
|
|
|
| NONE => NONE
|
|
|
|
|
end
|
2025-09-29 00:46:05 +01:00
|
|
|
|
2025-09-29 08:33:10 +01:00
|
|
|
and loop (pos, str, ast) =
|
2025-09-28 22:01:44 +01:00
|
|
|
if pos = String.size str then
|
2025-09-29 13:34:55 +01:00
|
|
|
SOME ast
|
2025-09-28 22:01:44 +01:00
|
|
|
else
|
2025-09-29 13:34:55 +01:00
|
|
|
case climb (pos, str, ast, altLevel) of
|
|
|
|
|
SOME (pos, ast) => loop (pos, str, ast)
|
|
|
|
|
| NONE => NONE
|
2025-09-28 22:01:44 +01:00
|
|
|
|
2025-09-29 08:33:10 +01:00
|
|
|
and parse str =
|
2025-09-29 13:34:55 +01:00
|
|
|
if String.size str > 0 then
|
2025-09-30 14:25:45 +01:00
|
|
|
(* todo: we currently assume that the first char is always a CHAR_LITERAL
|
|
|
|
|
* but we should actually check what character the chr is
|
|
|
|
|
* before deciding it represents one variant or another *)
|
2025-09-29 13:34:55 +01:00
|
|
|
let
|
|
|
|
|
val chr = String.sub (str, 0)
|
2025-10-01 10:48:45 +01:00
|
|
|
val chr = CHAR_LITERAL chr
|
2025-09-29 13:34:55 +01:00
|
|
|
in
|
|
|
|
|
loop (1, str, chr)
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
NONE
|
2025-09-29 08:33:10 +01:00
|
|
|
end
|
2025-09-28 22:01:44 +01:00
|
|
|
|
2025-09-29 08:33:10 +01:00
|
|
|
val parse = ParseNfa.parse
|
2025-09-28 22:01:44 +01:00
|
|
|
end
|