1 (* Copyright (C) 2004-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 module Ast = CicNotationPt
29 module Env = CicNotationEnv
30 module Pp = CicNotationPp
31 module Util = CicNotationUtil
40 let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *)
43 module IntSet = Set.Make (OrderedInt)
45 let int_set_of_int_list l =
46 List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
48 type pattern_kind = Variable | Constructor
55 val classify : pattern_t -> pattern_kind
56 val tag_of_pattern : pattern_t -> tag_t * pattern_t list
57 val tag_of_term : term_t -> tag_t * term_t list
58 val string_of_term: term_t -> string
59 val string_of_pattern: pattern_t -> string
62 module Matcher (P: PATTERN) =
64 type row_t = P.pattern_t list * P.pattern_t list * pattern_id
67 let compatible p1 p2 = P.classify p1 = P.classify p2
69 let matched = List.map (fun (matched, _, pid) -> matched, pid)
71 let partition t pidl =
72 let partitions = Hashtbl.create 11 in
73 let add pid row = Hashtbl.add partitions pid row in
76 with Invalid_argument _ -> assert false);
77 let pidset = int_set_of_int_list pidl in
80 match Hashtbl.find_all partitions pid with
82 | patterns -> (pid, List.rev patterns) :: acc)
87 | (_, [], _) :: _ -> true
88 (* if first row has an empty list of patterns, then others have as well *)
91 (* return 2 lists of rows, first one containing homogeneous rows according
92 * to "compatible" below *)
93 let horizontal_split t =
94 let ap, first_row, t', first_row_class =
98 assert false (* are_empty should have been invoked in advance *)
99 | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
101 let rec aux prev_t = function
102 | [] -> List.rev prev_t, []
103 | (_, [], _) :: _ -> assert false
104 | ((_, hd :: _, _) as row) :: tl when compatible ap hd ->
105 aux (row :: prev_t) tl
106 | t -> List.rev prev_t, t
108 let rows1, rows2 = aux [first_row] t' in
109 first_row_class, rows1, rows2
111 (* return 2 lists, first one representing first column, second one
112 * representing a new pattern matrix where matched patterns have been moved
114 let vertical_split t =
117 | decls, hd :: tl, pid -> hd :: decls, tl, pid
121 let variable_closure ksucc =
122 (fun matched_terms constructors terms ->
123 (* prerr_endline "variable_closure"; *)
125 | hd :: tl -> ksucc (hd :: matched_terms) constructors tl
128 let success_closure ksucc =
129 (fun matched_terms constructors terms ->
130 (* prerr_endline "success_closure"; *)
131 ksucc matched_terms constructors)
133 let constructor_closure ksuccs =
134 (fun matched_terms constructors terms ->
135 (* prerr_endline "constructor_closure"; *)
139 let tag, subterms = P.tag_of_term t in
141 if subterms = [] then t :: constructors else constructors
143 let k' = List.assoc tag ksuccs in
144 k' matched_terms constructors' (subterms @ tl)
145 with Not_found -> None)
146 | [] -> assert false)
148 let backtrack_closure ksucc kfail =
149 (fun matched_terms constructors terms ->
150 (* prerr_endline "backtrack_closure"; *)
151 match ksucc matched_terms constructors terms with
153 | None -> kfail matched_terms constructors terms)
155 let compiler rows match_cb fail_k =
158 (fun _ _ _ -> fail_k ())
159 else if are_empty t then
160 success_closure (match_cb (matched t))
162 match horizontal_split t with
163 | _, [], _ -> assert false
164 | Variable, t', [] -> variable_closure (aux (vertical_split t'))
165 | Constructor, t', [] ->
169 | _, p :: _, _ -> fst (P.tag_of_pattern p)
173 let clusters = partition t' tagl in
176 (fun (tag, cluster) ->
178 List.map (* add args as patterns heads *)
180 | matched_p, p :: tl, pid ->
181 let _, subpatterns = P.tag_of_pattern p in
182 matched_p, subpatterns @ tl, pid
189 constructor_closure ksuccs
190 | _, t', t'' -> backtrack_closure (aux t') (aux t'')
192 let t = List.map (fun (p, pid) -> [], [p], pid) rows in
193 let matcher = aux t in
194 (fun term -> matcher [] [] [term])
201 type pattern_t = Ast.term
202 type term_t = Ast.term
203 let rec classify = function
204 | Ast.AttributedTerm (_, t) -> classify t
205 | Ast.Variable _ -> Variable
208 | Ast.Literal _ as t -> assert false
210 let tag_of_pattern = CicNotationTag.get_tag
211 let tag_of_term t = CicNotationTag.get_tag t
212 let string_of_term = CicNotationPp.pp_term
213 let string_of_pattern = CicNotationPp.pp_term
216 module M = Matcher (Pattern21)
218 let extract_magic term =
219 let magic_map = ref [] in
221 let name = Util.fresh_name () in
222 magic_map := (name, m) :: !magic_map;
223 Ast.Variable (Ast.TermVar name)
225 let rec aux = function
226 | Ast.AttributedTerm (_, t) -> assert false
228 | Ast.Layout _ -> assert false
229 | Ast.Variable v -> Ast.Variable v
230 | Ast.Magic m -> add_magic m
231 | t -> Util.visit_ast aux t
233 let term' = aux term in
236 let env_of_matched pl tl =
241 Ast.Variable (Ast.TermVar name), _ ->
242 name, (Env.TermType, Env.TermValue t)
243 | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
244 name, (Env.NumType, Env.NumValue s)
245 | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
246 name, (Env.StringType, Env.StringValue s)
249 with Invalid_argument _ -> assert false
251 let rec compiler rows =
252 let rows', magic_maps =
256 let p', map = extract_magic p in
257 (p', pid), (pid, map))
260 let magichecker map =
263 let m_checker = compile_magic m in
265 match m_checker (Env.lookup_term env name) env ctors with
267 | Some (env, ctors) -> f env ctors))
268 (fun env ctors -> Some (env, ctors))
271 let magichooser candidates =
273 (fun f (pid, pl, checker) ->
274 (fun matched_terms constructors ->
275 let env = env_of_matched pl matched_terms in
276 match checker env constructors with
277 | None -> f matched_terms constructors
278 | Some (env, ctors') ->
280 try List.assoc pid magic_maps with Not_found -> assert false
282 let env' = Env.remove_names env (List.map fst magic_map) in
283 Some (env', ctors', pid)))
285 (List.rev candidates)
292 try List.assoc pid magic_maps with Not_found -> assert false
294 pid, pl, magichecker magic_map)
297 magichooser candidates
299 M.compiler rows' match_cb (fun _ -> None)
301 and compile_magic = function
302 | Ast.Fold (kind, p_base, names, p_rec) ->
303 let p_rec_decls = Env.declarations_of_term p_rec in
304 (* LUCA: p_rec_decls should not contain "names" *)
305 let acc_name = try List.hd names with Failure _ -> assert false in
306 let compiled_base = compiler [p_base, 0]
307 and compiled_rec = compiler [p_rec, 0] in
308 (fun term env ctors ->
310 match compiled_base term with
312 | Some (env', ctors', _) -> Some (env', ctors', [])
315 match compiled_rec term with
316 | None -> aux_base term
317 | Some (env', ctors', _) ->
319 let acc = Env.lookup_term env' acc_name in
320 let env'' = Env.remove_name env' acc_name in
322 | None -> aux_base term
323 | Some (base_env, ctors', rec_envl) ->
324 let ctors'' = ctors' @ ctors in
325 Some (base_env, ctors'',env'' :: rec_envl)
330 | Some (base_env, ctors, rec_envl) ->
332 base_env @ Env.coalesce_env p_rec_decls rec_envl @ env
337 | Ast.Default (p_some, p_none) -> (* p_none can't bound names *)
338 let p_some_decls = Env.declarations_of_term p_some in
339 let p_none_decls = Env.declarations_of_term p_none in
342 (fun decl -> not (List.mem decl p_none_decls))
345 let none_env = List.map Env.opt_binding_of_name p_opt_decls in
346 let compiled = compiler [p_some, 0] in
347 (fun term env ctors ->
348 match compiled term with
349 | None -> Some (none_env, ctors) (* LUCA: @ env ??? *)
350 | Some (env', ctors', 0) ->
353 (fun (name, (ty, v)) as binding ->
354 if List.exists (fun (name', _) -> name = name') p_opt_decls
355 then Env.opt_binding_some binding
359 Some (env' @ env, ctors' @ ctors)
362 | Ast.If (p_test, p_true, p_false) ->
363 let compiled_test = compiler [p_test, 0]
364 and compiled_true = compiler [p_true, 0]
365 and compiled_false = compiler [p_false, 0] in
366 (fun term env ctors ->
368 match compiled_test term with
369 | None -> compiled_false
370 | Some _ -> compiled_true
372 match branch term with
374 | Some (env', ctors', _) -> Some (env' @ env, ctors' @ ctors))
376 | Ast.Fail -> (fun _ _ _ -> None)
387 | Uri of UriManager.uri
388 | Appl of cic_mask_t list
390 let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
392 let mask_of_cic = function
393 | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl
394 | Cic.AConst (_, _, [])
395 | Cic.AVar (_, _, [])
396 | Cic.AMutInd (_, _, _, [])
397 | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), []
401 let mask, tl = mask_of_cic t in
402 Hashtbl.hash mask, tl
404 let mask_of_appl_pattern = function
405 | Ast.UriPattern uri -> Uri uri, []
406 | Ast.ImplicitPattern
407 | Ast.VarPattern _ -> Blob, []
408 | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
410 let tag_of_pattern p =
411 let mask, pl = mask_of_appl_pattern p in
412 Hashtbl.hash mask, pl
414 type pattern_t = Ast.cic_appl_pattern
415 type term_t = Cic.annterm
417 let string_of_pattern = GrafiteAstPp.pp_cic_appl_pattern
418 let string_of_term t = CicPp.ppterm (Deannotate.deannotate_term t)
420 let classify = function
421 | Ast.ImplicitPattern
422 | Ast.VarPattern _ -> Variable
424 | Ast.ApplPattern _ -> Constructor
427 module M = Matcher (Pattern32)
431 let pl, pid = try List.hd rows with Not_found -> assert false in
432 (fun matched_terms constructors ->
438 | Ast.ImplicitPattern -> Util.fresh_name (), t
439 | Ast.VarPattern name -> name, t
442 with Invalid_argument _ -> assert false
444 Some (env, constructors, pid))
446 M.compiler rows match_cb (fun () -> None)