From: Enrico Tassi Date: Tue, 15 Nov 2005 11:12:31 +0000 (+0000) Subject: added print_grammar X-Git-Tag: V_0_7_2_3~81 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3059c9a2b5e06003080c6294bd5ea6687ba80ca1 added print_grammar --- diff --git a/helm/ocaml/cic_notation/.cvsignore b/helm/ocaml/cic_notation/.cvsignore index 36ef68a9e..45ec2c22f 100644 --- a/helm/ocaml/cic_notation/.cvsignore +++ b/helm/ocaml/cic_notation/.cvsignore @@ -4,3 +4,4 @@ test_lexer test_parser test_dep +print_grammar diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 65251b820..cfd1ad505 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -33,7 +33,7 @@ IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(NULL) -all: test_lexer test_parser test_dep +all: test_lexer test_parser test_dep print_grammar LOCAL_LINKOPTS = -package helm-cic_notation -linkpkg test: test_lexer test_parser test_dep @@ -44,7 +44,8 @@ test_parser: test_parser.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< test_dep: test_dep.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< - +print_grammar: print_grammar.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) diff --git a/helm/ocaml/cic_notation/grafiteParser.mli b/helm/ocaml/cic_notation/grafiteParser.mli index 5cd6c2622..fa732218f 100644 --- a/helm/ocaml/cic_notation/grafiteParser.mli +++ b/helm/ocaml/cic_notation/grafiteParser.mli @@ -32,4 +32,6 @@ val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) (** @raise End_of_file *) val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list - + +val statement: statement Grammar.Entry.e + diff --git a/helm/ocaml/cic_notation/print_grammar.ml b/helm/ocaml/cic_notation/print_grammar.ml new file mode 100644 index 000000000..99ab9ad62 --- /dev/null +++ b/helm/ocaml/cic_notation/print_grammar.ml @@ -0,0 +1,273 @@ +(* 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/ + *) + +open Gramext + +let tex_of_unicode s = + let no_expansion = ["|";",";"(";")";"[";"]";":";"_";".";"=";";";"{";"}"] in + let contractions = + ("\\Longrightarrow","=>") :: [] + in + if List.exists ((=) s) no_expansion then s + else + let s = Utf8Macro.tex_of_unicode s in + try List.assoc s contractions with Not_found -> s + +let visit_description desc fmt = + let skip s = List.mem s [ ] in + let inline s = List.mem s [ "int" ] in + + let rec visit_entry e todo is_son nesting = + let { ename = ename; edesc = desc } = e in + if inline ename then + visit_desc desc todo is_son nesting + else + begin + Format.fprintf fmt "%s " ename; + if skip ename then + todo + else + todo @ [e] + end + + and visit_desc d todo is_son nesting = + match d with + | Dlevels [] -> todo + | Dlevels [lev] -> visit_level lev todo is_son nesting + | Dlevels (lev::levels) -> + let todo = visit_level lev todo is_son nesting in + List.fold_left + (fun acc l -> + Format.fprintf fmt "@ | "; + visit_level l acc is_son nesting) + todo levels; + | _ -> todo + + and visit_level l todo is_son nesting = + let { lsuffix = suff ; lprefix = pref } = l in + let todo = visit_tree suff todo is_son nesting in + visit_tree pref todo is_son nesting + + and visit_tree t todo is_son nesting = + match t with + | Node node -> visit_node node todo is_son nesting + | _ -> todo + + and visit_node n todo is_son nesting = + let is_tree_printable t = + match t with + | Node _ -> true + | _ -> false + in + let needs_brackets t = + let rec count_brothers = function + | Node {brother = brother} -> 1 + count_brothers brother + | _ -> 0 + in + count_brothers t > 1 + in + let { node = symbol; son = son ; brother = brother } = n in + let todo = visit_symbol symbol todo is_son nesting in + let todo = + if is_tree_printable son then + begin + let need_b = needs_brackets son in + if not is_son then + Format.fprintf fmt "@["; + if need_b then + Format.fprintf fmt "( "; + let todo = visit_tree son todo true nesting in + if need_b then + Format.fprintf fmt ")"; + if not is_son then + Format.fprintf fmt "@]"; + todo + end + else + todo + in + if is_tree_printable brother then + begin + Format.fprintf fmt "@ | "; + visit_tree brother todo is_son nesting + end + else + todo + + and visit_symbol s todo is_son nesting = + match s with + | Smeta (name, sl, _) -> + Format.fprintf fmt "%s " name; + List.fold_left ( + fun acc s -> + let todo = visit_symbol s acc is_son nesting in + if is_son then + Format.fprintf fmt "@ "; + todo) + todo sl + | Snterm entry -> visit_entry entry todo is_son nesting + | Snterml (entry,_) -> visit_entry entry todo is_son nesting + | Slist0 symbol -> + Format.fprintf fmt "@[{ "; + let todo = visit_symbol symbol todo is_son (nesting+1) in + Format.fprintf fmt "}@] @ "; + todo + | Slist0sep (symbol,sep) -> + Format.fprintf fmt "@[[ "; + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "@[{ "; + let todo = visit_symbol sep todo is_son (nesting + 2) in + Format.fprintf fmt " "; + let todo = visit_symbol symbol todo is_son (nesting + 2) in + Format.fprintf fmt "}@] @ ]@] @ "; + todo + | Slist1 symbol -> + Format.fprintf fmt "@[{ "; + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "}+@] @ "; + todo + | Slist1sep (symbol,sep) -> + let todo = visit_symbol symbol todo is_son nesting in + Format.fprintf fmt " @[{ "; + let todo = visit_symbol sep todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "}@] @ "; + todo + | Sopt symbol -> + Format.fprintf fmt "@[[ "; + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "]@] @ "; + todo + | Sself -> Format.fprintf fmt "self "; todo + | Snext -> Format.fprintf fmt "next "; todo + | Stoken pattern -> + let constructor, keyword = pattern in + if keyword = "" then + Format.fprintf fmt "'%s' " constructor + else + Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword); + todo + | Stree tree -> visit_tree tree todo is_son nesting + in + visit_desc desc [] false 0 +;; + +let rec clean_dummy_desc = function + | Dlevels l -> Dlevels (clean_levels l) + | x -> x + +and clean_levels = function + | [] -> [] + | l :: tl -> clean_level l @ clean_levels tl + +and clean_level = function + | x -> + let pref = clean_tree x.lprefix in + let suff = clean_tree x.lsuffix in + match pref,suff with + | DeadEnd, DeadEnd -> [] + | _ -> [{x with lprefix = pref; lsuffix = suff}] + +and clean_tree = function + | Node n -> clean_node n + | x -> x + +and clean_node = function + | {node=node;son=son;brother=brother} when + is_symbol_dummy node && + is_tree_dummy son && + is_tree_dummy brother -> DeadEnd + | x -> Node x + +and is_level_dummy = function + | {lsuffix=lsuffix;lprefix=lprefix} -> + is_tree_dummy lsuffix && is_tree_dummy lprefix + +and is_desc_dummy = function + | Dlevels l -> List.for_all is_level_dummy l + | Dparser _ -> true + +and is_entry_dummy = function + | {edesc=edesc} -> is_desc_dummy edesc + +and is_symbol_dummy = function + | Stoken ("DUMMY", _) -> true + | Stoken _ -> false + | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt + | Snterm e | Snterml (e, _) -> is_entry_dummy e + | Slist1 x | Slist0 x -> is_symbol_dummy x + | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y + | Sopt x -> is_symbol_dummy x + | Sself -> false + | Snext -> true + | Stree t -> is_tree_dummy t + +and is_tree_dummy = function + | Node {node=node} -> is_symbol_dummy node + | _ -> true +;; + + +let rec visit_entries todo pped = + let fmt = Format.std_formatter in + match todo with + | [] -> () + | hd :: tl -> + let todo = + if not (List.memq hd pped) then + begin + let { ename = ename; edesc = desc } = hd in + Format.fprintf fmt "@[%s ::=@ " ename; + let desc = clean_dummy_desc desc in + let todo = visit_description desc fmt @ todo in + Format.fprintf fmt "@]"; + Format.pp_print_newline fmt (); + Format.pp_print_newline fmt (); + todo + end + else + todo + in + let clean_todo todo = + let name_of_entry e = e.ename in + let pped = hd :: pped in + let todo = tl @ todo in + let todo = List.filter (fun e -> not(List.memq e pped)) todo in + HExtlib.list_uniq + ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2)) + (List.sort + (fun e1 e2 -> + Pervasives.compare (name_of_entry e1) (name_of_entry e2)) + todo), + pped + in + let todo,pped = clean_todo todo in + visit_entries todo pped +;; + +let _ = +(* let g_entry = Grammar.Entry.obj CicNotationParser.term in*) + let g_entry = Grammar.Entry.obj GrafiteParser.statement in + visit_entries [g_entry] []