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 module type PATTERN =
  48   sig
  49   type pattern_t
  50   val compatible : pattern_t -> pattern_t -> bool
  51   end
  52
  53 module Patterns (P: PATTERN) =
  54   struct
  55   type row_t = P.pattern_t list * P.pattern_t list * pattern_id
  56   type t = row_t list
  57
  58   let empty = []
  59
  60   let matched = List.map (fun (matched, _, pid) -> matched, pid)
  61
  62   let partition t pidl =
  63     let partitions = Hashtbl.create 11 in
  64     let add pid row = Hashtbl.add partitions pid row in
  65     (try
  66       List.iter2 add pidl t
  67     with Invalid_argument _ -> assert false);
  68     let pidset = int_set_of_int_list pidl in
  69     IntSet.fold
  70       (fun pid acc ->
  71         match Hashtbl.find_all partitions pid with
  72         | [] -> acc
  73         | patterns -> (pid, List.rev patterns) :: acc)
  74       pidset []
  75
  76   let are_empty t =
  77     match t with
  78     | (_, [], _) :: _ -> true
  79       (* if first row has an empty list of patterns, then others have as well *)
  80     | _ -> false
  81
  82     (* return 2 lists of rows, first one containing homogeneous rows according
  83      * to "compatible" below *)
  84   let horizontal_split t =
  85     let ap, first_row, t' =
  86       match t with
  87       | [] -> assert false
  88       | (_, [], _) :: _ ->
  89           assert false  (* are_empty should have been invoked in advance *)
  90       | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl
  91     in
  92     let rec aux prev_t = function
  93       | [] -> List.rev prev_t, []
  94       | (_, [], _) :: _ -> assert false
  95       | ((_, hd :: _, _) as row) :: tl when P.compatible ap hd ->
  96           aux (row :: prev_t) tl
  97       | t -> List.rev prev_t, t
  98     in
  99     aux [first_row] t'
 100
 101     (* return 2 lists, first one representing first column, second one
 102      * representing a new pattern matrix where matched patterns have been moved
 103      * to decl *)
 104   let vertical_split t =
 105     List.map
 106       (function
 107         | decls, hd :: tl, pid -> hd :: decls, tl, pid
 108         | _ -> assert false)
 109       t
 110   end
 111
 112 module T21 =
 113 struct
 114
 115 module P = Patterns (CicNotationTag)
 116
 117 (* let return_closure matched =
 118   (fun matched_terms terms ->
 119     prerr_endline "T21.return_closure";
 120     match terms with
 121     | [] -> matched_terms, matched
 122     | _ -> assert false) *)
 123
 124 let variable_closure k =
 125   (fun matched_terms terms ->
 126     prerr_endline "T21.variable_closure";
 127     match terms with
 128     | hd :: tl ->
 129         prerr_endline (sprintf "binding: %s" (CicNotationPp.pp_term hd));
 130         k (hd :: matched_terms) tl
 131     | _ -> assert false)
 132
 133 let constructor_closure ks k =
 134   (fun matched_terms terms ->
 135     prerr_endline "T21.constructor_closure";
 136     match terms with
 137     | t :: tl ->
 138         prerr_endline (sprintf "on term %s" (CicNotationPp.pp_term t));
 139         (try
 140           let tag, subterms = CicNotationTag.get_tag t in
 141           let k' = List.assoc tag ks in
 142           k' matched_terms (subterms @ tl)
 143         with Not_found -> k matched_terms terms)
 144     | [] -> assert false)
 145
 146 (* let fold_closure kind p_names names matcher success_k k =
 147   let acc_name = try List.hd names with Failure _ -> assert false in
 148 |+   List.iter (fun (name, _) -> Printf.printf "/// %s\n" name) p_names ; +|
 149   (fun matched_terms terms ->
 150     prerr_endline "T21.fold_closure";
 151     (match terms with
 152     | t :: tl ->
 153         let rec aux t =
 154           prerr_endline "PORCA TORCIA SONO IN AUX" ;
 155           match matcher t with
 156           | _, [] -> None
 157           | matched_terms, [matched_p, 0] -> Some (matched_terms, [])
 158           | matched_terms, [matched_p, 1] ->
 159               let acc = CicNotationEnv.lookup_term env acc_name in
 160               let env = CicNotationEnv.remove env acc_name in
 161               (match aux acc with
 162               | None -> None
 163               | Some env' -> Some (env :: env'))
 164           | envl ->
 165               List.iter
 166                 (fun (env, pid) ->
 167                    Printf.printf "*** %s %d\n" (CicNotationPp.pp_env env) pid)
 168                 envl ;
 169               flush stdout ;
 170               assert false |+ overlapping patterns, to be handled ... +|
 171         in
 172         (match aux t with
 173         | None -> k terms envl
 174         | Some env ->
 175             let magic_env = CicNotationEnv.coalesce_env p_names env in
 176             List.map (fun (env, pid) -> magic_env @ env, pid) envl)
 177     | [] -> assert false)) *)
 178
 179 let compiler0 rows match_cb fail_k =
 180   let rec aux t k =
 181     if t = [] then
 182       k
 183     else if P.are_empty t then
 184       match_cb (P.matched t)
 185     else
 186       match P.horizontal_split t with
 187       | t', [] ->
 188           (match t' with
 189           | []
 190           | (_, [], _) :: _ -> assert false
 191           | (_, Pt.Variable _ :: _, _) :: _ ->
 192               variable_closure (aux (P.vertical_split t') k)
 193           | _ ->
 194               let tagl =
 195                 List.map
 196                   (function
 197                     | _, p :: _, _ -> fst (CicNotationTag.get_tag p)
 198                     | _ -> assert false)
 199                   t'
 200               in
 201               let clusters = P.partition t' tagl in
 202               let ks =
 203                 List.map
 204                   (fun (tag, cluster) ->
 205                     let cluster' =
 206                       List.map  (* add args as patterns heads *)
 207                         (function
 208                           | matched_p, p :: tl, pid ->
 209                               let _, subpatterns = CicNotationTag.get_tag p in
 210                               matched_p, subpatterns @ tl, pid
 211                           | _ -> assert false)
 212                         cluster
 213                     in
 214                     tag, aux cluster' k)
 215                   clusters
 216               in
 217               constructor_closure ks k)
 218       | t', tl -> aux t' (aux tl k)
 219   in
 220   let t = List.map (fun (p, pid) -> [], [p], pid) rows in
 221   let matcher = aux t (fun _ _ -> fail_k ()) in
 222   (fun term -> matcher [] [term])
 223
 224 let extract_magic term =
 225   let magic_map = ref [] in
 226   let add_magic m =
 227     let name = Util.fresh_name () in
 228     magic_map := (name, m) :: !magic_map;
 229     Pt.Variable (Pt.TermVar name)
 230   in
 231   let rec aux = function
 232     | Pt.AttributedTerm (_, t) -> aux t
 233     | Pt.Literal _
 234     | Pt.Layout _ -> assert false
 235     | Pt.Variable v -> Pt.Variable v
 236     | Pt.Magic m -> add_magic m
 237     | t -> Util.visit_ast aux t
 238   in
 239   let term' = aux term in
 240   term', !magic_map
 241
 242 let env_of_matched pl tl =
 243   List.map2
 244     (fun p t ->
 245       match p, t with
 246         Pt.Variable (Pt.TermVar name), _ ->
 247           name, (Env.TermType, Env.TermValue t)
 248       | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) ->
 249           name, (Env.NumType, Env.NumValue s)
 250       | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) ->
 251           name, (Env.StringType, Env.StringValue s)
 252       | _ -> assert false)
 253     pl tl
 254
 255 let decls_of_pattern p =
 256   List.map Env.declaration_of_var (Util.variables_of_term p)
 257
 258 let rec compiler rows =
 259   let rows', magic_maps =
 260     List.split
 261       (List.map
 262         (fun (p, pid) ->
 263           let p', map = extract_magic p in
 264           (p', pid), (pid, map))
 265         rows)
 266   in
 267   let magichecker map =
 268     List.fold_left
 269       (fun f (name, m) ->
 270         let m_checker = compile_magic m in
 271         (fun env ->
 272           match m_checker (Env.lookup_term env name) env with
 273           | None -> None
 274           | Some env' -> f env'))
 275       (fun env -> Some env)
 276       map
 277   in
 278   let magichooser candidates =
 279     List.fold_left
 280       (fun f (pid, pl, checker) ->
 281         (fun matched_terms ->
 282           let env = env_of_matched pl matched_terms in
 283           match checker env with
 284           | None -> f matched_terms
 285           | Some env -> Some (env, pid)))
 286       (fun _ -> None)
 287       candidates
 288   in
 289   let match_cb rows =
 290     prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
 291     let candidates =
 292       List.map
 293         (fun (pl, pid) ->
 294           let magic_map =
 295             try List.assoc pid magic_maps with Not_found -> assert false
 296           in
 297           pid, pl, magichecker magic_map)
 298         rows
 299     in
 300     (fun matched_terms _ -> magichooser candidates matched_terms)
 301   in
 302   compiler0 rows match_cb (fun _ -> None)
 303
 304 and compile_magic = function
 305   | Pt.Fold (kind, p_base, names, p_rec) ->
 306       let p_rec_decls = decls_of_pattern p_rec in
 307       let acc_name = try List.hd names with Failure _ -> assert false in
 308       let t_magic = [p_base, 0; p_rec, 1] in
 309       let compiled = compiler t_magic in
 310       (fun term env ->
 311         let rec aux term =
 312           match compiled term with
 313           | None -> None
 314           | Some (env', 0) -> Some (env', [])
 315           | Some (env', 1) ->
 316               begin
 317                 let acc = Env.lookup_term env' acc_name in
 318                 let env'' = Env.remove env' acc_name in
 319                 match aux acc with
 320                 | None -> None
 321                 | Some (base_env, rec_envl) ->
 322                     Some (base_env, env'' :: rec_envl )
 323               end
 324           | _ -> assert false
 325         in
 326           match aux term with
 327           | None -> None
 328           | Some (base_env, rec_envl) ->
 329               Some (base_env @ Env.coalesce_env p_rec_decls rec_envl))
 330   | _ -> assert false
 331
 332 end
 333