diff options
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 39 |
1 files changed, 24 insertions, 15 deletions
diff --git a/common/AST.v b/common/AST.v index 8595b95..1f7f7d3 100644 --- a/common/AST.v +++ b/common/AST.v @@ -17,6 +17,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import Coqlib. +Require String. Require Import Errors. Require Import Integers. Require Import Floats. @@ -32,16 +33,19 @@ Definition ident := positive. Definition ident_eq := peq. -(** The intermediate languages are weakly typed, using only two types: - [Tint] for integers and pointers, and [Tfloat] for floating-point - numbers. *) +Parameter ident_of_string : String.string -> ident. + +(** The intermediate languages are weakly typed, using only three + types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit + floating-point numbers, [Tlong] for 64-bit integers. *) Inductive typ : Type := - | Tint : typ - | Tfloat : typ. + | Tint + | Tfloat + | Tlong. Definition typesize (ty: typ) : Z := - match ty with Tint => 4 | Tfloat => 8 end. + match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 end. Lemma typesize_pos: forall ty, typesize ty > 0. Proof. destruct ty; simpl; omega. Qed. @@ -54,6 +58,9 @@ Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}. Proof. decide equality. apply typ_eq. Defined. Global Opaque opt_typ_eq. +Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} + := list_eq_dec typ_eq. + (** Additionally, function definitions and function calls are annotated by function signatures indicating the number and types of arguments, as well as the type of the returned value if any. These signatures @@ -76,14 +83,15 @@ Definition proj_sig_res (s: signature) : typ := chunk of memory being accessed. *) Inductive memory_chunk : Type := - | Mint8signed : memory_chunk (**r 8-bit signed integer *) - | Mint8unsigned : memory_chunk (**r 8-bit unsigned integer *) - | Mint16signed : memory_chunk (**r 16-bit signed integer *) - | Mint16unsigned : memory_chunk (**r 16-bit unsigned integer *) - | Mint32 : memory_chunk (**r 32-bit integer, or pointer *) - | Mfloat32 : memory_chunk (**r 32-bit single-precision float *) - | Mfloat64 : memory_chunk (**r 64-bit double-precision float *) - | Mfloat64al32 : memory_chunk. (**r 64-bit double-precision float, 4-aligned *) + | Mint8signed (**r 8-bit signed integer *) + | Mint8unsigned (**r 8-bit unsigned integer *) + | Mint16signed (**r 16-bit signed integer *) + | Mint16unsigned (**r 16-bit unsigned integer *) + | Mint32 (**r 32-bit integer, or pointer *) + | Mint64 (**r 64-bit integer *) + | Mfloat32 (**r 32-bit single-precision float *) + | Mfloat64 (**r 64-bit double-precision float *) + | Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *) (** The type (integer/pointer or float) of a chunk. *) @@ -94,6 +102,7 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Mint16signed => Tint | Mint16unsigned => Tint | Mint32 => Tint + | Mint64 => Tlong | Mfloat32 => Tfloat | Mfloat64 => Tfloat | Mfloat64al32 => Tfloat @@ -105,6 +114,7 @@ Inductive init_data: Type := | Init_int8: int -> init_data | Init_int16: int -> init_data | Init_int32: int -> init_data + | Init_int64: int64 -> init_data | Init_float32: float -> init_data | Init_float64: float -> init_data | Init_space: Z -> init_data @@ -549,4 +559,3 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := end. End TRANSF_PARTIAL_FUNDEF. - |