+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-type pattern_kind = Variable | Constructor
-type tag_t = int
-
-type pattern_id = int
-
-module OrderedInt =
-struct
- type t = int
- let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *)
-end
-
-module IntSet = Set.Make (OrderedInt)
-
-let int_set_of_int_list l =
- List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
-
-module type PATTERN =
-sig
- type pattern_t
- type term_t
- val classify : pattern_t -> pattern_kind
- val tag_of_pattern : pattern_t -> tag_t * pattern_t list
- val tag_of_term : term_t -> tag_t * term_t list
- val string_of_term: term_t -> string
- val string_of_pattern: pattern_t -> string
-end
-
-module Matcher (P: PATTERN) =
-struct
- type row_t = P.pattern_t list * P.pattern_t list * pattern_id
- type t = row_t list
-
- let compatible p1 p2 = P.classify p1 = P.classify p2
-
- let matched = List.map (fun (matched, _, pid) -> matched, pid)
-
- let partition t pidl =
- let partitions = Hashtbl.create 11 in
- let add pid row = Hashtbl.add partitions pid row in
- (try
- List.iter2 add pidl t
- with Invalid_argument _ -> assert false);
- let pidset = int_set_of_int_list pidl in
- IntSet.fold
- (fun pid acc ->
- match Hashtbl.find_all partitions pid with
- | [] -> acc
- | patterns -> (pid, List.rev patterns) :: acc)
- pidset []
-
- let are_empty t =
- match t with
- | (_, [], _) :: _ -> true
- (* if first row has an empty list of patterns, then others have as well *)
- | _ -> false
-
- (* return 2 lists of rows, first one containing homogeneous rows according
- * to "compatible" below *)
- let horizontal_split t =
- let ap, first_row, t', first_row_class =
- match t with
- | [] -> assert false
- | (_, [], _) :: _ ->
- assert false (* are_empty should have been invoked in advance *)
- | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd
- in
- let rec aux prev_t = function
- | [] -> List.rev prev_t, []
- | (_, [], _) :: _ -> assert false
- | ((_, hd :: _, _) as row) :: tl when compatible ap hd ->
- aux (row :: prev_t) tl
- | t -> List.rev prev_t, t
- in
- let rows1, rows2 = aux [first_row] t' in
- first_row_class, rows1, rows2
-
- (* return 2 lists, first one representing first column, second one
- * representing a new pattern matrix where matched patterns have been moved
- * to decl *)
- let vertical_split t =
- List.map
- (function
- | decls, hd :: tl, pid -> hd :: decls, tl, pid
- | _ -> assert false)
- t
-
- let variable_closure ksucc =
- (fun matched_terms constructors terms ->
-(* prerr_endline "variable_closure"; *)
- match terms with
- | hd :: tl -> ksucc (hd :: matched_terms) constructors tl
- | _ -> assert false)
-
- let success_closure ksucc =
- (fun matched_terms constructors terms ->
-(* prerr_endline "success_closure"; *)
- ksucc matched_terms constructors)
-
- let constructor_closure ksuccs =
- (fun matched_terms constructors terms ->
-(* prerr_endline "constructor_closure"; *)
- match terms with
- | t :: tl ->
- (try
- let tag, subterms = P.tag_of_term t in
- let constructors' =
- if subterms = [] then t :: constructors else constructors
- in
- let k' = List.assoc tag ksuccs in
- k' matched_terms constructors' (subterms @ tl)
- with Not_found -> None)
- | [] -> assert false)
-
- let backtrack_closure ksucc kfail =
- (fun matched_terms constructors terms ->
-(* prerr_endline "backtrack_closure"; *)
- match ksucc matched_terms constructors terms with
- | Some x -> Some x
- | None -> kfail matched_terms constructors terms)
-
- let compiler rows match_cb fail_k =
- let rec aux t =
- if t = [] then
- (fun _ _ _ -> fail_k ())
- else if are_empty t then
- success_closure (match_cb (matched t))
- else
- match horizontal_split t with
- | _, [], _ -> assert false
- | Variable, t', [] -> variable_closure (aux (vertical_split t'))
- | Constructor, t', [] ->
- let tagl =
- List.map
- (function
- | _, p :: _, _ -> fst (P.tag_of_pattern p)
- | _ -> assert false)
- t'
- in
- let clusters = partition t' tagl in
- let ksuccs =
- List.map
- (fun (tag, cluster) ->
- let cluster' =
- List.map (* add args as patterns heads *)
- (function
- | matched_p, p :: tl, pid ->
- let _, subpatterns = P.tag_of_pattern p in
- matched_p, subpatterns @ tl, pid
- | _ -> assert false)
- cluster
- in
- tag, aux cluster')
- clusters
- in
- constructor_closure ksuccs
- | _, t', t'' -> backtrack_closure (aux t') (aux t'')
- in
- let t = List.map (fun (p, pid) -> [], [p], pid) rows in
- let matcher = aux t in
- (fun term -> matcher [] [] [term])
-end
-
projects / helm.git / blobdiff