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
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 "@[<v>";
+ (match name with
+ |Some name -> Format.fprintf fmt "Precedence %s:@ " name
+ | None -> ());
+ Format.fprintf fmt "@[<v>";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ if List.for_all is_symbol_dummy x then todo else (
+ Format.fprintf fmt "@[<h> | ";
+ 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 "@[<hov2>";
- 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 "{@[<hov2> ";
- 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 "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
- 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 "{@[<hov2> ";
- 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 "{@[<hov2> ";
- 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 "[@[<hov2> ";
- 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
| 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 "@[<hov2>( ";
- 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 ->
if not (List.memq hd pped) then
begin
let { ename = ename; edesc = desc } = hd in
- Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
+ Format.fprintf fmt "@[<hv 2>%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
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
+;;
projects / helm.git / blobdiff