]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/pxp/pxp/pxp_dfa.ml
Initial revision
[helm.git] / helm / DEVEL / pxp / pxp / pxp_dfa.ml
1 (* $Id$
2  * ----------------------------------------------------------------------
3  *
4  *)
5
6 module StringOrd = struct
7   type t = string
8   let compare = (compare : string -> string -> int)
9 end;;
10
11 module StringMap = Map.Make(StringOrd);;
12   (* 'a StringMap.t: the type of maps (dictionaries) from string to 'a *)
13
14 module Graph = struct
15   type vertex =
16       { mutable edges_out : (string * vertex) list;
17         mutable edges_out_map : vertex StringMap.t;
18         mutable edges_in : (vertex * string) list;
19         mutable graph : graph;
20         mutable id : int;
21       }
22   and graph =
23       { mutable vertexes : vertex list;
24         mutable mid : int;   (* maximum id + 1 *)
25       }
26
27   exception Edge_not_unique
28
29   let create () =
30     { vertexes = [];
31       mid = 0;
32     }
33
34   let new_vertex g =
35     let v =
36       { edges_out = [];
37         edges_out_map = StringMap.empty;
38         edges_in = [];
39         graph = g;
40         id = g.mid;
41       } in
42     g.vertexes <- v :: g.vertexes;
43     g.mid <- g.mid + 1;
44     v
45
46   let new_edge v_from e v_to =
47     if v_from.graph != v_to.graph then
48       invalid_arg "Pxp_dfa.Graph.new_edge";
49     try 
50       let v = StringMap.find e v_from.edges_out_map in
51       if v != v_to then
52         raise Edge_not_unique;
53     with
54         Not_found ->
55           v_from.edges_out     <- (e, v_to) :: v_from.edges_out;
56           v_from.edges_out_map <- StringMap.add e v_to v_from.edges_out_map;
57           v_to.edges_in        <- (v_from, e) :: v_to.edges_in;
58           ()
59
60   let graph_of_vertex v = v.graph
61
62   let union g1 g2 =
63     List.iter
64       (fun v ->
65          v.graph <- g1;
66          v.id <- v.id + g1.mid;
67       )
68       g2.vertexes;
69     g1.vertexes <- g2.vertexes @ g1.vertexes;
70     g1.mid <- g1.mid + g2.mid;
71     g2.vertexes <- [];
72     g2.mid <- 0
73
74   let outgoing_edges v =
75     v.edges_out
76
77   let ingoing_edges v =
78     v.edges_in
79
80   let follow_edge v e =
81     StringMap.find e v.edges_out_map  (* or raise Not_found *)
82 end
83 ;;
84
85
86 module VertexOrd = struct
87   type t = Graph.vertex
88   let compare v1 v2 =
89     if v1.Graph.graph != v2.Graph.graph then
90       invalid_arg "Pxp_dfa.VertexOrd.compare";
91     compare v1.Graph.id v2.Graph.id
92 end
93 ;;
94
95 module VertexSet = Set.Make(VertexOrd);;
96
97
98 type dfa_definition =
99     { dfa_graph : Graph.graph;
100       dfa_start : Graph.vertex;
101       dfa_stops : VertexSet.t;
102       dfa_null  : bool;
103     }
104 ;;
105
106 (**********************************************************************)
107
108 (* Now that we have all the auxiliary data types, it is time for the
109  * algorithm that transforms regexps to DFAs.
110  *)
111
112 open Pxp_types
113
114 let dfa_of_regexp_content_model re =
115   let rec get_dfa re =
116     match re with
117         Child e ->
118           let g = Graph.create() in
119           let v1 = Graph.new_vertex g in
120           let v2 = Graph.new_vertex g in
121           Graph.new_edge v1 e v2;
122           { dfa_graph = g;
123             dfa_start = v1;
124             dfa_stops = VertexSet.singleton v2;
125             dfa_null = false;
126           }
127           
128       | Seq [] ->
129           invalid_arg "Pxp_dfa.dfa_of_regexp_content_model"
130       | Seq [re'] ->
131           get_dfa re'
132       | Seq (re1 :: seq2) ->
133           let dfa1 = get_dfa re1 in
134           let dfa2 = get_dfa (Seq seq2) in
135           (* Merge the two graphs. The result is in dfa1.dfa_graph: *)
136           Graph.union dfa1.dfa_graph dfa2.dfa_graph;
137           (* Concatenation I: Add additional edges to the graph such
138            * that if w1 matches dfa1, and w2 matches dfa2, and w2 is not
139            * empty, w1w2 will match the merged DFAs.
140            *)
141           List.iter
142             (fun (e,v') ->
143                VertexSet.iter
144                  (fun v ->
145                     Graph.new_edge v e v')
146                  dfa1.dfa_stops
147             )
148             (Graph.outgoing_edges dfa2.dfa_start);
149           (* Concatenation II: If the emtpy string matches dfa2, the stop
150            * nodes of dfa1 remain stop nodes.
151            *)
152           let stops =
153             if dfa2.dfa_null then
154               VertexSet.union dfa1.dfa_stops dfa2.dfa_stops
155             else
156               dfa2.dfa_stops
157           in
158           (* The resulting DFA: *)
159           { dfa_graph = dfa1.dfa_graph;
160             dfa_start = dfa1.dfa_start;
161             dfa_stops = stops;
162             dfa_null  = dfa1.dfa_null && dfa2.dfa_null;
163           }
164
165       | Alt [] ->
166           invalid_arg "Pxp_dfa.dfa_of_regexp_content_model"
167       | Alt [re'] ->
168           get_dfa re'
169       | Alt alt ->
170           let dfa_alt = List.map get_dfa alt in
171           (* Merge the graphs. The result is in g: *)
172           let g = (List.hd dfa_alt).dfa_graph in
173           List.iter
174             (fun dfa ->
175                Graph.union g dfa.dfa_graph
176             )
177             (List.tl dfa_alt);
178           (* Get the new start node: *)
179           let start = Graph.new_vertex g in
180           (* Add the new edges starting at 'start': *)
181           List.iter
182             (fun dfa ->
183                List.iter
184                  (fun (e, v) ->
185                     Graph.new_edge start e v)
186                  (Graph.outgoing_edges dfa.dfa_start)
187             )
188             dfa_alt;
189           (* If one of the old start nodes was a stop node, the new start
190            * node will be a stop node, too.
191            *)
192           let null = List.exists (fun dfa -> dfa.dfa_null) dfa_alt in
193           let stops =
194             List.fold_left
195               (fun s dfa -> VertexSet.union s dfa.dfa_stops)
196               VertexSet.empty
197               dfa_alt in
198           let stops' =
199             if null then
200               VertexSet.union stops (VertexSet.singleton start)
201             else
202               stops in
203           (* The resulting DFA: *)
204           { dfa_graph = g;
205             dfa_start = start;
206             dfa_stops = stops';
207             dfa_null  = null;
208           }
209
210       | Optional re' ->
211           let dfa' = get_dfa re' in
212           if dfa'.dfa_null then
213             (* simple case *)
214             dfa'
215           else begin
216             (* Optimization possible: case ingoing_edges dfa_start = [] *)
217             let start = Graph.new_vertex dfa'.dfa_graph in
218             List.iter
219               (fun (e, v) ->
220                  Graph.new_edge start e v)
221               (Graph.outgoing_edges dfa'.dfa_start);
222             
223             (* The resulting DFA: *)
224             { dfa_graph = dfa'.dfa_graph;
225               dfa_start = start;
226               dfa_stops = VertexSet.union dfa'.dfa_stops 
227                                           (VertexSet.singleton start);
228               dfa_null  = true;
229             }
230           end
231
232       | Repeated1 re' ->
233           let dfa' = get_dfa re' in
234           List.iter
235             (fun (e, v') ->
236                VertexSet.iter
237                  (fun v ->
238                     Graph.new_edge v e v')
239                  dfa'.dfa_stops
240             )
241             (Graph.outgoing_edges dfa'.dfa_start);
242
243             (* The resulting DFA: *)
244             { dfa_graph = dfa'.dfa_graph;
245               dfa_start = dfa'.dfa_start;
246               dfa_stops = dfa'.dfa_stops;
247               dfa_null  = dfa'.dfa_null;
248             }
249
250       | Repeated re' ->
251           get_dfa (Optional (Repeated1 re'))
252
253   in
254   try
255     get_dfa re
256   with
257       Graph.Edge_not_unique -> raise Not_found
258 ;;
259
260 (* ======================================================================
261  * History:
262  * 
263  * $Log$
264  * Revision 1.1  2000/11/17 09:57:29  lpadovan
265  * Initial revision
266  *
267  * Revision 1.1  2000/07/23 02:16:08  gerd
268  *      Initial revision.
269  *
270  * 
271  *)