- added arrow notation

[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 934223e5ce276644c3875d145d83a5d339fa279e..b0b1dd4f792930f9427f2468a1cfecab20ceebfe 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -28,7 +28,7 @@
 (*                           PROJECT HELM                                 *)
 (*                                                                        *)
 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             28/6/2003                                   *)
+(*                             28/6/2003                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -130,6 +130,15 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
           [Box.Text([],"(");
             Box.V([],List.map ast2box l);
             Box.Text([],")")])
+    | A.Binder (`Forall, (Cic.Anonymous, typ), body)
+    | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
+       Box.V(map_attributes attr,
+             [Box.H([],[(match typ with
+                         | None -> Box.Text([], "?")
+                         | Some typ -> ast2box typ);
+                        Box.smallskip;
+                         Box.Text([], "\\to")]);
+               Box.indent(ast2box body)])
     | A.Binder(kind, var, body) ->
        Box.V(map_attributes attr,
              [Box.H([],[resolve_binder kind;
@@ -161,9 +170,18 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                    [Box.V([], 
                           (make_rule "[" r)::(List.map (make_rule "|") tl));
                     Box.Text([],"]")]) in
+        let ty_box =
+          match ty with
+          | Some ty ->
+              [ Box.H([],[Box.Text([],"[");
+                         ast2box ty;
+                         Box.Text([],"]")]) ]
+          | None -> []
+        in
        if is_big arg then
          Box.V(map_attributes attr,
-               [Box.Text([],"match");
+                 ty_box @
+                 [Box.Text([],"match");
                 Box.H([],[Box.skip;
                           bigast2box arg;
                           Box.smallskip;
@@ -171,6 +189,7 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                 plbox])
        else
          Box.V(map_attributes attr,
+                ty_box @
                [Box.H(map_attributes attr,
                       [Box.Text([],"match");
                        Box.smallskip;