version 0.7.1

[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 cafd80c4a855b70a80b226af93bab225b700b10e..5c1ea95d766be9e53e2afea1fb3856110404b7aa 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -77,8 +77,10 @@ and countterm current_size t =
                let size1 = countvar c var in
                countterm size1 s) current_size l in
           countterm size1 t
-    | A.Ident(s,None) -> current_size + (String.length s)
-    | A.Ident(s,Some l) ->
+    | A.Ident (s,None)
+    | A.Uri (s, None) -> current_size + (String.length s)
+    | A.Ident (s,Some l)
+    | A.Uri (s,Some l) ->
         List.fold_left 
           (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
@@ -93,6 +95,8 @@ and countterm current_size t =
     | A.Num (s, _) -> current_size + String.length s
     | A.Sort _ -> current_size + 4 (* sort name *)
     | A.Symbol (s,_) -> current_size + String.length s
+
+    | A.UserInput -> current_size
 ;;
 
 let is_big t = 
@@ -134,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)
 =
@@ -161,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)
@@ -226,14 +227,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
@@ -241,7 +244,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
@@ -249,7 +252,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
@@ -258,7 +261,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])
@@ -269,14 +272,14 @@ 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
         Box.V(make_attributes [Some "helm","xref"] [xref],
               definitions@[ast2box ~tail body])
-    | A.Ident (s, subst) ->
+    | A.Ident (s, subst)
+    | A.Uri (s, subst) ->
         let subst =
           let rec make_substs start_txt = 
             function
@@ -328,6 +331,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
     | A.Symbol (s, _) -> 
         Box.Text([],s)
 
+    | A.UserInput -> Box.Text([],"")
+
   and aux_option ~tail = function
       None  -> Box.Text([],"_")
     | Some ast -> ast2box ~tail ast 
@@ -419,7 +424,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.Symbol (name,_) -> 
         let attr = make_std_attributes xref in
         P.Mi (attr,name)
-    | A.Ident (name,subst) ->
+    | A.Ident (name,subst)
+    | A.Uri (name,subst) ->
         let attr = make_std_attributes xref in
         let rec make_subst =
           (function 
@@ -463,22 +469,13 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) =
     | A.Sort `Type -> P.Mtext ([], "Type")
     | A.Sort `CProp -> P.Mtext ([], "CProp")
     | A.Implicit -> P.Mtext([], "?")
+    | 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)
@@ -542,7 +539,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 @
@@ -581,7 +579,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" ;
@@ -594,7 +592,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)
 
@@ -688,4 +686,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 ":");