milly/examples/regex_matcher.mil

59 lines
1.8 KiB
Plaintext

datatype regex {
Empty,
Lit of string,
Cat of (regex, regex),
Alt of (regex, regex),
Star of regex
}
datatype 'a list {
Empty,
Cons of ('a, 'a list)
}
# Check if a regex matches the null string
typecheck nullable? : regex -> bool
def nullable? <Empty> = false
| nullable? <Lit s> = string_null? s
| nullable? <Cat l r> = logical_and (nullable? l) (nullable? r)
| nullable? <Alt l r> = logical_or (nullable? l) (nullable? r)
| nullable? <Star _> = true
# Check if a regex represents the empty language
typecheck unsatisfiable? : regex -> bool
def unsatisfiable? <Empty> = true
| unsatisfiable? <Lit _> = false
| unsatisfiable? <Cat l r> = logical_or (unsatisfiable? l) (unsatisfiable? r)
| unsatisfiable? <Alt l r> = logical_and (unsatisfiable? l) (unsatisfiable? r)
| unsatisfiable? <Star _> = false
# Regex derivative with respect to a character
typecheck derive : char -> regex -> regex
def derive c <Empty> = Empty
| derive c <Lit s> =
match string_null? s {
case true -> Empty
case false ->
match equal (string_head s) c {
case true -> Lit (string_tail s)
case false -> Empty
}
}
| derive c <Alt l r> = Alt (derive c l) (derive c r)
| derive c <Star r> = Cat (derive c r) (Star r)
| derive c <Cat l r> =
match nullable? l {
case true -> Alt (Cat (derive c l) r) (derive c r)
case false -> Cat (derive c l) r
}
# Let us leverage the regex derivative algorithm to define a regex matcher
typecheck match_regex : string -> regex -> bool
def match_regex str regex =
let
def match_regex1 <Empty> r = nullable? regex
| match_regex1 <Cons c cs> r = match_regex1 cs (derive c cs)
in
match_regex1 (string_to_list str) regex