Module Qcert.Imp.Lang.ImpEJsonSize

Require Import String.
Require Import Lia.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import EJsonRuntime.
Require Import Imp.
Require Import ImpSize.
Require Import ImpEJson.

Section ImpEJsonSize.
  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 imp_ejson_expr_size (e:@imp_ejson_expr foreign_ejson_model foreign_ejson_runtime_op) : nat :=
    imp_expr_size e.

  Definition imp_ejson_stmt_size (stmt:@imp_ejson_stmt foreign_ejson_model foreign_ejson_runtime_op) : nat :=
    imp_stmt_size stmt.

  Definition imp_ejson_function_size (q:@imp_ejson_function foreign_ejson_model foreign_ejson_runtime_op) : nat :=
    imp_function_size q.

  Definition imp_ejson_size (q: @imp_ejson foreign_ejson_model foreign_ejson_runtime_op) : nat :=
    imp_size q.

End ImpEJsonSize.