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/environment.ma".
28 (* id: accesso all'ambiente con stringa *)
29 inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
30 AST_ID: ∀str:aux_str_type.
31 (* D *) check_desc_env e str → ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)).
33 (* -------------------------- *)
36 inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
37 AST_EXPR_BYTE8 : byte8 → ast_expr e AST_BASE_TYPE_BYTE8
38 | AST_EXPR_WORD16: word16 → ast_expr e AST_BASE_TYPE_WORD16
39 | AST_EXPR_WORD32: word32 → ast_expr e AST_BASE_TYPE_WORD32
41 | AST_EXPR_NEG: ∀t:ast_base_type.
42 ast_expr e t → ast_expr e t
43 | AST_EXPR_NOT: ∀t:ast_base_type.
44 ast_expr e t → ast_expr e t
45 | AST_EXPR_COM: ∀t:ast_base_type.
46 ast_expr e t → ast_expr e t
48 | AST_EXPR_ADD: ∀t:ast_base_type.
49 ast_expr e t → ast_expr e t → ast_expr e t
50 | AST_EXPR_SUB: ∀t:ast_base_type.
51 ast_expr e t → ast_expr e t → ast_expr e t
52 | AST_EXPR_MUL: ∀t:ast_base_type.
53 ast_expr e t → ast_expr e t → ast_expr e t
54 | AST_EXPR_DIV: ∀t:ast_base_type.
55 ast_expr e t → ast_expr e t → ast_expr e t
56 | AST_EXPR_SHR: ∀t:ast_base_type.
57 ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
58 | AST_EXPR_SHL: ∀t:ast_base_type.
59 ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
61 | AST_EXPR_GT : ∀t:ast_base_type.
62 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
63 | AST_EXPR_GTE: ∀t:ast_base_type.
64 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
65 | AST_EXPR_LT : ∀t:ast_base_type.
66 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
67 | AST_EXPR_LTE: ∀t:ast_base_type.
68 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
69 | AST_EXPR_EQ : ∀t:ast_base_type.
70 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
71 | AST_EXPR_NEQ: ∀t:ast_base_type.
72 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
74 | AST_EXPR_B8toW16 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD16
75 | AST_EXPR_B8toW32 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD32
76 | AST_EXPR_W16toB8 : ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_BYTE8
77 | AST_EXPR_W16toW32: ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_WORD32
78 | AST_EXPR_W32toB8 : ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_BYTE8
79 | AST_EXPR_W32toW16: ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_WORD16
81 | AST_EXPR_ID: ∀b:bool.∀t:ast_base_type.
82 ast_var e b (AST_TYPE_BASE t) → ast_expr e t
84 (* espressioni generalizzate: anche non uniformi per tipo *)
85 with ast_base_expr : Type ≝
86 AST_BASE_EXPR: ∀t:ast_base_type.
87 ast_expr e t → ast_base_expr e
89 (* variabile: modificatori di array/struct dell'id *)
90 with ast_var : bool → ast_type → Type ≝
91 AST_VAR_ID: ∀b:bool.∀t:ast_type.
92 ast_id e b t → ast_var e b t
93 (* NB: l'index out of bound e' delegato a runtime? *)
94 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
95 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
96 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
97 ast_var e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n).
99 (* -------------------------- *)
101 (* statement: assegnamento/while/if else if else *)
102 inductive ast_stm : aux_env_type → Type ≝
103 AST_STM_ASG: ∀e:aux_env_type.∀t:ast_base_type.
104 ast_var e false (AST_TYPE_BASE t) → ast_expr e t → ast_stm e
105 | AST_STM_MEMCPY_ASG: ∀e:aux_env_type.∀b:bool.∀t:ast_type.
106 (* D *) isnt_ast_base_type t → ast_var e false t → ast_var e b t → ast_stm e
107 | AST_STM_WHILE: ∀e:aux_env_type.
108 ast_base_expr e → ast_decl e → ast_stm e
109 | AST_STM_IF: ∀e:aux_env_type.
110 ne_list (Prod (ast_base_expr e) (ast_decl e)) → option (ast_decl e) → ast_stm e
113 with ast_decl : aux_env_type → Type ≝
114 AST_NO_DECL: ∀e:aux_env_type.
115 list (ast_stm e) → ast_decl e
116 | AST_BASE_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_base_type.
117 (* D *) (check_not_already_def_env e str) → option (ast_expr e t) → ast_decl (add_desc_env e str c (AST_TYPE_BASE t)) → ast_decl e
118 | AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
119 (* D *) (check_not_already_def_env e str) → (* D *) isnt_ast_base_type t → ast_decl (add_desc_env e str c t) → ast_decl e.
121 (* -------------------------- *)
124 inductive ast_root : Type ≝
125 AST_ROOT: ast_decl empty_env → ast_root.
127 (* -------------------------- *)
129 (* programma vuoto *)
130 definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)).