(**************************************************************************) (* ___ *) (* ||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.