source: LTS/common_variable_stack.ma

Last change on this file was 3580, checked in by piccolo, 4 years ago
File size: 2.3 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "variable.ma".
16include alias "arithmetics/nat.ma".
17
18let rec get_expr_bound (e : expr) on e : ℕ ≝
19match e with
20[ Var v ⇒ S v
21| Const n ⇒ O
22| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
23| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
24].
25
26let rec get_cond_bound (c : condition) on c : ℕ ≝
27match c with
28[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
29| Not c ⇒ get_cond_bound c
30].
31
32let rec get_instr_bound (i : frame_Instructions) ≝
33match i with
34[ EMPTY ⇒ O
35| RETURN exp ⇒ get_expr_bound exp
36| SEQ seq opt_l instr ⇒
37  let c_bound ≝ get_instr_bound instr in
38  match seq with
39  [ Seq_i seq' ⇒
40     match seq' with [ sAss v e ⇒ max (get_expr_bound e) c_bound ]
41  | PopReg v ⇒ max (S v) c_bound
42  ]
43| COND cond ltrue i_true lfalse i_false instr ⇒
44  let i_true_bound ≝ get_instr_bound i_true in
45  let i_false_bound ≝ get_instr_bound i_false in
46  let c_bound ≝ get_instr_bound instr in 
47   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))
48| LOOP cond ltrue i_true lfalse instr ⇒
49  let i_true_bound ≝ get_instr_bound i_true in
50  let c_bound ≝ get_instr_bound instr in
51   max (get_cond_bound cond) (max i_true_bound c_bound)
52| CALL f act_p opt_l instr ⇒
53  let c_bound ≝ get_instr_bound instr in
54   max (get_expr_bound act_p) c_bound
55| IO lin io lout instr ⇒ ?
56].
57cases io
58qed.
Note: See TracBrowser for help on using the repository browser.