X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst2Box.ml;h=1c6723186ca6e1aeb70606e15dbcbb3487559b91;hb=9d8e81db720417f58591ea42f72c6750b886a83d;hp=cb06a8edf6dc9d67f410fed7689a6bf6ad2e8230;hpb=7e7ce7bb6b95e9bd10dc180671ba7512ff2537dd;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index cb06a8edf..1c6723186 100644
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -44,19 +44,19 @@ let rec count_tactic current_size tac =
     | Auto _ -> current_size + 4
     | Assumption _ -> current_size + 10
     | Change (_, t1, t2, where) ->
+(*
 	let size1 = countterm (current_size + 12) t1 in (* change, with *)
 	let size2 = countterm size1 t2 in
         (match where with 
 	     None -> size2
 	   | Some ident -> size2 + 3 + String.length ident)
-    | Change_pattern _ -> assert false  (* TODO *)
+*) assert false
+(*     | Change_pattern _ -> assert false  (* TODO *) *)
     | Contradiction _ -> current_size + 13
     | Cut (_, term) -> countterm (current_size + 4) term
-    | Decompose (_, ident, principles) ->
-	List.fold_left
-	  (fun size s -> size + (String.length s))
-	  (current_size + 11 + String.length ident) principles
-    | Discriminate (_, ident) -> current_size + 12 + (String.length ident)
+    | Decompose (_, term) ->
+       countterm (current_size + 11) term
+    | Discriminate (_, term) -> countterm (current_size + 12) term
     | Elim (_, term, using) ->
 	let size1 = countterm (current_size + 5) term in
 	  (match using with 
@@ -68,8 +68,10 @@ let rec count_tactic current_size tac =
     | Fold (_, kind, term) ->
 	countterm (current_size + 5) term
     | Fourier _ -> current_size + 7
+    | Generalize (_,term,pattern) -> assert false (* TODO *)
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
-    | Injection (_, ident) -> current_size + 10 + (String.length ident)
+    | Injection (_, term) ->
+       countterm (current_size + 10) term
     | Intros (_, num, idents) ->
 	List.fold_left 
 	  (fun size s -> size + (String.length s))
@@ -77,12 +79,13 @@ let rec count_tactic current_size tac =
     | Left _ -> current_size + 4
     | LetIn (_, term, ident) ->
 	countterm (current_size + 5 + String.length ident) term
+(*     | Reduce _ *)
     | Reduce _ -> assert false  (* TODO *)
     | Reflexivity _ -> current_size + 11
     | Replace (_, t1, t2) -> 
 	let size1 = countterm (current_size + 14) t1 in (* replace, with *)
 	  countterm size1 t2	
-    | Replace_pattern _ -> assert false  (* TODO *)
+(*     | Replace_pattern _ -> assert false  (* TODO *) *)
     | Rewrite _ -> assert false (* TODO *)
     | Right _ -> current_size + 5
     | Ring _ -> current_size + 4
@@ -106,6 +109,7 @@ let string_of_kind = function
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
   | `Whd -> "whd"
+  | `Normalize -> "normalize"
 
 let dummy_tbl = Hashtbl.create 0
 
@@ -134,6 +138,7 @@ and big_tactic2box = function
   | Assumption _ -> Box.Text([],"assumption")
   | Auto _ -> Box.Text([],"auto")
   | Change (_, t1, t2, where) ->
+(*
       let where =
 	(match where with 
 	     None -> []
@@ -148,22 +153,17 @@ and big_tactic2box = function
 	      (pretty_append 
 		 [Box.Text([],"with")]
 		 t2)@where)
-  | Change_pattern _ -> assert false  (* TODO *)
+*) assert false
+(*   | Change_pattern _ -> assert false  (* TODO *) *)
   | Contradiction _ -> Box.Text([],"contradiction")
   | Cut (_, term) -> 
       Box.V([],[Box.Text([],"cut");
 		Box.indent(ast2astBox term)])
-  | Decompose (_, ident, principles) ->
-      let principles =
-	List.map (fun x -> Box.Text([],x)) principles in
+  | Decompose (_, term) ->
       Box.V([],[Box.Text([],"decompose");
-		Box.H([],[Box.Text([],"[");
-			  Box.V([],principles);
-			  Box.Text([],"]")]);
-		Box.Text([],ident)])
-  | Discriminate (_, ident) -> 
-      Box.V([],[Box.Text([],"discriminate");
-		Box.Text([],ident)])
+		Box.indent(ast2astBox term)])
+  | Discriminate (_, term) -> 
+      Box.V([],pretty_append [Box.Text([],"discriminate")] term)
   | Elim (_, term, using) ->
       let using =
 	(match using with 
@@ -189,10 +189,9 @@ and big_tactic2box = function
 			  Box.Text([],string_of_kind kind)]);
 		Box.indent(ast2astBox term)])
   | Fourier _ -> Box.Text([],"fourier")
+  | Generalize _ -> assert false  (* TODO *)
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
-  | Injection (_, ident) -> 
-      Box.V([],[Box.Text([],"transitivity");
-		Box.indent (Box.Text([],ident))])
+  | Injection (_, term) -> assert false (* TODO *)
   | Intros (_, num, idents) ->
       let num =
 	(match num with 
@@ -211,6 +210,7 @@ and big_tactic2box = function
 			  Box.smallskip;
 			  Box.Text([],"=")]);
 		Box.indent (ast2astBox term)])
+(*   | Reduce _ *)
   | Reduce _ -> assert false  (* TODO *)
   | Reflexivity _ -> Box.Text([],"reflexivity")
   | Replace (_, t1, t2) -> 
@@ -221,7 +221,7 @@ and big_tactic2box = function
 	    (pretty_append 
 	       [Box.Text([],"with")]
 	       t2))
-  | Replace_pattern _ -> assert false  (* TODO *)
+(*   | Replace_pattern _ -> assert false  (* TODO *) *)
   | Rewrite _ -> assert false (* TODO *)
   | Right _ -> Box.Text([],"right")
   | Ring _ ->  Box.Text([],"ring")