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       prerr_endline "variable_closure";
 121       match terms with
 122       | hd :: tl -> k (hd :: matched_terms) tl
 123       | _ -> assert false)
 124
 125   let constructor_closure ks k =
 126     (fun matched_terms terms ->
 127       prerr_endline "constructor_closure";
 128       match terms with
 129       | t :: tl ->
 130           (try
 131             let tag, subterms = P.tag_of_term t in
 132             let k' = List.assoc tag ks in
 133             k' matched_terms (subterms @ tl)
 134           with Not_found -> k matched_terms terms)
 135       | [] -> assert false)
 136
 137   let compiler rows match_cb fail_k =
 138     let rec aux t k =
 139       if t = [] then
 140         k
 141       else if are_empty t then
 142         let res = match_cb (matched t) in
 143         (fun matched_terms _ -> res matched_terms)
 144       else
 145         match horizontal_split t with
 146         | _, [], _ -> assert false
 147         | Variable, t', [] -> variable_closure (aux (vertical_split t') k)
 148         | Constructor, t', [] ->
 149             let tagl =
 150               List.map
 151                 (function
 152                   | _, p :: _, _ -> fst (P.tag_of_pattern p)
 153                   | _ -> assert false)
 154                 t'
 155             in
 156             let clusters = partition t' tagl in
 157             let ks =
 158               List.map
 159                 (fun (tag, cluster) ->
 160                   let cluster' =
 161                     List.map  (* add args as patterns heads *)
 162                       (function
 163                         | matched_p, p :: tl, pid ->
 164                             let _, subpatterns = P.tag_of_pattern p in
 165                             matched_p, subpatterns @ tl, pid
 166                         | _ -> assert false)
 167                       cluster
 168                   in
 169                   tag, aux cluster' k)
 170                 clusters
 171             in
 172             constructor_closure ks k
 173         | _, t', t'' -> aux t' (aux t'' k)
 174     in
 175     let t = List.map (fun (p, pid) -> [], [p], pid) rows in
 176     let matcher = aux t (fun _ _ -> fail_k ()) in
 177     (fun term -> matcher [] [term])
 178 end
 179
 180 module Matcher21 =
 181 struct
 182   module Pattern21 =
 183   struct
 184     type pattern_t = Pt.term
 185     type term_t = Pt.term
 186     let classify = function
 187       | Pt.Variable _ -> Variable
 188       | Pt.Magic _
 189       | Pt.Layout _
 190       | Pt.Literal _ as t ->
 191           prerr_endline (CicNotationPp.pp_term t);
 192           assert false
 193       | _ -> Constructor
 194     let tag_of_pattern = CicNotationTag.get_tag
 195     let tag_of_term = CicNotationTag.get_tag
 196   end
 197
 198   module M = Matcher (Pattern21)
 199
 200   let extract_magic term =
 201     let magic_map = ref [] in
 202     let add_magic m =
 203       let name = Util.fresh_name () in
 204       magic_map := (name, m) :: !magic_map;
 205       Pt.Variable (Pt.TermVar name)
 206     in
 207     let rec aux = function
 208       | Pt.AttributedTerm (_, t) -> aux t
 209       | Pt.Literal _
 210       | Pt.Layout _ -> assert false
 211       | Pt.Variable v -> Pt.Variable v
 212       | Pt.Magic m -> add_magic m
 213       | t -> Util.visit_ast aux t
 214     in
 215     let term' = aux term in
 216     term', !magic_map
 217
 218   let env_of_matched pl tl =
 219     List.map2
 220       (fun p t ->
 221         match p, t with
 222           Pt.Variable (Pt.TermVar name), _ ->
 223             name, (Env.TermType, Env.TermValue t)
 224         | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) ->
 225             name, (Env.NumType, Env.NumValue s)
 226         | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) ->
 227             name, (Env.StringType, Env.StringValue s)
 228         | _ -> assert false)
 229       pl tl
 230
 231   let rec compiler rows =
 232     let rows', magic_maps =
 233       List.split
 234         (List.map
 235           (fun (p, pid) ->
 236             let p', map = extract_magic p in
 237             (p', pid), (pid, map))
 238           rows)
 239     in
 240     let magichecker map =
 241       List.fold_left
 242         (fun f (name, m) ->
 243           let m_checker = compile_magic m in
 244           (fun env ->
 245             match m_checker (Env.lookup_term env name) env with
 246             | None -> None
 247             | Some env' -> f env'))
 248         (fun env -> Some env)
 249         map
 250     in
 251     let magichooser candidates =
 252       List.fold_left
 253         (fun f (pid, pl, checker) ->
 254           (fun matched_terms ->
 255             let env = env_of_matched pl matched_terms in
 256             match checker env with
 257             | None -> f matched_terms
 258             | Some env -> Some (env, pid)))
 259         (fun _ -> None)
 260         candidates
 261     in
 262     let match_cb rows =
 263       prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
 264       let candidates =
 265         List.map
 266           (fun (pl, pid) ->
 267             let magic_map =
 268               try List.assoc pid magic_maps with Not_found -> assert false
 269             in
 270             pid, pl, magichecker magic_map)
 271           rows
 272       in
 273       magichooser candidates
 274     in
 275     M.compiler rows' match_cb (fun _ -> None)
 276
 277   and compile_magic = function
 278     | Pt.Fold (kind, p_base, names, p_rec) ->
 279         let p_rec_decls = Env.declarations_of_term p_rec in
 280         let acc_name = try List.hd names with Failure _ -> assert false in
 281         let compiled = compiler [p_base, 0; p_rec, 1] in
 282         (fun term env ->
 283           let rec aux term =
 284             match compiled term with
 285             | None -> None
 286             | Some (env', 0) -> Some (env', [])
 287             | Some (env', 1) ->
 288                 begin
 289                   let acc = Env.lookup_term env' acc_name in
 290                   let env'' = Env.remove env' acc_name in
 291                   match aux acc with
 292                   | None -> None
 293                   | Some (base_env, rec_envl) ->
 294                       Some (base_env, env'' :: rec_envl )
 295                 end
 296             | _ -> assert false
 297           in
 298             match aux term with
 299             | None -> None
 300             | Some (base_env, rec_envl) ->
 301                 Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
 302     | Pt.Default (p_some, p_none) ->  (* p_none can't bound names *)
 303         let p_some_decls = Env.declarations_of_term p_some in
 304         let none_env = List.map Env.opt_binding_of_name p_some_decls in
 305         let compiled = compiler [p_some, 0] in
 306         (fun term env ->
 307           match compiled term with
 308           | None -> Some none_env
 309           | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env)
 310           | _ -> assert false)
 311     | _ -> assert false
 312 end
 313
 314 module Matcher32 =
 315 struct
 316   module Pattern32 =
 317   struct
 318     type cic_mask_t =
 319       Blob
 320     | Uri of string
 321     | Appl of cic_mask_t list
 322
 323     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
 324
 325     let mask_of_cic = function
 326       | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl
 327       | Cic.AConst (_, _, [])
 328       | Cic.AVar (_, _, [])
 329       | Cic.AMutInd (_, _, _, [])
 330       | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), []
 331       | _ -> Blob, []
 332
 333     let tag_of_term t =
 334       let mask, tl = mask_of_cic t in
 335       Hashtbl.hash mask, tl
 336
 337     let mask_of_appl_pattern = function
 338       | Pt.UriPattern s -> Uri s, []
 339       | Pt.VarPattern _ -> Blob, []
 340       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 341
 342     let tag_of_pattern p =
 343       let mask, pl = mask_of_appl_pattern p in
 344       Hashtbl.hash mask, pl
 345
 346     type pattern_t = Pt.cic_appl_pattern
 347     type term_t = Cic.annterm
 348
 349     let classify = function
 350       | Pt.VarPattern _ -> Variable
 351       | _ -> Constructor
 352   end
 353
 354   module M = Matcher (Pattern32)
 355
 356   let compiler rows =
 357     let match_cb rows =
 358       prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
 359       let pl, pid = try List.hd rows with Not_found -> assert false in
 360       (fun matched_terms ->
 361         let env =
 362           List.map2
 363             (fun p t ->
 364               match p with
 365               | Pt.VarPattern name -> name, t
 366               | _ -> assert false)
 367             pl matched_terms
 368         in
 369         Some (env, pid))
 370     in
 371     M.compiler rows match_cb (fun () -> None)
 372 end
 373