From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Jun 2009 13:39:59 +0000 Subject: Adapted to work with Coq 8.2-1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index ac790470..b332e216 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -31,11 +31,11 @@ Require Import AST. bit size of the type. An integer type is a pair of a signed/unsigned flag and a bit size: 8, 16 or 32 bits. *) -Inductive signedness : Set := +Inductive signedness : Type := | Signed: signedness | Unsigned: signedness. -Inductive intsize : Set := +Inductive intsize : Type := | I8: intsize | I16: intsize | I32: intsize. @@ -43,7 +43,7 @@ Inductive intsize : Set := (** Float types come in two sizes: 32 bits (single precision) and 64-bit (double precision). *) -Inductive floatsize : Set := +Inductive floatsize : Type := | F32: floatsize | F64: floatsize. @@ -82,7 +82,7 @@ Inductive floatsize : Set := structure or union, but not to the structure or union directly. *) -Inductive type : Set := +Inductive type : Type := | Tvoid: type (**r the [void] type *) | Tint: intsize -> signedness -> type (**r integer types *) | Tfloat: floatsize -> type (**r floating-point types *) @@ -93,11 +93,11 @@ Inductive type : Set := | Tunion: ident -> fieldlist -> type (**r union types *) | Tcomp_ptr: ident -> type (**r pointer to named struct or union *) -with typelist : Set := +with typelist : Type := | Tnil: typelist | Tcons: type -> typelist -> typelist -with fieldlist : Set := +with fieldlist : Type := | Fnil: fieldlist | Fcons: ident -> type -> fieldlist -> fieldlist. @@ -105,12 +105,12 @@ with fieldlist : Set := (** Arithmetic and logical operators. *) -Inductive unary_operation : Set := +Inductive unary_operation : Type := | Onotbool : unary_operation (**r boolean negation ([!] in C) *) | Onotint : unary_operation (**r integer complement ([~] in C) *) | Oneg : unary_operation. (**r opposite (unary [-]) *) -Inductive binary_operation : Set := +Inductive binary_operation : Type := | Oadd : binary_operation (**r addition (binary [+]) *) | Osub : binary_operation (**r subtraction (binary [-]) *) | Omul : binary_operation (**r multiplication (binary [*]) *) @@ -138,10 +138,10 @@ Inductive binary_operation : Set := description (type [expr_descr]). *) -Inductive expr : Set := +Inductive expr : Type := | Expr: expr_descr -> type -> expr -with expr_descr : Set := +with expr_descr : Type := | Econst_int: int -> expr_descr (**r integer literal *) | Econst_float: float -> expr_descr (**r float literal *) | Evar: ident -> expr_descr (**r variable *) @@ -168,7 +168,7 @@ Definition typeof (e: expr) : type := the [default] case must occur last. Blocks and block-scoped declarations are not supported. *) -Inductive statement : Set := +Inductive statement : Type := | Sskip : statement (**r do nothing *) | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *) | Scall: option expr -> expr -> list expr -> statement (**r function call *) @@ -182,7 +182,7 @@ Inductive statement : Set := | Sreturn : option expr -> statement (**r [return] statement *) | Sswitch : expr -> labeled_statements -> statement (**r [switch] statement *) -with labeled_statements : Set := (**r cases of a [switch] *) +with labeled_statements : Type := (**r cases of a [switch] *) | LSdefault: statement -> labeled_statements | LScase: int -> statement -> labeled_statements -> labeled_statements. @@ -193,7 +193,7 @@ with labeled_statements : Set := (**r cases of a [switch] *) and types of its local variables ([fn_vars]), and the body of the function (a statement, [fn_body]). *) -Record function : Set := mkfunction { +Record function : Type := mkfunction { fn_return: type; fn_params: list (ident * type); fn_vars: list (ident * type); @@ -203,7 +203,7 @@ Record function : Set := mkfunction { (** Functions can either be defined ([Internal]) or declared as external functions ([External]). *) -Inductive fundef : Set := +Inductive fundef : Type := | Internal: function -> fundef | External: ident -> typelist -> type -> fundef. @@ -213,7 +213,7 @@ Inductive fundef : Set := of named global variables, carrying their types and optional initialization data. See module [AST] for more details. *) -Definition program : Set := AST.program fundef type. +Definition program : Type := AST.program fundef type. (** * Operations over types *) @@ -409,9 +409,9 @@ Proof. destruct (ident_eq id1 i); destruct (ident_eq id2 i). congruence. subst i. intros. inv H; inv H0. - exploit field_offset_rec_in_range; eauto. tauto. + exploit field_offset_rec_in_range. eexact H1. eauto. tauto. subst i. intros. inv H1; inv H2. - exploit field_offset_rec_in_range; eauto. tauto. + exploit field_offset_rec_in_range. eexact H. eauto. tauto. intros. eapply IHfld; eauto. apply H with fld0 0; auto. @@ -449,7 +449,7 @@ type must be accessed: - [By_nothing]: no access is possible, e.g. for the [void] type. *) -Inductive mode: Set := +Inductive mode: Type := | By_value: memory_chunk -> mode | By_reference: mode | By_nothing: mode. @@ -482,7 +482,7 @@ end. compiler (module [Cshmgen]). *) -Inductive classify_add_cases : Set := +Inductive classify_add_cases : Type := | add_case_ii: classify_add_cases (**r int , int *) | add_case_ff: classify_add_cases (**r float , float *) | add_case_pi: type -> classify_add_cases (**r ptr or array, int *) @@ -500,7 +500,7 @@ Definition classify_add (ty1: type) (ty2: type) := | _, _ => add_default end. -Inductive classify_sub_cases : Set := +Inductive classify_sub_cases : Type := | sub_case_ii: classify_sub_cases (**r int , int *) | sub_case_ff: classify_sub_cases (**r float , float *) | sub_case_pi: type -> classify_sub_cases (**r ptr or array , int *) @@ -520,7 +520,7 @@ Definition classify_sub (ty1: type) (ty2: type) := | _ ,_ => sub_default end. -Inductive classify_mul_cases : Set:= +Inductive classify_mul_cases : Type:= | mul_case_ii: classify_mul_cases (**r int , int *) | mul_case_ff: classify_mul_cases (**r float , float *) | mul_default: classify_mul_cases . (**r other *) @@ -532,7 +532,7 @@ Definition classify_mul (ty1: type) (ty2: type) := | _,_ => mul_default end. -Inductive classify_div_cases : Set:= +Inductive classify_div_cases : Type:= | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *) | div_case_ii: classify_div_cases (**r int , int *) | div_case_ff: classify_div_cases (**r float , float *) @@ -547,7 +547,7 @@ Definition classify_div (ty1: type) (ty2: type) := | _ ,_ => div_default end. -Inductive classify_mod_cases : Set:= +Inductive classify_mod_cases : Type:= | mod_case_I32unsi: classify_mod_cases (**r unsigned I32 , int *) | mod_case_ii: classify_mod_cases (**r int , int *) | mod_default: classify_mod_cases . (**r other *) @@ -560,7 +560,7 @@ Definition classify_mod (ty1: type) (ty2: type) := | _ , _ => mod_default end . -Inductive classify_shr_cases :Set:= +Inductive classify_shr_cases :Type:= | shr_case_I32unsi: classify_shr_cases (**r unsigned I32 , int *) | shr_case_ii :classify_shr_cases (**r int , int *) | shr_default : classify_shr_cases . (**r other *) @@ -572,7 +572,7 @@ Definition classify_shr (ty1: type) (ty2: type) := | _ , _ => shr_default end. -Inductive classify_cmp_cases : Set:= +Inductive classify_cmp_cases : Type:= | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *) | cmp_case_ipip: classify_cmp_cases (**r int|ptr|array , int|ptr|array*) | cmp_case_ff: classify_cmp_cases (**r float , float *) @@ -593,7 +593,7 @@ Definition classify_cmp (ty1: type) (ty2: type) := | _ , _ => cmp_default end. -Inductive classify_fun_cases : Set:= +Inductive classify_fun_cases : Type:= | fun_case_f: typelist -> type -> classify_fun_cases (**r (pointer to) function *) | fun_default: classify_fun_cases . (**r other *) -- cgit