X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=c82f0fb8add1cfa8366d68a4b2740b89f8e25171;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=0eba3757fcb5b016846151d19b63ec9742177878;hpb=66a331a32509281f0c28ced014640e98a49cc0e0;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 0eba3757f..c82f0fb8a 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -138,6 +138,12 @@ let append_tail ~tail box =
   | [] -> box
   | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
 
+let rec find_symbol idref = function
+  | A.AttributedTerm (`Loc _, t) -> find_symbol None t
+  | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
+  | A.Symbol (name, _) -> `Symbol (name, idref)
+  | _ -> `None
+
 let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
   (t, ids_to_uris)
 =
@@ -165,19 +171,10 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
     | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
     | A.Appl [] -> assert false
     | A.Appl ((hd::tl) as l) ->
-        let rec find_symbol idref = function
-          | A.AttributedTerm (`Loc _, t) -> find_symbol None t
-          | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
-          | A.Symbol (name, _) ->
-              (match idref with
-              | None -> assert false
-              | Some idref -> `Symbol (name, idref))
-          | _ -> `None
-        in
         let aattr = make_attributes [Some "helm","xref"] [xref] in
         (match find_symbol None hd with
         | `Symbol (name, sxref) ->
-            let sattr = make_std_attributes (Some sxref) in
+            let sattr = make_std_attributes sxref in
             (try 
               (let f = Hashtbl.find symbol_table_charcount name in
                f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
@@ -230,14 +227,15 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                       Box.smallskip; 
                       Box.Text([],map_tex unicode "Rightarrow");
                       Box.smallskip; 
-                      Box.Object([],rhs)]) in
-        let plbox = match pl with
-            [] -> Box.Text([],"[]")
+                      append_tail ~tail (Box.Object([],rhs))]) in
+        let plbox =
+          match pl with
+            [] -> append_tail ~tail (Box.Text([],"[]"))
           | r::tl -> 
               Box.V([],
                 (make_rule ~tail:[] "[" r) ::
                 (make_args
-                  (fun ~tail pat -> make_rule ~tail:[] "|" pat)
+                  (fun ~tail pat -> make_rule ~tail "|" pat)
                   ~tail:("]" :: tail)
                   tl))
         in
@@ -245,7 +243,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
           match ty with
           | Some ty ->
               [ Box.H([],[Box.Text([],"[");
-                         ast2box ~tail ty;
+                         ast2box ~tail:[] ty;
                          Box.Text([],"]")]) ]
           | None -> []
         in
@@ -253,7 +251,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
           Box.V(make_attributes [Some "helm","xref"] [xref],
                  ty_box @
                  [Box.Text([],"match");
-                 Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg]));
+                 Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg]));
                  Box.Text([],"with");
                  Box.indent plbox])
         else
@@ -262,7 +260,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                 [Box.H(make_attributes [Some "helm","xref"] [xref],
                        [Box.Text([],"match");
                         Box.smallskip;
-                        ast2box ~tail arg;
+                        ast2box ~tail:[] arg;
                         Box.smallskip;
                         Box.Text([],"with")]);
                  Box.indent plbox])
@@ -273,8 +271,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
         let definitions =
           let rec make_defs let_txt = function
               [] -> []
-            | [(var,s,_)] -> 
-                make_def let_txt var s "in"
+            | [(var,s,_)] -> make_def let_txt var s "in"
             | (var,s,_)::tl ->
                 (make_def let_txt var s "")@(make_defs "and" tl) in
           make_defs "let rec" vars in
@@ -474,20 +471,10 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.UserInput -> P.Mtext([], "")
     | A.Appl [] -> assert false
     | A.Appl ((hd::tl) as l) ->
-        let rec find_symbol idref = function
-          | A.AttributedTerm (`Loc _, t) -> find_symbol None t
-          | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
-          | A.Symbol (name, _) ->
-              (match idref with
-              | None -> assert false
-              | Some idref -> `Symbol (name, idref))
-          | term ->
-              `None
-        in
         let aattr = make_attributes [Some "helm","xref"] [xref] in
         (match find_symbol None hd with
         | `Symbol (name, sxref) ->
-            let sattr = make_std_attributes (Some sxref) in
+            let sattr = make_std_attributes sxref in
             (try 
               (let f = Hashtbl.find symbol_table name in
                f tl ~priority ~assoc ~ids_to_uris aattr sattr)
@@ -551,7 +538,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
           let lhs = 
             P.Mtext([], constr) ::
               (List.concat
-                (List.map (fun var -> P.smallskip :: make_capture_variable var)
+                (List.map
+                  (fun var -> P.smallskip :: make_capture_variable var)
                   vars))
           in
           lhs @
@@ -697,4 +685,5 @@ let _ = (** fill symbol_table *)
   add_binary_op "times" 70 (`Ascii "*");
   add_binary_op "minus" 60 (`Ascii "-");
   add_binary_op "div" 60 (`Ascii "/");
+  add_binary_op "cast" 80 (`Ascii ":");