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 (?;; ?) ?Q ] eapply Seq_Spec
  | [ |- TripleT ?P ?k (?;; ?) ?Q ] eapply Seq_SpecT
  end.

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

Ltac hstep_Switch :=
  lazymatch goal with
  | [ |- Triple ?P (Switch ? ?) ?Q ] eapply Switch_Spec
  | [ |- TripleT ?P ?k (Switch ? ?) ?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':= y _) (Q:= y _); [smpl_dupfree | ])
        else (eapply LiftTapes_Spec with (Q':= y _) (Q:= y _); [smpl_dupfree | ]))
    else
      (tryif triple_with_space then (eapply LiftTapes_Spec_space_con with (R':= y _) (R:= y _); [smpl_dupfree | | ])
        else (eapply LiftTapes_Spec_con with (R':= y _) (R:= 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':= y _) (Q:= y _) _ _); [smpl_dupfree | ])
        else (refine (LiftTapes_SpecT (Q':= y _) (Q:= y _) _ _); [smpl_dupfree | ]))
    else
      (tryif triple_with_space then (eapply LiftTapes_SpecT_space_con with (R':= y _) (R:= y _); [smpl_dupfree | | ])
        else (eapply LiftTapes_SpecT_con with (R':= y _) (R:= 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:= y _) (:= y _); [ | ])
        else (eapply ChangeAlphabet_Spec_pre with (Q:= y _) (:= y _); [ | ]))
    else
      (tryif triple_with_space then (eapply ChangeAlphabet_Spec_space_pre_post with (Q':= y _) (:= y _); [ | | ])
        else (eapply ChangeAlphabet_Spec_pre_post with (Q':= y _) (Q':= y _) (:= 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:= y _) (:= y _); [ | ])
        else (eapply ChangeAlphabet_SpecT_pre with (Q:= y _) (:= y _); [ | ]))
    else
      (tryif triple_with_space then (eapply ChangeAlphabet_SpecT_space_pre_post with (Q':= y _) (:= y _); [ | | ])
        else (eapply ChangeAlphabet_SpecT_pre_post with (Q:= y _) (Q':= y _) (:= 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:= y _) (Q':= y _) _); now (intros; hstep_Spec))
              || (refine (TripleT_RemoveSpace (Q:= y _) (Q':= 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:= y _) (Q':= 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 _
  | [ |- (y : finType_CS unit), ?H] intros []
  | [ |- (y : unit), ?H] intros []
  end.

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

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
  | [ |- 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
  | |- 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.