helm/software/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 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
  61  match t1 with
  62   [ AST_TYPE_BASE bType1 ⇒ match t2 with
  63    [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2 | _ ⇒ false ]
  64   | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
  65    [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
  66   | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
  67    [ AST_TYPE_STRUCT nelSubType2 ⇒
  68     fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with
  69                                        [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with
  70                                         [ None ⇒ pair ?? false (S (snd ?? t))
  71                                         | Some cfr ⇒ match eq_ast_type h cfr with
  72                                          [ true ⇒ pair ?? true (S (snd ?? t))
  73                                          | false ⇒ pair ?? false (S (snd ?? t)) ]]
  74                                        | false ⇒ t]) (pair ?? true O) nelSubType1)
  75    | _ ⇒ false ]
  76   ].
  77
  78 lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
  79  do 2 intro;
  80  cases t1; cases t2;
  81  [ 2,3,4,6,7,8: normalize; intro; destruct H
  82  | 1: change in ⊢ (? ? % ?→?) with (eq_ast_base_type a a1);
  83       intro;
  84       apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
  85  | 5: change in ⊢ (? ? % ?→?) with ((eq_ast_type a a1) ⊗ (eqb n n1));
  86       intro;
  87       cut (a = a1 ∧ n = n1);
  88       elim daemon.
  89  | 9: elim daemon
  90  ].
  91 qed.
  92
  93 (* PERCHE' ??
  94  se in testa includo
  95  include "demo/natural_deduction.ma".
  96  la dimostrazione va fino in fondo ma poi impazzisce ast_tree.ma
  97  dicendo che la dichiarazione ast_id e' scorretta
  98
  99       [ 1: alias id "And_elim_l" = "cic:/matita/demo/natural_deduction/And_elim_l.con".
 100            alias id "And_elim_r" = "cic:/matita/demo/natural_deduction/And_elim_r.con".
 101            apply (eq_f2 ??? (λx.λy.? x y) a a1 n n1 (And_elim_l ?? Hcut) (And_elim_r ?? Hcut))
 102       | 2: split;
 103            [ 2: apply (eqb_true_to_eq n n1 (andb_true_true_r ?? H))
 104            | 1: cut (eq_ast_Type a a1 = true);
 105                 [ 2: apply (andb_true_true ?? H)
 106                 | 1: TODO elim daemon
 107                 ]
 108            ]
 109       ]
 110  | 9: TODO elim daemon
 111  ]
 112 qed.
 113 *)
 114
 115 definition is_ast_base_type ≝
 116 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
 117
 118 definition isb_ast_base_type ≝
 119 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
 120
 121 lemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
 122  unfold isb_ast_base_type;
 123  unfold is_ast_base_type;
 124  intros;
 125  elim ast;
 126  [ normalize; autobatch |
 127    normalize; autobatch |
 128    normalize; autobatch ]
 129 qed.
 130
 131 definition isnt_ast_base_type ≝
 132 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
 133
 134 definition isntb_ast_base_type ≝
 135 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
 136
 137 lemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
 138  unfold isntb_ast_base_type;
 139  unfold isnt_ast_base_type;
 140  intros;
 141  elim ast;
 142  [ normalize; autobatch |
 143    normalize; autobatch |
 144    normalize; autobatch ]
 145 qed.
 146
 147 definition eval_size_base_type ≝
 148 λast:ast_base_type.match ast with
 149  [ AST_BASE_TYPE_BYTE8 ⇒ 1
 150  | AST_BASE_TYPE_WORD16 ⇒ 2
 151  | AST_BASE_TYPE_WORD32 ⇒ 4
 152  ].
 153
 154 let rec eval_size_type (ast:ast_type) on ast ≝
 155  match ast with
 156   [ AST_TYPE_BASE b ⇒ eval_size_base_type b
 157   | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
 158   | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast
 159   ].