(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "variable.ma".
include alias "arithmetics/nat.ma".

let rec get_expr_bound (e : expr) on e : ℕ ≝ 
match e with
[ Var v ⇒ S v
| Const n ⇒ O
| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
].

let rec get_cond_bound (c : condition) on c : ℕ ≝ 
match c with
[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
| Not c ⇒ get_cond_bound c
].

let rec get_instr_bound (i : frame_Instructions) ≝ 
match i with
[ EMPTY ⇒ O
| RETURN exp ⇒ get_expr_bound exp
| SEQ seq opt_l instr ⇒ 
  let c_bound ≝ get_instr_bound instr in
  match seq with
  [ Seq_i seq' ⇒ 
     match seq' with [ sAss v e ⇒ max (get_expr_bound e) c_bound ]
  | PopReg v ⇒ max (S v) c_bound
  ]
| COND cond ltrue i_true lfalse i_false instr ⇒
  let i_true_bound ≝ get_instr_bound i_true in
  let i_false_bound ≝ get_instr_bound i_false in
  let c_bound ≝ get_instr_bound instr in  
   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))
| LOOP cond ltrue i_true lfalse instr ⇒ 
  let i_true_bound ≝ get_instr_bound i_true in 
  let c_bound ≝ get_instr_bound instr in
   max (get_cond_bound cond) (max i_true_bound c_bound)
| CALL f act_p opt_l instr ⇒ 
  let c_bound ≝ get_instr_bound instr in
   max (get_expr_bound act_p) c_bound
| IO lin io lout instr ⇒ ?
].
cases io
qed.