Require Import List.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import RuntimeStructures.
Require Import Heap.

Module RuntimeStructuresImpl
  (_ProgramStructures: PROGRAM_STRUCTURES_WITH_MAP)
  (_Heap: HEAP with Module M_ProgramStructures := _ProgramStructures)
  <: RUNTIME_STRUCTURES.

Open Scope type_scope.

Module M_Heap := _Heap.
Import M_Heap.M_ProgramStructures.M_ValuesAndTypes.
Import M_Heap.M_ProgramStructures.
Import M_Heap.

Definition TVarsGeneric: Set → Type := M_VarMap.t.
Section GenericVarsDefinition.
  Variable t: Set.
Definition varsEmpty := @M_VarMap.empty t.
Definition varsGet := @M_VarMap.find t.
Definition varsSet := @M_VarMap.add t.
Definition varsEquiv (vars1 vars2: TVarsGeneric t): Prop :=
  ∀ var, varsGet var vars1 = varsGet var vars2.

Section VarsProperties.
Variable vars: TVarsGeneric t.
Variable x y: TVar.
Variable v: t.

Lemma PvarsEmptyGet: varsGet x varsEmpty = None.
Proof.
  case_eq (varsGet x varsEmpty); intros.
  apply M_VarMap.find_2 in H.
  apply M_VarMap.empty_1 in H.
  contradiction.
  reflexivity.
Qed.

Lemma PvarsSetGet:
  varsGet x (varsSet x v vars) = Some v.
Proof.
  intros.
  apply M_VarMap.find_1.
  apply M_VarMap.add_1.
  reflexivity.
Qed.

Lemma noneNotMapsTo:
  ∀ vars' y,
  varsGet y vars' = None →
  ∀ w, ¬ M_VarMap.MapsTo y w vars'.
Proof.
  unfold not.
  intros.
  apply M_VarMap.find_1 in H0.
  unfold varsGet in H.
  rewrite H in H0.
  discriminate H0.
Qed.

Lemma notMapsToNone:
  ∀ vars' y,
  (∀ w, ¬ M_VarMap.MapsTo y w vars') →
  varsGet y vars' = None.
Proof.
  unfold not.
  intros.
  case_eq (varsGet y0 vars'); intros.
  apply M_VarMap.find_2 in H0.
  apply H in H0.
  contradiction.
  reflexivity.
Qed.

Lemma PvarsSetGetOther:
  x ≠ y →
  varsGet y vars = varsGet y (varsSet x v vars).
Proof.
  case_eq (varsGet y (varsSet x v vars)); intros.
  apply M_VarMap.find_1.
  apply M_VarMap.find_2 in H.
  apply M_VarMap.add_3 in H.
  assumption.
  assumption.

  eapply notMapsToNone; intros.
  eapply noneNotMapsTo in H.
  unfold not; intros.
  apply H; clear H.
  unfold varsSet.
  eapply M_VarMap.add_2.
  apply H0.
  eassumption.
Qed.

Axiom PvarsEqEquiv:
  varsEquiv vars vars.
Axiom PvarsSetSameEquiv:
  varsGet x vars = Some v →
  varsEquiv (varsSet x v vars) vars.
End VarsProperties.
  End GenericVarsDefinition.
  Arguments varsEmpty [t].
  Arguments varsGet [t] _ _.
  Arguments varsSet [t] _ _ _.
  Arguments PvarsEmptyGet [t] _.
  Arguments PvarsSetGet [t] _ _ _.
  Arguments PvarsSetGetOther [t] _ _ _ _ _.

Section GenericStackDefinition.
  Variable t: Set.
  Definition TLocalStackGeneric: Set := list t.
End GenericStackDefinition.

  Definition TVars := TVarsGeneric TVarValue.
  Definition TLocalStack := TLocalStackGeneric TValue.
  Definition TVarsKShadow := TVarsGeneric TVarKind.
  Definition TLocalStackKShadow := TLocalStackGeneric TKind.
  Definition TVarsTShadow := TVarsGeneric TType.
  Definition TLocalStackTShadow := TLocalStackGeneric TType.

  Parameter varsKAbstraction: TVars → TVarsKShadow.
  Parameter varsKConcretisation: TVarsKShadow → TVars.

  Axiom PvarsKAbstractionConsistent: ∀ vars var,
    varsGet var (varsKAbstraction vars) = option_map kindOfVarValue (varsGet var vars).

  Axiom PvarsKAbstractionConsistentSome: ∀ vars var v,
    varsGet var vars = Some v →
    varsGet var (varsKAbstraction vars) = Some (kindOfVarValue v).

  Axiom PvarsKAbstractionConsistentSet: ∀ vars var v,
    varsKAbstraction (varsSet var v vars) =
    varsSet var (kindOfVarValue v) (varsKAbstraction vars).

  Axiom PvarsKConcretisationConsistent: ∀ kvars var,
    option_map kindOfVarValue (varsGet var (varsKConcretisation kvars)) = varsGet var kvars.

  Axiom PvarsKConcretisationConsistentSome: ∀ kvars var k,
    varsGet var kvars = Some k →
    ∃ v, kindOfVarValue v = k ∧
      varsGet var (varsKConcretisation kvars) = Some v.

  Axiom PvarsKConcretisationAbstraction: ∀ varssh,
    varsKAbstraction (varsKConcretisation varssh) = varssh.

  Definition localStackKAbstraction: TLocalStack → TLocalStackKShadow :=
    map kindOfValue.

  Definition localStackKConcretisation: TLocalStackKShadow → TLocalStack :=
    map defaultForKind.

  Axiom PlocalStackKConcretisationAbstraction: ∀ sksh,
    localStackKAbstraction (localStackKConcretisation sksh) = sksh.

  Record TFrame := frameMake {
    frameGetVars: TVars;
    frameGetLocalStack: TLocalStack;
    frameGetPC: TPC
  }.

  Record TFrameKShadow := frameKShadowMake {
    frameKShadowGetVars: TVarsKShadow;
    frameKShadowGetLocalStack: TLocalStackKShadow;
    frameKShadowGetPC: TPC
  }.

  Definition frameKAbstraction (fr: TFrame): TFrameKShadow :=
    frameKShadowMake
      (varsKAbstraction (frameGetVars fr))
      (localStackKAbstraction (frameGetLocalStack fr))
      (frameGetPC fr).

  Definition frameKConcretisation (fr: TFrameKShadow): TFrame :=
    frameMake
      (varsKConcretisation (frameKShadowGetVars fr))
      (localStackKConcretisation (frameKShadowGetLocalStack fr))
      (frameKShadowGetPC fr).

  Axiom PframeKConcretisationAbstraction: ∀ frsh,
    frameKAbstraction (frameKConcretisation frsh) = frsh.

  Record TCurrentMethod: Set := cmMake {
    cmQName: TQualifiedMethodName;
    cmCurrentClass: TClassName;
    cmCtxObjectLoc: TLoc
  }.

  Definition cmDeclClass (cm: TCurrentMethod): TClassName :=
    fst (cmQName cm).

  Definition cmSignature (cm: TCurrentMethod): TSignature :=
    snd (cmQName cm).

  Definition TRichFrame :=
    TCurrentMethod × TFrame.

  Definition TEvalState := TLoc.

  Record TThread := threadMake {
    threadGetId: M_Heap.TThreadId;
    threadGetEvalState: TEvalState;
    threadGetCallStack: list TRichFrame
  }.

  Record TJVM := jvmMake {
    jvmGetHeap: M_Heap.THeap;
    jvmGetThreads: list TThread
  }.

  Inductive TResultOrException (A: Type): Type :=
  | Result (result: A)
  | Exception (cn: TClassName).
End RuntimeStructuresImpl.