Library OracleLanguages.Imp.Syntax

Require Import Common.
Require Export ZArith.
Require Export FMapWeakList.
Require Export FMapFacts.

Module Imp (Var_as_DT : UsualDecidableTypeOrig).
  Module M := FMapWeakList.Make(Var_as_DT).
  Module MProps := FMapFacts.WProperties_fun Var_as_DT M.
  Module MFacts := MProps.F.

  Definition varid := Var_as_DT.t.

  Inductive exp :=
      | Var : varid → exp
      | Int : Z → exp
      | Sum : exp → exp → exp
      | Mult : exp → exp → exp
      | Sub : exp → exp → exp
      | Div : exp → exp → exp
      | Modulo : exp → exp → exp.

  Fixpoint In_exp_var (x : varid) (e : exp) : Prop :=
    match e with
      | Var y ⇒
        x = y
      | Int _ ⇒
        False
      | Sum e₁ e₂ | Mult e₁ e₂ | Sub e₁ e₂ | Div e₁ e₂ | Modulo e₁ e₂ ⇒
        In_exp_var x e₁ ∨ In_exp_var x e₂
    end.

  Fixpoint In_exp_div (div : exp) (e : exp) : Prop :=
    match e with
      | Var _ | Int _ ⇒
        False
      | Sum e₁ e₂ | Mult e₁ e₂ | Sub e₁ e₂ ⇒
        In_exp_div div e₁ ∨ In_exp_div div e₂
      | Div e₁ e₂ | Modulo e₁ e₂ ⇒
        e₂ = div ∨ In_exp_div div e₁ ∨ In_exp_div div e₂
    end.

  Lemma exp_eq_dec:
    ∀ (e₁ e₂ : exp), { e₁ = e₂ } + { e₁ ≠ e₂ }.

  Lemma In_exp_var_dec:
    ∀ x e, {In_exp_var x e} + {¬ In_exp_var x e}.

  Lemma In_exp_div_dec:
    ∀ d e, {In_exp_div d e} + {¬ In_exp_div d e}.

  Definition beq_exp (e₁ e₂ : exp) : bool :=
    if exp_eq_dec e₁ e₂ then true else false.

  Property beq_exp_reflx:
    ∀ e, beq_exp e e = true.

  Inductive bexp :=
      | True | False
      | EQ : exp → exp → bexp
      | LT : exp → exp → bexp
      | LE : exp → exp → bexp
      | EQB : bexp → bexp → bexp
      | AND : bexp → bexp → bexp
      | OR : bexp → bexp → bexp
      | NOT : bexp → bexp.

  Fixpoint In_bexp_var (x : varid) (b : bexp) : Prop :=
    match b with
      | True | False ⇒
        Logic.False
      | EQ e₁ e₂ | LT e₁ e₂ | LE e₁ e₂ ⇒
        In_exp_var x e₁ ∨ In_exp_var x e₂
      | AND b₁ b₂ | OR b₁ b₂ | EQB b₁ b₂ ⇒
        In_bexp_var x b₁ ∨ In_bexp_var x b₂
      | NOT b ⇒
        In_bexp_var x b
    end.

  Fixpoint In_bexp_div (div : exp) (b : bexp) : Prop :=
    match b with
      | True | False ⇒
        Logic.False
      | EQ e₁ e₂ | LT e₁ e₂ | LE e₁ e₂ ⇒
        In_exp_div div e₁ ∨ In_exp_div div e₂
      | AND b₁ b₂ | OR b₁ b₂ | EQB b₁ b₂ ⇒
        In_bexp_div div b₁ ∨ In_bexp_div div b₂
      | NOT b ⇒
        In_bexp_div div b
    end.

  Lemma bexp_eq_dec:
    ∀ (b₁ b₂ : bexp), { b₁ = b₂ } + { b₁ ≠ b₂ }.

  Lemma In_bexp_var_dec:
    ∀ x b, {In_bexp_var x b} + {¬ In_bexp_var x b}.

  Lemma In_bexp_div_dec:
    ∀ e b, {In_bexp_div e b} + {¬ In_bexp_div e b}.

  Definition beq_bexp (b₁ b₂ : bexp) : bool :=
    if bexp_eq_dec b₁ b₂ then true else false.

  Inductive cmd :=
      | Skip
      | Seq : cmd → cmd → cmd
      | Assign : varid → exp → cmd
      | ITE : bexp → cmd → cmd → cmd
      | While : bexp → cmd → cmd
      | Assert : bexp → cmd.

  Fixpoint In_var (x : varid) (c : cmd) :=
    match c with
      | Skip ⇒ Logic.False
      | Seq c₁ c₂ ⇒ In_var x c₁ ∨ In_var x c₂
      | Assign y e ⇒ x = y ∨ In_exp_var x e
      | ITE b c₁ c₂ ⇒ In_bexp_var x b ∨ In_var x c₁ ∨ In_var x c₂
      | While b c' ⇒ In_bexp_var x b ∨ In_var x c'
      | Assert b ⇒ In_bexp_var x b
    end.

  Lemma In_var_dec:
    ∀ x c, {In_var x c} + {¬ In_var x c}.

  Lemma cmd_eq_dec:
    ∀ (c₁ c₂ : cmd), { c₁ = c₂ } + { c₁ ≠ c₂}.

  Definition beq_cmd (c₁ c₂ : cmd) : bool :=
    if cmd_eq_dec c₁ c₂ then true else false.

  Property beq_cmd_reflx:
    ∀ c, beq_cmd c c = true.

  Property beq_cmd_true_iff:
    ∀ c₁ c₂, beq_cmd c₁ c₂ = true ↔ c₁ = c₂.

  Property beq_cmd_false_iff:
    ∀ c₁ c₂, beq_cmd c₁ c₂ = false ↔ c₁ ≠ c₂.

  Hint Rewrite beq_cmd_reflx : cmd.

  Definition store := M.t Z.

  Definition store_equal (s₁ s₂ : store) :=
    M.equal Z.eqb s₁ s₂.

  Lemma store_equal_true_iff:
    ∀ (s₁ s₂ : store), store_equal s₁ s₂ = true ↔ M.Equal s₁ s₂.

  Lemma store_Equal_dec:
  
    ∀ (s₁ s₂ : store), {M.Equal s₁ s₂} + {¬ M.Equal s₁ s₂}.

  Fixpoint eval_exp (s : store) (e : exp) : option Z :=
    match e with
    | Int n ⇒ ret n
    | Var x ⇒ M.find x s
    | Sum e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y, ret (x + y)%Z
    | Sub e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y, ret (x - y)%Z
    | Mult e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y, ret (x × y)%Z
    | Div e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y,
      match y with
      | Z0 ⇒ None
      | _ ⇒ ret (Z.div x y)
      end
    | Modulo e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y,
      match y with
      | Z0 ⇒ None
      | _ ⇒ ret (Z.modulo x y)
      end
    end.

  Lemma store_equal_eval_exp:
    ∀ e s₁ s₂, M.Equal s₁ s₂ → eval_exp s₁ e = eval_exp s₂ e.

  Fixpoint eval_bexp (s : store) (b : bexp) : option bool :=
    match b with
    | True ⇒ ret true
    | False ⇒ ret false
    | EQ e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y, ret (Z.eqb x y)
    | LT e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y, ret (Z.ltb x y)
    | LE e₁ e₂ ⇒ eval_exp s e₁ >>= λ x, eval_exp s e₂ >>= λ y, ret (Z.leb x y)
    | EQB b₁ b₂ ⇒ eval_bexp s b₁ >>= λ x, eval_bexp s b₂ >>= λ y, ret (eqb x y)
    | AND b₁ b₂ ⇒
      eval_bexp s b₁ >>= λ x,
      if x then
        eval_bexp s b₂
      else
        ret false
    | OR b₁ b₂ ⇒
      eval_bexp s b₁ >>= λ x,
      if x then
        ret true
      else
        eval_bexp s b₂
    | NOT b ⇒ eval_bexp s b >>= λ x, ret (negb x)
    end.

  Lemma store_equal_eval_bexp:
    ∀ b s₁ s₂, M.Equal s₁ s₂ → eval_bexp s₁ b = eval_bexp s₂ b.

  Module Notations.
    Notation "a + b" := (Sum a b)
      (at level 50, left associativity) : ast_scope.
    Notation "a - b" := (Sub a b)
      (at level 50, left associativity) : ast_scope.
    Notation "a / b" := (Div a b)
      (at level 40, left associativity) : ast_scope.
    Notation "a * b" := (Mult a b)
      (at level 40, left associativity) : ast_scope.
    Notation "a '%' b" := (Modulo a b)
      (at level 40, left associativity) : ast_scope.

    Notation "a == b" := (EQ a b)
      (at level 70, no associativity) : ast_scope.
    Notation "a < b" := (LT a b)
      (at level 70, no associativity) : ast_scope.
    Notation "a ≤ b" := (LE a b)
      (at level 70, no associativity) : ast_scope.
    Notation "a || b" := (OR a b)
      (at level 50, left associativity) : ast_scope.
    Notation "a && b" := (AND a b)
      (at level 40, left associativity) : ast_scope.
    Notation "¬ b" := (NOT b)
      (at level 75, right associativity) : ast_scope.

    Notation "x ← e" := (Assign x e)
                          (at level 80, no associativity) : ast_scope.
    Notation "{ x ; y ; .. ; z }" := (Seq x (Seq y .. (Seq z Skip) ..)) : ast_scope.
    Notation "'IF' b 'THEN' c₁ 'ELSE' c₂" := (ITE b c₁ c₂) (at level 200) : ast_scope.
    Notation "'WHILE' b 'DO' c" := (While b c) (at level 200) : ast_scope.

    Delimit Scope ast_scope with AST.
  End Notations.
End Imp.