X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=9fc2533aefecf84b405d2c99d76c820e7865ad14;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=9679501ab460d2c8ae707edfbc36db396037ac22;hpb=9766d606b71ec69594919ca34b067e268afeabf0;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 9679501ab..9fc2533ae 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -75,18 +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
-    | A.Ident(s,l) ->
+          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 *)
@@ -102,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
@@ -122,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([],"->")]);
-		      Box.indent (bigast2box rhs)])
-	  else
-	    Box.H([],[Box.Text([],sep);
-		      Box.smallskip; 
-		      make_pattern constr vars;
-		      Box.smallskip; 
-		      Box.Text([],"->");
-		      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 ->
@@ -177,75 +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) in
-	  make_substs "[" subst in
-	Box.V([], (* attr here or on Vbox? *)
-	      [Box.Text(map_attributes attr,s);
-	       Box.indent(Box.V([],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)
+          in
+          match subst with
+          | 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))])
     | 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([],"_")
@@ -258,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);
@@ -300,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
@@ -315,7 +320,7 @@ and pretty_append l ast tail =
 
 ;;
 
-			  
+