Nicer handling of automatic text insertion.

[helm.git] / helm / ocaml / cic_transformations / ast2pres.ml

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 0eba3757fcb5b016846151d19b63ec9742177878..0e7a01306f9489f3eb989d73240bb179bb9da4ab 100644 (file)
--- 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
@@ -138,6 +140,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 +173,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 +229,16 @@ 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] -> (make_rule ~tail:("]" :: tail) "[" r)
           | 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 +246,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 +254,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,10 +263,14 @@ 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])
+    | 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])
@@ -273,8 +278,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 +478,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)
@@ -498,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
@@ -551,7 +549,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 @
@@ -590,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" ;
@@ -603,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)
 
@@ -697,4 +696,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 ":");