From 38e7f42c1f3eb0da34c25c281f6ba18ef91c970a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 9 Jun 2005 21:12:04 +0000 Subject: [PATCH] test file --- helm/DEVEL/lablgtksourceview/test/test.txt | 373 +++++++++++++++++++++ 1 file changed, 373 insertions(+) create mode 100644 helm/DEVEL/lablgtksourceview/test/test.txt diff --git a/helm/DEVEL/lablgtksourceview/test/test.txt b/helm/DEVEL/lablgtksourceview/test/test.txt new file mode 100644 index 000000000..08a4617f7 --- /dev/null +++ b/helm/DEVEL/lablgtksourceview/test/test.txt @@ -0,0 +1,373 @@ +(* Copyright (C) 2004-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/ + *) + +open Printf + +module Pt = CicNotationPt +module Env = CicNotationEnv +module Util = CicNotationUtil + +type pattern_id = int + +exception No_match + +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 + +type pattern_kind = Variable | Constructor +type tag_t = int + +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 +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 k = + (fun matched_terms terms -> + prerr_endline "variable_closure"; + match terms with + | hd :: tl -> k (hd :: matched_terms) tl + | _ -> assert false) + + let constructor_closure ks k = + (fun matched_terms terms -> + prerr_endline "constructor_closure"; + match terms with + | t :: tl -> + (try + let tag, subterms = P.tag_of_term t in + let k' = List.assoc tag ks in + k' matched_terms (subterms @ tl) + with Not_found -> k matched_terms terms) + | [] -> assert false) + + let compiler rows match_cb fail_k = + let rec aux t k = + if t = [] then + k + else if are_empty t then + let res = match_cb (matched t) in + (fun matched_terms _ -> res matched_terms) + else + match horizontal_split t with + | _, [], _ -> assert false + | Variable, t', [] -> variable_closure (aux (vertical_split t') k) + | 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 ks = + 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' k) + clusters + in + constructor_closure ks k + | _, t', t'' -> aux t' (aux t'' k) + in + let t = List.map (fun (p, pid) -> [], [p], pid) rows in + let matcher = aux t (fun _ _ -> fail_k ()) in + (fun term -> matcher [] [term]) +end + +module Matcher21 = +struct + module Pattern21 = + struct + type pattern_t = Pt.term + type term_t = Pt.term + let classify = function + | Pt.Variable _ -> Variable + | Pt.Magic _ + | Pt.Layout _ + | Pt.Literal _ as t -> + prerr_endline (CicNotationPp.pp_term t); + assert false + | _ -> Constructor + let tag_of_pattern = CicNotationTag.get_tag + let tag_of_term = CicNotationTag.get_tag + end + + module M = Matcher (Pattern21) + + let extract_magic term = + let magic_map = ref [] in + let add_magic m = + let name = Util.fresh_name () in + magic_map := (name, m) :: !magic_map; + Pt.Variable (Pt.TermVar name) + in + let rec aux = function + | Pt.AttributedTerm (_, t) -> aux t + | Pt.Literal _ + | Pt.Layout _ -> assert false + | Pt.Variable v -> Pt.Variable v + | Pt.Magic m -> add_magic m + | t -> Util.visit_ast aux t + in + let term' = aux term in + term', !magic_map + + let env_of_matched pl tl = + List.map2 + (fun p t -> + match p, t with + Pt.Variable (Pt.TermVar name), _ -> + name, (Env.TermType, Env.TermValue t) + | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> + name, (Env.NumType, Env.NumValue s) + | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> + name, (Env.StringType, Env.StringValue s) + | _ -> assert false) + pl tl + + let rec compiler rows = + let rows', magic_maps = + List.split + (List.map + (fun (p, pid) -> + let p', map = extract_magic p in + (p', pid), (pid, map)) + rows) + in + let magichecker map = + List.fold_left + (fun f (name, m) -> + let m_checker = compile_magic m in + (fun env -> + match m_checker (Env.lookup_term env name) env with + | None -> None + | Some env' -> f env')) + (fun env -> Some env) + map + in + let magichooser candidates = + List.fold_left + (fun f (pid, pl, checker) -> + (fun matched_terms -> + let env = env_of_matched pl matched_terms in + match checker env with + | None -> f matched_terms + | Some env -> Some (env, pid))) + (fun _ -> None) + candidates + in + let match_cb rows = + prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); + let candidates = + List.map + (fun (pl, pid) -> + let magic_map = + try List.assoc pid magic_maps with Not_found -> assert false + in + pid, pl, magichecker magic_map) + rows + in + magichooser candidates + in + M.compiler rows' match_cb (fun _ -> None) + + and compile_magic = function + | Pt.Fold (kind, p_base, names, p_rec) -> + let p_rec_decls = Env.declarations_of_term p_rec in + let acc_name = try List.hd names with Failure _ -> assert false in + let compiled = compiler [p_base, 0; p_rec, 1] in + (fun term env -> + let rec aux term = + match compiled term with + | None -> None + | Some (env', 0) -> Some (env', []) + | Some (env', 1) -> + begin + let acc = Env.lookup_term env' acc_name in + let env'' = Env.remove env' acc_name in + match aux acc with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env, env'' :: rec_envl ) + end + | _ -> assert false + in + match aux term with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env @ Env.coalesce_env p_rec_decls rec_envl)) + | Pt.Default (p_some, p_none) -> (* p_none can't bound names *) + let p_some_decls = Env.declarations_of_term p_some in + let none_env = List.map Env.opt_binding_of_name p_some_decls in + let compiled = compiler [p_some, 0] in + (fun term env -> + match compiled term with + | None -> Some none_env + | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) + | _ -> assert false) + | _ -> assert false +end + +module Matcher32 = +struct + module Pattern32 = + struct + type cic_mask_t = + Blob + | Uri of string + | Appl of cic_mask_t list + + let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) + + let mask_of_cic = function + | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl + | Cic.AConst (_, _, []) + | Cic.AVar (_, _, []) + | Cic.AMutInd (_, _, _, []) + | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), [] + | _ -> Blob, [] + + let tag_of_term t = + let mask, tl = mask_of_cic t in + Hashtbl.hash mask, tl + + let mask_of_appl_pattern = function + | Pt.UriPattern s -> Uri s, [] + | Pt.VarPattern _ -> Blob, [] + | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl + + let tag_of_pattern p = + let mask, pl = mask_of_appl_pattern p in + Hashtbl.hash mask, pl + + type pattern_t = Pt.cic_appl_pattern + type term_t = Cic.annterm + + let classify = function + | Pt.VarPattern _ -> Variable + | _ -> Constructor + end + + module M = Matcher (Pattern32) + + let compiler rows = + let match_cb rows = + prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); + let pl, pid = try List.hd rows with Not_found -> assert false in + (fun matched_terms -> + let env = + List.map2 + (fun p t -> + match p with + | Pt.VarPattern name -> name, t + | _ -> assert false) + pl matched_terms + in + Some (env, pid)) + in + M.compiler rows match_cb (fun () -> None) +end + -- 2.39.2