Add new example

examples/regex_matcher.mil

@@ -0,0 +1,58 @@
+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