X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=62a63c7753f5341d0e45891fc197d377ecd7f68f;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=c82f0fb8add1cfa8366d68a4b2740b89f8e25171;hpb=e5f4d8fa36a154bbc0a555eefa5ccc0bdb29afb0;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index c82f0fb8a..62a63c775 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -66,6 +66,8 @@ and countterm current_size t =
              let size3 =
                List.fold_left countvar (c+String.length constr) vars in
              countterm size3 action) size2 pl 
+    | A.Cast (bo,ty) ->
+       countterm (countterm (current_size + 3) bo) ty
     | A.LetIn (var,s,t) ->
         let size1 = countvar current_size var in
         let size2 = countterm size1 s in
@@ -230,7 +232,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                       append_tail ~tail (Box.Object([],rhs))]) in
         let plbox =
           match pl with
-            [] -> append_tail ~tail (Box.Text([],"[]"))
+          | [] -> append_tail ~tail (Box.Text([],"[]"))
+          | [r] -> (make_rule ~tail:("]" :: tail) "[" r)
           | r::tl -> 
               Box.V([],
                 (make_rule ~tail:[] "[" r) ::
@@ -264,6 +267,10 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                         Box.smallskip;
                         Box.Text([],"with")]);
                  Box.indent plbox])
+    | A.Cast (bo,ty) ->
+        Box.V(make_attributes [Some "helm","xref"] [xref],
+              [Box.H([],[Box.Text([],"("); ast2box ~tail:[] bo]);
+               Box.H([],[Box.Text([],":"); ast2box ~tail ty;Box.Text([],")")])])
     | A.LetIn (var, s, t) ->
         Box.V(make_attributes [Some "helm","xref"] [xref],
               (make_def "let" var s "in")@[ast2box ~tail t])
@@ -360,7 +367,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                        (* ignoring the type *)
                        (Cic.Anonymous, _) -> Box.Text([],"_")
                      | (Cic.Name s, _) -> Box.Text([],s) in
-                   Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
+                   Box.smallskip::bv::acc) vars [Box.Text([],")")] in
             Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
       
 
@@ -485,6 +492,10 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
         | `None ->
             P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
             [m_close_fence]))
+    | A.Cast (bo,ty) ->
+       let attr = make_attributes [Some "helm","xref"] [xref] in
+        P.Mrow (attr,
+         [m_open_fence; aux bo; P.Mo ([],":"); aux ty; m_close_fence])
     | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
     | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
         let attr = make_attributes [Some "helm","xref"] [xref] in
@@ -578,7 +589,7 @@ let box_prefix = "b";;
 
 let add_xml_declaration stream =
   [<
-    Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+    Xml.xml_cdata "<?xml version=\"1.0\" ?>\n" ;
     Xml.xml_cdata "\n";
     Xml.xml_nempty ~prefix:box_prefix "box"
       [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
@@ -591,7 +602,7 @@ let add_xml_declaration stream =
 let ast2mpresXml ((ast, ids_to_uris) as arg) =
   let astBox = ast2astBox arg in
   let smallAst2mpresXml ast =
-    P.print_mpres (ast2mpres (ast, ids_to_uris))
+    P.print_mpres (fun _ -> assert false) (ast2mpres (ast, ids_to_uris))
   in
   (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)