transformations no longer use Content_expression, but rather CicAst

[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 4b79607f52b0384951baba7fe9921c00c8ed0967..1d82c0aebd0fbe29fa23895d28b352f5f77a24e3 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst2Box.ml
+++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml
@@ -40,8 +40,8 @@ let rec count_tactic current_size tac =
   if current_size > maxsize then current_size 
   else match tac with 
       LocatedTactic (_, tac) -> count_tactic current_size tac
-    | Absurd -> current_size + 6
-    | Apply term -> countterm (current_size+6) term
+    | Absurd term -> countterm (current_size + 6) term
+    | Apply term -> countterm (current_size + 6) term
     | Assumption -> current_size + 10
     | Change (t1, t2, where) ->
        let size1 = countterm (current_size + 12) t1 in (* change, with *)
@@ -98,7 +98,7 @@ let is_big_tac tac =
 ;;
 
 (* prova *)
-let rec small_tactic2box ?(attr = []) tac =
+let rec small_tactic2box tac =
   Box.Text([], TacticAstPp.pp_tactic tac)
 
 let string_of_kind = function
@@ -106,19 +106,32 @@ let string_of_kind = function
   | `Simpl -> "simpl"
   | `Whd -> "whd"
 
-let rec tactic2box ?(attr = []) tac =
+let dummy_tbl = Hashtbl.create 0
+
+let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl)
+
+let pretty_append l ast =
+  if is_big ast then
+    [Box.H([],l);
+     Box.H([],[Box.skip; ast2astBox ast])]
+  else
+    [Box.H([],l@[Box.smallskip; ast2astBox ast])]
+
+let rec tactic2box tac =
   if (is_big_tac tac) then
-    big_tactic2box ~attr tac
+    big_tactic2box tac
   else 
-    small_tactic2box ~attr tac
+    small_tactic2box tac
 
-and big_tactic2box ?(attr = []) = function
+and big_tactic2box = function
     LocatedTactic (loc, tac) -> 
-      big_tactic2box ~attr tac
-  | Absurd -> Box.Text([],"absurd")
+      big_tactic2box tac
+  | Absurd term ->
+      Box.V([],[Box.Text([],"absurd");
+               ast2astBox term])
   | Apply term -> 
       Box.V([],[Box.Text([],"apply");
-               ast2box ~attr term])
+               ast2astBox term])
   | Assumption -> Box.Text([],"assumption")
   | Change (t1, t2, where) ->
       let where =
@@ -131,17 +144,15 @@ and big_tactic2box ?(attr = []) = function
        Box.V([],
              (pretty_append 
                 [Box.Text([],"change")]
-                t1
-                [])@
+                t1)@
              (pretty_append 
                 [Box.Text([],"with")]
-                t2
-                [])@where)
+                t2)@where)
   | Change_pattern (_, _, _) -> assert false  (* TODO *)
   | Contradiction -> Box.Text([],"contradiction")
   | Cut term -> 
       Box.V([],[Box.Text([],"cut");
-               Box.indent(ast2box term)])
+               Box.indent(ast2astBox term)])
   | Decompose (ident, principles) ->
       let principles =
        List.map (fun x -> Box.Text([],x)) principles in
@@ -160,25 +171,23 @@ and big_tactic2box ?(attr = []) = function
           | Some term -> 
               (pretty_append
                  [Box.Text([],"using")]
-                 term
-                 [])) in
+                 term)) in
       Box.V([],
            (pretty_append
               [Box.Text([],"elim")]
-              term
-              [])@using)
+              term)@using)
   | ElimType term -> 
       Box.V([],[Box.Text([],"elim type");
-               Box.indent(ast2box term)])
+               Box.indent(ast2astBox term)])
   | Exact term -> 
       Box.V([],[Box.Text([],"exact");
-               Box.indent(ast2box term)])
+               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(ast2box term)])
+               Box.indent(ast2astBox term)])
   | Fourier -> Box.Text([],"fourier")
   | Injection ident -> 
       Box.V([],[Box.Text([],"transitivity");
@@ -200,19 +209,17 @@ and big_tactic2box ?(attr = []) = function
                          Box.Text([],ident);
                          Box.smallskip;
                          Box.Text([],"=")]);
-               Box.indent (ast2box term)])
+               Box.indent (ast2astBox term)])
   | Reduce (_, _, _) -> assert false  (* TODO *)
   | Reflexivity -> Box.Text([],"reflexivity")
   | Replace (t1, t2) -> 
       Box.V([],
            (pretty_append 
               [Box.Text([],"replace")]
-              t1
-              [])@
+              t1)@
            (pretty_append 
               [Box.Text([],"with")]
-              t2
-              []))
+              t2))
   | Replace_pattern (_, _) -> assert false  (* TODO *)
   | Rewrite (_, _, _) -> assert false (* TODO *)
   | Right -> Box.Text([],"right")
@@ -221,12 +228,12 @@ and big_tactic2box ?(attr = []) = function
   | Symmetry -> Box.Text([],"symmetry")
   | Transitivity term -> 
       Box.V([],[Box.Text([],"transitivity");
-               Box.indent (ast2box term)])
+               Box.indent (ast2astBox term)])
 ;;
 
 open TacticAst
 
-let rec tactical2box ?(attr = []) = function
+let rec tactical2box = function
   | LocatedTactical (loc, tac) -> tactical2box tac
 
   | Tactic tac -> tactic2box tac