]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/extlib/patternMatcher.ml
missing notation file
[helm.git] / matitaB / components / extlib / patternMatcher.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 type pattern_kind = Variable | Constructor
31 type tag_t = int
32
33 type pattern_id = int
34
35 module OrderedInt =
36 struct
37   type t = int
38   let compare (x1:t) (x2:t) = Pervasives.compare x2 x1  (* reverse order *)
39 end
40
41 module IntSet = Set.Make (OrderedInt)
42
43 let int_set_of_int_list l =
44   List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
45
46 module type PATTERN =
47 sig
48   type pattern_t
49   type term_t
50   val classify : pattern_t -> pattern_kind
51   val tag_of_pattern : pattern_t -> tag_t * pattern_t list
52   val tag_of_term : term_t -> tag_t * term_t list
53   val string_of_term: term_t -> string
54   val string_of_pattern: pattern_t -> string
55 end
56
57 module Matcher (P: PATTERN) =
58 struct
59   type row_t = P.pattern_t list * P.pattern_t list * pattern_id
60   type t = row_t list
61
62   let compatible p1 p2 = P.classify p1 = P.classify p2
63
64   let matched = List.map (fun (matched, _, pid) -> matched, pid)
65
66   let partition t pidl =
67     let partitions = Hashtbl.create 11 in
68     let add pid row = Hashtbl.add partitions pid row in
69     (try
70       List.iter2 add pidl t
71     with Invalid_argument _ -> assert false);
72     let pidset = int_set_of_int_list pidl in
73     IntSet.fold
74       (fun pid acc ->
75         match Hashtbl.find_all partitions pid with
76         | [] -> acc
77         | patterns -> (pid, List.rev patterns) :: acc)
78       pidset []
79
80   let are_empty t =
81     match t with
82     | (_, [], _) :: _ -> true
83       (* if first row has an empty list of patterns, then others have as well *)
84     | _ -> false
85
86     (* return 2 lists of rows, first one containing homogeneous rows according
87      * to "compatible" below *)
88   let horizontal_split t =
89     let ap, first_row, t', first_row_class =
90       match t with
91       | [] -> assert false
92       | (_, [], _) :: _ ->
93           assert false  (* are_empty should have been invoked in advance *)
94       | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
95     in
96     let rec aux prev_t = function
97       | [] -> List.rev prev_t, []
98       | (_, [], _) :: _ -> assert false
99       | ((_, hd :: _, _) as row) :: tl when compatible ap hd ->
100           aux (row :: prev_t) tl
101       | t -> List.rev prev_t, t
102     in
103     let rows1, rows2 = aux [first_row] t' in
104     first_row_class, rows1, rows2
105
106     (* return 2 lists, first one representing first column, second one
107      * representing a new pattern matrix where matched patterns have been moved
108      * to decl *)
109   let vertical_split t =
110     List.map
111       (function
112         | decls, hd :: tl, pid -> hd :: decls, tl, pid
113         | _ -> assert false)
114       t
115
116   let variable_closure ksucc =
117     (fun matched_terms constructors terms ->
118 (* prerr_endline "variable_closure"; *)
119       match terms with
120       | hd :: tl -> ksucc (hd :: matched_terms) constructors tl
121       | _ -> assert false)
122
123   let success_closure ksucc =
124     (fun matched_terms constructors terms ->
125 (* prerr_endline "success_closure"; *)
126        ksucc matched_terms constructors)
127
128   let constructor_closure ksuccs =
129     (fun matched_terms constructors terms ->
130 (* prerr_endline "constructor_closure"; *)
131       match terms with
132       | t :: tl ->
133           (try
134             let tag, subterms = P.tag_of_term t in
135             let constructors' =
136               if subterms = [] then t :: constructors else constructors
137             in
138             let k' = List.assoc tag ksuccs in
139             k' matched_terms constructors' (subterms @ tl)
140           with Not_found -> None)
141       | [] -> assert false)
142
143   let backtrack_closure ksucc kfail =
144     (fun matched_terms constructors terms ->
145 (* prerr_endline "backtrack_closure"; *)
146       match ksucc matched_terms constructors terms with
147       | Some x -> Some x
148       | None -> kfail matched_terms constructors terms)
149
150   let compiler rows match_cb fail_k =
151     let rec aux t =
152       if t = [] then
153         (fun _ _ _ -> fail_k ())
154       else if are_empty t then
155         success_closure (match_cb (matched t))
156       else
157         match horizontal_split t with
158         | _, [], _ -> assert false
159         | Variable, t', [] -> variable_closure (aux (vertical_split t'))
160         | Constructor, t', [] ->
161             let tagl =
162               List.map
163                 (function
164                   | _, p :: _, _ -> fst (P.tag_of_pattern p)
165                   | _ -> assert false)
166                 t'
167             in
168             let clusters = partition t' tagl in
169             let ksuccs =
170               List.map
171                 (fun (tag, cluster) ->
172                   let cluster' =
173                     List.map  (* add args as patterns heads *)
174                       (function
175                         | matched_p, p :: tl, pid ->
176                             let _, subpatterns = P.tag_of_pattern p in
177                             matched_p, subpatterns @ tl, pid
178                         | _ -> assert false)
179                       cluster
180                   in
181                   tag, aux cluster')
182                 clusters
183             in
184             constructor_closure ksuccs
185         | _, t', t'' -> backtrack_closure (aux t') (aux t'')
186     in
187     let t = List.map (fun (p, pid) -> [], [p], pid) rows in
188     let matcher = aux t in
189     (fun term -> matcher [] [] [term])
190 end
191