From 11184b03e0d7f02d3710d0364e0d0f17ea5eebbf Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Jul 2005 13:49:56 +0000
Subject: [PATCH] More cases implemented in tactic_count.

---
 .../cic_transformations/tacticAst2Box.ml      | 51 +++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml
index ba14fd0d6..fc5119324 100644
--- 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
-- 
2.39.2