(* Copyright (c) 2017, the Dart project authors.  Please see the AUTHORS file
 * for details. All rights reserved. Use of this source code is governed by a
 * BSD-style license that can be found in the LICENSE file. *)

Require Import Common.
Require Export CpdtTactics.

Import OptionMonad.

Ltac extract E x y := set (x := E); assert (y : E = x); [auto|rewrite y in *].

Ltac force_expr E :=
  let v1 := fresh in
  let v2 := fresh in
  extract E v1 v2; destruct v1; [idtac|crush].

Lemma bind_some : forall A B x f, @opt_bind A B (Some x) f = f x.
Proof.
  crush.
Qed.

Ltac force_options :=
  repeat match goal with
         | [ H : (opt_bind ?y (fun x => ?z)) = Some ?w |- _ ] =>
           force_expr y; rewrite bind_some in H
         | [ H : (if ?cond then ?x else None) = Some ?w |- _ ] =>
           force_expr cond
         | [ H : (match ?x with _ => _ end) = Some ?w |- _ ] =>
           force_expr x
         end.

Inductive ltac_no_arg : Set :=
| Ltac_No_Arg : ltac_no_arg.

Ltac extract_head_2 term H varid eqid :=
  match type of H with
  | context[term ?X] => extract_head_2 (term X) H varid eqid
  | context[term] => remember term as varid eqn:eqid
  end.

Ltac extract_head_1 term H varid := let eqid := fresh varid "Eq" in extract_head_2 term H varid eqid.
Ltac extract_head_0 term H := let varid := fresh H in extract_head_1 term H varid.

Tactic Notation "extract_head" constr(term) "in" constr(H) := extract_head_0 term H.
Tactic Notation "extract_head" constr(term) "in" constr(H) "as" ident(name) := extract_head_1 term H name.
Tactic Notation "extract_head" constr(term) "in" constr(H) "as" ident(name) "," ident(name2) := extract_head_2 term H name name2.

Ltac continue_with H :=
  match type of H with
  | ?X -> ?Y =>
    let K := fresh H in
    let H' := fresh H in
    assert (X) as K; [idtac|pose proof (H K) as H']
  end.