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 *)
let is_big_tac tac =
let n = (count_tactic 0 tac) in
- prerr_endline ("Lunghezza: " ^ (string_of_int n));
+(* prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
n > maxsize
;;
(* prova *)
-let rec small_tactic2box ?(attr = []) tac =
+let rec small_tactic2box tac =
Box.Text([], TacticAstPp.pp_tactic tac)
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 =
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
| 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");
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")
| 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
- LocatedTactical (loc, tac) -> tactical2box tac
+let rec tactical2box = function
+ | LocatedTactical (loc, tac) -> tactical2box tac
+
+ | 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)])
| Seq tacs ->
Box.V([],tacticals2box tacs)
- | Tactic tac -> tactic2box tac
| Then (tac, tacs) ->
Box.V([],[tactical2box tac;
Box.H([],[Box.skip;