Asts generalized: a lot of tactics where restricted to identifiers in place

[helm.git] / helm / ocaml / cic_transformations / tacticAst2Box.ml

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index f43091c755a012cd059cfd64d52c289151013e06..1c6723186ca6e1aeb70606e15dbcbb3487559b91 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -44,18 +44,18 @@ 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)
+*) 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
+    | 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
@@ -70,7 +70,8 @@ let rec count_tactic current_size tac =
     | 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))
@@ -137,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 -> []
@@ -151,19 +153,15 @@ and big_tactic2box = function
              (pretty_append 
                 [Box.Text([],"with")]
                 t2)@where)
+*) 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)])
+               Box.indent(ast2astBox term)])
   | Discriminate (_, term) -> 
       Box.V([],pretty_append [Box.Text([],"discriminate")] term)
   | Elim (_, term, using) ->
@@ -193,9 +191,7 @@ and big_tactic2box = function
   | 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