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 ninductive ast_type : Type ≝
  37   AST_TYPE_BASE: ast_base_type → ast_type
  38 | AST_TYPE_ARRAY: ast_type → nat → ast_type
  39 | AST_TYPE_STRUCT: ne_list ast_type → ast_type.
  40
  41 (* principio di eliminazione arricchito *)
  42 nlet rec ast_type_index_aux (P:ast_type → Prop)
  43                             (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  44                             (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  45                             (f2:Πt.P t)
  46                             (t:ne_list ast_type) on t ≝
  47  match t return λt.P (AST_TYPE_STRUCT t) with
  48   [ ne_nil h ⇒ f h (f2 h)
  49   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t)
  50   ].
  51
  52 nlet rec ast_type_index (P:ast_type → Prop)
  53                         (f:Πb.P (AST_TYPE_BASE b))
  54                         (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
  55                         (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  56                         (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  57                         (t:ast_type) on t : P t ≝
  58  match t return λt.P t with
  59   [ AST_TYPE_BASE b ⇒ f b
  60   | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t')
  61   | AST_TYPE_STRUCT nl ⇒ match nl with
  62    [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h)
  63    | ne_cons h t ⇒ f3 h t (ast_type_index P f f1 f2 f3 h) (ast_type_index_aux P f2 f3 (ast_type_index P f f1 f2 f3) t)
  64    ]
  65   ].
  66
  67 nlet rec ast_type_rectex_aux (P:ast_type → Type)
  68                              (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  69                              (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  70                              (f2:Πt.P t)
  71                              (t:ne_list ast_type) on t ≝
  72  match t return λt.P (AST_TYPE_STRUCT t) with
  73   [ ne_nil h ⇒ f h (f2 h)
  74   | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t)
  75   ].
  76
  77 nlet rec ast_type_rectex (P:ast_type → Type)
  78                          (f:Πb.P (AST_TYPE_BASE b))
  79                          (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
  80                          (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
  81                          (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
  82                          (t:ast_type) on t : P t ≝
  83  match t return λt.P t with
  84   [ AST_TYPE_BASE b ⇒ f b
  85   | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t')
  86   | AST_TYPE_STRUCT nl ⇒ match nl with
  87    [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h)
  88    | ne_cons h t ⇒ f3 h t (ast_type_rectex P f f1 f2 f3 h) (ast_type_rectex_aux P f2 f3 (ast_type_rectex P f f1 f2 f3) t)
  89    ]
  90   ].
  91
  92 ndefinition eq_ast_base_type ≝
  93 λt1,t2:ast_base_type.match t1 with
  94  [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
  95   [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
  96  | AST_BASE_TYPE_WORD16 ⇒ match t2 with
  97   [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
  98  | AST_BASE_TYPE_WORD32 ⇒ match t2 with
  99   [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
 100  ].
 101
 102 nlet rec eq_ast_type (t1,t2:ast_type) on t1 ≝
 103  match t1 with
 104   [ AST_TYPE_BASE bType1 ⇒ match t2 with
 105    [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2
 106    | _ ⇒ false ]
 107   | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
 108    [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2)
 109    | _ ⇒ false ]
 110   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
 111    [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_ast_type x1 x2) nelSubType1 nelSubType2
 112    | _ ⇒ false
 113    ]
 114   ].
 115
 116 ndefinition is_ast_base_type ≝
 117 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
 118
 119 ndefinition isb_ast_base_type ≝
 120 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
 121
 122 ndefinition isnt_ast_base_type ≝
 123 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
 124
 125 ndefinition isntb_ast_base_type ≝
 126 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
 127
 128 ndefinition eval_size_base_type ≝
 129 λast:ast_base_type.match ast with
 130  [ AST_BASE_TYPE_BYTE8 ⇒ 1
 131  | AST_BASE_TYPE_WORD16 ⇒ 2
 132  | AST_BASE_TYPE_WORD32 ⇒ 4
 133  ].
 134
 135 nlet rec eval_size_type (ast:ast_type) on ast ≝
 136  match ast with
 137   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
 138   | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
 139   | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast
 140   ].