Вот код от неэксперта. Он показывает, как выглядит проблема, если вы ограничиваете свои шаблоны списком конструкторов. Другими словами, шаблоны могут использоваться только со списками, которые содержат списки. Вот несколько таких списков: [], [[]], [[];[]].
Если вы включите -rectypes в интерпретаторе OCaml, этот набор списков будет одного типа: ('a list) as 'a.
type reclist = ('a list) as 'a
Вот тип для представления шаблонов, которые соответствуют типу reclist:
type p = Nil | Any | Cons of p * p
Чтобы перевести шаблон OCaml в эту форму, сначала переписать, используя (: :). Затем замените []
с Nil, _ с Any, и (: :) с Cons. Таким образом, шаблон [] :: _ переводится в
Cons (Nil, Any)
Вот функция, которая сопоставляет шаблон с списком:
let rec pmatch (p: p) (l: reclist) =
match p, l with
| Any, _ -> true
| Nil, [] -> true
| Cons (p', q'), h :: t -> pmatch p' h && pmatch q' t
| _ -> false
Вот как это выглядит при использовании. Обратите внимание на использование -rectypes:
$ ocaml312 -rectypes
Objective Caml version 3.12.0
# #use "pat.ml";;
type p = Nil | Any | Cons of p * p
type reclist = 'a list as 'a
val pmatch : p -> reclist -> bool = <fun>
# pmatch (Cons(Any, Nil)) [];;
- : bool = false
# pmatch (Cons(Any, Nil)) [[]];;
- : bool = true
# pmatch (Cons(Any, Nil)) [[]; []];;
- : bool = false
# pmatch (Cons (Any, Nil)) [ [[]; []] ];;
- : bool = true
#
Шаблон Cons (Any, Nil) должен соответствовать любому списку длины 1, и он определенно работает.
Итак, кажется довольно простым написать функцию intersect, которая принимает два шаблона и возвращает шаблон, который соответствует пересечению того, что соответствует двум шаблонам. Поскольку шаблоны могут вообще не пересекаться, он возвращает None, когда пересечения нет, и Some p в противном случае.
let rec inter_exc pa pb =
match pa, pb with
| Nil, Nil -> Nil
| Cons (a, b), Cons (c, d) -> Cons (inter_exc a c, inter_exc b d)
| Any, b -> b
| a, Any -> a
| _ -> raise Not_found
let intersect pa pb =
try Some (inter_exc pa pb) with Not_found -> None
let intersectn ps =
(* Intersect a list of patterns.
*)
match ps with
| [] -> None
| head :: tail ->
List.fold_left
(fun a b -> match a with None -> None | Some x -> intersect x b)
(Some head) tail
В качестве простого теста пересекайте шаблон [_, []] с шаблоном [[], _].
Первый такой же, как _ :: [] :: [], и Cons (Any, Cons (Nil, Nil)).
Последний такой же, как [] :: _ :: [], и Cons (Nil, (Cons (Any, Nil)).
# intersect (Cons (Any, Cons (Nil, Nil))) (Cons (Nil, Cons (Any, Nil)));;
- : p option = Some (Cons (Nil, Cons (Nil, Nil)))
Результат выглядит довольно правильно: [[], []].
Кажется, этого достаточно, чтобы ответить на вопрос о перекрывающихся шаблонах. Два шаблона перекрываются, если их пересечение не None.
Для исчерпываемости вам нужно поработать со списком шаблонов. Вот функция
exhaust, который проверяет, является ли данный список шаблонов исчерпывающим:
let twoparts l =
(* All ways of partitioning l into two sets.
*)
List.fold_left
(fun accum x ->
let absent = List.map (fun (a, b) -> (a, x :: b)) accum
in
List.fold_left (fun accum (a, b) -> (x :: a, b) :: accum)
absent accum)
[([], [])] l
let unique l =
(* Eliminate duplicates from the list. Makes things
* faster.
*)
let rec u sl=
match sl with
| [] -> []
| [_] -> sl
| h1 :: ((h2 :: _) as tail) ->
if h1 = h2 then u tail else h1 :: u tail
in
u (List.sort compare l)
let mkpairs ps =
List.fold_right
(fun p a -> match p with Cons (x, y) -> (x, y) :: a | _ -> a) ps []
let rec submatches pairs =
(* For each matchable subset of fsts, return a list of the
* associated snds. A matchable subset has a non-empty
* intersection, and the intersection is not covered by the rest of
* the patterns. I.e., there is at least one thing that matches the
* intersection without matching any of the other patterns.
*)
let noncovint (prs, rest) =
let prs_firsts = List.map fst prs in
let rest_firsts = unique (List.map fst rest) in
match intersectn prs_firsts with
| None -> false
| Some i -> not (cover i rest_firsts)
in let pairparts = List.filter noncovint (twoparts pairs)
in
unique (List.map (fun (a, b) -> List.map snd a) pairparts)
and cover_pairs basepr pairs =
cover (fst basepr) (unique (List.map fst pairs)) &&
List.for_all (cover (snd basepr)) (submatches pairs)
and cover_cons basepr ps =
let pairs = mkpairs ps
in let revpair (a, b) = (b, a)
in
pairs <> [] &&
cover_pairs basepr pairs &&
cover_pairs (revpair basepr) (List.map revpair pairs)
and cover basep ps =
List.mem Any ps ||
match basep with
| Nil -> List.mem Nil ps
| Any -> List.mem Nil ps && cover_cons (Any, Any) ps
| Cons (a, b) -> cover_cons (a, b) ps
let exhaust ps =
cover Any ps
Шаблон похож на дерево с Cons во внутренних узлах и Nil или Any на листьях. Основная идея заключается в том, что набор шаблонов является исчерпывающим, если вы всегда достигаете Any хотя бы в одном из шаблонов (независимо от того, как выглядит вход). И по пути, вы должны увидеть как ноль, так и минусы в каждой точке. Если вы достигнете Nil в одном и том же месте во всех шаблонах, это означает, что есть более длинный ввод, который не будет сопоставлен ни одному из них. С другой стороны, если вы видите только Cons в одном и том же месте во всех шаблонах, есть вход, который заканчивается в этой точке, который не будет соответствовать.
Трудная часть - проверка полноты двух шаблонов минусов. Этот код работает так же, как и я, когда я проверяю вручную: он находит все различные подмножества, которые могут совпадать слева, а затем удостоверяется, что соответствующие правые подшаблоны являются исчерпывающими в каждом случае. Затем то же самое с левым и правым наоборот. Поскольку я неопытный (все более очевидный для меня), вероятно, есть лучшие способы сделать это.
Вот сеанс с этой функцией:
# exhaust [Nil];;
- : bool = false
# exhaust [Any];;
- : bool = true
# exhaust [Nil; Cons (Nil, Any); Cons (Any, Nil)];;
- : bool = false
# exhaust [Nil; Cons (Any, Any)];;
- : bool = true
# exhaust [Nil; Cons (Any, Nil); Cons (Any, (Cons (Any, Any)))];;
- : bool = true
Я проверил этот код по 30 000 случайно сгенерированных шаблонов, и поэтому я уверен, что он прав. Я надеюсь, что эти скромные наблюдения могут оказаться полезными.