From Undecidability Require Import L.Util.L_facts.

From Undecidability.Shared.Libs.PSL Require Import FinTypes Vectors.
Require Import List.

Require Import Undecidability.TM.Util.TM_facts.

From Undecidability Require Import ProgrammingTools LM_heap_def WriteValue CaseList Copy ListTM Hoare.
From Undecidability.TM.L Require Import JumpTargetTM Alphabets M_LHeapInterpreter.
From Undecidability Require Import L.AbstractMachines.FlatPro.LM_heap_correct.

Require Import List.

Import Vector.VectorNotations.
Import ListNotations ResourceMeasures.

From Undecidability.TM.L Require Import UnfoldClos.

Import CasePair Code.CaseList.

Set Default Proof Using "Type".

Module EvalL.
Section Fix.

  Variable Σ : finType.

  Definition Σintern :Type := sigStep + sigList (sigPair sigHClos sigNat).

  Context (retr_eval : Retract Σintern Σ) (retr_pro : Retract sigPro Σ).

  Definition retr_unfolder : Retract (sigList (sigPair sigHClos sigNat)) Σ := ComposeRetract retr_eval _.
  Definition retr_interpreter : Retract sigStep Σ := ComposeRetract retr_eval _.

  Local Instance retr_closs_intrp : Retract (sigList (sigHClos)) Σ := ComposeRetract retr_interpreter _.
  Local Instance retr_clos_intrp : Retract sigHClos Σ := ComposeRetract retr_closs_intrp _.
  Local Instance retr_pro_intrp : Retract sigPro Σ := ComposeRetract retr_clos_intrp _.

  Local Instance retr_nat_clos_ad' : Retract sigNat sigHClos := Retract_sigPair_X _ (Retract_id _).
  Local Instance retr_nat_clos_ad : Retract sigNat Σ := ComposeRetract _ retr_nat_clos_ad'.
  Local Instance retr_heap : Retract sigHeap Σ := ComposeRetract retr_interpreter _.


  Definition M : pTM (Σ^+) unit 11 :=
    Translate retr_pro retr_pro_intrp @ [||];;
    CopyValue _ @ [|;|];;
    Reset _ @[||];;
    WriteValue 0 retr_nat_clos_ad @ [| |];;
    Constr_pair _ _ retr_clos_intrp @ [|;|];;
    Reset _ @ [||];;
    WriteValue ( []%list) retr_closs_intrp @ [| |];;
    Constr_cons _ retr_closs_intrp @ [|;|];;
    Reset _ @ [||];;
    WriteValue ( []%list) retr_closs_intrp @ [| |];;
    WriteValue ( []%list ) retr_heap @ [| |];;
    M_LHeapInterpreter.Loop retr_interpreter;;
    Reset _ @ [||];;
    CaseList _ retr_closs_intrp @ [| ; |];;
    Reset _ @ [||];;
    UnfoldClos.M retr_unfolder retr_heap retr_clos_intrp @ [| ;;;;;;;;;|];;
    Reset _ @ [||];;
    Translate (UnfoldClos.retr_pro _) retr_pro @ [||].


  Arguments "+" : simpl never.
  Arguments "*" : simpl never.

  Definition steps (s : term) (k:) (t:term) Hcl (HR:evalIn k s t):=
    1 + Translate_steps (compile s) +
    (1 + CopyValue_steps (compile s) +
    (1 + Reset_steps (compile s) +
      (1 + WriteValue_steps (size 0) +
      (1 + Constr_pair_steps 0 +
        (1 + Reset_steps 0 +
        (1 + WriteValue_steps (size []%list) +
          (1 + Constr_cons_steps (0, compile s) +
          (1 + Reset_steps (0, compile s) +
            (1 + WriteValue_steps (size []%list) +
            (1 + WriteValue_steps (size []%list) +
              (1 + Loop_steps [(0, compile s)] [] []%list (3 * k + 1) +
              (1 + Reset_steps []%list +
                let (g,tmp) := completenessTimeInformative (proj2 (timeBS_evalIn _ _ _) HR) Hcl in
                let (H,_):= tmp in
                (1 + CaseList_steps [g] +
                (1 + Reset_steps []%list +
                  (1 + UnfoldClos.steps H g t +
                  (1 + Reset_steps H + Translate_steps (compile t))))))))))))))))).
  Arguments steps : clear implicits.

  Lemma SpecT s k t (Hcl: closed s) (HR:evalIn k s t):
    TripleT ≃≃([],[|Contains retr_pro (compile s)|] Vector.const Void _)
      (steps s k t Hcl HR) M
      ( _ ≃≃([],[|Contains retr_pro (compile t)|] Vector.const Void _)).
  Proof.
    unfold steps. destruct completenessTimeInformative as (g&H&?&?). clear HR.
    eapply ConsequenceT_pre. 2:reflexivity.
    unfold M.
    do 11 (hstep_seq;[]). cbn.
    hstep_seq;[| | ] .
    { refine (TripleT_RemoveSpace _). intros. eapply Interpreter_SpecT. eassumption. inversion 1. }
    now cbn; tspec_ext.
    do 2 (hstep_seq;[]).
    hintros _ _.
    hstep_seq;[].
    hstep_seq;[|].
    { eapply UnfoldClos.SpecT. eassumption. }
    cbn.
    do 2 (hstep_seq;[]). reflexivity.
    unfold steps. reflexivity.
  Qed.



  Lemma Spec s :
   closed s
    Triple ≃≃([],[|Contains retr_pro (compile s)|] Vector.const Void _)
      M
      ( _ t s', t ≃≃ ([s s']%list,[|Contains retr_pro (compile s')|] Vector.const Void _)).
  Proof.
    intros cls.
    unfold M.
    do 11 (hstep_seq;[]). cbn.
    hstep.
    {
      eapply Consequence with (:= y _) (:= y _).
      eapply ChangeAlphabet_Spec_ex with (Q:= y x _) (Q':= y x _) (Ctx:= x (H:Prop) (steps_k (snd x) _ (fst x) halt_state (fst x))
        (fst (fst (fst x)) = []%list
        H)).
      now refine (Interpreter_Spec [(0,compile s)] [] [])%list. now unfold "",Proper,Basics.impl. now cbn; tspec_ext. cbn;intros _. apply reflexivity.
    }
    cbn. intros _.
    eapply Triple_exists_pre. intros [[[T' V'] H'] k'];cbn.
    eapply Triple_and_pre. intros [HR Hhalt].
    unfold steps_k in*.
    edestruct soundness with (1:=cls) as (?&?&?&Heq&?&?). {split. now eapply pow_star. eassumption. }
    injection Heq as [= ].
    eapply Triple_forall_pre. exists eq_refl.
    do 2 (hstep_seq;[]).
    hintros ? _.
    do 2 hstep_seq;[|].
    { refine (TripleT_Triple _). refine (UnfoldClos.SpecT _ _ _ _). eassumption. }
    cbn.
    hstep_seq.
    eapply Triple_exists_con. eexists _.
    change ( x ?h x) with h.
    eapply Consequence_post.
    now hsteps_cbn.
    cbn. intros _. tspec_ext. easy.
  Qed.


End Fix.
End EvalL.