matitaB/matita/contribs/assembly/compiler/ast_type.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/utility.ma".
  23 include "freescale/word32.ma".
  24
  25 (* ************************* *)
  26 (* dimensioni degli elementi *)
  27 (* ************************* *)
  28
  29 (* usato per definire nell'ast *)
  30 inductive ast_base_type : Type ≝
  31   AST_BASE_TYPE_BYTE8: ast_base_type
  32 | AST_BASE_TYPE_WORD16: ast_base_type
  33 | AST_BASE_TYPE_WORD32: ast_base_type.
  34
  35 inductive ast_type : Type ≝
  36   AST_TYPE_BASE: ast_base_type → ast_type
  37 | AST_TYPE_ARRAY: ast_type → nat → ast_type
  38 | AST_TYPE_STRUCT: ne_list ast_type → ast_type.
  39
  40 definition eq_ast_base_type ≝
  41 λt1,t2:ast_base_type.match t1 with
  42  [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
  43   [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
  44  | AST_BASE_TYPE_WORD16 ⇒ match t2 with
  45   [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
  46  | AST_BASE_TYPE_WORD32 ⇒ match t2 with
  47   [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
  48  ].
  49
  50 lemma eqastbasetype_to_eq : ∀t1,t2:ast_base_type.(eq_ast_base_type t1 t2 = true) → (t1 = t2).
  51  unfold eq_ast_base_type;
  52  intros;
  53  elim t1 in H:(%);
  54  elim t2 in H:(%);
  55  normalize in H:(%);
  56  try reflexivity;
  57  destruct H.
  58 qed.
  59
  60 lemma eq_to_eqastbasetype : ∀t1,t2.t1 = t2 → eq_ast_base_type t1 t2 = true.
  61  do 2 intro;
  62  elim t1 0;
  63  elim t2 0;
  64  normalize;
  65  intro;
  66  try destruct H;
  67  reflexivity.
  68 qed.
  69
  70 definition eq_ast_type_aux ≝
  71 λT:Type.λf:T → T → bool.
  72  let rec aux (nl1,nl2:ne_list T) on nl1 ≝
  73   match nl1 with
  74    [ ne_nil h ⇒ match nl2 with
  75     [ ne_nil h' ⇒ f h h'
  76     | ne_cons h' _ ⇒ false
  77     ]
  78    | ne_cons h t ⇒ match nl2 with
  79     [ ne_nil h' ⇒ false
  80     | ne_cons h' t' ⇒ (f h h') ⊗ (aux t t')
  81     ]
  82    ] in aux.
  83
  84 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
  85  match t1 with
  86   [ AST_TYPE_BASE bType1 ⇒ match t2 with
  87    [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2 | _ ⇒ false ]
  88   | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
  89    [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
  90   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
  91    [ AST_TYPE_STRUCT nelSubType2 ⇒ eq_ast_type_aux ? eq_ast_type nelSubType1 nelSubType2
  92    | _ ⇒ false ]
  93   ].
  94
  95 lemma eq_ast_type_elim :
  96  ∀P:ast_type → Prop.
  97   (∀x.P (AST_TYPE_BASE x)) →
  98   (∀t:ast_type.∀n.(P t) → (P (AST_TYPE_ARRAY t n))) →
  99   (∀x.(P x) → (P (AST_TYPE_STRUCT (ne_nil ? x)))) →
 100   (∀x,l.(P x) → (P (AST_TYPE_STRUCT l)) → (P (AST_TYPE_STRUCT (ne_cons ? x l)))) →
 101   (∀t.(P t)).
 102  intros;
 103  apply
 104   (let rec aux t ≝
 105     match t
 106      return λt.P t
 107     with
 108      [ AST_TYPE_BASE b ⇒ H b
 109      | AST_TYPE_ARRAY t n ⇒ H1 t n (aux t)
 110      | AST_TYPE_STRUCT l ⇒
 111       let rec aux_l (l:ne_list ast_type ) ≝
 112        match l
 113         return λl.P (AST_TYPE_STRUCT l)
 114        with
 115         [ ne_nil t => H2 t (aux t)
 116         | ne_cons hd tl => H3 hd tl (aux hd) (aux_l tl)
 117         ] in aux_l l
 118      ] in aux t);
 119 qed.
 120
 121 lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
 122  intro;
 123  elim t1 using eq_ast_type_elim 0;
 124  [ 1: intros 2;
 125       elim t2 using eq_ast_type_elim 0;
 126       [ 1: intros;
 127            simplify in H;
 128            rewrite > (eqastbasetype_to_eq ?? H);
 129            reflexivity
 130       | 2: simplify;
 131            intros;
 132            destruct H1
 133       | 3: simplify;
 134            intros;
 135            destruct H1
 136       | 4: simplify;
 137            intros;
 138            destruct H2
 139       ]
 140  | 2: intros 4;
 141       elim t2 using eq_ast_type_elim 0;
 142       [ 1: simplify;
 143            intros;
 144            destruct H1
 145       | 2: simplify;
 146            intros;
 147            lapply (andb_true_true ?? H2) as H3;
 148            lapply (andb_true_true_r ?? H2) as H4;
 149            rewrite > (H ? H3);
 150            rewrite > (eqb_true_to_eq ?? H4);
 151            reflexivity
 152       | 3: simplify;
 153            intros;
 154            destruct H2
 155       | 4: simplify;
 156            intros;
 157            destruct H3
 158       ]
 159  | 3: intros 3;
 160       elim t2 using eq_ast_type_elim 0;
 161       [ 1: simplify;
 162            intros;
 163            destruct H1
 164       | 2: simplify;
 165            intros;
 166            destruct H2
 167       | 3: intros;
 168            simplify in H2;
 169            rewrite > (H x1);
 170            [ reflexivity
 171            | apply H2
 172            ]
 173       | 4: intros;
 174            simplify in H3;
 175            destruct H3
 176       ]
 177  | 4: intros 5;
 178       elim t2 using eq_ast_type_elim 0;
 179       [ 1: simplify;
 180            intros;
 181            destruct H2
 182       | 2: simplify;
 183            intros;
 184            destruct H3
 185       | 3: simplify;
 186            intros;
 187            destruct H3
 188       | 4: intros;
 189            simplify in H4;
 190            lapply (andb_true_true ?? H4) as H5;
 191            lapply (andb_true_true_r ?? H4) as H6;
 192            rewrite > (H ? H5);
 193            lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K;
 194            destruct (K ?);
 195            [ apply H6
 196            | reflexivity
 197            ]
 198       ]
 199  ].
 200 qed.
 201
 202 lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
 203  intro;
 204  elim t1 using eq_ast_type_elim 0;
 205  [ 1: intros 2;
 206       elim t2 using eq_ast_type_elim 0;
 207       [ 1: simplify;
 208            intros;
 209            destruct H;
 210            apply (eq_to_eqastbasetype x x (refl_eq ??))
 211       | 2: simplify;
 212            intros;
 213            destruct H1
 214       | 3: simplify;
 215            intros;
 216            destruct H1
 217       | 4: simplify;
 218            intros;
 219            destruct H2
 220       ]
 221  | 2: intros 4;
 222       elim t2 using eq_ast_type_elim 0;
 223       [ 1: simplify;
 224            intros;
 225            destruct H1
 226       | 2: intros;
 227            simplify;
 228            destruct H2;
 229            rewrite > (H t (refl_eq ??));
 230            rewrite > (eq_to_eqb_true n n (refl_eq ??));
 231            reflexivity
 232       | 3: simplify;
 233            intros;
 234            destruct H2
 235       | 4: simplify;
 236            intros;
 237            destruct H3
 238       ]
 239  | 3: intros 3;
 240       elim t2 using eq_ast_type_elim 0;
 241       [ 1: simplify;
 242            intros;
 243            destruct H1
 244       | 2: simplify;
 245            intros;
 246            destruct H2
 247       | 3: intros;
 248            simplify;
 249            destruct H2;
 250            rewrite > (H x (refl_eq ??));
 251            reflexivity
 252       | 4: simplify;
 253            intros;
 254            destruct H3
 255       ]
 256  | 4: intros 5;
 257       elim t2 using eq_ast_type_elim 0;
 258       [ 1: simplify;
 259            intros;
 260            destruct H2
 261       | 2: simplify;
 262            intros;
 263            destruct H3
 264       | 3: simplify;
 265            intros;
 266            destruct H3
 267       | 4: intros;
 268            simplify;
 269            destruct H4;
 270            rewrite > (H x (refl_eq ??));
 271            rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??));
 272            reflexivity
 273       ]
 274  ].
 275 qed.
 276
 277 definition is_ast_base_type ≝
 278 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
 279
 280 definition isb_ast_base_type ≝
 281 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
 282
 283 lemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
 284  unfold isb_ast_base_type;
 285  unfold is_ast_base_type;
 286  intros;
 287  elim ast;
 288  [ normalize; autobatch |
 289    normalize; autobatch |
 290    normalize; autobatch ]
 291 qed.
 292
 293 definition isnt_ast_base_type ≝
 294 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
 295
 296 definition isntb_ast_base_type ≝
 297 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
 298
 299 lemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
 300  unfold isntb_ast_base_type;
 301  unfold isnt_ast_base_type;
 302  intros;
 303  elim ast;
 304  [ normalize; autobatch |
 305    normalize; autobatch |
 306    normalize; autobatch ]
 307 qed.
 308
 309 definition eval_size_base_type ≝
 310 λast:ast_base_type.match ast with
 311  [ AST_BASE_TYPE_BYTE8 ⇒ 1
 312  | AST_BASE_TYPE_WORD16 ⇒ 2
 313  | AST_BASE_TYPE_WORD32 ⇒ 4
 314  ].
 315
 316 let rec eval_size_type (ast:ast_type) on ast ≝
 317  match ast with
 318   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
 319   | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
 320   | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast
 321   ].