Changeset 961 for src/common/AST.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r882 r961  
    2020include "common/Integers.ma".
    2121include "common/Floats.ma".
    22 include "ASM/BitVector.ma".
     22include "ASM/Arithmetic.ma".
    2323include "common/Identifiers.ma".
    2424
     
    110110definition SigType_Ptr ≝ ASTptr Any.
    111111
     112(* Define these carefully so that we always know that the result is nonzero,
     113   and can be used in dependent types of the form (S n).
     114   (At the time of writing this is only used for bitsize_of_intsize.) *)
     115
    112116definition size_intsize : intsize → nat ≝
    113 λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
     117λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     118
     119definition bitsize_of_intsize : intsize → nat ≝
     120λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
     121
     122definition eq_intsize : intsize → intsize → bool ≝
     123λsz1,sz2.
     124  match sz1 with
     125  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
     126  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
     127  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
     128  ].
     129
     130lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
     131  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
     132* * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
     133qed.
     134
     135lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
     136* @refl
     137qed.
     138
     139lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
     140* * * #NE try @refl @False_ind @NE @refl
     141qed.
     142
     143(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
     144   if it is returns [e1] where the type of [n] has its dependency on [sz1]
     145   changed to [sz2], and if not returns [e2]. *)
     146let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
     147  P sz1 → (P sz2 → A) → A → A ≝
     148match sz1 return λsz. P sz → (P sz2 → A) → A → A with
     149[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     150| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     151| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     152].
     153
     154lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
     155  intsize_eq_elim A sz sz P p f d = f p.
     156#A * //
     157qed.
     158
     159lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
     160  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
     161#A * * #P #p #f #d #Q #Hne #Heq
     162[ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
     163| *: whd in ⊢ (?%) @Hne % #E destruct
     164] qed.
     165
     166
     167(* A type for the integers that appear in the semantics. *)
     168definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
     169
     170definition repr : ∀sz:intsize. nat → bvint sz ≝
     171λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
     172
    114173
    115174definition size_floatsize : floatsize → nat ≝
    116 λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
     175λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
    117176
    118177definition typesize : typ → nat ≝ λty.
     
    187246
    188247inductive init_data: Type[0] ≝
    189   | Init_int8: int → init_data
    190   | Init_int16: int → init_data
    191   | Init_int32: int → init_data
     248  | Init_int8: bvint I8 → init_data
     249  | Init_int16: bvint I16 → init_data
     250  | Init_int32: bvint I32 → init_data
    192251  | Init_float32: float → init_data
    193252  | Init_float64: float → init_data
    194253  | Init_space: nat → init_data
    195254  | Init_null: region → init_data
    196   | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
     255  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
    197256
    198257(* * Whole programs consist of:
Note: See TracChangeset for help on using the changeset viewer.