misc -> domMisc

[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 cb06a8edf6dc9d67f410fed7689a6bf6ad2e8230..ba14fd0d635372a4480f3e9e7daa4af681e14ecf 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -43,20 +43,20 @@ let rec count_tactic current_size tac =
     | Apply (_, term) -> countterm (current_size + 6) term
     | 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 *)
+    | Compare (_, term) -> countterm (current_size + 7) term
+    | Constructor (_, n) -> current_size + 12
     | 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)
+    | Cut (_, ident, term) ->
+       let id_size =
+        match ident with
+           None -> 0
+         | Some id -> String.length id + 4
+       in
+        countterm (current_size + 4 + id_size) term
+    | DecideEquality _ -> current_size + 15
+    | 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 
@@ -65,11 +65,10 @@ 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
-    | Fold (_, kind, term) ->
-       countterm (current_size + 5) term
     | Fourier _ -> current_size + 7
     | 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,13 +76,7 @@ let rec count_tactic current_size tac =
     | Left _ -> current_size + 4
     | LetIn (_, term, ident) ->
        countterm (current_size + 5 + String.length ident) term
-    | 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 *)
-    | Rewrite _ -> assert false (* TODO *)
     | Right _ -> current_size + 5
     | Ring _ -> current_size + 4
     | Split _ -> current_size + 5
@@ -106,6 +99,7 @@ let string_of_kind = function
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
   | `Whd -> "whd"
+  | `Normalize -> "normalize"
 
 let dummy_tbl = Hashtbl.create 0
 
@@ -133,37 +127,17 @@ and big_tactic2box = function
                ast2astBox term])
   | Assumption _ -> Box.Text([],"assumption")
   | Auto _ -> Box.Text([],"auto")
-  | Change (_, t1, t2, where) ->
-      let where =
-       (match where with 
-            None -> []
-          | Some ident -> 
-              [Box.Text([],"in");
-               Box.smallskip;
-               Box.Text([],ident)]) in
-       Box.V([],
-             (pretty_append 
-                [Box.Text([],"change")]
-                t1)@
-             (pretty_append 
-                [Box.Text([],"with")]
-                t2)@where)
-  | Change_pattern _ -> assert false  (* TODO *)
-  | Contradiction _ -> Box.Text([],"contradiction")
-  | Cut (_, term) -> 
-      Box.V([],[Box.Text([],"cut");
+  | Compare (_, term) ->
+      Box.V([],[Box.Text([],"compare");
                Box.indent(ast2astBox term)])
-  | Decompose (_, ident, principles) ->
-      let principles =
-       List.map (fun x -> Box.Text([],x)) principles in
+  | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n)
+  | Contradiction _ -> Box.Text([],"contradiction")
+  | DecideEquality _ -> Box.Text([],"decide equality")
+  | 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 
@@ -183,16 +157,8 @@ and big_tactic2box = function
       Box.V([],[Box.Text([],"exact");
                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(ast2astBox term)])
   | Fourier _ -> Box.Text([],"fourier")
   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
-  | Injection (_, ident) -> 
-      Box.V([],[Box.Text([],"transitivity");
-               Box.indent (Box.Text([],ident))])
   | Intros (_, num, idents) ->
       let num =
        (match num with 
@@ -211,18 +177,7 @@ and big_tactic2box = function
                          Box.smallskip;
                          Box.Text([],"=")]);
                Box.indent (ast2astBox term)])
-  | Reduce _ -> assert false  (* TODO *)
   | Reflexivity _ -> Box.Text([],"reflexivity")
-  | Replace (_, t1, t2) -> 
-      Box.V([],
-           (pretty_append 
-              [Box.Text([],"replace")]
-              t1)@
-           (pretty_append 
-              [Box.Text([],"with")]
-              t2))
-  | Replace_pattern _ -> assert false  (* TODO *)
-  | Rewrite _ -> assert false (* TODO *)
   | Right _ -> Box.Text([],"right")
   | Ring _ ->  Box.Text([],"ring")
   | Split _ -> Box.Text([],"split")
@@ -236,16 +191,9 @@ open TacticAst
 
 let rec tactical2box = function
   | 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);
                Box.indent (tactical2box tac)])
-  | IdTac _ -> Box.Text([],"id")
   | Repeat (_, tac) -> 
       Box.V([],[Box.Text([],"repeat");
                Box.indent (tactical2box tac)])