X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2Fprint_grammar.ml;h=47f42356f4854e8f2f08242a9f8d7ec7fb4f3115;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=6a05865de8f2c9149b6e6a6c6e7ca4b274afd315;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml index 6a05865de..47f42356f 100644 --- a/helm/software/components/grafite_parser/print_grammar.ml +++ b/helm/software/components/grafite_parser/print_grammar.ml @@ -27,12 +27,75 @@ open Gramext -let tex_of_unicode s = - let contractions = ("\\Longrightarrow","=>") :: [] in - if String.length s <= 1 then s - else (* probably an extended unicode symbol *) - let s = Utf8Macro.tex_of_unicode s in - try List.assoc s contractions with Not_found -> s +let rec flatten_tree = function + | DeadEnd -> [] + | LocAct _ -> [[]] + | Node {node = n; brother = b; son = s} -> + List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b + +let tex_of_unicode s = s + +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} -> + let bn = is_symbol_dummy node in + let bs = is_tree_dummy son in + let bb = is_tree_dummy brother in + let son = if bs then DeadEnd else son in + let brother = if bb then DeadEnd else brother in + if bb && bs && bn then + DeadEnd + else + if bn then + Node {node=Sself;son=son;brother=brother} + else + Node {node=node;son=son;brother=brother} + +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,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y + | Sopt x -> is_symbol_dummy x + | Sself | Snext -> false + | Stree t -> is_tree_dummy t + | _ -> assert false + +and is_tree_dummy = function + | Node {node=node} -> is_symbol_dummy node + | _ -> true let needs_brackets t = let rec count_brothers = function @@ -42,121 +105,111 @@ let needs_brackets t = count_brothers t > 1 let visit_description desc fmt self = - let skip s = List.mem s [ ] in + let skip s = true in let inline s = List.mem s [ "int" ] in - let rec visit_entry e todo is_son nesting = + let rec visit_entry e ?level todo is_son = let { ename = ename; edesc = desc } = e in if inline ename then - visit_desc desc todo is_son nesting + visit_desc desc todo is_son else begin - Format.fprintf fmt "%s " ename; - if skip ename then - todo - else - todo @ [e] + (match level with + | None -> Format.fprintf fmt "%s " ename; + | Some _ -> Format.fprintf fmt "%s " ename;); + if skip ename then + todo + else + todo @ [e] end - and visit_desc d todo is_son nesting = + and visit_desc d todo is_son = 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 + | Dlevels l -> 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 + (fun acc l -> + Format.fprintf fmt "@ "; + visit_level l acc is_son ) + todo l; + | Dparser _ -> todo - and visit_tree t todo is_son nesting = - match t with - | Node node -> visit_node node todo is_son nesting - | _ -> todo + and visit_level l todo is_son = + let { lname = name ; lsuffix = suff ; lprefix = pref } = l in + visit_tree name + (List.map + (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref) + todo is_son - and visit_node n todo is_son nesting = - let is_tree_printable t = - match t with - | Node _ -> true - | _ -> false + and visit_tree name t todo is_son = + if List.for_all (List.for_all is_symbol_dummy) t then todo else ( + Format.fprintf fmt "@["; + (match name with + |Some name -> Format.fprintf fmt "Precedence %s:@ " name + | None -> ()); + Format.fprintf fmt "@["; + let todo = + List.fold_left + (fun acc x -> + if List.for_all is_symbol_dummy x then todo else ( + Format.fprintf fmt "@[ | "; + let todo = + List.fold_left + (fun acc x -> + let todo = visit_symbol x acc true in + Format.fprintf fmt "@ "; + todo) + acc x + in + Format.fprintf fmt "@]@ "; + todo)) + todo t 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 + Format.fprintf fmt "@]"; + Format.fprintf fmt "@]"; + todo) - and visit_symbol s todo is_son nesting = + and visit_symbol s todo is_son = 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 + let todo = visit_symbol s acc is_son 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 + | Snterm entry -> visit_entry entry todo is_son + | Snterml (entry,level) -> visit_entry entry ~level todo is_son | Slist0 symbol -> Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son (nesting+1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo - | Slist0sep (symbol,sep) -> + | Slist0sep (symbol,sep,false) -> Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son (nesting + 2) in + let todo = visit_symbol sep todo is_son in Format.fprintf fmt " "; - let todo = visit_symbol symbol todo is_son (nesting + 2) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @]] @ "; todo | Slist1 symbol -> Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]}+ @ "; todo - | Slist1sep (symbol,sep) -> - let todo = visit_symbol symbol todo is_son nesting in + | Slist1sep (symbol,sep,false) -> + let todo = visit_symbol symbol todo is_son 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 + let todo = visit_symbol sep todo is_son in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo | Sopt symbol -> Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]] @ "; todo | Sself -> Format.fprintf fmt "%s " self; todo @@ -164,89 +217,20 @@ let visit_description desc fmt self = | Stoken pattern -> let constructor, keyword = pattern in if keyword = "" then - Format.fprintf fmt "`%s' " constructor + (if constructor <> "DUMMY" then + Format.fprintf fmt "`%s' " constructor) else - Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword); + Format.fprintf fmt "%s " (tex_of_unicode keyword); todo | Stree tree -> - if needs_brackets tree then - begin - Format.fprintf fmt "@[( "; - let todo = visit_tree tree todo is_son (nesting + 1) in - Format.fprintf fmt ")@] @ "; - todo - end - else - visit_tree tree todo is_son (nesting + 1) + visit_tree None (flatten_tree tree) todo is_son + | _ -> assert false in - visit_desc desc [] false 0 + visit_desc desc [] false ;; -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} -> - let bn = is_symbol_dummy node in - let bs = is_tree_dummy son in - let bb = is_tree_dummy brother in - let son = if bs then DeadEnd else son in - let brother = if bb then DeadEnd else brother in - if bb && bs && bn then - DeadEnd - else - if bn then - Node {node=Sself;son=son;brother=brother} - else - Node {node=node;son=son;brother=brother} - -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 | Snext -> false - | 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 +let rec visit_entries fmt todo pped = match todo with | [] -> () | hd :: tl -> @@ -254,12 +238,10 @@ let rec visit_entries todo pped = if not (List.memq hd pped) then begin let { ename = ename; edesc = desc } = hd in - Format.fprintf fmt "@[%s ::=@ " ename; + Format.fprintf fmt "@[%s ::= " ename; let desc = clean_dummy_desc desc in let todo = visit_description desc fmt ename @ todo in - Format.fprintf fmt "@]"; - Format.pp_print_newline fmt (); - Format.pp_print_newline fmt (); + Format.fprintf fmt "@]\n\n"; todo end else @@ -279,9 +261,15 @@ let rec visit_entries todo pped = pped in let todo,pped = clean_todo todo in - visit_entries todo pped + visit_entries fmt todo pped ;; -let _ = - let g_entry = Grammar.Entry.obj GrafiteParser.statement in - visit_entries [g_entry] [] +let ebnf_of_term () = + let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in + let buff = Buffer.create 100 in + let fmt = Format.formatter_of_buffer buff in + visit_entries fmt [g_entry] []; + Format.fprintf fmt "@?"; + let s = Buffer.contents buff in + s +;;