\Assign and \subst to match the parser.

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 6541356993fdbeac13f725a1c1d7d442fbe4d24e..9fc2533aefecf84b405d2c99d76c820e7865ad14 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -75,19 +75,19 @@ and countterm current_size t =
             (fun c (var,s,_) -> 
                let size1 = countvar c var in
                countterm size1 s) current_size l in
-         countterm size1 t
+          countterm size1 t
     | A.Ident(s,None) -> current_size + (String.length s)
     | A.Ident(s,Some l) ->
         List.fold_left 
-         (fun c (v,t) -> countterm (c + (String.length v)) t) 
+          (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
     | A.Implicit -> current_size + 1 (* underscore *)
     | A.Meta (_,l) ->
-       List.fold_left 
-         (fun c t -> 
+        List.fold_left 
+          (fun c t -> 
              match t with
-                None -> c + 1 (* underscore *)
-              | Some t -> countterm c t)
+                 None -> c + 1 (* underscore *)
+               | Some t -> countterm c t)
           (current_size + 1) l (* num *)
     | A.Num (s, _) -> current_size + String.length s
     | A.Sort _ -> current_size + 4 (* sort name *)
@@ -103,7 +103,7 @@ let map_attribute =
       `Loc (n,m) -> 
         (Some "helm","loc",(string_of_int n)^" "^(string_of_int m))
     | `IdRef s -> 
-       (Some "helm","xref",s)
+        (Some "helm","xref",s)
 ;;
 
 let map_attributes = List.map map_attribute
@@ -123,53 +123,53 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
       A.AttributedTerm (attr1, t) -> 
         (* attr should be empty, since AtrtributedTerm are not
            supposed to be directly nested *)
-       bigast2box ~priority ~assoc ~attr:(attr1::~attr) t 
+        bigast2box ~priority ~assoc ~attr:(attr1::~attr) t 
     | A.Appl l ->
-       Box.H 
+        Box.H 
           (map_attributes attr, 
-          [Box.Text([],"(");
+           [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
+        Box.V(map_attributes attr,
+              [Box.H([],[(match typ with
                          | None -> Box.Text([], "?")
                          | Some typ -> ast2box typ);
-                        Box.smallskip;
+                         Box.smallskip;
                          Box.Text([], "\\to")]);
                Box.indent(ast2box body)])
     | A.Binder(kind, var, body) ->
-       Box.V(map_attributes attr,
-             [Box.H([],[resolve_binder kind;
-                        Box.smallskip;
-                        make_var var;
-                        Box.Text([],".")]);
-              Box.indent (ast2box body)])
+        Box.V(map_attributes attr,
+              [Box.H([],[resolve_binder kind;
+                         Box.smallskip;
+                         make_var var;
+                         Box.Text([],".")]);
+               Box.indent (ast2box body)])
     | A.Case(arg, _, ty, pl) ->
-       let make_rule sep ((constr,vars),rhs) =
-         if (is_big rhs) then
-           Box.V([],[Box.H([],[Box.Text([],sep);
-                               Box.smallskip; 
-                               make_pattern constr vars;
-                               Box.smallskip; 
-                               Box.Text([],"\Rightarrow")]);
-                     Box.indent (bigast2box rhs)])
-         else
-           Box.H([],[Box.Text([],sep);
-                     Box.smallskip; 
-                     make_pattern constr vars;
-                     Box.smallskip; 
-                     Box.Text([],"\Rightarrow");
-                     Box.smallskip; 
-                     Box.Object([],rhs)]) in
-       let plbox = match pl with
-           [] -> Box.Text([],"[]")
-         | r::tl -> 
-             Box.H([],
-                   [Box.V([], 
-                          (make_rule "[" r)::(List.map (make_rule "|") tl));
-                    Box.Text([],"]")]) in
+        let make_rule sep ((constr,vars),rhs) =
+          if (is_big rhs) then
+            Box.V([],[Box.H([],[Box.Text([],sep);
+                                Box.smallskip; 
+                                 make_pattern constr vars;
+                                Box.smallskip; 
+                                Box.Text([],"\Rightarrow")]);
+                      Box.indent (bigast2box rhs)])
+          else
+            Box.H([],[Box.Text([],sep);
+                      Box.smallskip; 
+                      make_pattern constr vars;
+                      Box.smallskip; 
+                      Box.Text([],"\Rightarrow");
+                      Box.smallskip; 
+                      Box.Object([],rhs)]) in
+        let plbox = match pl with
+            [] -> Box.Text([],"[]")
+          | r::tl -> 
+              Box.H([],
+                    [Box.V([], 
+                           (make_rule "[" r)::(List.map (make_rule "|") tl));
+                     Box.Text([],"]")]) in
         let ty_box =
           match ty with
           | Some ty ->
@@ -178,79 +178,79 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                          Box.Text([],"]")]) ]
           | None -> []
         in
-       if is_big arg then
-         Box.V(map_attributes attr,
+        if is_big arg then
+          Box.V(map_attributes attr,
                  ty_box @
                  [Box.Text([],"match");
-                Box.H([],[Box.skip;
-                          bigast2box arg;
-                          Box.smallskip;
-                          Box.Text([],"with")]);
-                plbox])
-       else
-         Box.V(map_attributes attr,
+                 Box.H([],[Box.skip;
+                           bigast2box arg;
+                           Box.smallskip;
+                           Box.Text([],"with")]);
+                 plbox])
+        else
+          Box.V(map_attributes attr,
                 ty_box @
-               [Box.H(map_attributes attr,
-                      [Box.Text([],"match");
-                       Box.smallskip;
-                       ast2box arg;
-                       Box.smallskip;
-                       Box.Text([],"with")]);
-                plbox])
+                [Box.H(map_attributes attr,
+                       [Box.Text([],"match");
+                        Box.smallskip;
+                        ast2box arg;
+                        Box.smallskip;
+                        Box.Text([],"with")]);
+                 plbox])
     | A.LetIn (var, s, t) ->
-       Box.V(map_attributes attr,
-             (make_def "let" var s "in")@[ast2box t])
+        Box.V(map_attributes attr,
+              (make_def "let" var s "in")@[ast2box t])
     | A.LetRec (_, vars, body) ->
-       let definitions =
-         let rec make_defs let_txt = function
-             [] -> []
-           | [(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(map_attributes attr,
-             definitions@[ast2box body])
+        let definitions =
+          let rec make_defs let_txt = function
+              [] -> []
+            | [(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(map_attributes attr,
+              definitions@[ast2box body])
     | A.Ident (s, subst) ->
-       let subst =
-         let rec make_substs start_txt = 
-           function
-             [] -> []
-           | [(s,t)] -> 
-               make_subst start_txt s t "]"
-           | (s,t)::tl ->
-               (make_subst start_txt s t ";")@(make_substs " " tl)
+        let subst =
+          let rec make_substs start_txt = 
+            function
+              [] -> []
+            | [(s,t)] -> 
+                make_subst start_txt s t "]"
+            | (s,t)::tl ->
+                (make_subst start_txt s t ";")@(make_substs " " tl)
           in
           match subst with
-          | Some subst -> make_substs "[" subst
+          | Some subst -> make_substs "\\subst [" subst
           | None -> []
         in
-       Box.V([], (* attr here or on Vbox? *)
-             [Box.Text(map_attributes attr,s);
-              Box.indent(Box.V([],subst))])
+        Box.V([], (* attr here or on Vbox? *)
+              [Box.Text(map_attributes attr,s);
+               Box.indent(Box.V([],subst))])
     | A.Implicit -> 
-       Box.Text([],"_") (* big? *)
+        Box.Text([],"_") (* big? *)
     | A.Meta (n, l) ->
-       let local_context =
-         List.map 
-           (function t -> 
-              Box.H([],[aux_option t; Box.Text([],";")])) 
-           l in
-       Box.V(map_attributes attr,
-             [Box.Text([],"?"^(string_of_int n));
-              Box.H([],[Box.Text([],"[");
-                        Box.V([],local_context);
-                        Box.Text([],"]")])])
+        let local_context =
+          List.map 
+            (function t -> 
+               Box.H([],[aux_option t; Box.Text([],";")])) 
+            l in
+        Box.V(map_attributes attr,
+              [Box.Text([],"?"^(string_of_int n));
+               Box.H([],[Box.Text([],"[");
+                         Box.V([],local_context);
+                         Box.Text([],"]")])])
     | A.Num (s, _) -> 
-        Box.Text([],s)
+         Box.Text([],s)
     | A.Sort kind ->
-       (match kind with 
-            `Prop -> Box.Text([],"Prop")
-          | `Set -> Box.Text([],"Set")
-          | `Type -> Box.Text([],"Type")   
-          | `CProp -> Box.Text([],"CProp"))    
+        (match kind with 
+             `Prop -> Box.Text([],"Prop")
+           | `Set -> Box.Text([],"Set")
+           | `Type -> Box.Text([],"Type")   
+           | `CProp -> Box.Text([],"CProp"))    
     | A.Symbol (s, _) -> 
-       Box.Text([],s)
+        Box.Text([],s)
 
 and aux_option = function
     None  -> Box.Text([],"_")
@@ -263,32 +263,32 @@ and make_var = function
   | (Cic.Name s, None) -> Box.Text([],s)
   | (Cic.Name s, Some t) ->
       if is_big t then
-       Box.V([],[Box.Text([],s^":");
-                 Box.indent(bigast2box t)])
+        Box.V([],[Box.Text([],s^":");
+                  Box.indent(bigast2box t)])
       else
-       Box.H([],[Box.Text([],s^":");Box.Object([],t)])
+        Box.H([],[Box.Text([],s^":");Box.Object([],t)])
 
 and make_pattern constr = 
   function
       [] -> Box.Text([],constr)
     | vars -> 
-       let bvars =
-         List.fold_right 
-           (fun var acc -> 
-              let bv = 
-                match var with
-                    (* ignoring the type *)
-                    (Cic.Anonymous, _) -> Box.Text([],"_")
-                  | (Cic.Name s, _) -> Box.Text([],s) in
-                Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
-         Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
+        let bvars =
+          List.fold_right 
+            (fun var acc -> 
+               let bv = 
+                 match var with
+                     (* ignoring the type *)
+                     (Cic.Anonymous, _) -> Box.Text([],"_")
+                   | (Cic.Name s, _) -> Box.Text([],s) in
+                 Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
+          Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
     
 
 and make_def let_txt var def end_txt =
   let name = 
     (match var with
          (* ignoring the type *)
-        (Cic.Anonymous, _) -> Box.Text([],"_") 
+         (Cic.Anonymous, _) -> Box.Text([],"_") 
        | (Cic.Name s, _) -> Box.Text([],s)) in
   pretty_append 
     [Box.Text([],let_txt);
@@ -305,11 +305,11 @@ and make_subst start_txt varname body end_txt =
     [Box.Text([],start_txt);
      Box.Text([],varname);
      Box.smallskip;
-     Box.Text([],":=")
+     Box.Text([],"\Assign")
     ]
     body
     [Box.Text([],end_txt)] 
-         
+          
 and pretty_append l ast tail =
   prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
   if is_big ast then
@@ -320,7 +320,7 @@ and pretty_append l ast tail =
 
 ;;
 
-                         
+