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 --- common/AST.v | 38 +++++++++---------- common/Errors.v | 18 ++++----- common/Events.v | 6 +-- common/Globalenvs.v | 106 ++++++++++++++++++++++++++-------------------------- common/Mem.v | 22 +++++------ common/Smallstep.v | 16 ++++---- common/Switch.v | 4 +- common/Values.v | 4 +- 8 files changed, 107 insertions(+), 107 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index ec8053d..a8655c2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -36,7 +36,7 @@ Definition ident_eq := peq. [Tint] for integers and pointers, and [Tfloat] for floating-point numbers. *) -Inductive typ : Set := +Inductive typ : Type := | Tint : typ | Tfloat : typ. @@ -58,7 +58,7 @@ Proof. decide equality. apply typ_eq. Qed. are used in particular to determine appropriate calling conventions for the function. *) -Record signature : Set := mksignature { +Record signature : Type := mksignature { sig_args: list typ; sig_res: option typ }. @@ -73,7 +73,7 @@ Definition proj_sig_res (s: signature) : typ := a ``memory chunk'' indicating the type, size and signedness of the chunk of memory being accessed. *) -Inductive memory_chunk : Set := +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 *) @@ -84,7 +84,7 @@ Inductive memory_chunk : Set := (** Initialization data for global variables. *) -Inductive init_data: Set := +Inductive init_data: Type := | Init_int8: int -> init_data | Init_int16: int -> init_data | Init_int32: int -> init_data @@ -104,16 +104,16 @@ for variables vary among the various intermediate languages and are taken as parameters to the [program] type. The other parts of whole programs are common to all languages. *) -Record program (F V: Set) : Set := mkprogram { +Record program (F V: Type) : Type := mkprogram { prog_funct: list (ident * F); prog_main: ident; prog_vars: list (ident * list init_data * V) }. -Definition prog_funct_names (F V: Set) (p: program F V) : list ident := +Definition prog_funct_names (F V: Type) (p: program F V) : list ident := map (@fst ident F) p.(prog_funct). -Definition prog_var_names (F V: Set) (p: program F V) : list ident := +Definition prog_var_names (F V: Type) (p: program F V) : list ident := map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars). (** * Generic transformations over programs *) @@ -124,7 +124,7 @@ Definition prog_var_names (F V: Set) (p: program F V) : list ident := Section TRANSF_PROGRAM. -Variable A B V: Set. +Variable A B V: Type. Variable transf: A -> B. Definition transf_program (l: list (ident * A)) : list (ident * B) := @@ -158,7 +158,7 @@ Open Local Scope string_scope. Section MAP_PARTIAL. -Variable A B C: Set. +Variable A B C: Type. Variable prefix_errmsg: A -> errmsg. Variable f: B -> res C. @@ -207,7 +207,7 @@ Qed. End MAP_PARTIAL. Remark map_partial_total: - forall (A B C: Set) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), + forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), map_partial prefix (fun b => OK (f b)) l = OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l). Proof. @@ -217,7 +217,7 @@ Proof. Qed. Remark map_partial_identity: - forall (A B: Set) (prefix: A -> errmsg) (l: list (A * B)), + forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)), map_partial prefix (fun b => OK b) l = OK l. Proof. induction l; simpl. @@ -227,7 +227,7 @@ Qed. Section TRANSF_PARTIAL_PROGRAM. -Variable A B V: Set. +Variable A B V: Type. Variable transf_partial: A -> res B. Definition prefix_funct_name (id: ident) : errmsg := @@ -271,7 +271,7 @@ End TRANSF_PARTIAL_PROGRAM. Section TRANSF_PARTIAL_PROGRAM2. -Variable A B V W: Set. +Variable A B V W: Type. Variable transf_partial_function: A -> res B. Variable transf_partial_variable: V -> res W. @@ -322,7 +322,7 @@ End TRANSF_PARTIAL_PROGRAM2. Section MATCH_PROGRAM. -Variable A B V W: Set. +Variable A B V W: Type. Variable match_fundef: A -> B -> Prop. Variable match_varinfo: V -> W -> Prop. @@ -344,7 +344,7 @@ Definition match_program (p1: program A V) (p2: program B W) : Prop := End MATCH_PROGRAM. Remark transform_partial_program2_match: - forall (A B V W: Set) + forall (A B V W: Type) (transf_partial_function: A -> res B) (transf_partial_variable: V -> res W) (p: program A V) (tp: program B W), @@ -375,12 +375,12 @@ Qed. (a.k.a. system calls) that emit an event when applied. We define a type for such functions and some generic transformation functions. *) -Record external_function : Set := mkextfun { +Record external_function : Type := mkextfun { ef_id: ident; ef_sig: signature }. -Inductive fundef (F: Set): Set := +Inductive fundef (F: Type): Type := | Internal: F -> fundef F | External: external_function -> fundef F. @@ -388,7 +388,7 @@ Implicit Arguments External [F]. Section TRANSF_FUNDEF. -Variable A B: Set. +Variable A B: Type. Variable transf: A -> B. Definition transf_fundef (fd: fundef A): fundef B := @@ -401,7 +401,7 @@ End TRANSF_FUNDEF. Section TRANSF_PARTIAL_FUNDEF. -Variable A B: Set. +Variable A B: Type. Variable transf_partial: A -> res B. Definition transf_partial_fundef (fd: fundef A): res (fundef B) := diff --git a/common/Errors.v b/common/Errors.v index 2c9bbc3..2165db3 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -28,11 +28,11 @@ Set Implicit Arguments. as a list of either substrings or positive numbers encoding a source-level identifier (see module AST). *) -Inductive errcode: Set := +Inductive errcode: Type := | MSG: string -> errcode | CTX: positive -> errcode. -Definition errmsg: Set := list errcode. +Definition errmsg: Type := list errcode. Definition msg (s: string) : errmsg := MSG s :: nil. @@ -42,7 +42,7 @@ Definition msg (s: string) : errmsg := MSG s :: nil. The return value is either [OK res] to indicate success, or [Error msg] to indicate failure. *) -Inductive res (A: Set) : Set := +Inductive res (A: Type) : Type := | OK: A -> res A | Error: errmsg -> res A. @@ -51,13 +51,13 @@ Implicit Arguments Error [A]. (** To automate the propagation of errors, we use a monadic style with the following [bind] operation. *) -Definition bind (A B: Set) (f: res A) (g: A -> res B) : res B := +Definition bind (A B: Type) (f: res A) (g: A -> res B) : res B := match f with | OK x => g x | Error msg => Error msg end. -Definition bind2 (A B C: Set) (f: res (A * B)) (g: A -> B -> res C) : res C := +Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C := match f with | OK (x, y) => g x y | Error msg => Error msg @@ -74,7 +74,7 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) : error_monad_scope. Remark bind_inversion: - forall (A B: Set) (f: res A) (g: A -> res B) (y: B), + forall (A B: Type) (f: res A) (g: A -> res B) (y: B), bind f g = OK y -> exists x, f = OK x /\ g x = OK y. Proof. @@ -84,7 +84,7 @@ Proof. Qed. Remark bind2_inversion: - forall (A B C: Set) (f: res (A*B)) (g: A -> B -> res C) (z: C), + forall (A B C: Type) (f: res (A*B)) (g: A -> B -> res C) (z: C), bind2 f g = OK z -> exists x, exists y, f = OK (x, y) /\ g x y = OK z. Proof. @@ -97,14 +97,14 @@ Open Local Scope error_monad_scope. (** This is the familiar monadic map iterator. *) -Fixpoint mmap (A B: Set) (f: A -> res B) (l: list A) {struct l} : res (list B) := +Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) := match l with | nil => OK nil | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl') end. Remark mmap_inversion: - forall (A B: Set) (f: A -> res B) (l: list A) (l': list B), + forall (A B: Type) (f: A -> res B) (l: list A) (l': list B), mmap f l = OK l' -> list_forall2 (fun x y => f x = OK y) l l'. Proof. diff --git a/common/Events.v b/common/Events.v index c44da01..011c454 100644 --- a/common/Events.v +++ b/common/Events.v @@ -32,11 +32,11 @@ Require Import Values. allow pointers to be exchanged between the program and the outside world. *) -Inductive eventval: Set := +Inductive eventval: Type := | EVint: int -> eventval | EVfloat: float -> eventval. -Record event : Set := mkevent { +Record event : Type := mkevent { ev_name: ident; ev_args: list eventval; ev_res: eventval @@ -56,7 +56,7 @@ Definition Eextcall Definition Eapp (t1 t2: trace) : trace := t1 ++ t2. -CoInductive traceinf : Set := +CoInductive traceinf : Type := | Enilinf: traceinf | Econsinf: event -> traceinf -> traceinf. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index f720914..1ce7bf5 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -47,43 +47,43 @@ Module Type GENV. (** ** Types and operations *) - Variable t: Set -> Set. + Variable t: Type -> Type. (** The type of global environments. The parameter [F] is the type of function descriptions. *) - Variable globalenv: forall (F V: Set), program F V -> t F. + Variable globalenv: forall (F V: Type), program F V -> t F. (** Return the global environment for the given program. *) - Variable init_mem: forall (F V: Set), program F V -> mem. + Variable init_mem: forall (F V: Type), program F V -> mem. (** Return the initial memory state for the given program. *) - Variable find_funct_ptr: forall (F: Set), t F -> block -> option F. + Variable find_funct_ptr: forall (F: Type), t F -> block -> option F. (** Return the function description associated with the given address, if any. *) - Variable find_funct: forall (F: Set), t F -> val -> option F. + Variable find_funct: forall (F: Type), t F -> val -> option F. (** Same as [find_funct_ptr] but the function address is given as a value, which must be a pointer with offset 0. *) - Variable find_symbol: forall (F: Set), t F -> ident -> option block. + Variable find_symbol: forall (F: Type), t F -> ident -> option block. (** Return the address of the given global symbol, if any. *) (** ** Properties of the operations. *) Hypothesis find_funct_inv: - forall (F: Set) (ge: t F) (v: val) (f: F), + forall (F: Type) (ge: t F) (v: val) (f: F), find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. Hypothesis find_funct_find_funct_ptr: - forall (F: Set) (ge: t F) (b: block), + forall (F: Type) (ge: t F) (b: block), find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b. Hypothesis find_symbol_exists: - forall (F V: Set) (p: program F V) + forall (F V: Type) (p: program F V) (id: ident) (init: list init_data) (v: V), In (id, init, v) (prog_vars p) -> exists b, find_symbol (globalenv p) id = Some b. Hypothesis find_funct_ptr_exists: - forall (F V: Set) (p: program F V) (id: ident) (f: F), + forall (F V: Type) (p: program F V) (id: ident) (f: F), list_norepet (prog_funct_names p) -> list_disjoint (prog_funct_names p) (prog_var_names p) -> In (id, f) (prog_funct p) -> @@ -91,49 +91,49 @@ Module Type GENV. /\ find_funct_ptr (globalenv p) b = Some f. Hypothesis find_funct_ptr_inversion: - forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> exists id, In (id, f) (prog_funct p). Hypothesis find_funct_inversion: - forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F), find_funct (globalenv p) v = Some f -> exists id, In (id, f) (prog_funct p). Hypothesis find_funct_ptr_symbol_inversion: - forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F), + forall (F V: Type) (p: program F V) (id: ident) (b: block) (f: F), find_symbol (globalenv p) id = Some b -> find_funct_ptr (globalenv p) b = Some f -> In (id, f) p.(prog_funct). Hypothesis find_funct_ptr_prop: - forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct_ptr (globalenv p) b = Some f -> P f. Hypothesis find_funct_prop: - forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct (globalenv p) v = Some f -> P f. Hypothesis initmem_nullptr: - forall (F V: Set) (p: program F V), + forall (F V: Type) (p: program F V), let m := init_mem p in valid_block m nullptr /\ m.(blocks) nullptr = empty_block 0 0. Hypothesis initmem_inject_neutral: - forall (F V: Set) (p: program F V), + forall (F V: Type) (p: program F V), mem_inject_neutral (init_mem p). Hypothesis find_funct_ptr_negative: - forall (F V: Set) (p: program F V) (b: block) (f: F), + forall (F V: Type) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> b < 0. Hypothesis find_symbol_not_fresh: - forall (F V: Set) (p: program F V) (id: ident) (b: block), + forall (F V: Type) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). Hypothesis find_symbol_not_nullptr: - forall (F V: Set) (p: program F V) (id: ident) (b: block), + forall (F V: Type) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b <> nullptr. Hypothesis global_addresses_distinct: - forall (F V: Set) (p: program F V) id1 id2 b1 b2, + forall (F V: Type) (p: program F V) id1 id2 b1 b2, id1<>id2 -> find_symbol (globalenv p) id1 = Some b1 -> find_symbol (globalenv p) id2 = Some b2 -> @@ -143,30 +143,30 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f). Hypothesis find_funct_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> find_funct (globalenv (transform_program transf p)) v = Some (transf f). Hypothesis find_symbol_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (s: ident), find_symbol (globalenv (transform_program transf p)) s = find_symbol (globalenv p) s. Hypothesis init_mem_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), init_mem (transform_program transf p) = init_mem p. Hypothesis find_funct_ptr_rev_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (b : block) (tf : B), find_funct_ptr (globalenv (transform_program transf p)) b = Some tf -> exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf. Hypothesis find_funct_rev_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (v : val) (tf : B), find_funct (globalenv (transform_program transf p)) v = Some tf -> exists f : A, find_funct (globalenv p) v = Some f /\ transf f = tf. @@ -175,37 +175,37 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'. Hypothesis find_funct_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> exists f', find_funct (globalenv p') v = Some f' /\ transf f = OK f'. Hypothesis find_symbol_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> init_mem p' = init_mem p. Hypothesis find_funct_ptr_rev_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (b : block) (tf : B), find_funct_ptr (globalenv p') b = Some tf -> exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. Hypothesis find_funct_rev_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> @@ -213,7 +213,7 @@ Module Type GENV. find_funct (globalenv p) v = Some f /\ transf f = OK tf. Hypothesis find_funct_ptr_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (b: block) (f: A), @@ -221,7 +221,7 @@ Module Type GENV. exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. Hypothesis find_funct_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (v: val) (f: A), @@ -229,18 +229,18 @@ Module Type GENV. exists f', find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Hypothesis find_symbol_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> init_mem p' = init_mem p. Hypothesis find_funct_ptr_rev_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (b : block) (tf : B), @@ -248,7 +248,7 @@ Module Type GENV. exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. Hypothesis find_funct_rev_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (v : val) (tf : B), @@ -260,7 +260,7 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (b : block) (f : A), @@ -268,7 +268,7 @@ Module Type GENV. exists tf : B, find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf. Hypothesis find_funct_ptr_rev_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (b : block) (tf : B), @@ -276,27 +276,27 @@ Module Type GENV. exists f : A, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf. Hypothesis find_funct_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (v : val) (f : A), find_funct (globalenv p) v = Some f -> exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf. Hypothesis find_funct_rev_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf. Hypothesis find_symbol_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (s : ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> init_mem p' = init_mem p. @@ -310,10 +310,10 @@ Module Genv: GENV. Section GENV. -Variable F: Set. (* The type of functions *) -Variable V: Set. (* The type of information over variables *) +Variable F: Type. (* The type of functions *) +Variable V: Type. (* The type of information over variables *) -Record genv : Set := mkgenv { +Record genv : Type := mkgenv { functions: ZMap.t (option F); (* mapping function ptr -> function *) nextfunction: Z; symbols: PTree.t block (* mapping symbol -> block *) @@ -588,7 +588,7 @@ Proof. generalize (find_symbol_above_nextfunction _ _ X). unfold block; unfold ZIndexed.t; intro; omega. - intros. exploit H; eauto. assumption. intros [b [X Y]]. + intros. exploit H; eauto. intros [b [X Y]]. exists b; split. unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. @@ -770,7 +770,7 @@ End GENV. Section MATCH_PROGRAM. -Variable A B V W: Set. +Variable A B V W: Type. Variable match_fun: A -> B -> Prop. Variable match_var: V -> W -> Prop. Variable p: program A V. @@ -950,7 +950,7 @@ End MATCH_PROGRAM. Section TRANSF_PROGRAM_PARTIAL2. -Variable A B V W: Set. +Variable A B V W: Type. Variable transf_fun: A -> res B. Variable transf_var: V -> res W. Variable p: program A V. @@ -1024,7 +1024,7 @@ End TRANSF_PROGRAM_PARTIAL2. Section TRANSF_PROGRAM_PARTIAL. -Variable A B V: Set. +Variable A B V: Type. Variable transf: A -> res B. Variable p: program A V. Variable p': program B V. @@ -1089,7 +1089,7 @@ End TRANSF_PROGRAM_PARTIAL. Section TRANSF_PROGRAM. -Variable A B V: Set. +Variable A B V: Type. Variable transf: A -> B. Variable p: program A V. Let tp := transform_program transf p. diff --git a/common/Mem.v b/common/Mem.v index e169dfc..01c1975 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -31,20 +31,20 @@ Require Import Integers. Require Import Floats. Require Import Values. -Definition update (A: Set) (x: Z) (v: A) (f: Z -> A) : Z -> A := +Definition update (A: Type) (x: Z) (v: A) (f: Z -> A) : Z -> A := fun y => if zeq y x then v else f y. Implicit Arguments update [A]. Lemma update_s: - forall (A: Set) (x: Z) (v: A) (f: Z -> A), + forall (A: Type) (x: Z) (v: A) (f: Z -> A), update x v f x = v. Proof. intros; unfold update. apply zeq_true. Qed. Lemma update_o: - forall (A: Set) (x: Z) (v: A) (f: Z -> A) (y: Z), + forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z), x <> y -> update x v f y = f y. Proof. intros; unfold update. apply zeq_false; auto. @@ -62,17 +62,17 @@ Qed. [d+2] and [d+3]. The [Cont] contents enable detecting future writes that would partially overlap the 4-byte value. *) -Inductive content : Set := +Inductive content : Type := | Undef: content (**r undefined contents *) | Datum: nat -> val -> content (**r first byte of a value *) | Cont: content. (**r continuation bytes for a multi-byte value *) -Definition contentmap : Set := Z -> content. +Definition contentmap : Type := Z -> content. (** A memory block comprises the dimensions of the block (low and high bounds) plus a mapping from byte offsets to contents. *) -Record block_contents : Set := mkblock { +Record block_contents : Type := mkblock { low: Z; high: Z; contents: contentmap @@ -82,7 +82,7 @@ Record block_contents : Set := mkblock { integers) to blocks. We also maintain the address of the next unallocated block, and a proof that this address is positive. *) -Record mem : Set := mkmem { +Record mem : Type := mkmem { blocks: Z -> block_contents; nextblock: block; nextblock_pos: nextblock > 0 @@ -455,7 +455,7 @@ Proof. Defined. Lemma in_bounds_true: - forall m chunk b ofs (A: Set) (a1 a2: A), + forall m chunk b ofs (A: Type) (a1 a2: A), valid_access m chunk b ofs -> (if in_bounds m chunk b ofs then a1 else a2) = a1. Proof. @@ -858,7 +858,7 @@ Qed. Inductive load_store_cases (chunk1: memory_chunk) (b1: block) (ofs1: Z) - (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Set := + (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type := | lsc_similar: b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 = size_chunk chunk2 -> load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 @@ -1277,7 +1277,7 @@ Qed. Section GENERIC_INJECT. -Definition meminj : Set := block -> option (block * Z). +Definition meminj : Type := block -> option (block * Z). Variable val_inj: meminj -> val -> val -> Prop. @@ -2838,7 +2838,7 @@ Qed. (** Signed 8- and 16-bit stores can be performed like unsigned stores. *) Remark in_bounds_equiv: - forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A), + forall chunk1 chunk2 m b ofs (A: Type) (a1 a2: A), size_chunk chunk1 = size_chunk chunk2 -> (if in_bounds m chunk1 b ofs then a1 else a2) = (if in_bounds m chunk2 b ofs then a1 else a2). diff --git a/common/Smallstep.v b/common/Smallstep.v index a2634be..f41fe4e 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -33,8 +33,8 @@ Set Implicit Arguments. Section CLOSURES. -Variable genv: Set. -Variable state: Set. +Variable genv: Type. +Variable state: Type. (** A one-step transition relation has the following signature. It is parameterized by a global environment, which does not @@ -197,7 +197,7 @@ Qed. (** An alternate, equivalent definition of [forever] that is useful for coinductive reasoning. *) -Variable A: Set. +Variable A: Type. Variable order: A -> A -> Prop. CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := @@ -290,7 +290,7 @@ Qed. finite prefix of this trace, or the whole trace.) *) -Inductive program_behavior: Set := +Inductive program_behavior: Type := | Terminates: trace -> int -> program_behavior | Diverges: traceinf -> program_behavior. @@ -326,8 +326,8 @@ Section SIMULATION. (** The first small-step semantics is axiomatized as follows. *) -Variable genv1: Set. -Variable state1: Set. +Variable genv1: Type. +Variable state1: Type. Variable step1: genv1 -> state1 -> trace -> state1 -> Prop. Variable initial_state1: state1 -> Prop. Variable final_state1: state1 -> int -> Prop. @@ -335,8 +335,8 @@ Variable ge1: genv1. (** The second small-step semantics is also axiomatized. *) -Variable genv2: Set. -Variable state2: Set. +Variable genv2: Type. +Variable state2: Type. Variable step2: genv2 -> state2 -> trace -> state2 -> Prop. Variable initial_state2: state2 -> Prop. Variable final_state2: state2 -> int -> Prop. diff --git a/common/Switch.v b/common/Switch.v index 8124aea..179d4d2 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -23,7 +23,7 @@ Require Import Integers. (** A multi-way branch is composed of a list of (key, action) pairs, plus a default action. *) -Definition table : Set := list (int * nat). +Definition table : Type := list (int * nat). Fixpoint switch_target (n: int) (dfl: nat) (cases: table) {struct cases} : nat := @@ -37,7 +37,7 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table) Each node of the tree performs an equality test or a less-than test against one of the keys. *) -Inductive comptree : Set := +Inductive comptree : Type := | CTaction: nat -> comptree | CTifeq: int -> nat -> comptree -> comptree | CTiflt: int -> comptree -> comptree -> comptree. diff --git a/common/Values.v b/common/Values.v index 8182d7a..9645e8a 100644 --- a/common/Values.v +++ b/common/Values.v @@ -21,7 +21,7 @@ Require Import AST. Require Import Integers. Require Import Floats. -Definition block : Set := Z. +Definition block : Type := Z. Definition eq_block := zeq. (** A value is either: @@ -33,7 +33,7 @@ Definition eq_block := zeq. value of an uninitialized variable. *) -Inductive val: Set := +Inductive val: Type := | Vundef: val | Vint: int -> val | Vfloat: float -> val -- cgit v1.2.3