X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=1d82c0aebd0fbe29fa23895d28b352f5f77a24e3;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=3c4026f95137deba0ecb6da57323c2cfd5f43770;hpb=9766d606b71ec69594919ca34b067e268afeabf0;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index 3c4026f95..1d82c0aeb 100644
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -40,8 +40,8 @@ let rec count_tactic current_size tac =
   if current_size > maxsize then current_size 
   else match tac with 
       LocatedTactic (_, tac) -> count_tactic current_size tac
-    | Absurd -> current_size + 6
-    | Apply term -> countterm (current_size+6) term
+    | Absurd term -> countterm (current_size + 6) term
+    | Apply term -> countterm (current_size + 6) term
     | Assumption -> current_size + 10
     | Change (t1, t2, where) ->
 	let size1 = countterm (current_size + 12) t1 in (* change, with *)
@@ -93,12 +93,12 @@ let rec count_tactic current_size tac =
 
 let is_big_tac tac =
   let n = (count_tactic 0 tac) in
-  prerr_endline ("Lunghezza: " ^ (string_of_int n));
+(*   prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
   n > maxsize
 ;;
 
 (* prova *)
-let rec small_tactic2box ?(attr = []) tac =
+let rec small_tactic2box tac =
   Box.Text([], TacticAstPp.pp_tactic tac)
 
 let string_of_kind = function
@@ -106,19 +106,32 @@ let string_of_kind = function
   | `Simpl -> "simpl"
   | `Whd -> "whd"
 
-let rec tactic2box ?(attr = []) tac =
+let dummy_tbl = Hashtbl.create 0
+
+let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl)
+
+let pretty_append l ast =
+  if is_big ast then
+    [Box.H([],l);
+     Box.H([],[Box.skip; ast2astBox ast])]
+  else
+    [Box.H([],l@[Box.smallskip; ast2astBox ast])]
+
+let rec tactic2box tac =
   if (is_big_tac tac) then
-    big_tactic2box ~attr tac
+    big_tactic2box tac
   else 
-    small_tactic2box ~attr tac
+    small_tactic2box tac
 
-and big_tactic2box ?(attr = []) = function
+and big_tactic2box = function
     LocatedTactic (loc, tac) -> 
-      big_tactic2box ~attr tac
-  | Absurd -> Box.Text([],"absurd")
+      big_tactic2box tac
+  | Absurd term ->
+      Box.V([],[Box.Text([],"absurd");
+		ast2astBox term])
   | Apply term -> 
       Box.V([],[Box.Text([],"apply");
-		ast2box ~attr term])
+		ast2astBox term])
   | Assumption -> Box.Text([],"assumption")
   | Change (t1, t2, where) ->
       let where =
@@ -131,17 +144,15 @@ and big_tactic2box ?(attr = []) = function
 	Box.V([],
 	      (pretty_append 
 		 [Box.Text([],"change")]
-		 t1
-		 [])@
+		 t1)@
 	      (pretty_append 
 		 [Box.Text([],"with")]
-		 t2
-		 [])@where)
+		 t2)@where)
   | Change_pattern (_, _, _) -> assert false  (* TODO *)
   | Contradiction -> Box.Text([],"contradiction")
   | Cut term -> 
       Box.V([],[Box.Text([],"cut");
-		Box.indent(ast2box term)])
+		Box.indent(ast2astBox term)])
   | Decompose (ident, principles) ->
       let principles =
 	List.map (fun x -> Box.Text([],x)) principles in
@@ -160,25 +171,23 @@ and big_tactic2box ?(attr = []) = function
 	   | Some term -> 
 	       (pretty_append
 		  [Box.Text([],"using")]
-		  term
-		  [])) in
+		  term)) in
       Box.V([],
 	    (pretty_append
 	       [Box.Text([],"elim")]
-	       term
-	       [])@using)
+	       term)@using)
   | ElimType term -> 
       Box.V([],[Box.Text([],"elim type");
-		Box.indent(ast2box term)])
+		Box.indent(ast2astBox term)])
   | Exact term -> 
       Box.V([],[Box.Text([],"exact");
-		Box.indent(ast2box term)])
+		Box.indent(ast2astBox term)])
   | Exists -> Box.Text([],"exists")
   | Fold (kind, term) ->
       Box.V([],[Box.H([],[Box.Text([],"fold");
 			  Box.smallskip;
 			  Box.Text([],string_of_kind kind)]);
-		Box.indent(ast2box term)])
+		Box.indent(ast2astBox term)])
   | Fourier -> Box.Text([],"fourier")
   | Injection ident -> 
       Box.V([],[Box.Text([],"transitivity");
@@ -200,19 +209,17 @@ and big_tactic2box ?(attr = []) = function
 			  Box.Text([],ident);
 			  Box.smallskip;
 			  Box.Text([],"=")]);
-		Box.indent (ast2box term)])
+		Box.indent (ast2astBox term)])
   | Reduce (_, _, _) -> assert false  (* TODO *)
   | Reflexivity -> Box.Text([],"reflexivity")
   | Replace (t1, t2) -> 
       Box.V([],
 	    (pretty_append 
 	       [Box.Text([],"replace")]
-	       t1
-	       [])@
+	       t1)@
 	    (pretty_append 
 	       [Box.Text([],"with")]
-	       t2
-	       []))
+	       t2))
   | Replace_pattern (_, _) -> assert false  (* TODO *)
   | Rewrite (_, _, _) -> assert false (* TODO *)
   | Right -> Box.Text([],"right")
@@ -221,13 +228,18 @@ and big_tactic2box ?(attr = []) = function
   | Symmetry -> Box.Text([],"symmetry")
   | Transitivity term -> 
       Box.V([],[Box.Text([],"transitivity");
-		Box.indent (ast2box term)])
+		Box.indent (ast2astBox term)])
 ;;
 
 open TacticAst
 
-let rec tactical2box ?(attr = []) = function
-    LocatedTactical (loc, tac) -> tactical2box tac
+let rec tactical2box = function
+  | LocatedTactical (loc, tac) -> tactical2box tac
+
+  | Tactic tac -> tactic2box tac
+  | Command cmd -> (* TODO dummy implementation *)
+      Box.Text([], TacticAstPp.pp_tactical (Command cmd))
+
   | Fail -> Box.Text([],"fail")
   | Do (count, tac) -> 
       Box.V([],[Box.Text([],"do " ^ string_of_int count);
@@ -238,7 +250,6 @@ let rec tactical2box ?(attr = []) = function
 		Box.indent (tactical2box tac)])
   | Seq tacs -> 
       Box.V([],tacticals2box tacs)
-  | Tactic tac -> tactic2box tac
   | Then (tac, tacs) -> 
       Box.V([],[tactical2box tac;
 		Box.H([],[Box.skip;