Deep_fail.v

(*
Ltac users know that Ltac 'match' involves backtracking when one of match cases
has failed.  Sometimes it's undesirable, and Ltac code should fail without
checking other match branches.
Here is a dumb solution.
*)

Module Deep_fail.

Inductive deep_failure (A : Type) (s : A) : Type :=
  Deep_failure : deep_failure A s.

Ltac fail_deep s := set (deep_failure := Deep_failure _ s).

Ltac with_deep_failure := fun tac =>
  match goal with
  | [ F : deep_failure _ ?s |- _ ] =>
        let ss := eval compute in s in
        clear F;
        tac ss
  end
.

Ltac show_deep_failure :=
  with_deep_failure ltac:(fun ss => fail 1 ss)
.

Ltac map_deep_failure f :=
  with_deep_failure ltac:(fun ss => fail_deep (f ss))
.

End Deep_fail.


(* usage:

Ltac inner_tac :=
  ...
  fail_deep "deep error"
.

Ltac outer_tac :=
  match goal with
  | ... => inner_tac
  ... other cases -- we don't want Coq to examine them ...
.

Ltac run_it :=
  outer_tac;
  map_deep_failure (fun s => "error while applying my tactic: " ++ s); show_deep_failure
.

*)