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 term -> countterm (current_size + 6) term
- | Apply term -> countterm (current_size + 6) term
- | Auto -> current_size + 4
- | Assumption -> current_size + 10
- | Change (t1, t2, where) ->
+ | Absurd (_, term) -> countterm (current_size + 6) term
+ | 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 *)
- | Contradiction -> current_size + 13
- | Cut term -> countterm (current_size + 4) term
- | Decompose (ident, principles) ->
+ | 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) ->
+ | Discriminate (_, ident) -> current_size + 12 + (String.length ident)
+ | 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) ->
+ | 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
- | Hint -> current_size + 4
- | Injection ident -> current_size + 10 + (String.length ident)
- | Intros (num, idents) ->
+ | Fourier _ -> current_size + 7
+ | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
+ | Hint _ -> current_size + 4
+ | Injection (_, ident) -> current_size + 10 + (String.length ident)
+ | 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) ->
+ | 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 ->
+ | 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) ->
countterm (current_size + 13) term
;;
small_tactic2box tac
and big_tactic2box = function
- LocatedTactic (loc, tac) ->
- big_tactic2box tac
- | Absurd term ->
+ | Absurd (_, term) ->
Box.V([],[Box.Text([],"absurd");
ast2astBox term])
- | Apply term ->
+ | Apply (_, term) ->
Box.V([],[Box.Text([],"apply");
ast2astBox term])
- | Assumption -> Box.Text([],"assumption")
- | Auto -> Box.Text([],"auto")
- | Change (t1, t2, where) ->
+ | Assumption _ -> Box.Text([],"assumption")
+ | Auto _ -> Box.Text([],"auto")
+ | Change (_, t1, t2, where) ->
let where =
(match where with
None -> []
(pretty_append
[Box.Text([],"with")]
t2)@where)
- | Change_pattern (_, _, _) -> assert false (* TODO *)
- | Contradiction -> Box.Text([],"contradiction")
- | Cut term ->
+ | Change_pattern _ -> assert false (* TODO *)
+ | Contradiction _ -> Box.Text([],"contradiction")
+ | Cut (_, term) ->
Box.V([],[Box.Text([],"cut");
Box.indent(ast2astBox term)])
- | Decompose (ident, principles) ->
+ | Decompose (_, ident, principles) ->
let principles =
List.map (fun x -> Box.Text([],x)) principles in
Box.V([],[Box.Text([],"decompose");
Box.V([],principles);
Box.Text([],"]")]);
Box.Text([],ident)])
- | Discriminate ident ->
+ | Discriminate (_, ident) ->
Box.V([],[Box.Text([],"discriminate");
Box.Text([],ident)])
- | Elim (term, using) ->
+ | Elim (_, term, using) ->
let using =
(match using with
None -> []
(pretty_append
[Box.Text([],"elim")]
term)@using)
- | ElimType term ->
+ | ElimType (_, term) ->
Box.V([],[Box.Text([],"elim type");
Box.indent(ast2astBox term)])
- | Exact term ->
+ | Exact (_, term) ->
Box.V([],[Box.Text([],"exact");
Box.indent(ast2astBox term)])
- | Exists -> Box.Text([],"exists")
- | Fold (kind, 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")
- | Hint -> Box.Text([],"hint")
- | Injection ident ->
+ | Fourier _ -> Box.Text([],"fourier")
+ | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
+ | Hint _ -> Box.Text([],"hint")
+ | Injection (_, ident) ->
Box.V([],[Box.Text([],"transitivity");
Box.indent (Box.Text([],ident))])
- | Intros (num, idents) ->
+ | 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 (ast2astBox term)])
- | Reduce (_, _) -> assert false (* TODO *)
- | Reflexivity -> Box.Text([],"reflexivity")
- | Replace (t1, t2) ->
+ | Reduce _ -> assert false (* TODO *)
+ | Reflexivity _ -> Box.Text([],"reflexivity")
+ | Replace (_, t1, t2) ->
Box.V([],
(pretty_append
[Box.Text([],"replace")]
(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 ->
+ | 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.V([],[Box.Text([],"transitivity");
Box.indent (ast2astBox term)])
;;
open TacticAst
let rec tactical2box = function
- | LocatedTactical (loc, tac) -> tactical2box tac
-
- | Tactic tac -> tactic2box tac
+ | Tactic (_, tac) -> tactic2box tac
+(*
| Command cmd -> (* TODO dummy implementation *)
Box.Text([], TacticAstPp.pp_tactical (Command cmd))
+*)
- | Fail -> Box.Text([],"fail")
- | Do (count, tac) ->
+ | 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 ->
+ | IdTac _ -> Box.Text([],"id")
+ | Repeat (_, tac) ->
Box.V([],[Box.Text([],"repeat");
Box.indent (tactical2box tac)])
- | Seq tacs ->
+ | Seq (_, tacs) ->
Box.V([],tacticals2box tacs)
- | 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