Module Qcert.NNRS.Lang.NNRSSize

Require Import String.
Require Import Lia.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import NNRS.

Section NNRSSize.
  Context {fruntime:foreign_runtime}.

  Fixpoint nnrs_expr_size (n:nnrs_expr) : nat
    := match n with
       | NNRSGetConstant v => 1
       | NNRSVar v => 1
       | NNRSConst d => 1
       | NNRSBinop op n₁ n₂ => S (nnrs_expr_size n₁ + nnrs_expr_size n₂)
       | NNRSUnop op n₁ => S (nnrs_expr_size n₁)
       | NNRSGroupBy g sl e => S (nnrs_expr_size e)
       end.

    Fixpoint nnrs_stmt_size (n:nnrs_stmt) : nat
    := match n with
       | NNRSSeq s₁ s₂ => S (nnrs_stmt_size s₁ + nnrs_stmt_size s₂)
       | NNRSLet v e s => S (nnrs_expr_size e + nnrs_stmt_size s)
       | NNRSLetMut v eo s => S (nnrs_stmt_size s + nnrs_stmt_size s)
       | NNRSLetMutColl _ s₁ s₂ => S (nnrs_stmt_size s₁ + nnrs_stmt_size s₂)
       | NNRSAssign _ e => S (nnrs_expr_size e)
       | NNRSPush _ e => S (nnrs_expr_size e)
       | NNRSFor v n₁ n₂ => S (nnrs_expr_size n₁ + nnrs_stmt_size n₂)
       | NNRSIf n₁ n₂ n₃ => S (nnrs_expr_size n₁ + nnrs_stmt_size n₂ + nnrs_stmt_size n₃)
       | NNRSEither nd vl nl vr nr => S (nnrs_expr_size nd + nnrs_stmt_size nl + nnrs_stmt_size nr)
       end.

    Definition nnrs_size (q:nnrs) : nat :=
      let (n, v) := q in
      nnrs_stmt_size n.

    Lemma nnrs_expr_size_nzero (n:nnrs_expr) : nnrs_expr_size n <> 0.

    Lemma nnrs_stmt_size_nzero (n:nnrs_stmt) : nnrs_stmt_size n <> 0.

    Corollary nnrs_size_nzero (q:nnrs) : nnrs_size q <> 0.

    Section Core.
      Program Definition nnrs_core_size (q:nnrs_core) : nat
        := nnrs_size q.

      Lemma nnrs_core_size_nzero (q:nnrs_core) :
        nnrs_core_size q <> 0.
    End Core.

End NNRSSize.