helm/software/matita/contribs/ng_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 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "utility/utility.ma".
  24 include "freescale/nat_lemmas.ma".
  25
  26 (* ************************* *)
  27 (* dimensioni degli elementi *)
  28 (* ************************* *)
  29
  30 (* usato per definire nell'ast *)
  31 ninductive ast_base_type : Type ≝
  32   AST_BASE_TYPE_BYTE8: ast_base_type
  33 | AST_BASE_TYPE_WORD16: ast_base_type
  34 | AST_BASE_TYPE_WORD32: ast_base_type.
  35
  36 ndefinition ast_base_type_ind
  37  : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
  38    Πa:ast_base_type.P a ≝
  39 λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
  40 λa:ast_base_type.
  41  match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
  42
  43 ndefinition ast_base_type_rec
  44  : ΠP:ast_base_type → Set.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
  45    Πa:ast_base_type.P a ≝
  46 λP:ast_base_type → Set.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
  47 λa:ast_base_type.
  48  match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
  49
  50 ndefinition ast_base_type_rect
  51  : ΠP:ast_base_type → Type.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
  52    Πa:ast_base_type.P a ≝
  53 λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
  54 λa:ast_base_type.
  55  match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
  56
  57 ninductive ast_type : Type ≝
  58   AST_TYPE_BASE: ast_base_type → ast_type
  59 | AST_TYPE_ARRAY: ast_type → nat → ast_type
  60 | AST_TYPE_STRUCT: ne_list ast_type → ast_type.
  61
  62 nlet rec ast_type_ind_aux (P:ast_type → Prop)
  63                           (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  64                           (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  65                           (f2:Πt.P t)
  66                           (t:ne_list ast_type) on t ≝
  67  match t return λt.P (AST_TYPE_STRUCT t) with
  68   [ ne_nil h ⇒ f h (f2 h)
  69   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t)
  70   ].
  71
  72 nlet rec ast_type_ind (P:ast_type → Prop)
  73                       (f:Πb.P (AST_TYPE_BASE b))
  74                       (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
  75                       (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  76                       (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  77                       (t:ast_type) on t : P t ≝
  78  match t return λt.P t with
  79   [ AST_TYPE_BASE b ⇒ f b
  80   | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_ind P f f1 f2 f3 t')
  81   | AST_TYPE_STRUCT nl ⇒ match nl with
  82    [ ne_nil h ⇒ f2 h (ast_type_ind P f f1 f2 f3 h)
  83    | ne_cons h t ⇒ f3 h t (ast_type_ind P f f1 f2 f3 h) (ast_type_ind_aux P f2 f3 (ast_type_ind P f f1 f2 f3) t)
  84    ]
  85   ].
  86
  87 nlet rec ast_type_rec_aux (P:ast_type → Set)
  88                           (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  89                           (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  90                           (f2:Πt.P t)
  91                           (t:ne_list ast_type) on t ≝
  92  match t return λt.P (AST_TYPE_STRUCT t) with
  93   [ ne_nil h ⇒ f h (f2 h)
  94   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rec_aux P f f1 f2 t)
  95   ].
  96
  97 nlet rec ast_type_rec (P:ast_type → Set)
  98                       (f:Πb.P (AST_TYPE_BASE b))
  99                       (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
 100                       (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
 101                       (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
 102                       (t:ast_type) on t : P t ≝
 103  match t return λt.P t with
 104   [ AST_TYPE_BASE b ⇒ f b
 105   | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rec P f f1 f2 f3 t')
 106   | AST_TYPE_STRUCT nl ⇒ match nl with
 107    [ ne_nil h ⇒ f2 h (ast_type_rec P f f1 f2 f3 h)
 108    | ne_cons h t ⇒ f3 h t (ast_type_rec P f f1 f2 f3 h) (ast_type_rec_aux P f2 f3 (ast_type_rec P f f1 f2 f3) t)
 109    ]
 110   ].
 111
 112 nlet rec ast_type_rect_aux (P:ast_type → Type)
 113                            (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
 114                            (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
 115                            (f2:Πt.P t)
 116                            (t:ne_list ast_type) on t ≝
 117  match t return λt.P (AST_TYPE_STRUCT t) with
 118   [ ne_nil h ⇒ f h (f2 h)
 119   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rect_aux P f f1 f2 t)
 120   ].
 121
 122 nlet rec ast_type_rect (P:ast_type → Type)
 123                        (f:Πb.P (AST_TYPE_BASE b))
 124                        (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
 125                        (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
 126                        (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
 127                        (t:ast_type) on t : P t ≝
 128  match t return λt.P t with
 129   [ AST_TYPE_BASE b ⇒ f b
 130   | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rect P f f1 f2 f3 t')
 131   | AST_TYPE_STRUCT nl ⇒ match nl with
 132    [ ne_nil h ⇒ f2 h (ast_type_rect P f f1 f2 f3 h)
 133    | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t)
 134    ]
 135   ].
 136
 137 ndefinition eq_ast_base_type ≝
 138 λt1,t2:ast_base_type.match t1 with
 139  [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
 140   [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
 141  | AST_BASE_TYPE_WORD16 ⇒ match t2 with
 142   [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
 143  | AST_BASE_TYPE_WORD32 ⇒ match t2 with
 144   [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
 145  ].
 146
 147 nlet rec eq_ast_type (t1,t2:ast_type) on t1 ≝
 148  match t1 with
 149   [ AST_TYPE_BASE bType1 ⇒ match t2 with
 150    [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2
 151    | _ ⇒ false ]
 152   | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
 153    [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2)
 154    | _ ⇒ false ]
 155   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
 156    [ AST_TYPE_STRUCT nelSubType2 ⇒
 157     match eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2)
 158      return λx.eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = x → bool
 159     with
 160      [ true ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = true).
 161       fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
 162                          true nelSubType1 nelSubType2
 163                          (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p)
 164      | false ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = false).false
 165      ] (refl_eq ? (eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2)))
 166    | _ ⇒ false
 167    ]
 168   ].
 169
 170 ndefinition is_ast_base_type ≝
 171 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
 172
 173 ndefinition isb_ast_base_type ≝
 174 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
 175
 176 ndefinition isnt_ast_base_type ≝
 177 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
 178
 179 ndefinition isntb_ast_base_type ≝
 180 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
 181
 182 ndefinition eval_size_base_type ≝
 183 λast:ast_base_type.match ast with
 184  [ AST_BASE_TYPE_BYTE8 ⇒ 1
 185  | AST_BASE_TYPE_WORD16 ⇒ 2
 186  | AST_BASE_TYPE_WORD32 ⇒ 4
 187  ].
 188
 189 nlet rec eval_size_type (ast:ast_type) on ast ≝
 190  match ast with
 191   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
 192   | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
 193   | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast
 194   ].