Module Qcert.Imp.Optim.ImpEJsonOptimizer

Require Import String.
Require Import EJsonRuntime.
Require Import Imp.
Require Import ImpEJson.
Require Import ImpEJsonEval.
Require Import ImpEJsonOptimizerEngine.
Require Import ImpEJsonRewrite.

Section ImpEJsonOptimizer.
  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}.

  Definition nooptims (q:@imp_ejson_stmt foreign_ejson_model foreign_ejson_runtime_op) := q.
  Lemma nooptims_correct h s j:
    imp_ejson_stmt_eval h s j = imp_ejson_stmt_eval h (nooptims s) j.

  Definition imp_ejson_optim_top (q:@imp_ejson foreign_ejson_model foreign_ejson_runtime_op) : imp_ejson :=
    imp_ejson_block_rewrite
      nooptims
      q.

  Section Correctness.
    Lemma imp_ejson_optim_top_correct h (σ : list (string * ejson)) (q:imp_ejson) :
        imp_ejson_eval_top_on_ejson h σ q =
        imp_ejson_eval_top_on_ejson h σ (imp_ejson_optim_top q).
      
  End Correctness.
End ImpEJsonOptimizer.