X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fprint_grammar.ml;h=d7d6f3c965e126eb825dee1ac3d93acd6a7907d5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=99ab9ad62e658767ecf7e155c121f0891fcf92e8;hpb=3059c9a2b5e06003080c6294bd5ea6687ba80ca1;p=helm.git

diff --git a/helm/ocaml/cic_notation/print_grammar.ml b/helm/ocaml/cic_notation/print_grammar.ml
index 99ab9ad62..d7d6f3c96 100644
--- a/helm/ocaml/cic_notation/print_grammar.ml
+++ b/helm/ocaml/cic_notation/print_grammar.ml
@@ -26,16 +26,20 @@
 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 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 visit_description desc fmt = 
+let needs_brackets t =
+  let rec count_brothers = function 
+    | Node {brother = brother} -> 1 + count_brothers brother
+    | _ -> 0
+  in
+  count_brothers t > 1
+
+let visit_description desc fmt self = 
   let skip s = List.mem s [ ] in
   let inline s = List.mem s [ "int" ] in
   
@@ -81,13 +85,6 @@ let visit_description desc fmt =
       | 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 =
@@ -130,46 +127,55 @@ let visit_description desc fmt =
     | Snterm entry -> visit_entry entry todo is_son nesting 
     | Snterml (entry,_) -> visit_entry entry todo is_son nesting
     | Slist0 symbol -> 
-        Format.fprintf fmt "@[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol symbol todo is_son (nesting+1) in
-        Format.fprintf fmt "}@] @ ";
+        Format.fprintf fmt "@]} @ ";
         todo
     | Slist0sep (symbol,sep) ->
-        Format.fprintf fmt "@[<hov2>[ ";
+        Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son (nesting + 1) in
-        Format.fprintf fmt "@[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         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 "}@] @ ]@] @ ";
+        Format.fprintf fmt "@]} @]] @ ";
         todo
     | Slist1 symbol -> 
-        Format.fprintf fmt "@[<hov2>{ ";
+        Format.fprintf fmt "{@[<hov2> ";
         let todo = visit_symbol symbol todo is_son (nesting + 1) in
-        Format.fprintf fmt "}+@] @ ";
+        Format.fprintf fmt "@]}+ @ ";
         todo 
     | Slist1sep (symbol,sep) ->
         let todo = visit_symbol symbol todo is_son nesting in
-        Format.fprintf fmt " @[<hov2>{ ";
+        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
-        Format.fprintf fmt "}@] @ ";
+        Format.fprintf fmt "@]} @ ";
         todo
     | Sopt symbol -> 
-        Format.fprintf fmt "@[<hov2>[ ";
+        Format.fprintf fmt "[@[<hov2> ";
         let todo = visit_symbol symbol todo is_son (nesting + 1) in
-        Format.fprintf fmt "]@] @ ";
+        Format.fprintf fmt "@]] @ ";
         todo
-    | Sself -> Format.fprintf fmt "self "; todo
+    | Sself -> Format.fprintf fmt "%s " self; todo
     | Snext -> Format.fprintf fmt "next "; todo
     | Stoken pattern -> 
         let constructor, keyword = pattern in
         if keyword = "" then
-          Format.fprintf fmt "'%s' " constructor
+          Format.fprintf fmt "`%s' " constructor
         else
           Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword);
         todo
-    | Stree tree -> visit_tree tree todo is_son nesting
+    | 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)
   in
   visit_desc desc [] false 0
 ;;
@@ -195,11 +201,19 @@ and clean_tree = function
   | 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
+  | {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} -> 
@@ -220,8 +234,7 @@ and is_symbol_dummy = function
   | 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
+  | Sself | Snext -> false
   | Stree t -> is_tree_dummy t
   
 and is_tree_dummy = function
@@ -241,7 +254,7 @@ let rec visit_entries todo pped =
             let { ename = ename; edesc = desc } = hd in 
             Format.fprintf fmt "@[<hv2>%s ::=@ " ename;
             let desc = clean_dummy_desc desc in 
-            let todo = visit_description desc fmt @ todo in
+            let todo = visit_description desc fmt ename @ todo in
             Format.fprintf fmt "@]";
             Format.pp_print_newline fmt ();
             Format.pp_print_newline fmt ();
@@ -268,6 +281,5 @@ let rec 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] []