More tactics are now available to matita.

[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 1c6723186ca6e1aeb70606e15dbcbb3487559b91..0eb2fbde130bb5a50a84e48d0fc79a94b5ae1fa1 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -43,17 +43,11 @@ 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)
-*) assert false
-(*     | 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
+    | DecideEquality _ -> current_size + 15
     | Decompose (_, term) ->
        countterm (current_size + 11) term
     | Discriminate (_, term) -> countterm (current_size + 12) term
@@ -68,7 +62,6 @@ 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 (_, term) ->
        countterm (current_size + 10) term
@@ -79,14 +72,10 @@ 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 *) *)
-    | Rewrite _ -> assert false (* TODO *)
     | Right _ -> current_size + 5
     | Ring _ -> current_size + 4
     | Split _ -> current_size + 5
@@ -137,28 +126,15 @@ 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)
-*) assert false
-(*   | Change_pattern _ -> assert false  (* TODO *) *)
+  | Compare (_, term) ->
+      Box.V([],[Box.Text([],"compare");
+               Box.indent(ast2astBox term)])
+  | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n)
   | Contradiction _ -> Box.Text([],"contradiction")
   | Cut (_, term) -> 
       Box.V([],[Box.Text([],"cut");
                Box.indent(ast2astBox term)])
+  | DecideEquality _ -> Box.Text([],"decide equality")
   | Decompose (_, term) ->
       Box.V([],[Box.Text([],"decompose");
                Box.indent(ast2astBox term)])
@@ -189,9 +165,7 @@ 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 (_, term) -> assert false (* TODO *)
   | Intros (_, num, idents) ->
       let num =
        (match num with 
@@ -210,8 +184,6 @@ and big_tactic2box = function
                          Box.smallskip;
                          Box.Text([],"=")]);
                Box.indent (ast2astBox term)])
-(*   | Reduce _ *)
-  | Reduce _ -> assert false  (* TODO *)
   | Reflexivity _ -> Box.Text([],"reflexivity")
   | Replace (_, t1, t2) -> 
       Box.V([],
@@ -221,8 +193,6 @@ and big_tactic2box = function
            (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")