Module Qcert.Imp.Lang.ImpSize

Require Import String.
Require Import Lia.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import Imp.

Section ImpSize.

  Context {Model: Set}.
  Context {Op: Set}.
  Context {Runtime: Set}.

  Definition imp_expr := @Imp.imp_expr Model Op Runtime.
  Definition imp_stmt := @Imp.imp_stmt Model Op Runtime.
  Definition imp_function := @Imp.imp_function Model Op Runtime.
  Definition imp := @Imp.imp Model Op Runtime.


  Fixpoint imp_expr_size (e:imp_expr) : nat
    := match e with
       | ImpExprError v => 1
       | ImpExprVar v => 1
       | ImpExprConst v => 1
       | ImpExprOp op l => S (List.fold_left (fun acc e => acc + imp_expr_size e ) l 0)
       | ImpExprRuntimeCall f args => S (List.fold_left (fun acc e => acc + imp_expr_size e) args 0)
       end.

    Fixpoint imp_stmt_size (stmt:imp_stmt) : nat
      := match stmt with
         | ImpStmtBlock decls stmts =>
           S (List.fold_left
                (fun acc (decl: var * option imp_expr) =>
                   let (x, eopt) := decl in
                   acc + match eopt with
                         | None => 1
                         | Some e => 1 + imp_expr_size e
                         end)
                decls
                (List.fold_left
                   (fun acc s => acc + imp_stmt_size s)
                   stmts 0))
         | ImpStmtAssign x e => 1 + imp_expr_size e
         | ImpStmtFor i e s => 1 + imp_expr_size e + imp_stmt_size s
         | ImpStmtForRange i e1 e2 s =>
           1 + imp_expr_size e1 + imp_expr_size e2 + imp_stmt_size s
         | ImpStmtIf e s1 s2 =>
           1 + imp_expr_size e + imp_stmt_size s1 + imp_stmt_size s2
         end.

    Definition imp_function_size (q:imp_function) : nat :=
      match q with
      | ImpFun args s ret => imp_stmt_size s
      end.

    Definition imp_size (q: imp) : nat :=
      match q with
      | ImpLib l =>
        List.fold_left
          (fun acc (decl: string * imp_function) =>
             let (fname, fdef) := decl in acc + imp_function_size fdef)
          l 0
      end.

    Lemma imp_expr_size_nzero (e:imp_expr) : imp_expr_size e <> 0.

    Lemma imp_stmt_size_nzero (s:imp_stmt) : imp_stmt_size s <> 0.

    Corollary imp_function_size_nzero (q:imp_function) : imp_function_size q <> 0.


End ImpSize.