Library CoqDefs

Require Import Utf8.

Require Import ZArith.
Require Import List.
Import ListNotations.
Require Import Bool.

Require Import Equalities.
Require Import FMapWeakList.
Require Import FMapFacts.

Definition ret {A : Type} (x : A) := Some x.
Definition bind {A B : Type} (a : option A) (f : A option B) :=
    match a with
    | NoneNone
    | Some xf x
    end.

Notation "a >>= f" := (bind a f) (at level 40, left associativity).

Module Languages (Var_as_DT : UsualDecidableTypeOrig).
  Module VarMap := FMapWeakList.Make(Var_as_DT).
  Module VarMapFacts := FMapFacts.WFacts_fun Var_as_DT VarMap.
  Module VarMapProps := FMapFacts.WProperties_fun Var_as_DT VarMap.

  Definition var := Var_as_DT.t.

Lvalues
  Inductive lvalue :=
    | Var : var lvalue
    | ArrayAccess : lvalue exp lvalue
  
Abstract syntax of expressions
  with exp :=
    | Lval : lvalue exp
    | Int : Z exp
    | Sum : exp exp exp
    | Diff : exp exp exp
    | Mult : exp exp exp
    | Div : exp exp exp.

  Scheme exp_mut := Induction for exp Sort Prop
  with lvalue_mut := Induction for lvalue Sort Prop.

  Fixpoint exp_beq (e e' : exp) : bool :=
    match e, e' with
    | Lval x, Lval yif lvalue_beq x y then true else false
    | Int n, Int n'Zeq_bool n n'
    | Sum e₁ e₂, Sum e₁' e₂' | Diff e₁ e₂, Diff e₁' e₂'
    | Mult e₁ e₂, Mult e₁' e₂'andb (exp_beq e₁ e₁') (exp_beq e₂ e₂')
    | _, _false
    end
  with lvalue_beq (x y : lvalue) : bool :=
    match x, y with
    | Var x, Var yif Var_as_DT.eq_dec x y then true else false
    | ArrayAccess x n, ArrayAccess y n'andb (lvalue_beq x y) (exp_beq n n')
    | _, _false
    end.

Abstract syntax of boolean expressions
  Inductive bexp :=
    | BTrue : bexp
    | BFalse : bexp
    | BAnd : bexp bexp bexp
    | BOr : bexp bexp bexp
    | BNot : bexp bexp
    | BLE : exp exp bexp
    | BGE : exp exp bexp
    | BLT : exp exp bexp
    | BGT : exp exp bexp
    | BEQ : exp exp bexp
    | BNEQ : exp exp bexp.

Abstract syntax of commands
  Inductive cmd_a :=
    | Skip | Break | Continue
    | Assign : lvalue exp cmd_a.

  Fixpoint cmda_beq (a a' : cmd_a) : bool :=
    match a, a' with
    | Skip, Skip | Continue, Continue | Break, Breaktrue
    | Assign x e, Assign y e'andb (lvalue_beq x y) (exp_beq e e')
    | _, _false
    end.

  Inductive cmd :=
    | Leaf : cmd_a cmd
    | Seq : cmd cmd cmd
    | While : bexp cmd cmd
    | IfThenElse : bexp cmd cmd cmd.

  Inductive value :=
    | IntValue : Z value
    | ArrayValue : list value value.
  Definition store := VarMap.t value.

  Definition z_to_nat (n : Z) : option nat :=
    match n with
    | Z0Some 0
    | Zpos pSome (Pos.to_nat p)
    | _None
    end.

  Fixpoint my_nth {A : Type} (n : nat) (l : list A) : option A :=
    match n, l with
    | O, x::_Some x
    | S n', _::l'my_nth n' l'
    | _, _None
    end.

  Property my_nth_implies_nth:
     {A} (l : list A) n (x : A), my_nth n l = Some x
     y, nth n l y = x.
  Proof.
    intros A l n. revert l. induction n ; intro l.
    × intros x H. simpl in H. destruct l.
      + discriminate H.
      + inversion_clear H. simpl. auto.
    × intros x H. destruct l.
      + discriminate H.
      + apply IHn. simpl in H. auto.
  Qed.

Interpretation of an expression e in a store s. Returns None if the expression could not be evaluated within this store. Returns Some v with v the result of the evaluation of e in s otherwise.
  Fixpoint interp_exp (e : exp) (s : store) : option Z :=
    match e with
    | Int nret n
    | Lval xread_lval x s >>= λ x, match x with
      | IntValue nSome n
      | _None
      end
    | Sum e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x + y)%Z
    | Diff e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x - y)%Z
    | Mult e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x × y)%Z
    | Div e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x / y)%Z
    end
  with read_lval (x : lvalue) (s : store) : option value :=
    match x with
    | Var xVarMap.find x s
    | ArrayAccess x n
      interp_exp n s >>= λ idx,
      read_lval x s >>= λ value,
      match value with
      | ArrayValue l
        z_to_nat idx >>= λ n,
        my_nth n l
      | _None
      end
    end.

  Fixpoint set_lval (x : lvalue) (v : value) (s : store) : option store :=
    match x with
    | Var xSome (VarMap.add x v s)
    | ArrayAccess x n
      interp_exp n s >>= λ idx,
      read_lval x s >>= λ value,
      match value with
      | ArrayValue l
        z_to_nat idx >>= λ n,
        let v' := (firstn n l) ++ [v] ++ (skipn (S n) l) in
        set_lval x (ArrayValue v') s
      | _None
      end
    end.

Interpretation of a boolean expression b in a store s. Returns None if the expression could not be evaluated within this store. Returns Some v with v the result of the evaluation of b in s otherwise.
  Fixpoint interp_bexp (b : bexp) (s : store) : option bool :=
    match b with
    | BTrueret true
    | BFalseret false
    | BAnd b₁ b₂
        interp_bexp b₁ s >>= λ x, interp_bexp b₂ s >>= λ y, ret (x && y)
    | BOr b₁ b₂
        interp_bexp b₁ s >>= λ x, interp_bexp b₂ s >>= λ y, ret (x || y)
    | BNot b
        interp_bexp b s >>= λ x, ret (negb x)
    | BLE e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.leb x y)
    | BGE e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.geb x y)
    | BLT e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.ltb x y)
    | BGT e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.gtb x y)
    | BEQ e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.eqb x y)
    | BNEQ e₁ e₂
        interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (negb (Z.eqb x y))
    end.

Execution mode used in the big-step semantics of the input language to denote the different TODO
  Inductive mode :=
    | MNormal
    | MBreak
    | MContinue.

Big-step semantics of the input language
  Inductive big_step : store cmd mode store Prop :=
    | j_assign : x e v s s',
      interp_exp e s = Some v
      set_lval x (IntValue v) s = Some s'
      big_step s (Leaf (Assign x e)) MNormal s'
    | j_skip : s,
      big_step s (Leaf Skip) MNormal s
    | j_seq_normal : s m c₁ s₁ c₂ s',
      big_step s c₁ MNormal s₁
      big_step s₁ c₂ m s'
      big_step s (Seq c₁ c₂) m s'
    | j_if_then : s m s' b c₁ c₂,
      interp_bexp b s = Some true
      big_step s c₁ m s'
      big_step s (IfThenElse b c₁ c₂) m s'
    | j_if_else : s m s' b c₁ c₂,
      interp_bexp b s = Some false
      big_step s c₂ m s'
      big_step s (IfThenElse b c₁ c₂) m s'
    | j_while_false : s b c,
      interp_bexp b s = Some false
      big_step s (While b c) MNormal s
    | j_while_true : s m s₁ s' b c₁,
      interp_bexp b s = Some true
      big_step s c₁ m s₁
      m MBreak
      big_step s₁ (While (b) c₁) MNormal s'
      big_step s (While (b) c₁) MNormal s'
    | j_seq_interrupt : s c₁ c₂ m s',
      m MNormal
      big_step s c₁ m s'
      big_step s (Seq c₁ c₂) m s'
    | j_while_break : s s₁ b c₁,
      interp_bexp b s = Some true
      big_step s c₁ MBreak s₁
      big_step s (While (b) c₁) MNormal s₁
    | j_break : s, big_step s (Leaf Break) MBreak s
    | j_continue : s, big_step s (Leaf Continue) MContinue s.

  Hint Constructors big_step.

  Inductive guard :=
    | ε : guard
    | S0 : guard guard
    | S1 : guard guard.

  Lemma eq_guard_dec:
     (x y : guard), { x = y } + {x y }.
  Proof.
    decide equality.
  Defined.

  Module guard_as_DT <: DecidableType.
    Definition t := guard.

    Definition eq := @eq guard.
    Definition eq_refl := @eq_refl t.
    Definition eq_sym := @eq_sym t.
    Definition eq_trans := @eq_trans t.
    Definition eq_dec := eq_guard_dec.
  End guard_as_DT.

  Module GuardMap := FMapWeakList.Make(guard_as_DT).
  Module GuardMapFacts := FMapFacts.WFacts_fun guard_as_DT GuardMap.
  Module GuardMapProps := FMapFacts.WProperties_fun guard_as_DT GuardMap.
  Definition gstore := GuardMap.t bool.

  Definition path := guard.

  Inductive path_suffix : path path Prop :=
    | suffix_eq : s, path_suffix s s
    | suffix_S0 : p s, path_suffix p s path_suffix (S0 p) s
    | suffix_S1 : p s, path_suffix p s path_suffix (S1 p) s.

  Hint Constructors path_suffix.

  Definition guard_conj := list (bool × guard).
  Definition guard_disj := list guard_conj.

  Inductive acmd_g :=
    | GAAssign : lvalue exp acmd_g
    | GAGAssign : guard bexp acmd_g.

  Inductive cmd_g :=
    | GSeq : cmd_g cmd_g cmd_g
    | GSkip : cmd_g
    | GWhile : guard_disj cmd_g cmd_g
    | GAtomic : guard_conj acmd_g cmd_g
    | GCPoint : cmd_g.

  Notation "A ; B" := (Seq A B)
    (at level 80, right associativity, format "A ; '//' B") : ast_scope.
  Notation "A ; B" := (GSeq A B)
    (at level 80, right associativity, format "A ; '//' B") : gast_scope.
  Delimit Scope ast_scope with AST.
  Delimit Scope gast_scope with GAST.

  Fixpoint interp_guard_conj G gl :=
    match gl with
    | []Some true
    | (b, π)::gl'GuardMap.find π G >>= λ v,
      if eqb v b then interp_guard_conj G gl' else Some false
    end.

  Definition guard_conj_evals_to G gl b :=
    interp_guard_conj G gl = Some b.

  Definition guard_disj_evals_to G cl b :=
    match b with
    | trueList.Exists (λ gl, guard_conj_evals_to G gl true) cl
    | falseList.Forall (λ gl, guard_conj_evals_to G gl false) cl
    end.

  Inductive big_step_g : store gstore cmd_g store gstore Prop :=
    | j_gatomic_false : a s gs l,
      guard_conj_evals_to gs l false
      big_step_g s gs (GAtomic l a) s gs
    | j_gassign : x e v s s' gs l,
      interp_exp e s = Some v
      set_lval x (IntValue v) s = Some s'
      guard_conj_evals_to gs l true
      big_step_g s gs (GAtomic l (GAAssign x e)) s' gs
    | j_ggassign : g b v s gs l,
      interp_bexp b s = Some v
      guard_conj_evals_to gs l true
      big_step_g s gs (GAtomic l (GAGAssign g b)) s (GuardMap.add g v gs)
    | j_gskip : s gs,
      big_step_g s gs GSkip s gs
    | j_gseq : s gs c₁ s₁ gs₁ c₂ s' gs',
      big_step_g s gs c₁ s₁ gs₁
      big_step_g s₁ gs₁ c₂ s' gs'
      big_step_g s gs (GSeq c₁ c₂) s' gs'
    | j_gwhile_false : s gs cl c,
      guard_disj_evals_to gs cl false
      big_step_g s gs (GWhile cl c) s gs
    | j_gwhile_true : s gs s₁ gs₁ s' gs' cl c₁,
      guard_disj_evals_to gs cl true
      big_step_g s gs c₁ s₁ gs₁
      big_step_g s₁ gs₁ (GWhile cl c₁) s' gs'
      big_step_g s gs (GWhile cl c₁) s' gs'
    | j_gcpoint : s gs,
      big_step_g s gs GCPoint s gs.


  Inductive cmd_diff :=
    | SeqDelL : cmd cmd_diff cmd_diff
    | SeqDelR : cmd_diff cmd cmd_diff
    | SeqInsL : cmd cmd_diff cmd_diff
    | SeqInsR : cmd_diff cmd cmd_diff
    | SeqMut : cmd_diff cmd_diff cmd_diff
    | IfMut : bexp × bexp cmd_diff cmd_diff cmd_diff
    | WhileMut : bexp × bexp cmd_diff cmd_diff
    | ITEAddIf : bexp cmd cmd_diff cmd_diff
    | ITEAddElse : bexp cmd_diff cmd cmd_diff
    | ITEDelIf : bexp cmd cmd_diff cmd_diff
    | ITEDelElse : bexp cmd_diff cmd cmd_diff
    | WhileAdd : bexp cmd_diff cmd_diff
    | WhileDel : bexp cmd_diff cmd_diff
    
    | LeafSubst : cmd_a cmd_a cmd_diff
    
    | CPoint : cmd_diff cmd_diff.

  Fixpoint Π₀ (cd : cmd_diff) : cmd :=
    match cd with
    | SeqDelL c cd ⇒ (c ; (Π₀ cd))%AST
    | SeqDelR cd c ⇒ ((Π₀ cd) ; c)%AST
    | SeqInsL _ cΠ₀ c
    | SeqInsR c _Π₀ c
    | SeqMut c c' ⇒ ((Π₀ c) ; (Π₀ c'))%AST
    | IfMut (b, _) c c'IfThenElse b (Π₀ c) (Π₀ c')
    | WhileMut (b, _) cWhile b (Π₀ c)
    | ITEAddIf _ _ c'Π₀ c'
    | ITEAddElse _ c _Π₀ c
    | ITEDelIf b c c'IfThenElse b c (Π₀ c')
    | ITEDelElse b c c'IfThenElse b (Π₀ c) c'
    | WhileAdd b cΠ₀ c
    | WhileDel b cWhile b (Π₀ c)
    
    | LeafSubst a _Leaf a
    
    | CPoint cdΠ₀ cd
    end.

  Fixpoint Π₁ (cd : cmd_diff) : cmd :=
    match cd with
    | SeqDelL c cd ⇒ (Π₁ cd)
    | SeqDelR cd c ⇒ (Π₁ cd)
    | SeqInsL c cd ⇒ (c ; (Π₁ cd))%AST
    | SeqInsR cd c' ⇒ ((Π₁ cd) ; c')%AST
    | SeqMut c c' ⇒ ((Π₁ c) ; (Π₁ c'))%AST
    | IfMut (_, b') c c'IfThenElse b' (Π₁ c) (Π₁ c')
    | WhileMut (_, b') cWhile b' (Π₁ c)
    | ITEAddIf b c c'IfThenElse b c (Π₁ c')
    | ITEAddElse b c c'IfThenElse b (Π₁ c) c'
    | ITEDelIf _ _ c'Π₁ c'
    | ITEDelElse _ c _Π₁ c
    | WhileAdd b cWhile b (Π₁ c)
    | WhileDel b cΠ₁ c
    
    | LeafSubst _ aLeaf a
    
    | CPoint cdΠ₁ cd
    end.

  Definition tag_store t (s : store) :=
    VarMap.fold (λ k v acc, VarMap.add (t k) v acc) s (VarMap.empty _).

  Definition store_included_tagged t (s s' : store) :=
     x v, VarMap.MapsTo x v s VarMap.MapsTo (t x) v s'.

  Definition join_stores t t' S₀ S₁ :=
    VarMapProps.update (tag_store t S₀) (tag_store t' S₁).

  Definition cp_algorithm_sound t t' correlating_program :=
     S₀ S₀' S₁ S₁' cd,
    big_step S₀ (Π₀ cd) MNormal S₀'
    big_step S₁ (Π₁ cd) MNormal S₁'
     G, S' G',
    big_step_g (join_stores t t' S₀ S₁) G (correlating_program cd) S' G'
     store_included_tagged t S₀' S' store_included_tagged t' S₁' S'.
End Languages.