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
- | 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 *)
- | 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)
- | Elim (term, using) ->
+ | Absurd (_, term) -> countterm (current_size + 6) term
+ | Apply (_, term) -> countterm (current_size + 6) term
+ | Auto _ -> current_size + 4
+ | Assumption _ -> current_size + 10
+ | Compare (_, term) -> countterm (current_size + 7) term
+ | Constructor (_, n) -> current_size + 12
+ | Contradiction _ -> current_size + 13
+ | 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
None -> size1
| Some term -> countterm (size1 + 7) term)
- | 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
- | Injection ident -> current_size + 10 + (String.length ident)
- | Intros (num, idents) ->
+ | ElimType (_, term) -> countterm (current_size + 10) term
+ | Exact (_, term) -> countterm (current_size + 6) term
+ | Exists _ -> current_size + 6
+ | Fourier _ -> current_size + 7
+ | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
+ | Injection (_, term) ->
+ countterm (current_size + 10) term
+ | Intros (_, num, idents) ->
List.fold_left
(fun size s -> size + (String.length s))
(current_size + 7) idents
- | Left -> current_size + 4
- | LetIn (term, ident) ->
+ | 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
- | Symmetry -> current_size + 8
- | Transitivity term ->
+ | Reflexivity _ -> current_size + 11
+ | Right _ -> current_size + 5
+ | Ring _ -> current_size + 4
+ | Split _ -> current_size + 5
+ | Symmetry _ -> current_size + 8
+ | Transitivity (_, term) ->
countterm (current_size + 13) term
;;
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
| `Reduce -> "reduce"
- | `Simpl -> "simpl"
+ | `Simpl -> "simplify"
| `Whd -> "whd"
+ | `Normalize -> "normalize"
+
+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 ?(attr = []) tac =
+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
- LocatedTactic (loc, tac) ->
- big_tactic2box ~attr tac
- | Absurd -> Box.Text([],"absurd")
- | Apply term ->
+and big_tactic2box = function
+ | Absurd (_, term) ->
+ Box.V([],[Box.Text([],"absurd");
+ ast2astBox term])
+ | Apply (_, term) ->
Box.V([],[Box.Text([],"apply");
- ast2box ~attr term])
- | Assumption -> Box.Text([],"assumption")
- | 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");
- Box.indent(ast2box term)])
- | Decompose (ident, principles) ->
- let principles =
- List.map (fun x -> Box.Text([],x)) principles in
+ ast2astBox term])
+ | Assumption _ -> Box.Text([],"assumption")
+ | Auto _ -> Box.Text([],"auto")
+ | Compare (_, term) ->
+ Box.V([],[Box.Text([],"compare");
+ Box.indent(ast2astBox term)])
+ | 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)])
- | Elim (term, using) ->
+ Box.indent(ast2astBox term)])
+ | Discriminate (_, term) ->
+ Box.V([],pretty_append [Box.Text([],"discriminate")] term)
+ | Elim (_, term, using) ->
let using =
(match using with
None -> []
| Some term ->
(pretty_append
[Box.Text([],"using")]
- term
- [])) in
+ term)) in
Box.V([],
(pretty_append
[Box.Text([],"elim")]
- term
- [])@using)
- | ElimType term ->
+ term)@using)
+ | ElimType (_, term) ->
Box.V([],[Box.Text([],"elim type");
- Box.indent(ast2box term)])
- | Exact term ->
+ Box.indent(ast2astBox term)])
+ | Exact (_, term) ->
Box.V([],[Box.Text([],"exact");
- Box.indent(ast2box 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)])
- | Fourier -> Box.Text([],"fourier")
- | Injection ident ->
- Box.V([],[Box.Text([],"transitivity");
- Box.indent (Box.Text([],ident))])
- | Intros (num, idents) ->
+ Box.indent(ast2astBox term)])
+ | Exists _ -> Box.Text([],"exists")
+ | Fourier _ -> Box.Text([],"fourier")
+ | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
+ | Intros (_, num, idents) ->
let num =
(match num with
None -> []
Box.V([],[Box.Text([],"decompose");
Box.H([],[Box.smallskip;
Box.V([],idents)])])
- | Left -> Box.Text([],"left")
- | LetIn (term, ident) ->
+ | Left _ -> Box.Text([],"left")
+ | LetIn (_, term, ident) ->
Box.V([],[Box.H([],[Box.Text([],"let");
Box.smallskip;
Box.Text([],ident);
Box.smallskip;
Box.Text([],"=")]);
- Box.indent (ast2box 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")
- | Symmetry -> Box.Text([],"symmetry")
- | Transitivity term ->
+ Box.indent (ast2astBox term)])
+ | Reflexivity _ -> Box.Text([],"reflexivity")
+ | Right _ -> Box.Text([],"right")
+ | Ring _ -> Box.Text([],"ring")
+ | Split _ -> Box.Text([],"split")
+ | 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
- | Fail -> Box.Text([],"fail")
- | Do (count, tac) ->
+let rec tactical2box = function
+ | Tactic (_, tac) -> tactic2box tac
+ | Do (_, count, tac) ->
Box.V([],[Box.Text([],"do " ^ string_of_int count);
Box.indent (tactical2box tac)])
- | IdTac -> Box.Text([],"id")
- | Repeat tac ->
+ | Repeat (_, tac) ->
Box.V([],[Box.Text([],"repeat");
Box.indent (tactical2box tac)])
- | Seq tacs ->
+ | Seq (_, tacs) ->
Box.V([],tacticals2box tacs)
- | Tactic tac -> tactic2box tac
- | Then (tac, tacs) ->
+ | Then (_, tac, tacs) ->
Box.V([],[tactical2box tac;
Box.H([],[Box.skip;
Box.Text([],"[");
Box.V([],tacticals2box tacs);
Box.Text([],"]");])])
- | Tries tacs ->
+ | Tries (_, tacs) ->
Box.V([],[Box.Text([],"try");
Box.H([],[Box.skip;
Box.Text([],"[");
Box.V([],tacticals2box tacs);
Box.Text([],"]");])])
- | Try tac ->
+ | Try (_, tac) ->
Box.V([],[Box.Text([],"try");
Box.indent (tactical2box tac)])
projects / helm.git / blobdiff