matita/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 type pattern_kind = Variable | Constructor
  29 type tag_t = int
  30
  31 type pattern_id = int
  32
  33 module OrderedInt =
  34 struct
  35   type t = int
  36   let compare (x1:t) (x2:t) = Stdlib.compare x2 x1  (* reverse order *)
  37 end
  38
  39 module IntSet = Set.Make (OrderedInt)
  40
  41 let int_set_of_int_list l =
  42   List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
  43
  44 module type PATTERN =
  45 sig
  46   type pattern_t
  47   type term_t
  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
  53 end
  54
  55 module Matcher (P: PATTERN) =
  56 struct
  57   type row_t = P.pattern_t list * P.pattern_t list * pattern_id
  58   type t = row_t list
  59
  60   let compatible p1 p2 = P.classify p1 = P.classify p2
  61
  62   let matched = List.map (fun (matched, _, pid) -> matched, pid)
  63
  64   let partition t pidl =
  65     let partitions = Hashtbl.create 11 in
  66     let add pid row = Hashtbl.add partitions pid row in
  67     (try
  68       List.iter2 add pidl t
  69     with Invalid_argument _ -> assert false);
  70     let pidset = int_set_of_int_list pidl in
  71     IntSet.fold
  72       (fun pid acc ->
  73         match Hashtbl.find_all partitions pid with
  74         | [] -> acc
  75         | patterns -> (pid, List.rev patterns) :: acc)
  76       pidset []
  77
  78   let are_empty t =
  79     match t with
  80     | (_, [], _) :: _ -> true
  81       (* if first row has an empty list of patterns, then others have as well *)
  82     | _ -> false
  83
  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 =
  88       match t with
  89       | [] -> assert false
  90       | (_, [], _) :: _ ->
  91           assert false  (* are_empty should have been invoked in advance *)
  92       | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
  93     in
  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
 100     in
 101     let rows1, rows2 = aux [first_row] t' in
 102     first_row_class, rows1, rows2
 103
 104     (* return 2 lists, first one representing first column, second one
 105      * representing a new pattern matrix where matched patterns have been moved
 106      * to decl *)
 107   let vertical_split t =
 108     List.map
 109       (function
 110         | decls, hd :: tl, pid -> hd :: decls, tl, pid
 111         | _ -> assert false)
 112       t
 113
 114   let variable_closure ksucc kfail =
 115     (fun matched_terms constructors terms ->
 116 (* prerr_endline "variable_closure"; *)
 117       match terms with
 118       | hd :: tl -> ksucc (hd :: matched_terms) constructors tl
 119       | _ -> kfail () (*CSC: was assert false, but it did happen*))
 120
 121   let success_closure ksucc =
 122     (fun matched_terms constructors _terms ->
 123 (* prerr_endline "success_closure"; *)
 124        ksucc matched_terms constructors)
 125
 126   let constructor_closure ksuccs =
 127     (fun matched_terms constructors terms ->
 128 (* prerr_endline "constructor_closure"; *)
 129       match terms with
 130       | t :: tl ->
 131           (try
 132             let tag, subterms = P.tag_of_term t in
 133             let constructors' =
 134               if subterms = [] then t :: constructors else constructors
 135             in
 136             let k' = List.assoc tag ksuccs in
 137             k' matched_terms constructors' (subterms @ tl)
 138           with Not_found -> None)
 139       | [] -> assert false)
 140
 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
 145       | Some x -> Some x
 146       | None -> kfail matched_terms constructors terms)
 147
 148   let compiler rows match_cb fail_k =
 149     let rec aux t =
 150       if t = [] then
 151         (fun _ _ _ -> fail_k ())
 152       else if are_empty t then
 153         success_closure (match_cb (matched t))
 154       else
 155         match horizontal_split t with
 156         | _, [], _ -> assert false
 157         | Variable, t', [] -> variable_closure (aux (vertical_split t')) fail_k
 158         | Constructor, t', [] ->
 159             let tagl =
 160               List.map
 161                 (function
 162                   | _, p :: _, _ -> fst (P.tag_of_pattern p)
 163                   | _ -> assert false)
 164                 t'
 165             in
 166             let clusters = partition t' tagl in
 167             let ksuccs =
 168               List.map
 169                 (fun (tag, cluster) ->
 170                   let cluster' =
 171                     List.map  (* add args as patterns heads *)
 172                       (function
 173                         | matched_p, p :: tl, pid ->
 174                             let _, subpatterns = P.tag_of_pattern p in
 175                             matched_p, subpatterns @ tl, pid
 176                         | _ -> assert false)
 177                       cluster
 178                   in
 179                   tag, aux cluster')
 180                 clusters
 181             in
 182             constructor_closure ksuccs
 183         | _, t', t'' -> backtrack_closure (aux t') (aux t'')
 184     in
 185     let t = List.map (fun (p, pid) -> [], [p], pid) rows in
 186     let matcher = aux t in
 187     (fun term -> matcher [] [] [term])
 188 end
 189