From: Stefano Zacchiroli Date: Thu, 23 Feb 2006 21:33:34 +0000 (+0000) Subject: Added module GrafiteWalker, which implements traversals (recursive and not) over X-Git-Tag: make_still_working~7528 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f462045c431db02d49ca3920bc8039974370d009;p=helm.git Added module GrafiteWalker, which implements traversals (recursive and not) over grafite scripts. Useful for grep/sed like operations over a bunch of scripts. --- diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index 360429635..2dc8a7cab 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -1,3 +1,4 @@ +grafiteWalker.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: dependenciesParser.cmi grafiteParser.cmi @@ -8,3 +9,5 @@ grafiteDisambiguator.cmo: grafiteDisambiguator.cmi grafiteDisambiguator.cmx: grafiteDisambiguator.cmi grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi +grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi +grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi diff --git a/helm/software/components/grafite_parser/Makefile b/helm/software/components/grafite_parser/Makefile index 8482825a6..434eaceaa 100644 --- a/helm/software/components/grafite_parser/Makefile +++ b/helm/software/components/grafite_parser/Makefile @@ -1,12 +1,13 @@ PACKAGE = grafite_parser PREDICATES = -INTERFACE_FILES = \ - dependenciesParser.mli \ - grafiteParser.mli \ - cicNotation2.mli \ - grafiteDisambiguator.mli \ - grafiteDisambiguate.mli \ +INTERFACE_FILES = \ + dependenciesParser.mli \ + grafiteParser.mli \ + cicNotation2.mli \ + grafiteDisambiguator.mli \ + grafiteDisambiguate.mli \ + grafiteWalker.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/grafite_parser/grafiteWalker.ml b/helm/software/components/grafite_parser/grafiteWalker.ml new file mode 100644 index 000000000..eb2eb22a5 --- /dev/null +++ b/helm/software/components/grafite_parser/grafiteWalker.ml @@ -0,0 +1,76 @@ +(* Copyright (C) 2006, 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/ + *) + +type statement_test = + GrafiteParser.ast_statement GrafiteParser.localized_option -> bool + +let get_loc = + function + | GrafiteParser.LSome (GrafiteAst.Executable (loc, _)) + | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) + | GrafiteParser.LNone loc -> + loc + +let grep_statement ?(status = LexiconEngine.initial_status) ?(callback = ignore) + ~fname test += + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + let content = HExtlib.input_file fname in + let lexbuf = Ulexing.from_utf8_string content in + let parse_fun status = + GrafiteParser.parse_statement lexbuf ~include_paths status in + let rec exaust acc status = (* extract "interesting" statement locations *) + let stm = + try Some (parse_fun status) + with End_of_file -> None in + match stm with + | None -> List.rev acc + | Some (status, stm) when test stm -> (* "interesting" statement *) + let loc_begin, loc_end = HExtlib.loc_of_floc (get_loc stm) in + let raw_statement = + String.sub content loc_begin (loc_end - loc_begin) in + callback raw_statement; + exaust (raw_statement :: acc) status + | Some (status, _stm) -> exaust acc status in + exaust [] status + +let ma_extension_test fname = Filename.check_suffix fname ".ma" + +let rgrep_statement ?status ?callback ?(fname_test = ma_extension_test) + ~dirname test += + let files = HExtlib.find ~test:fname_test dirname in + List.flatten + (List.map + (fun fname -> + let callback = + match callback with + | None -> None + | Some f -> Some (fun s -> f (fname, s)) in + List.map (fun raw -> fname, raw) + (grep_statement ?status ?callback ~fname test)) + files) + diff --git a/helm/software/components/grafite_parser/grafiteWalker.mli b/helm/software/components/grafite_parser/grafiteWalker.mli new file mode 100644 index 000000000..b4ca6f0d7 --- /dev/null +++ b/helm/software/components/grafite_parser/grafiteWalker.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2006, 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/ + *) + +type statement_test = + GrafiteParser.ast_statement GrafiteParser.localized_option -> bool + + (** @param status initial status, defaults to LexiconEngine.initial_status + * @param callback if given it will be invoked as soon as a matching + * statement is found (i.e. it provides incremental notification in case + * grepping takes a while) *) +val grep_statement: + ?status: LexiconEngine.status -> + ?callback: (string -> unit) -> + fname:string -> statement_test -> + string list + + (** As above, but act on all file (recursively) located under directory + * dirname whose name matches fname_test. Default test matches files with + * extension ".ma". + * @return list of pairs , as "grep -H" would do *) +val rgrep_statement: + ?status: LexiconEngine.status -> + ?callback: (string * string -> unit) -> + ?fname_test:(string -> bool) -> dirname:string -> statement_test -> + (string * string) list +