helm/ocaml/cic_notation/cicNotationMatcher.ml

   1 (* Copyright (C) 2004-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 open Printf
  27
  28 module Pt = CicNotationPt
  29 module Env = CicNotationEnv
  30 module Util = CicNotationUtil
  31
  32 type pattern_id = int
  33
  34 exception No_match
  35
  36 module OrderedInt =
  37 struct
  38   type t = int
  39   let compare (x1:t) (x2:t) = Pervasives.compare x2 x1  (* reverse order *)
  40 end
  41
  42 module IntSet = Set.Make (OrderedInt)
  43
  44 let int_set_of_int_list l =
  45   List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
  46
  47 type pattern_kind = Variable | Constructor
  48 type tag_t = int
  49
  50 module type PATTERN =
  51 sig
  52   type pattern_t
  53   type term_t
  54   val classify : pattern_t -> pattern_kind
  55   val tag_of_pattern : pattern_t -> tag_t * pattern_t list
  56   val tag_of_term : term_t -> tag_t * term_t list
  57 end
  58
  59 module Matcher (P: PATTERN) =
  60 struct
  61   type row_t = P.pattern_t list * P.pattern_t list * pattern_id
  62   type t = row_t list
  63
  64   let compatible p1 p2 = P.classify p1 = P.classify p2
  65
  66   let matched = List.map (fun (matched, _, pid) -> matched, pid)
  67
  68   let partition t pidl =
  69     let partitions = Hashtbl.create 11 in
  70     let add pid row = Hashtbl.add partitions pid row in
  71     (try
  72       List.iter2 add pidl t
  73     with Invalid_argument _ -> assert false);
  74     let pidset = int_set_of_int_list pidl in
  75     IntSet.fold
  76       (fun pid acc ->
  77         match Hashtbl.find_all partitions pid with
  78         | [] -> acc
  79         | patterns -> (pid, List.rev patterns) :: acc)
  80       pidset []
  81
  82   let are_empty t =
  83     match t with
  84     | (_, [], _) :: _ -> true
  85       (* if first row has an empty list of patterns, then others have as well *)
  86     | _ -> false
  87
  88     (* return 2 lists of rows, first one containing homogeneous rows according
  89      * to "compatible" below *)
  90   let horizontal_split t =
  91     let ap, first_row, t', first_row_class =
  92       match t with
  93       | [] -> assert false
  94       | (_, [], _) :: _ ->
  95           assert false  (* are_empty should have been invoked in advance *)
  96       | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
  97     in
  98     let rec aux prev_t = function
  99       | [] -> List.rev prev_t, []
 100       | (_, [], _) :: _ -> assert false
 101       | ((_, hd :: _, _) as row) :: tl when compatible ap hd ->
 102           aux (row :: prev_t) tl
 103       | t -> List.rev prev_t, t
 104     in
 105     let rows1, rows2 = aux [first_row] t' in
 106     first_row_class, rows1, rows2
 107
 108     (* return 2 lists, first one representing first column, second one
 109      * representing a new pattern matrix where matched patterns have been moved
 110      * to decl *)
 111   let vertical_split t =
 112     List.map
 113       (function
 114         | decls, hd :: tl, pid -> hd :: decls, tl, pid
 115         | _ -> assert false)
 116       t
 117
 118   let variable_closure k =
 119     (fun matched_terms terms ->
 120       match terms with
 121       | hd :: tl -> k (hd :: matched_terms) tl
 122       | _ -> assert false)
 123
 124   let constructor_closure ks k =
 125     (fun matched_terms terms ->
 126       match terms with
 127       | t :: tl ->
 128           (try
 129             let tag, subterms = P.tag_of_term t in
 130             let k' = List.assoc tag ks in
 131             k' matched_terms (subterms @ tl)
 132           with Not_found -> k matched_terms terms)
 133       | [] -> assert false)
 134
 135   let compiler rows match_cb fail_k =
 136     let rec aux t k =
 137       if t = [] then
 138         k
 139       else if are_empty t then
 140         let res = match_cb (matched t) in
 141         (fun matched_terms _ -> res matched_terms)
 142       else
 143         match horizontal_split t with
 144         | _, [], _ -> assert false
 145         | Variable, t', [] -> variable_closure (aux (vertical_split t') k)
 146         | Constructor, t', [] ->
 147             let tagl =
 148               List.map
 149                 (function
 150                   | _, p :: _, _ -> fst (P.tag_of_pattern p)
 151                   | _ -> assert false)
 152                 t'
 153             in
 154             let clusters = partition t' tagl in
 155             let ks =
 156               List.map
 157                 (fun (tag, cluster) ->
 158                   let cluster' =
 159                     List.map  (* add args as patterns heads *)
 160                       (function
 161                         | matched_p, p :: tl, pid ->
 162                             let _, subpatterns = P.tag_of_pattern p in
 163                             matched_p, subpatterns @ tl, pid
 164                         | _ -> assert false)
 165                       cluster
 166                   in
 167                   tag, aux cluster' k)
 168                 clusters
 169             in
 170             constructor_closure ks k
 171         | _, t', t'' -> aux t' (aux t'' k)
 172     in
 173     let t = List.map (fun (p, pid) -> [], [p], pid) rows in
 174     let matcher = aux t (fun _ _ -> fail_k ()) in
 175     (fun term -> matcher [] [term])
 176 end
 177
 178 module Matcher21 =
 179 struct
 180   module Pattern21 =
 181   struct
 182     type pattern_t = Pt.term
 183     type term_t = Pt.term
 184     let classify = function
 185       | Pt.Variable _ -> Variable
 186       | Pt.Magic _
 187       | Pt.Layout _
 188       | Pt.Literal _ as t -> assert false
 189       | _ -> Constructor
 190     let tag_of_pattern = CicNotationTag.get_tag
 191     let tag_of_term = CicNotationTag.get_tag
 192   end
 193
 194   module M = Matcher (Pattern21)
 195
 196   let extract_magic term =
 197     let magic_map = ref [] in
 198     let add_magic m =
 199       let name = Util.fresh_name () in
 200       magic_map := (name, m) :: !magic_map;
 201       Pt.Variable (Pt.TermVar name)
 202     in
 203     let rec aux = function
 204       | Pt.AttributedTerm (_, t) -> aux t
 205       | Pt.Literal _
 206       | Pt.Layout _ -> assert false
 207       | Pt.Variable v -> Pt.Variable v
 208       | Pt.Magic m -> add_magic m
 209       | t -> Util.visit_ast aux t
 210     in
 211     let term' = aux term in
 212     term', !magic_map
 213
 214   let env_of_matched pl tl =
 215     List.map2
 216       (fun p t ->
 217         match p, t with
 218           Pt.Variable (Pt.TermVar name), _ ->
 219             name, (Env.TermType, Env.TermValue t)
 220         | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) ->
 221             name, (Env.NumType, Env.NumValue s)
 222         | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) ->
 223             name, (Env.StringType, Env.StringValue s)
 224         | _ -> assert false)
 225       pl tl
 226
 227   let rec compiler rows =
 228     let rows', magic_maps =
 229       List.split
 230         (List.map
 231           (fun (p, pid) ->
 232             let p', map = extract_magic p in
 233             (p', pid), (pid, map))
 234           rows)
 235     in
 236     let magichecker map =
 237       List.fold_left
 238         (fun f (name, m) ->
 239           let m_checker = compile_magic m in
 240           (fun env ->
 241             match m_checker (Env.lookup_term env name) env with
 242             | None -> None
 243             | Some env' -> f env'))
 244         (fun env -> Some env)
 245         map
 246     in
 247     let magichooser candidates =
 248       List.fold_left
 249         (fun f (pid, pl, checker) ->
 250           (fun matched_terms ->
 251             let env = env_of_matched pl matched_terms in
 252             match checker env with
 253             | None -> f matched_terms
 254             | Some env -> Some (env, pid)))
 255         (fun _ -> None)
 256         candidates
 257     in
 258     let match_cb rows =
 259       let candidates =
 260         List.map
 261           (fun (pl, pid) ->
 262             let magic_map =
 263               try List.assoc pid magic_maps with Not_found -> assert false
 264             in
 265             pid, pl, magichecker magic_map)
 266           rows
 267       in
 268       magichooser candidates
 269     in
 270     M.compiler rows' match_cb (fun _ -> None)
 271
 272   and compile_magic = function
 273     | Pt.Fold (kind, p_base, names, p_rec) ->
 274         let p_rec_decls = Env.declarations_of_term p_rec in
 275         let acc_name = try List.hd names with Failure _ -> assert false in
 276         let compiled = compiler [p_base, 0; p_rec, 1] in
 277         (fun term env ->
 278           let rec aux term =
 279             match compiled term with
 280             | None -> None
 281             | Some (env', 0) -> Some (env', [])
 282             | Some (env', 1) ->
 283                 begin
 284                   let acc = Env.lookup_term env' acc_name in
 285                   let env'' = Env.remove env' acc_name in
 286                   match aux acc with
 287                   | None -> None
 288                   | Some (base_env, rec_envl) ->
 289                       Some (base_env, env'' :: rec_envl )
 290                 end
 291             | _ -> assert false
 292           in
 293             match aux term with
 294             | None -> None
 295             | Some (base_env, rec_envl) ->
 296                 Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
 297     | Pt.Default (p_some, p_none) ->  (* p_none can't bound names *)
 298         let p_some_decls = Env.declarations_of_term p_some in
 299         let none_env = List.map Env.opt_binding_of_name p_some_decls in
 300         let compiled = compiler [p_some, 0] in
 301         (fun term env ->
 302           match compiled term with
 303           | None -> Some none_env
 304           | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
 305           | _ -> assert false)
 306     | _ -> assert false
 307 end
 308
 309 module Matcher32 =
 310 struct
 311   module Pattern32 =
 312   struct
 313     type cic_mask_t =
 314       Blob
 315     | Uri of UriManager.uri
 316     | Appl of cic_mask_t list
 317
 318     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
 319
 320     let mask_of_cic = function
 321       | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl
 322       | Cic.AConst (_, _, [])
 323       | Cic.AVar (_, _, [])
 324       | Cic.AMutInd (_, _, _, [])
 325       | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), []
 326       | _ -> Blob, []
 327
 328     let tag_of_term t =
 329       let mask, tl = mask_of_cic t in
 330       Hashtbl.hash mask, tl
 331
 332     let mask_of_appl_pattern = function
 333       | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), []
 334       | Pt.VarPattern _ -> Blob, []
 335       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 336
 337     let tag_of_pattern p =
 338       let mask, pl = mask_of_appl_pattern p in
 339       Hashtbl.hash mask, pl
 340
 341     type pattern_t = Pt.cic_appl_pattern
 342     type term_t = Cic.annterm
 343
 344     let classify = function
 345       | Pt.VarPattern _ -> Variable
 346       | _ -> Constructor
 347   end
 348
 349   module M = Matcher (Pattern32)
 350
 351   let compiler rows =
 352     let match_cb rows =
 353       let pl, pid = try List.hd rows with Not_found -> assert false in
 354       (fun matched_terms ->
 355         let env =
 356           List.map2
 357             (fun p t ->
 358               match p with
 359               | Pt.VarPattern name -> name, t
 360               | _ -> assert false)
 361             pl matched_terms
 362         in
 363         Some (env, pid))
 364     in
 365     M.compiler rows match_cb (fun () -> None)
 366 end
 367