X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=c82f0fb8add1cfa8366d68a4b2740b89f8e25171;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=65e1c32c7e16ec85a676c4a18e900c03ae54c79f;hpb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 65e1c32c7..c82f0fb8a 100644
--- 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,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
@@ -241,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
@@ -249,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
@@ -258,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])
@@ -269,30 +271,41 @@ 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
               [] -> []
             | [(s,t)] -> 
-                make_subst start_txt s t "]"
+                make_subst start_txt s t ""
             | (s,t)::tl ->
-                (make_subst start_txt s t ";")@(make_substs " " tl)
+                (make_subst start_txt s t ";")@(make_substs "" tl)
           in
           match subst with
-          | Some subst -> make_substs ((map_tex unicode "subst") ^ "[") subst
-          | None -> []
+          | Some subst ->
+	      Box.H([],
+	            [Box.Text(make_std_attributes xref,s);
+		     Box.Action([],
+		       [Box.Text([],"[...]");
+		        Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
+	                 Box.V([], make_substs "" subst);
+		         Box.Text([], "]")])])])
+          | None -> Box.Text(make_std_attributes xref, s)
         in
-        Box.V([], (* attr here or on Vbox? *)
+	 subst
+	(*
+        Box.H([], (* attr here or on Vbox? *)
               [Box.Text(make_std_attributes xref,s);
-               Box.indent(Box.V([],subst))])
+	       Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
+               (* Box.indent(Box.V([],subst))]) *)
+	*)
     | A.Implicit -> 
         Box.Text([],"_") (* big? *)
     | A.Meta (n, l) ->
@@ -317,6 +330,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 
@@ -366,11 +381,11 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
 
   and make_subst start_txt varname body end_txt =
     pretty_append ~tail:[end_txt]
-      [Box.Text([],start_txt);
-       Box.Text([],varname);
-       Box.smallskip;
-       Box.Text([],map_tex unicode "Assign")
-      ]
+      ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
+       [Box.Text([],varname);
+        Box.smallskip;
+        Box.Text([],map_tex unicode "Assign")
+       ])
       body
             
   and pretty_append ~tail l ast =
@@ -408,7 +423,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 
@@ -452,22 +468,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)
@@ -531,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 @
@@ -677,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 ":");