Module Qcert.Imp.Optim.ImpEJsonRewrite

Require Import String.
Require Import List.
Require Import Bool.
Require Import Arith.
Require Import ZArith.
Require Import Utils.
Require Import JsAst.JsNumber.
Require Import EJsonRuntime.
Require Import Imp.
Require Import ImpEJson.
Require Import ImpEJsonVars.
Require Import ImpEJsonEval.

Section ImpEJsonRewrite.
  Import ListNotations.

  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.
  Context {foreign_ejson_runtime_op : Set}.
  Context {fejruntime:foreign_ejson_runtime foreign_ejson_runtime_op}.

  Section ForLetRewrite.

    Definition imp_ejson_stmt_for_let_rewrite (stmt: @imp_ejson_stmt foreign_ejson_model foreign_ejson_runtime_op): imp_ejson_stmt :=
      match stmt with
      | ImpStmtFor v e s =>
        let avoid := v :: imp_ejson_stmt_free_vars s in
        let src_id := fresh_var "src" avoid in
        let src := ImpExprVar src_id in
        ImpStmtBlock
          [ (src_id, Some e) ]
          [ ImpStmtFor v src s ]
      | _ => stmt
      end.

  End ForLetRewrite.

  Section CorrectnessForLetRewrite.

    Lemma lookup_first_var A (i0 : A) (v:var) σ :
      lookup EquivDec.equiv_dec ((v, i0) :: σ) v = Some i0.

    Lemma test1 h stmt v j σ σ':
      imp_ejson_stmt_eval h stmt
        ((fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), j) :: σ) = Some ((fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), j) :: σ') ->
      imp_ejson_stmt_eval h stmt σ = Some σ'.

    Lemma test2 h stmt x1 v j σ:
      imp_ejson_stmt_eval h stmt
        (x1 :: (fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), Some j) :: σ) = None <->
      imp_ejson_stmt_eval h stmt (x1 :: σ) = None.

    Lemma test3 h stmt v l σ σ' i0 :
      (fix for_fun
           (dl : list imp_ejson_model) (σ₁ : list (var * option imp_ejson_model)) {struct dl} :
         option (list (var * option imp_ejson_model)) :=
         match dl with
         | [] => Some σ₁
         | d :: dl' =>
           match imp_ejson_stmt_eval h stmt ((v, Some d) :: σ₁) with
           | Some (_ :: σ₂) => for_fun dl' σ₂
           | _ => None
           end
         end) l σ = Some σ' ->
      (fix for_fun
       (dl : list imp_ejson_model) (σ₁ : list (var * option imp_ejson_model)) {struct dl} :
         option (list (var * option imp_ejson_model)) :=
       match dl with
       | [] => Some σ₁
       | d :: dl' =>
           match imp_ejson_stmt_eval h stmt ((v, Some d) :: σ₁) with
           | Some (_ :: σ₂) => for_fun dl' σ₂
           | _ => None
           end
       end) l ((fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), Some i0) :: σ) = Some ((fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), Some i0) :: σ').

    Lemma test4 h stmt v l σ i0 :
      (fix for_fun
           (dl : list imp_ejson_model) (σ₁ : list (var * option imp_ejson_model)) {struct dl} :
         option (list (var * option imp_ejson_model)) :=
         match dl with
         | [] => Some σ₁
         | d :: dl' =>
           match imp_ejson_stmt_eval h stmt ((v, Some d) :: σ₁) with
           | Some (_ :: σ₂) => for_fun dl' σ₂
           | _ => None
           end
         end) l σ = None ->
      (fix for_fun
       (dl : list imp_ejson_model) (σ₁ : list (var * option imp_ejson_model)) {struct dl} :
         option (list (var * option imp_ejson_model)) :=
       match dl with
       | [] => Some σ₁
       | d :: dl' =>
           match imp_ejson_stmt_eval h stmt ((v, Some d) :: σ₁) with
           | Some (_ :: σ₂) => for_fun dl' σ₂
           | _ => None
           end
       end) l ((fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), Some i0) :: σ) = None.

    Lemma test5 h stmt v i0 i1 σ:
      imp_ejson_stmt_eval h stmt ((v, Some i1) :: σ) = None ->
      imp_ejson_stmt_eval h stmt
                          ((v, Some i1) :: (fresh_var "src" (v :: imp_ejson_stmt_free_vars stmt), Some i0) :: σ) = None.
    
    Lemma imp_ejson_stmt_for_let_rewrite_correct h (σ : pd_jbindings) (stmt:imp_ejson_stmt) :
        imp_ejson_stmt_eval h stmt σ =
        imp_ejson_stmt_eval h (imp_ejson_stmt_for_let_rewrite stmt) σ.

  End CorrectnessForLetRewrite.

  Section ForRewrite.

    Definition imp_ejson_stmt_for_rewrite (stmt: @imp_ejson_stmt foreign_ejson_model foreign_ejson_runtime_op): imp_ejson_stmt :=
      match stmt with
      | ImpStmtFor v (ImpExprVar src_id) s =>
        let avoid := imp_ejson_stmt_free_vars stmt in
        let i_id := fresh_var "i" avoid in
        let avoid := i_id :: avoid in
        let i := ImpExprVar i_id in
        ImpStmtForRange
          i_id
          (ImpExprConst (cejbigint 0))
          (ImpExprRuntimeCall
             EJsonRuntimeNatMinus [
               ImpExprRuntimeCall EJsonRuntimeArrayLength [ (ImpExprVar src_id) ]; ImpExprConst (cejbigint 1)
          ])
          (ImpStmtBlock
             [ (v, Some (ImpExprRuntimeCall EJsonRuntimeArrayAccess [ (ImpExprVar src_id); i ])) ]
             [ s ])
      | _ => stmt
      end.
  End ForRewrite.

  Section CorrectnessForRewrite.

    Lemma number_iterations A (l: list A):
      (ImpEval.nb_iter 0 (BinInt.Z.sub (BinInt.Z.of_nat (List.length l)) 1)) = length l.

    Fixpoint list_n_nat {A} (n:nat) (l:list A) :=
      match n with
      | 0 => nil
      | S n' =>
        match l with
        | nil => nil
        | x :: l' => x :: (list_n_nat n' l')
        end
      end.

    Definition list_tail_n_nat {A} n (l: list A) :=
      List.rev (list_n_nat n (List.rev l)).

    Lemma imp_ejson_stmt_for_rewrite_correct h (σ : pd_jbindings) (stmt:imp_ejson_stmt) :
        imp_ejson_stmt_eval h stmt σ =
        imp_ejson_stmt_eval h (imp_ejson_stmt_for_rewrite stmt) σ.

  End CorrectnessForRewrite.

End ImpEJsonRewrite.