More cases implemented in tactic_count.

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index ba14fd0d635372a4480f3e9e7daa4af681e14ecf..fc511932423723292b41ebd21d490b81790f5907 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -36,6 +36,18 @@
 open Ast2pres
 open TacticAst
 
+let count_pattern current_size p =
+ if current_size > maxsize then current_size
+ else
+assert false
+
+let count_kind =
+ function
+    `Reduce -> 6
+  | `Simpl -> 8
+  | `Whd -> 3
+  | `Normalize -> 9
+
 let rec count_tactic current_size tac =
   if current_size > maxsize then current_size 
   else match tac with 
@@ -43,6 +55,10 @@ let rec count_tactic current_size tac =
     | Apply (_, term) -> countterm (current_size + 6) term
     | Auto _ -> current_size + 4
     | Assumption _ -> current_size + 10
+    | Change (_,p,term) ->
+       count_pattern (countterm (current_size + 13) term) p
+    | Clear (_,id) -> current_size + 6 + String.length id
+    | ClearBody (_,id) -> current_size + 10 + String.length id
     | Compare (_, term) -> countterm (current_size + 7) term
     | Constructor (_, n) -> current_size + 12
     | Contradiction _ -> current_size + 13
@@ -65,18 +81,53 @@ let rec count_tactic current_size tac =
     | ElimType (_, term) -> countterm (current_size + 10) term
     | Exact (_, term) -> countterm (current_size + 6) term
     | Exists _ -> current_size + 6
+    | Fail _ -> current_size + 4
+    | Fold (_,kind,term,p) ->
+       count_pattern (countterm (current_size + count_kind kind + 6) term) p
     | Fourier _ -> current_size + 7
+    | FwdSimpl (_,id,idl) ->
+        List.fold_left (fun s id -> s + String.length id)
+         (current_size + 4 + String.length id) idl
+    | Generalize (_,p,id) ->
+       let id_size =
+        match id with
+           None -> 0
+         | Some id -> 4 + String.length id
+       in
+        count_pattern (current_size + 11 + id_size) p
     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
+    | IdTac _ -> current_size + 2
     | Injection (_, term) ->
        countterm (current_size + 10) term
     | Intros (_, num, idents) ->
        List.fold_left 
          (fun size s -> size + (String.length s))
          (current_size + 7) idents
+    | LApply (_,depth,terml,term,idopt) ->
+       let idopt_size =
+        match idopt with
+           None -> 0
+         | Some id -> 6 + String.length id in
+       let terml_size =
+        if terml = [] then 0
+        else
+         List.fold_left (fun s t -> countterm (s + 1) t) 3 terml in
+       let depth_size =
+        match depth with
+           None -> 0
+         | Some n -> 8 + n / 10
+       in
+        countterm (current_size + 7 + idopt_size + terml_size + depth_size) term
     | Left _ -> current_size + 4
     | LetIn (_, term, ident) ->
        countterm (current_size + 5 + String.length ident) term
+    | Reduce (_,kind,p) ->
+       count_pattern (current_size + count_kind kind + 1) p
     | Reflexivity _ -> current_size + 11
+    | Replace (_,p,term) ->
+       count_pattern (countterm (current_size + 11) term) p
+    | Rewrite (_,dir,term,p) ->
+       count_pattern (countterm (current_size + 10) term) p
     | Right _ -> current_size + 5
     | Ring _ -> current_size + 4
     | Split _ -> current_size + 5