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