Module Qcert.NNRC.Lang.NNRCSize


Section NNRCSize.
  Require Import String.
  Require Import Omega.
  Require Import EquivDec.
  Require Import Decidable.
  Require Import Utils.
  Require Import CommonRuntime.
  Require Import cNNRC.
  Require Import cNNRCShadow.

  Context {fruntime:foreign_runtime}.

  Fixpoint nnrc_size (n:nnrc) : nat
    := match n with
       | NNRCGetConstant v => 1
       | NNRCVar v => 1
       | NNRCConst d => 1
       | NNRCBinop op nn₂ => S (nnrc_size n₁ + nnrc_size n₂)
       | NNRCUnop op n₁ => S (nnrc_size n₁)
       | NNRCLet v nn₂ => S (nnrc_size n₁ + nnrc_size n₂)
       | NNRCFor v nn₂ => S (nnrc_size n₁ + nnrc_size n₂)
       | NNRCIf nnn₃ => S (nnrc_size n₁ + nnrc_size n₂ + nnrc_size n₃)
       | NNRCEither nd vl nl vr nr => S (nnrc_size nd + nnrc_size nl + nnrc_size nr)
       | NNRCGroupBy g sl n => S (nnrc_size n)
       end.

  Lemma nnrc_size_nzero (n:nnrc) : nnrc_size n <> 0.
Proof.
    induction n; simpl; omega.
  Qed.

  Lemma nnrc_rename_lazy_size n x1 x2:
    nnrc_size (nnrc_rename_lazy n x1 x2) = nnrc_size n.
Proof.
    nnrc_cases (induction n) Case;
    unfold nnrc_rename_lazy in *;
    simpl;
    destruct (equiv_dec x1 x2);
    simpl;
    try reflexivity;
    try solve [ rewrite IHn1;
                rewrite IHn2;
                rewrite IHn3;
                reflexivity ];
    try solve [ rewrite IHn1;
                rewrite IHn2;
                reflexivity ];
    try solve [ rewrite IHn;
                reflexivity ];
    try solve [ rewrite IHn1;
                destruct (equiv_dec v x1);
                simpl; try reflexivity;
                rewrite IHn2;
                reflexivity ].
    - Case "NNRCVar"%string.
      destruct (equiv_dec v x1);
        simpl; reflexivity.
    - Case "NNRCEither"%string.
      rewrite IHn1.
      destruct (equiv_dec v x1);
        destruct (equiv_dec v0 x1);
        simpl; try reflexivity.
      + rewrite IHn3.
        reflexivity.
      + rewrite IHn2.
        reflexivity.
      + rewrite IHn2.
        rewrite IHn3.
        reflexivity.
  Qed.

End NNRCSize.