(* 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 H :=
  let v1 := fresh in
  let v2 := fresh in
  extract E v1 v2; destruct v1; [idtac|simpl in H; contradict H; congruence].

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

Lemma simpl_if : forall A (e1 e2 : A), (if true then e1 else e2) = e1.
  auto.
Qed.

    (* remember (expression_type CE (NatMap.add v s TE) arg) as EXP. *)
(* destruct EXP; [rewrite bind_some in H1|simpl in H1; contradict H1; congruence]. *)
Ltac force_option :=
  match goal with
  | [ H : (opt_bind ?y (fun x => ?z)) = Some ?w |- _ ] =>
    force_expr y H; rewrite bind_some in H
  | [ H : (if ?cond then ?x else None) = Some ?w |- _ ] =>
    force_expr cond H; rewrite simpl_if in H
  | [ H : (match ?x with _ => _ end) = Some ?w |- _ ] =>
    force_expr x H
  end.

Ltac force_options := repeat force_option.

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.

Ltac extract_head_goal_2 term varid eqid :=
  match goal with
  | [ |- context[term ?X] ] => extract_head_goal_2 (term X) varid eqid
  | [ |- context[term] ] => remember term as varid eqn:eqid
  end.

Ltac extract_head_goal_1 term varid := let eqid := fresh varid "Eq" in extract_head_goal_2 term varid eqid.
Ltac extract_head_goal_0 term := let varid := fresh "G" in extract_head_goal_1 term 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.

Tactic Notation "extract_head" constr(term) := extract_head_goal_0 term.
Tactic Notation "extract_head" constr(term) "as" ident(name) := extract_head_goal_1 term name.
Tactic Notation "extract_head" constr(term) "as" ident(name) "," ident(name2) := extract_head_goal_2 term 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.