1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "compiler/env_to_flatenv.ma".
23 include "compiler/astfe_tree.ma".
25 (* ************************************************ *)
26 (* SUCCESSIONE APPIATITA DI ASSEGNAMENTI SU FLATENV *)
27 (* ************************************************ *)
29 inductive jumpNLabel : Type ≝
30 N_LABEL: nat → jumpNLabel.
32 inductive jumpLabel : Type ≝
33 LABEL_N: jumpNLabel → jumpLabel
34 | LABEL_END: jumpLabel.
38 EXPR L1 L2 := if(EXPR) then { goto L1; } else { goto L2; }
40 inductive jumpBlock (e:aux_flatEnv_type) : Type ≝
41 JUMPBLOCK_ABS: jumpLabel → jumpBlock e
42 | JUMPBLOCK_COND: astfe_base_expr e → jumpLabel → jumpLabel → jumpBlock e.
44 inductive linearfe_stm (e:aux_flatEnv_type) : Type ≝
45 LINEARFE_STM_ASG: ∀t:ast_type.
46 astfe_var e false t → astfe_expr e t → linearfe_stm e
47 | LINEARFE_STM_INIT: ∀b:bool.∀t:ast_type.
48 astfe_id e b t → astfe_init e t → linearfe_stm e.
50 (* LABEL + [ init/assegnamenti ] + if(EXPR) then { goto LABEL; } else { goto LABEL; } *)
51 inductive linearfe_elem (e:aux_flatEnv_type) : Type ≝
52 LINEARFE_ELEM: jumpNLabel → list (linearfe_stm e) → jumpBlock e → linearfe_elem e.
54 (* -------------------------- *)
56 definition linearfe_prog ≝ λe.list (linearfe_elem e).
58 (* -------------------------- *)
61 definition empty_linearfe_prog ≝ nil (linearfe_elem empty_flatEnv).