Module Qcert.NNRSimp.Optim.NNRSimpOptimizerEngine

Require Import String.
Require Import List.
Require Import ListSet.
Require Import Arith.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import NNRSimpSystem.

Section NNRSimpOptimizerEngine.
  Local Open Scope nnrs_imp.
  Local Open Scope string.

  Section map.
    Context {fruntime:foreign_runtime}.

    Fixpoint nnrs_imp_expr_map_deep
             (fe : nnrs_imp_expr -> nnrs_imp_expr)
             (e:nnrs_imp_expr) : nnrs_imp_expr
      := match e with
         | NNRSimpGetConstant v =>
           fe (NNRSimpGetConstant v)
         | NNRSimpVar v =>
           fe (NNRSimpVar v)
         | NNRSimpConst d =>
           fe (NNRSimpConst d)
         | NNRSimpBinop bop e1 e2 =>
           fe (NNRSimpBinop bop
                            (nnrs_imp_expr_map_deep fe e1)
                            (nnrs_imp_expr_map_deep fe e2))
         | NNRSimpUnop uop e1 =>
           fe (NNRSimpUnop uop
                           (nnrs_imp_expr_map_deep fe e1))
         | NNRSimpGroupBy g sl e1 =>
           fe (NNRSimpGroupBy g sl
                              (nnrs_imp_expr_map_deep fe e1))
         end.

    Fixpoint nnrs_imp_stmt_map_deep
             (fe : nnrs_imp_expr -> nnrs_imp_expr)
             (fs : nnrs_imp_stmt -> nnrs_imp_stmt)
             (s:nnrs_imp_stmt) : nnrs_imp_stmt
      := match s with
         | NNRSimpSkip => fs NNRSimpSkip
         | NNRSimpSeq s₁ s₂ =>
           fs (NNRSimpSeq
                 (nnrs_imp_stmt_map_deep fe fs s₁)
                 (nnrs_imp_stmt_map_deep fe fs s₂))
         | NNRSimpAssign v e =>
           fs (NNRSimpAssign v
                             (nnrs_imp_expr_map_deep fe e))
         | NNRSimpLet v None s₀ =>
           let s_opt := nnrs_imp_stmt_map_deep fe fs s₀ in
           let s_maybeopt :=
               if VarUsage_dec (nnrs_imp_stmt_var_usage s₀ v) VarMayBeUsedWithoutAssignment then
                 s_opt
               else
                 if VarUsage_dec (nnrs_imp_stmt_var_usage s_opt v) VarMayBeUsedWithoutAssignment
                 then s₀
                 else s_opt in
           fs (NNRSimpLet v None s_maybeopt)
         | NNRSimpLet v (Some e) s₀ =>
           fs (NNRSimpLet v
                          (Some (nnrs_imp_expr_map_deep fe e))
                          (nnrs_imp_stmt_map_deep fe fs s₀))
         | NNRSimpFor v e s₀ =>
           fs (NNRSimpFor v
                          (nnrs_imp_expr_map_deep fe e)
                          (nnrs_imp_stmt_map_deep fe fs s₀))
         | NNRSimpIf e s₁ s₂ =>
           fs (NNRSimpIf
                 (nnrs_imp_expr_map_deep fe e)
                 (nnrs_imp_stmt_map_deep fe fs s₁)
                 (nnrs_imp_stmt_map_deep fe fs s₂))
         | NNRSimpEither e x₁ s₁ x₂ s₂ =>
           fs (NNRSimpEither
                 (nnrs_imp_expr_map_deep fe e)
                 x₁
                 (nnrs_imp_stmt_map_deep fe fs s₁)
                 x₂
                 (nnrs_imp_stmt_map_deep fe fs s₂))
         end.

    Definition nnrs_imp_map_deep
               (fe : nnrs_imp_expr -> nnrs_imp_expr)
               (fs : nnrs_imp_stmt -> nnrs_imp_stmt)
               (fsi : nnrs_imp -> nnrs_imp)
               (si:nnrs_imp) : nnrs_imp
      :=
        let s_opt := nnrs_imp_stmt_map_deep fe fs (fst si) in
        let s_maybeopt :=
            if VarUsage_dec (nnrs_imp_stmt_var_usage (fst si) (snd si)) VarMayBeUsedWithoutAssignment then
              s_opt
            else
              if VarUsage_dec (nnrs_imp_stmt_var_usage s_opt (snd si)) VarMayBeUsedWithoutAssignment
              then fst si
              else s_opt in
        fsi (s_maybeopt, snd si).

  End map.

  Section correct_untyped.
    Context {fruntime:foreign_runtime}.
    
    Lemma nnrs_imp_expr_map_deep_eq_correctness
          (fe : nnrs_imp_expr -> nnrs_imp_expr)
          (e : nnrs_imp_expr) :
      (forall e', fe e' ≡ᵉ e') -> nnrs_imp_expr_map_deep fe e ≡ᵉ e.

    Lemma nnrs_imp_stmt_map_deep_eq_correctness
          (fe : nnrs_imp_expr -> nnrs_imp_expr)
          (fs : nnrs_imp_stmt -> nnrs_imp_stmt)
          (s : nnrs_imp_stmt) :
      (forall e', fe e' ≡ᵉ e') ->
      (forall s', fs s' ≡ˢ s') ->
      nnrs_imp_stmt_map_deep fe fs s ≡ˢ s.

    Lemma nnrs_imp_map_deep_eq_correctness
          (fe : nnrs_imp_expr -> nnrs_imp_expr)
          (fs : nnrs_imp_stmt -> nnrs_imp_stmt)
          (fsi : nnrs_imp -> nnrs_imp)
          (si : nnrs_imp) :
      (forall e', fe e' ≡ᵉ e') ->
      (forall s', fs s' ≡ˢ s') ->
      (forall si', fsi si' ≡ˢⁱ si') ->
      nnrs_imp_map_deep fe fs fsi si ≡ˢⁱ si.

  End correct_untyped.

  Section correct_typed.
    Context {model:basic_model}.

    Lemma nnrs_imp_expr_map_deep_trew_correctness
          (fe : nnrs_imp_expr -> nnrs_imp_expr)
          (e : nnrs_imp_expr) :
      (forall e', e' ⇒ᵉ fe e') -> e ⇒ᵉ nnrs_imp_expr_map_deep fe e.

    Lemma nnrs_imp_stmt_map_deep_trew_correctness
          (fe : nnrs_imp_expr -> nnrs_imp_expr)
          (fs : nnrs_imp_stmt -> nnrs_imp_stmt)
          (s : nnrs_imp_stmt) :
      (forall e', e' ⇒ᵉ fe e') ->
      (forall s', s' ⇒ˢ fs s') ->
      s ⇒ˢ nnrs_imp_stmt_map_deep fe fs s.

    Lemma nnrs_imp_map_deep_trew_correctness
          (fe : nnrs_imp_expr -> nnrs_imp_expr)
          (fs : nnrs_imp_stmt -> nnrs_imp_stmt)
          (fsi : nnrs_imp -> nnrs_imp)
          (si : nnrs_imp) :
      (forall e', e' ⇒ᵉ fe e') ->
      (forall s', s' ⇒ˢ fs s') ->
      (forall si', si' ⇒ˢⁱ fsi si') ->
      si ⇒ˢⁱ nnrs_imp_map_deep fe fs fsi si.

  End correct_typed.
  
End NNRSimpOptimizerEngine.

Ltac tcorrectness_prover :=
  simpl; repeat progress
                (try match goal with
                     | [|- context [match ?p with | _ => _ end] ] => destruct p
                     end; try reflexivity; try unfold Equivalence.equiv in *; try subst).

Ltac tprove_correctness p :=
  destruct p;
  tcorrectness_prover.