From Undecidability Require Import TMTac.
From Undecidability Require Import TM.Hoare.HoareLogic TM.Hoare.HoareCombinators TM.Hoare.HoareRegister TM.Hoare.HoareTacticsView.
From smpl Require Import Smpl.


Ltac contains_evar e := has_evar e.

Ltac triple_with_space :=
  lazymatch goal with
  | [ |- context [withSpace] ] => idtac
  end.


Smpl Create hstep_Spec.
Ltac hstep_Spec := smpl hstep_Spec.



Ltac hstep_Seq :=
  match goal with
  | [ |- Triple ?P (?M1;; ?M2) ?Q ] => eapply Seq_Spec
  | [ |- TripleT ?P ?k (?M1;; ?M2) ?Q ] => eapply Seq_SpecT
  end.

Ltac hstep_If :=
  cbn beta;
  lazymatch goal with
  | [ |- Triple _ (If ?M1 ?M2 ?M3) _ ] => eapply If_Spec
  | [ |- TripleT ≃≃( _,_) ?k (If ?M1 ?M2 ?M3) _ ] =>
    eapply If_SpecTReg with (R:= fun y => (_,_)) (Q:= fun y => (_,_))
  | [ |- TripleT ?P ?k (If ?M1 ?M2 ?M3) ?Q ] => eapply If_SpecT
  end.

Ltac hstep_Switch :=
  lazymatch goal with
  | [ |- Triple ?P (Switch ?M1 ?M2) ?Q ] => eapply Switch_Spec
  | [ |- TripleT ?P ?k (Switch ?M1 ?M2) ?Q ] => eapply Switch_SpecT
  end.

Ltac hstep_Return :=
  lazymatch goal with
  | [ |- Triple ?P (Return ?M ?x) ?Q ] =>
     (eapply Return_Spec_con)
  | [ |- TripleT ?P ?k (Return ?M ?x) ?Q ] =>
     (eapply Return_SpecT_con)

  | [ |- Triple ?P (Relabel ?M ?f) ?Q ] =>
     (eapply Relabel_Spec_con)
  | [ |- TripleT ?P ?k (Relabel ?M ?f) ?Q ] =>
     (eapply Relabel_SpecT_con)
  end.


Ltac hstep_LiftTapes :=
  lazymatch goal with
  | [ |- Triple ?PRE (LiftTapes ?M ?I) ?POST ] =>
    tryif contains_evar POST then
      (tryif triple_with_space
        then (eapply LiftTapes_Spec_space with (Q':= fun y => _) (Q:= fun y => _); [smpl_dupfree | ])
        else (eapply LiftTapes_Spec with (Q':= fun y => _) (Q:= fun y => _); [smpl_dupfree | ]))
    else
      (tryif triple_with_space then (eapply LiftTapes_Spec_space_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ])
        else (eapply LiftTapes_Spec_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ]))
  | [ |- TripleT ?PRE ?k (LiftTapes ?M ?I) ?POST ] =>
    tryif contains_evar POST then
      (tryif triple_with_space then (refine (LiftTapes_SpecT_space (Q':= fun y => _) (Q:= fun y => _) _ _); [smpl_dupfree | ])
        else (refine (LiftTapes_SpecT (Q':= fun y => _) (Q:= fun y => _) _ _); [smpl_dupfree | ]))
    else
      (tryif triple_with_space then (eapply LiftTapes_SpecT_space_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ])
        else (eapply LiftTapes_SpecT_con with (R':= fun y => _) (R:= fun y => _); [smpl_dupfree | | ]))
  end.

Ltac hstep_ChangeAlphabet :=
  lazymatch goal with
  | [ |- Triple ?PRE (ChangeAlphabet ?M ?I)?POST ] =>
    tryif contains_evar POST then
      (tryif triple_with_space then (eapply ChangeAlphabet_Spec_space_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ])
        else (eapply ChangeAlphabet_Spec_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ]))
    else
      (tryif triple_with_space then (eapply ChangeAlphabet_Spec_space_pre_post with (Q':= fun y => _) (Q0:= fun y => _); [ | | ])
        else (eapply ChangeAlphabet_Spec_pre_post with (Q':= fun y => _) (Q':= fun y => _) (Q0:= fun y => _); [ | | ]))
  | [ |- TripleT ?PRE ?k (ChangeAlphabet ?M ?I)?POST ] =>
    tryif contains_evar POST then
      (tryif triple_with_space then (eapply ChangeAlphabet_SpecT_space_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ])
        else (eapply ChangeAlphabet_SpecT_pre with (Q:= fun y => _) (Q0:= fun y => _); [ | ]))
    else
      (tryif triple_with_space then (eapply ChangeAlphabet_SpecT_space_pre_post with (Q':= fun y => _) (Q0:= fun y => _); [ | | ])
        else (eapply ChangeAlphabet_SpecT_pre_post with (Q:= fun y => _) (Q':= fun y => _) (Q0:= fun y => _); [ | | ]))
  end.






Local Tactic Notation "noSpace" tactic(t) :=
  let test :=
  tryif triple_with_space
   then fail
    else reflexivity
  in
  lazymatch goal with
  | [ |- Triple ?P ?M ?Q ] =>
  eapply Consequence_pre;[t| test ]
  | [ |- TripleT ?P _ ?M ?Q ] =>
  eapply ConsequenceT_pre;[t| test |reflexivity]
  end || fail "could not find user-rule applicable here".

Ltac hstep_user :=
  lazymatch goal with
  | [ |- Triple ?P ?M ?Q ] =>
    tryif contains_evar Q then
      (tryif triple_with_space then
          
          ((eapply TripleT_Triple; hstep_Spec)
           || (hstep_Spec))
        else ((eapply TripleT_Triple;refine (TripleT_RemoveSpace (Q:=fun y => _) (Q':=fun y => _) _); now (intros; hstep_Spec))
              || (refine (TripleT_RemoveSpace (Q:=fun y => _) (Q':=fun y => _) _); now (intros; hstep_Spec))
              || (eapply TripleT_Triple; hstep_Spec)
              || (noSpace hstep_Spec)))
    else (eapply Consequence_post; [ hstep_user | ])
  | [ |- TripleT ?P ?k ?M ?Q ] =>
    tryif contains_evar Q then
      (tryif triple_with_space then hstep_Spec
        else (refine (TripleT_RemoveSpace (Q:=fun y => _) (Q':=fun y => _)_); now (intros; hstep_Spec))
             || (noSpace hstep_Spec))
    else (eapply ConsequenceT_post; [ hstep_user | ])
  end.


Ltac hstep_Nop :=
  lazymatch goal with
  
  | [ |- TripleT ?P ?k Nop ?Q ] => eapply Nop_SpecT
  end.

Smpl Add hstep_Nop : hstep_Spec.


Ltac hstep_forall_unit :=
  hnf;
  lazymatch goal with
  | [ |- unit -> ?H ] => intros _
  | [ |- forall (y : finType_CS unit), ?H] => intros []
  | [ |- forall (y : unit), ?H] => intros []
  end.

Ltac hstep_pre := clear_abbrevs;cbn beta.
Ltac hstep_post := lazy beta.

Ltac hstep_Combinators := hstep_Seq || hstep_If || hstep_Switch || hstep_Return. Ltac hstep_Lifts := (hstep_LiftTapes || hstep_ChangeAlphabet).
Ltac hstep := hstep_pre; (hstep_forall_unit || hstep_Combinators || hstep_Lifts || hstep_user); hstep_post.
Ltac hsteps := repeat first [hstep | hstep_post] .
Ltac hsteps_cbn := repeat (cbn; hstep).

Ltac openFoldRight :=
  try (hnf;
  lazymatch goal with
  | |- _ /\ _ => refine (conj _ _);[ | openFoldRight]
  | |- True => exact I
  end).

Ltac tspec_solve :=
  lazymatch goal with
  | [ |- tspec (_,withSpace _ ?ss) ?t ] =>
    eapply tspec_space_solve;openFoldRight;[ .. | intros i; destruct_fin i;
    cbn [tspec_single withSpace_single Vector.map Vector.nth Vector.case0 Vector.caseS]; try (simple apply I || contains_ext || isVoid_mono)]
  | [ |- tspec (?P,?R) ?t ] =>
    eapply tspec_solve;openFoldRight;[ .. | intros i; destruct_fin i;
    cbn [tspec_single Vector.nth Vector.case0 Vector.caseS]; try (simple apply I || contains_ext || isVoid_mono)]
  end.


Ltac trySolveTrivEq := lazymatch goal with |- ?s = ?s => reflexivity | |- _ => idtac end.
Ltac tspec_ext :=
  unfold_abbrev;intros;
  
  lazymatch goal with
  | [ |- Entails (tspec _) (tspec _) ] => simple apply EntailsI;intros ? ?; tspec_ext
  | [ |- forall t, t ≃≃ ?P -> t ≃≃ ?Q ] =>
    let Ht := fresh "H"t in
    intros t Ht; tspec_ext; eauto
  | [ H : tspec (_,withSpace _ ?ss) ?t |- tspec (_,withSpace _ ?ss') ?t ] =>
    apply tspec_space_ext with (1 := H);[ cbn [implList];intros; openFoldRight;trySolveTrivEq |
    ((now eauto)
     || (intros i; destruct_fin i;
        cbn [tspec_single withSpace_single Vector.nth Vector.case0 Vector.caseS];
        intros; try (simple apply I ||contains_ext || isVoid_mono)))]
  | [ H : tspec (?P',?R') ?t |- tspec (?P,?R) ?t ] =>
    apply tspec_ext with (1 := H);[ cbn [implList];intros; openFoldRight;trySolveTrivEq |
    ((now eauto)
     || (intros i; destruct_fin i;
        cbn [tspec_single Vector.nth Vector.case0 Vector.caseS];
        intros; try (simple apply I || contains_ext || isVoid_mono)))]
  end.


Ltac underBinders t :=
  lazymatch goal with
  | |- forall x, _ => let x := fresh x in intros x;underBinders t;revert x
  | |- _ => t
  end.

Ltac introPure_prepare :=
  lazymatch goal with
  | |- Entails (tspec ((_,_))) _ => eapply tspec_introPure
  | |- Triple (tspec (?P,_)) _ _ => eapply Triple_introPure
  | |- TripleT (tspec (?P,_)) _ _ _ => eapply TripleT_introPure
  end;simpl implList at 1.

Tactic Notation "hintros" simple_intropattern_list(pat) := underBinders introPure_prepare;intros pat.

Ltac hstep_seq :=
lazymatch goal with
| |- ?R (_;;_) _ => hstep;[(hstep;hsteps_cbn;cbn);let n := numgoals in (tryif ( guard n = 1) then try tspec_ext else idtac ) |cbn;try hstep_forall_unit | reflexivity..]
| |- ?R (LiftTapes _ _) _ => hsteps_cbn
| |- ?R (ChangeAlphabet _ _) _ => hsteps_cbn
end.