]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/compiler/linearfe.ma
- exclusion binder in local environments allows to complete lfsx_lfsx !
[helm.git] / matita / matita / contribs / assembly / compiler / linearfe.ma
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
15 (* ********************************************************************** *)
16 (*                                                                        *)
17 (* Sviluppato da:                                                         *)
18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
19 (*                                                                        *)
20 (* ********************************************************************** *)
21
22 include "compiler/env_to_flatenv.ma".
23 include "compiler/astfe_tree.ma".
24
25 (* ************************************************ *)
26 (* SUCCESSIONE APPIATITA DI ASSEGNAMENTI SU FLATENV *)
27 (* ************************************************ *)
28
29 inductive jumpNLabel : Type ≝
30   N_LABEL: nat → jumpNLabel.
31
32 inductive jumpLabel : Type ≝
33   LABEL_N: jumpNLabel → jumpLabel
34 | LABEL_END: jumpLabel.
35
36 (* 
37    L1 := goto L1
38    EXPR L1 L2 := if(EXPR) then { goto L1; } else { goto L2; }
39 *)
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.
43
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.
49
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.
53
54 (* -------------------------- *)
55
56 definition linearfe_prog ≝ λe.list (linearfe_elem e).
57
58 (* -------------------------- *)
59
60 (* programma vuoto *)
61 definition empty_linearfe_prog ≝ nil (linearfe_elem empty_flatEnv).