1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 type pattern_kind = Variable | Constructor
36 let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *)
39 module IntSet = Set.Make (OrderedInt)
41 let int_set_of_int_list l =
42 List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
48 val classify : pattern_t -> pattern_kind
49 val tag_of_pattern : pattern_t -> tag_t * pattern_t list
50 val tag_of_term : term_t -> tag_t * term_t list
51 val string_of_term: term_t -> string
52 val string_of_pattern: pattern_t -> string
55 module Matcher (P: PATTERN) =
57 type row_t = P.pattern_t list * P.pattern_t list * pattern_id
60 let compatible p1 p2 = P.classify p1 = P.classify p2
62 let matched = List.map (fun (matched, _, pid) -> matched, pid)
64 let partition t pidl =
65 let partitions = Hashtbl.create 11 in
66 let add pid row = Hashtbl.add partitions pid row in
69 with Invalid_argument _ -> assert false);
70 let pidset = int_set_of_int_list pidl in
73 match Hashtbl.find_all partitions pid with
75 | patterns -> (pid, List.rev patterns) :: acc)
80 | (_, [], _) :: _ -> true
81 (* if first row has an empty list of patterns, then others have as well *)
84 (* return 2 lists of rows, first one containing homogeneous rows according
85 * to "compatible" below *)
86 let horizontal_split t =
87 let ap, first_row, t', first_row_class =
91 assert false (* are_empty should have been invoked in advance *)
92 | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
94 let rec aux prev_t = function
95 | [] -> List.rev prev_t, []
96 | (_, [], _) :: _ -> assert false
97 | ((_, hd :: _, _) as row) :: tl when compatible ap hd ->
98 aux (row :: prev_t) tl
99 | t -> List.rev prev_t, t
101 let rows1, rows2 = aux [first_row] t' in
102 first_row_class, rows1, rows2
104 (* return 2 lists, first one representing first column, second one
105 * representing a new pattern matrix where matched patterns have been moved
107 let vertical_split t =
110 | decls, hd :: tl, pid -> hd :: decls, tl, pid
114 let variable_closure ksucc =
115 (fun matched_terms constructors terms ->
116 (* prerr_endline "variable_closure"; *)
118 | hd :: tl -> ksucc (hd :: matched_terms) constructors tl
121 let success_closure ksucc =
122 (fun matched_terms constructors terms ->
123 (* prerr_endline "success_closure"; *)
124 ksucc matched_terms constructors)
126 let constructor_closure ksuccs =
127 (fun matched_terms constructors terms ->
128 (* prerr_endline "constructor_closure"; *)
132 let tag, subterms = P.tag_of_term t in
134 if subterms = [] then t :: constructors else constructors
136 let k' = List.assoc tag ksuccs in
137 k' matched_terms constructors' (subterms @ tl)
138 with Not_found -> None)
139 | [] -> assert false)
141 let backtrack_closure ksucc kfail =
142 (fun matched_terms constructors terms ->
143 (* prerr_endline "backtrack_closure"; *)
144 match ksucc matched_terms constructors terms with
146 | None -> kfail matched_terms constructors terms)
148 let compiler rows match_cb fail_k =
151 (fun _ _ _ -> fail_k ())
152 else if are_empty t then
153 success_closure (match_cb (matched t))
155 match horizontal_split t with
156 | _, [], _ -> assert false
157 | Variable, t', [] -> variable_closure (aux (vertical_split t'))
158 | Constructor, t', [] ->
162 | _, p :: _, _ -> fst (P.tag_of_pattern p)
166 let clusters = partition t' tagl in
169 (fun (tag, cluster) ->
171 List.map (* add args as patterns heads *)
173 | matched_p, p :: tl, pid ->
174 let _, subpatterns = P.tag_of_pattern p in
175 matched_p, subpatterns @ tl, pid
182 constructor_closure ksuccs
183 | _, t', t'' -> backtrack_closure (aux t') (aux t'')
185 let t = List.map (fun (p, pid) -> [], [p], pid) rows in
186 let matcher = aux t in
187 (fun term -> matcher [] [] [term])