type rpattern = Rnil | Remp | Rcha of char | Rplu of rpattern * rpattern | Rtim of rpattern * rpattern | Rsta of rpattern ;; datatype pattern with (nat,nat) = Pnil (0, 1) | Pemp(0, 0) | Pcha(0, 1) of char | {s1:nat}{s2:nat}{p1:nat | p1 > 0}{p2:nat | p2 > 0} Pplu(1+s1+s2, min(p1, p2)) of pattern(s1, p1) * pattern(s2, p2) | {s1:nat}{s2:nat}{p1:nat}{p2:nat | p1+p2 > 0} Ptim(1+s1+s2, p1+p2) of pattern(s1, p1) * pattern(s2, p2) | {s:nat}{p:nat | p > 0} Psta(1+s, 0) of pattern(s, p) ;; let rec delta = function Rnil -> Pnil | Remp -> Pemp | Rcha _ -> Pnil | Rplu (rp1, rp2) -> begin match delta rp1, delta rp2 with Pnil, Pnil -> Pnil | _, _ -> Pemp end | Rtim (rp1, rp2) -> begin match delta rp1, delta rp2 with Pemp, Pemp -> Pemp | _, _ -> Pnil end | Rsta rp -> Pemp withtype rpattern -> pattern ;; let rec norm = function Rnil -> Pnil | Remp -> Pnil | Rcha c -> Pcha c | Rplu (rp1, rp2) -> Pplu (norm rp1, norm rp2) | Rtim (rp1, rp2) -> let p1 = norm rp1 in let p2 = norm rp2 in Pplu (Pplu (Ptim (delta rp1, p2), Ptim (p1, delta rp2)), Ptim (p1, p2)) | Rsta rp -> let p = norm rp in Ptim (p, Psta p) withtype rpattern -> [s:nat][p:nat | p > 0] pattern(s,p) ;; let rec acc p cs k = match p with Pnil -> false | Pemp -> k (cs) | Pcha(c') -> begin match cs with | [] -> false | c :: cs' -> if (c = c') then k (cs') else false end | Pplu(p1, p2) -> if acc p1 cs k then true else acc p2 cs k | Ptim(p1, p2) -> acc p1 cs (fun cs' -> acc p2 cs' k) | Psta(p0) -> if k (cs) then true else acc p0 cs (fun cs' -> acc p cs' k) withtype {s:nat}{p:nat}{n:nat} pattern(s,p) -> char list(n) -> ({n':nat | n'+p <= n} char list(n') -> bool) -> bool ;; let accept rp cs = let k0 = (function [] -> true | _ :: _ -> false) in if (acc (delta rp) cs k0) then true else acc (norm rp) cs k0 withtype rpattern -> char list -> bool ;;