From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 5 Jun 2009 13:39:59 +0000
Subject: [PATCH] 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
---
Changelog | 5 +
arm/Asm.v | 18 +--
arm/Constprop.v | 12 +-
arm/Machregs.v | 2 +-
arm/Op.v | 28 ++--
arm/Selection.v | 42 +++---
arm/Selectionproof.v | 4 -
arm/linux/Stacklayout.v | 2 +-
backend/Allocproof.v | 4 +-
backend/Bounds.v | 8 +-
backend/CSE.v | 4 +-
backend/Cminor.v | 18 +--
backend/CminorSel.v | 14 +-
backend/Coloring.v | 4 +-
backend/Coloringproof.v | 20 +--
backend/InterfGraph.v | 22 +--
backend/Kildall.v | 10 +-
backend/LTL.v | 10 +-
backend/LTLin.v | 10 +-
backend/Linear.v | 10 +-
backend/Linearizeproof.v | 2 +-
backend/Locations.v | 4 +-
backend/Mach.v | 4 +-
backend/Machabstr.v | 6 +-
backend/Machconcr.v | 4 +-
backend/RTL.v | 10 +-
backend/RTLgen.v | 20 +--
backend/RTLgenspec.v | 185 ++++++++-----------------
backend/Registers.v | 6 +-
backend/Stacking.v | 2 +-
backend/Stackingproof.v | 4 +-
backend/Stackingtyping.v | 2 +-
backend/Tailcallproof.v | 8 +-
backend/Tunnelingproof.v | 6 +-
cfrontend/Cminorgen.v | 2 +-
cfrontend/Cminorgenproof.v | 4 +-
cfrontend/Csem.v | 2 +-
cfrontend/Csharpminor.v | 18 +--
cfrontend/Cshmgenproof1.v | 4 +-
cfrontend/Cshmgenproof3.v | 215 +++++++++++++++--------------
cfrontend/Csyntax.v | 52 +++----
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 +-
driver/Compiler.v | 14 +-
driver/Complements.v | 2 +-
extraction/Kildall.ml.patch | 31 ++---
extraction/convert | 5 +-
lib/Coqlib.v | 120 ++++++++--------
lib/Floats.v | 2 +-
lib/Inclusion.v | 24 ++--
lib/Integers.v | 6 +-
lib/Iteration.v | 8 +-
lib/Lattice.v | 27 +---
lib/Maps.v | 260 +++++++++++++++++------------------
lib/Ordered.v | 19 +++
lib/Parmov.v | 8 +-
powerpc/Asm.v | 16 +--
powerpc/Asmgen.v | 2 +-
powerpc/Constprop.v | 12 +-
powerpc/Machregs.v | 2 +-
powerpc/Op.v | 24 ++--
powerpc/Selection.v | 38 ++---
powerpc/Selectionproof.v | 2 +
powerpc/eabi/Stacklayout.v | 2 +-
powerpc/macosx/Stacklayout.v | 2 +-
71 files changed, 795 insertions(+), 852 deletions(-)
diff --git a/Changelog b/Changelog
index 3be2d3613..004d5cbec 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,8 @@
+Release 1.4.1, 2009-06-05
+=========================
+
+- Adapted to Coq 8.2-1. No changes in functionality.
+
Release 1.4, 2009-04-20
=======================
diff --git a/arm/Asm.v b/arm/Asm.v
index 3bb2cca24..79feee72b 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -30,13 +30,13 @@ Require Conventions.
(** Integer registers, floating-point registers. *)
-Inductive ireg: Set :=
+Inductive ireg: Type :=
| IR0: ireg | IR1: ireg | IR2: ireg | IR3: ireg
| IR4: ireg | IR5: ireg | IR6: ireg | IR7: ireg
| IR8: ireg | IR9: ireg | IR10: ireg | IR11: ireg
| IR12: ireg | IR13: ireg | IR14: ireg.
-Inductive freg: Set :=
+Inductive freg: Type :=
| FR0: freg | FR1: freg | FR2: freg | FR3: freg
| FR4: freg | FR5: freg | FR6: freg | FR7: freg.
@@ -48,7 +48,7 @@ Proof. decide equality. Defined.
(** Bits in the condition register. *)
-Inductive crbit: Set :=
+Inductive crbit: Type :=
| CReq: crbit (**r equal *)
| CRne: crbit (**r not equal *)
| CRhs: crbit (**r unsigned higher or same *)
@@ -74,7 +74,7 @@ Proof. decide equality. Defined.
Definition label := positive.
-Inductive shift_op : Set :=
+Inductive shift_op : Type :=
| SOimm: int -> shift_op
| SOreg: ireg -> shift_op
| SOlslimm: ireg -> int -> shift_op
@@ -86,7 +86,7 @@ Inductive shift_op : Set :=
| SOrorimm: ireg -> int -> shift_op
| SOrorreg: ireg -> ireg -> shift_op.
-Inductive shift_addr : Set :=
+Inductive shift_addr : Type :=
| SAimm: int -> shift_addr
| SAreg: ireg -> shift_addr
| SAlsl: ireg -> int -> shift_addr
@@ -94,7 +94,7 @@ Inductive shift_addr : Set :=
| SAasr: ireg -> int -> shift_addr
| SAror: ireg -> int -> shift_addr.
-Inductive instruction : Set :=
+Inductive instruction : Type :=
(* Core instructions *)
| Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *)
| Pand: ireg -> ireg -> shift_op -> instruction (**r bitwise and *)
@@ -242,7 +242,7 @@ Definition program := AST.program fundef unit.
(** The PowerPC has a great many registers, some general-purpose, some very
specific. We model only the following registers: *)
-Inductive preg: Set :=
+Inductive preg: Type :=
| IR: ireg -> preg (**r integer registers *)
| FR: freg -> preg (**r float registers *)
| CR: crbit -> preg (**r bits in the condition register *)
@@ -315,7 +315,7 @@ Variable ge: genv.
set and memory state after execution of the instruction at [rs#PC],
or [Error] if the processor is stuck. *)
-Inductive outcome: Set :=
+Inductive outcome: Type :=
| OK: regset -> mem -> outcome
| Error: outcome.
@@ -621,7 +621,7 @@ Definition loc_external_result (sg: signature) : preg :=
(** Execution of the instruction at [rs#PC]. *)
-Inductive state: Set :=
+Inductive state: Type :=
| State: regset -> mem -> state.
Inductive step: state -> trace -> state -> Prop :=
diff --git a/arm/Constprop.v b/arm/Constprop.v
index b51d974e6..5bd84b6d6 100644
--- a/arm/Constprop.v
+++ b/arm/Constprop.v
@@ -32,7 +32,7 @@ Require Import Kildall.
(** To each pseudo-register at each program point, the static analysis
associates a compile-time approximation taken from the following set. *)
-Inductive approx : Set :=
+Inductive approx : Type :=
| Novalue: approx (** No value possible, code is unreachable. *)
| Unknown: approx (** All values are possible,
no compile-time information is available. *)
@@ -139,7 +139,7 @@ Definition eval_static_condition (cond: condition) (vl: list approx) :=
end.
*)
-Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Set :=
+Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type :=
| eval_static_condition_case1:
forall c n1 n2,
eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil)
@@ -274,7 +274,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
end.
*)
-Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Set :=
+Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type :=
| eval_static_operation_case1:
forall v1,
eval_static_operation_cases (Omove) (v1::nil)
@@ -735,7 +735,7 @@ Definition cond_strength_reduction (cond: condition) (args: list reg) :=
end.
*)
-Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg), Set :=
+Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg), Type :=
| cond_strength_reduction_case1:
forall c r1 r2,
cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil)
@@ -886,7 +886,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
end.
*)
-Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg), Set :=
+Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg), Type :=
| op_strength_reduction_case1:
forall r1 r2,
op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil)
@@ -1120,7 +1120,7 @@ Definition addr_strength_reduction (addr: addressing) (args: list reg) :=
end.
*)
-Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Set :=
+Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Type :=
| addr_strength_reduction_case1:
forall r1 r2,
addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil)
diff --git a/arm/Machregs.v b/arm/Machregs.v
index 3466c0b08..2e422d272 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -29,7 +29,7 @@ Require Import AST.
The type [mreg] does not include special-purpose machine registers
such as the stack pointer and the condition codes. *)
-Inductive mreg: Set :=
+Inductive mreg: Type :=
(** Allocatable integer regs *)
| R0: mreg | R1: mreg | R2: mreg | R3: mreg
| R4: mreg | R5: mreg | R6: mreg | R7: mreg
diff --git a/arm/Op.v b/arm/Op.v
index bde725206..47cbc0cea 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -34,13 +34,13 @@ Require Import Globalenvs.
Set Implicit Arguments.
-Record shift_amount : Set :=
+Record shift_amount : Type :=
mk_shift_amount {
s_amount: int;
s_amount_ltu: Int.ltu s_amount (Int.repr 32) = true
}.
-Inductive shift : Set :=
+Inductive shift : Type :=
| Slsl: shift_amount -> shift
| Slsr: shift_amount -> shift
| Sasr: shift_amount -> shift
@@ -48,7 +48,7 @@ Inductive shift : Set :=
(** Conditions (boolean-valued operators). *)
-Inductive condition : Set :=
+Inductive condition : Type :=
| Ccomp: comparison -> condition (**r signed integer comparison *)
| Ccompu: comparison -> condition (**r unsigned integer comparison *)
| Ccompshift: comparison -> shift -> condition (**r signed integer comparison *)
@@ -61,7 +61,7 @@ Inductive condition : Set :=
(** Arithmetic and logical operations. In the descriptions, [rd] is the
result of the operation and [r1], [r2], etc, are the arguments. *)
-Inductive operation : Set :=
+Inductive operation : Type :=
| Omove: operation (**r [rd = r1] *)
| Ointconst: int -> operation (**r [rd] is set to the given integer constant *)
| Ofloatconst: float -> operation (**r [rd] is set to the given float constant *)
@@ -119,7 +119,7 @@ Inductive operation : Set :=
(** Addressing modes. [r1], [r2], etc, are the arguments to the
addressing. *)
-Inductive addressing: Set :=
+Inductive addressing: Type :=
| Aindexed: int -> addressing (**r Address is [r1 + offset] *)
| Aindexed2: addressing (**r Address is [r1 + r2] *)
| Aindexed2shift: shift -> addressing (**r Address is [r1 + shifted r2] *)
@@ -217,7 +217,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
end.
Definition eval_operation
- (F: Set) (genv: Genv.t F) (sp: val)
+ (F: Type) (genv: Genv.t F) (sp: val)
(op: operation) (vl: list val): option val :=
match op, vl with
| Omove, v1::nil => Some v1
@@ -301,7 +301,7 @@ Definition eval_operation
end.
Definition eval_addressing
- (F: Set) (genv: Genv.t F) (sp: val)
+ (F: Type) (genv: Genv.t F) (sp: val)
(addr: addressing) (vl: list val) : option val :=
match addr, vl with
| Aindexed n, Vptr b1 n1 :: nil =>
@@ -382,7 +382,7 @@ Qed.
Section GENV_TRANSF.
-Variable F1 F2: Set.
+Variable F1 F2: Type.
Variable ge1: Genv.t F1.
Variable ge2: Genv.t F2.
Hypothesis agree_on_symbols:
@@ -413,14 +413,14 @@ End GENV_TRANSF.
(** Recognition of move operations. *)
Definition is_move_operation
- (A: Set) (op: operation) (args: list A) : option A :=
+ (A: Type) (op: operation) (args: list A) : option A :=
match op, args with
| Omove, arg :: nil => Some arg
| _, _ => None
end.
Lemma is_move_operation_correct:
- forall (A: Set) (op: operation) (args: list A) (a: A),
+ forall (A: Type) (op: operation) (args: list A) (a: A),
is_move_operation op args = Some a ->
op = Omove /\ args = a :: nil.
Proof.
@@ -523,7 +523,7 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
Section SOUNDNESS.
-Variable A: Set.
+Variable A: Type.
Variable genv: Genv.t A.
Lemma type_of_operation_sound:
@@ -584,7 +584,7 @@ End SOUNDNESS.
Section EVAL_OP_TOTAL.
-Variable F: Set.
+Variable F: Type.
Variable genv: Genv.t F.
Definition find_symbol_offset (id: ident) (ofs: int) : val :=
@@ -774,7 +774,7 @@ End EVAL_OP_TOTAL.
Section EVAL_LESSDEF.
-Variable F: Set.
+Variable F: Type.
Variable genv: Genv.t F.
Ltac InvLessdef :=
@@ -900,7 +900,7 @@ Definition op_for_binary_addressing (addr: addressing) : operation :=
end.
Lemma eval_op_for_binary_addressing:
- forall (F: Set) (ge: Genv.t F) sp addr args v,
+ forall (F: Type) (ge: Genv.t F) sp addr args v,
(length args >= 2)%nat ->
eval_addressing ge sp addr args = Some v ->
eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
diff --git a/arm/Selection.v b/arm/Selection.v
index d04a4ca35..12cc1b27a 100644
--- a/arm/Selection.v
+++ b/arm/Selection.v
@@ -118,7 +118,7 @@ Definition notint (e: expr) :=
characterizes the expressions that match each of the 4 cases of interest.
*)
-Inductive notint_cases: forall (e: expr), Set :=
+Inductive notint_cases: forall (e: expr), Type :=
| notint_case1:
forall s t1,
notint_cases (Eop (Oshift s) (t1:::Enil))
@@ -208,7 +208,7 @@ Definition addimm (n: int) (e: expr) :=
end.
*)
-Inductive addimm_cases: forall (e: expr), Set :=
+Inductive addimm_cases: forall (e: expr), Type :=
| addimm_case1:
forall m,
addimm_cases (Eop (Ointconst m) Enil)
@@ -270,7 +270,7 @@ Definition add (e1: expr) (e2: expr) :=
end.
*)
-Inductive add_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
| add_case1:
forall n1 t2,
add_cases (Eop (Ointconst n1) Enil) (t2)
@@ -352,7 +352,7 @@ Definition sub (e1: expr) (e2: expr) :=
end.
*)
-Inductive sub_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
| sub_case1:
forall t1 n2,
sub_cases (t1) (Eop (Ointconst n2) Enil)
@@ -430,7 +430,7 @@ Definition shlimm (e1: expr) :=
end.
*)
-Inductive shlimm_cases: forall (e1: expr), Set :=
+Inductive shlimm_cases: forall (e1: expr), Type :=
| shlimm_case1:
forall n1,
shlimm_cases (Eop (Ointconst n1) Enil)
@@ -481,7 +481,7 @@ Definition shruimm (e1: expr) :=
end.
*)
-Inductive shruimm_cases: forall (e1: expr), Set :=
+Inductive shruimm_cases: forall (e1: expr), Type :=
| shruimm_case1:
forall n1,
shruimm_cases (Eop (Ointconst n1) Enil)
@@ -531,7 +531,7 @@ Definition shrimm (e1: expr) :=
end.
*)
-Inductive shrimm_cases: forall (e1: expr), Set :=
+Inductive shrimm_cases: forall (e1: expr), Type :=
| shrimm_case1:
forall n1,
shrimm_cases (Eop (Ointconst n1) Enil)
@@ -598,7 +598,7 @@ Definition mulimm (n1: int) (e2: expr) :=
end.
*)
-Inductive mulimm_cases: forall (e2: expr), Set :=
+Inductive mulimm_cases: forall (e2: expr), Type :=
| mulimm_case1:
forall (n2: int),
mulimm_cases (Eop (Ointconst n2) Enil)
@@ -642,7 +642,7 @@ Definition mul (e1: expr) (e2: expr) :=
end.
*)
-Inductive mul_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive mul_cases: forall (e1: expr) (e2: expr), Type :=
| mul_case1:
forall (n1: int) (t2: expr),
mul_cases (Eop (Ointconst n1) Enil) (t2)
@@ -690,7 +690,7 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
Enil) :::
Enil))).
-Inductive divu_cases: forall (e2: expr), Set :=
+Inductive divu_cases: forall (e2: expr), Type :=
| divu_case1:
forall (n2: int),
divu_cases (Eop (Ointconst n2) Enil)
@@ -759,7 +759,7 @@ Definition and (e1: expr) (e2: expr) :=
end.
*)
-Inductive and_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive and_cases: forall (e1: expr) (e2: expr), Type :=
| and_case1:
forall s t1 t2,
and_cases (Eop (Oshift s) (t1:::Enil)) (t2)
@@ -836,7 +836,7 @@ Definition or (e1: expr) (e2: expr) :=
(* TODO: symmetric of first case *)
-Inductive or_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
| or_case1:
forall n1 t1 n2 t2,
or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil))
@@ -886,7 +886,7 @@ Definition xor (e1: expr) (e2: expr) :=
end.
*)
-Inductive xor_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive xor_cases: forall (e1: expr) (e2: expr), Type :=
| xor_case1:
forall s t1 t2,
xor_cases (Eop (Oshift s) (t1:::Enil)) (t2)
@@ -919,7 +919,7 @@ Definition xor (e1: expr) (e2: expr) :=
(** ** General shifts *)
-Inductive shift_cases: forall (e1: expr), Set :=
+Inductive shift_cases: forall (e1: expr), Type :=
| shift_case1:
forall (n2: int),
shift_cases (Eop (Ointconst n2) Enil)
@@ -961,7 +961,7 @@ Definition shr (e1: expr) (e2: expr) :=
(** ** Truncations and sign extensions *)
-Inductive cast8signed_cases: forall (e1: expr), Set :=
+Inductive cast8signed_cases: forall (e1: expr), Type :=
| cast8signed_case1:
forall (e2: expr),
cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
@@ -983,7 +983,7 @@ Definition cast8signed (e: expr) :=
| cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil)
end.
-Inductive cast8unsigned_cases: forall (e1: expr), Set :=
+Inductive cast8unsigned_cases: forall (e1: expr), Type :=
| cast8unsigned_case1:
forall (e2: expr),
cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil))
@@ -1005,7 +1005,7 @@ Definition cast8unsigned (e: expr) :=
| cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil)
end.
-Inductive cast16signed_cases: forall (e1: expr), Set :=
+Inductive cast16signed_cases: forall (e1: expr), Type :=
| cast16signed_case1:
forall (e2: expr),
cast16signed_cases (Eop Ocast16signed (e2 ::: Enil))
@@ -1027,7 +1027,7 @@ Definition cast16signed (e: expr) :=
| cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil)
end.
-Inductive cast16unsigned_cases: forall (e1: expr), Set :=
+Inductive cast16unsigned_cases: forall (e1: expr), Type :=
| cast16unsigned_case1:
forall (e2: expr),
cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil))
@@ -1049,7 +1049,7 @@ Definition cast16unsigned (e: expr) :=
| cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil)
end.
-Inductive singleoffloat_cases: forall (e1: expr), Set :=
+Inductive singleoffloat_cases: forall (e1: expr), Type :=
| singleoffloat_case1:
forall (e2: expr),
singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil))
@@ -1084,7 +1084,7 @@ Definition comp (e1: expr) (e2: expr) :=
end.
*)
-Inductive comp_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
| comp_case1:
forall n1 t2,
comp_cases (Eop (Ointconst n1) Enil) (t2)
@@ -1204,7 +1204,7 @@ Definition addressing (e: expr) :=
end.
*)
-Inductive addressing_cases: forall (e: expr), Set :=
+Inductive addressing_cases: forall (e: expr), Type :=
| addressing_case2:
forall n,
addressing_cases (Eop (Oaddrstack n) Enil)
diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v
index 10f93f3a4..967e2292c 100644
--- a/arm/Selectionproof.v
+++ b/arm/Selectionproof.v
@@ -1389,10 +1389,6 @@ Proof.
econstructor. destruct k; simpl in H; simpl; auto.
rewrite <- H0; reflexivity.
constructor; auto.
- (* assign *)
- exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split.
- constructor. auto with evalexpr.
- constructor; auto.
(* store *)
econstructor; split.
eapply eval_store; eauto with evalexpr.
diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v
index dd3c6a1da..b374bfd9d 100644
--- a/arm/linux/Stacklayout.v
+++ b/arm/linux/Stacklayout.v
@@ -40,7 +40,7 @@ the boundaries between areas in the frame part.
Definition fe_ofs_arg := 0.
-Record frame_env : Set := mk_frame_env {
+Record frame_env : Type := mk_frame_env {
fe_size: Z;
fe_ofs_link: Z;
fe_ofs_retaddr: Z;
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3971fb6d7..e2387b5d0 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -167,7 +167,7 @@ Proof.
eapply DS.fixpoint_solution. unfold analyze in H; eauto.
auto. auto. auto. auto.
unfold transfer. rewrite H3.
- red; intros. elim (Regset.empty_1 _ H4).
+ red; intros. elim (Regset.empty_1 H4).
unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
Qed.
@@ -581,7 +581,7 @@ Proof.
rewrite H. simpl.
caseEq (Regset.mem res live!!pc); intro LV;
rewrite LV in AG.
- generalize (Regset.mem_2 _ _ LV). intro LV'.
+ generalize (Regset.mem_2 LV). intro LV'.
generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
unfold correct_alloc_instr, is_redundant_move.
caseEq (is_move_operation op args).
diff --git a/backend/Bounds.v b/backend/Bounds.v
index d1ed28d57..8c5f536da 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -30,7 +30,7 @@ Require Import Conventions.
These properties are used later to reason about the layout of
the activation record. *)
-Record bounds : Set := mkbounds {
+Record bounds : Type := mkbounds {
bound_int_local: Z;
bound_float_local: Z;
bound_int_callee_save: Z;
@@ -116,7 +116,7 @@ Definition slots_of_instr (i: instruction) : list slot :=
| _ => nil
end.
-Definition max_over_list (A: Set) (valu: A -> Z) (l: list A) : Z :=
+Definition max_over_list (A: Type) (valu: A -> Z) (l: list A) : Z :=
List.fold_left (fun m l => Zmax m (valu l)) l 0.
Definition max_over_instrs (valu: instruction -> Z) : Z :=
@@ -151,7 +151,7 @@ Definition outgoing_space (i: instruction) :=
match i with Lcall sig _ => size_arguments sig | _ => 0 end.
Lemma max_over_list_pos:
- forall (A: Set) (valu: A -> Z) (l: list A),
+ forall (A: Type) (valu: A -> Z) (l: list A),
max_over_list A valu l >= 0.
Proof.
intros until valu. unfold max_over_list.
@@ -196,7 +196,7 @@ Qed.
(** We now show the correctness of the inferred bounds. *)
Lemma max_over_list_bound:
- forall (A: Set) (valu: A -> Z) (l: list A) (x: A),
+ forall (A: Type) (valu: A -> Z) (l: list A) (x: A),
In x l -> valu x <= max_over_list A valu l.
Proof.
intros until x. unfold max_over_list.
diff --git a/backend/CSE.v b/backend/CSE.v
index 13e9be8e0..cad350349 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -49,7 +49,7 @@ Require Import Kildall.
Definition valnum := positive.
-Inductive rhs : Set :=
+Inductive rhs : Type :=
| Op: operation -> list valnum -> rhs
| Load: memory_chunk -> addressing -> list valnum -> rhs.
@@ -85,7 +85,7 @@ Qed.
we maintain the next unused value number, so as to easily generate
fresh value numbers. *)
-Record numbering : Set := mknumbering {
+Record numbering : Type := mknumbering {
num_next: valnum;
num_eqs: list (valnum * rhs);
num_reg: PTree.t valnum
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 35bf39160..b48db2d6e 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -33,13 +33,13 @@ Require Import Switch.
statements, functions and programs. We first define the constants
and operators that occur within expressions. *)
-Inductive constant : Set :=
+Inductive constant : Type :=
| Ointconst: int -> constant (**r integer constant *)
| Ofloatconst: float -> constant (**r floating-point constant *)
| Oaddrsymbol: ident -> int -> constant (**r address of the symbol plus the offset *)
| Oaddrstack: int -> constant. (**r stack pointer plus the given offset *)
-Inductive unary_operation : Set :=
+Inductive unary_operation : Type :=
| Ocast8unsigned: unary_operation (**r 8-bit zero extension *)
| Ocast8signed: unary_operation (**r 8-bit sign extension *)
| Ocast16unsigned: unary_operation (**r 16-bit zero extension *)
@@ -55,7 +55,7 @@ Inductive unary_operation : Set :=
| Ofloatofint: unary_operation (**r float to signed integer *)
| Ofloatofintu: unary_operation. (**r float to unsigned integer *)
-Inductive binary_operation : Set :=
+Inductive binary_operation : Type :=
| Oadd: binary_operation (**r integer addition *)
| Osub: binary_operation (**r integer subtraction *)
| Omul: binary_operation (**r integer multiplication *)
@@ -81,7 +81,7 @@ Inductive binary_operation : Set :=
arithmetic operations, reading store locations, and conditional
expressions (similar to [e1 ? e2 : e3] in C). *)
-Inductive expr : Set :=
+Inductive expr : Type :=
| Evar : ident -> expr
| Econst : constant -> expr
| Eunop : unary_operation -> expr -> expr
@@ -97,7 +97,7 @@ Inductive expr : Set :=
Definition label := ident.
-Inductive stmt : Set :=
+Inductive stmt : Type :=
| Sskip: stmt
| Sassign : ident -> expr -> stmt
| Sstore : memory_chunk -> expr -> expr -> stmt
@@ -120,7 +120,7 @@ Inductive stmt : Set :=
automatically before the function returns. Pointers into this block
can be taken with the [Oaddrstack] operator. *)
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
fn_sig: signature;
fn_params: list ident;
fn_vars: list ident;
@@ -172,7 +172,7 @@ Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
(** Continuations *)
-Inductive cont: Set :=
+Inductive cont: Type :=
| Kstop: cont (**r stop program execution *)
| Kseq: stmt -> cont -> cont (**r execute stmt, then cont *)
| Kblock: cont -> cont (**r exit a block, then do cont *)
@@ -181,7 +181,7 @@ Inductive cont: Set :=
(** States *)
-Inductive state: Set :=
+Inductive state: Type :=
| State: (**r Execution within a function *)
forall (f: function) (**r currently executing function *)
(s: stmt) (**r statement under consideration *)
@@ -536,7 +536,7 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
statements evaluate to``outcomes'' indicating how execution should
proceed afterwards. *)
-Inductive outcome: Set :=
+Inductive outcome: Type :=
| Out_normal: outcome (**r continue in sequence *)
| Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *)
| Out_return: option val -> outcome (**r return immediately to caller *)
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index bfe92a40a..1e798b5f6 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -40,7 +40,7 @@ Require Import Smallstep.
boolean value only and not their exact value.
*)
-Inductive expr : Set :=
+Inductive expr : Type :=
| Evar : ident -> expr
| Eop : operation -> exprlist -> expr
| Eload : memory_chunk -> addressing -> exprlist -> expr
@@ -48,13 +48,13 @@ Inductive expr : Set :=
| Elet : expr -> expr -> expr
| Eletvar : nat -> expr
-with condexpr : Set :=
+with condexpr : Type :=
| CEtrue: condexpr
| CEfalse: condexpr
| CEcond: condition -> exprlist -> condexpr
| CEcondition : condexpr -> condexpr -> condexpr -> condexpr
-with exprlist : Set :=
+with exprlist : Type :=
| Enil: exprlist
| Econs: expr -> exprlist -> exprlist.
@@ -62,7 +62,7 @@ with exprlist : Set :=
if/then/else conditional is a [condexpr], and the [Sstore] construct
uses a machine-dependent addressing mode. *)
-Inductive stmt : Set :=
+Inductive stmt : Type :=
| Sskip: stmt
| Sassign : ident -> expr -> stmt
| Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
@@ -78,7 +78,7 @@ Inductive stmt : Set :=
| Slabel: label -> stmt -> stmt
| Sgoto: label -> stmt.
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
fn_sig: signature;
fn_params: list ident;
fn_vars: list ident;
@@ -108,7 +108,7 @@ Definition letenv := list val.
(** Continuations *)
-Inductive cont: Set :=
+Inductive cont: Type :=
| Kstop: cont (**r stop program execution *)
| Kseq: stmt -> cont -> cont (**r execute stmt, then cont *)
| Kblock: cont -> cont (**r exit a block, then do cont *)
@@ -117,7 +117,7 @@ Inductive cont: Set :=
(** States *)
-Inductive state: Set :=
+Inductive state: Type :=
| State: (**r execution within a function *)
forall (f: function) (**r currently executing function *)
(s: stmt) (**r statement under consideration *)
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 7204bc797..67824ae3d 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -93,7 +93,7 @@ Require Import InterfGraph.
Definition add_interf_live
(filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
- Regset.fold graph
+ Regset.fold
(fun r g => if filter r then add_interf r res g else g) live g.
Definition add_interf_op
@@ -113,7 +113,7 @@ Definition add_interf_move
Definition add_interf_destroyed
(live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
List.fold_left
- (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g)
+ (fun g mr => Regset.fold (fun r g => add_interf_mreg r mr g) live g)
destroyed g.
Definition add_interfs_indirect_call
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index c86652a36..92ac0676d 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -148,7 +148,7 @@ Qed.
Lemma add_interf_destroyed_incl_aux_2:
forall mr live g,
graph_incl g
- (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
+ (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
Proof.
intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1.
Qed.
@@ -219,7 +219,7 @@ Lemma add_interf_destroyed_correct_aux_2:
forall mr live g r,
Regset.In r live ->
interfere_mreg r mr
- (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
+ (Regset.fold (fun r g => add_interf_mreg r mr g) live g).
Proof.
intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1.
apply Regset.elements_1. auto.
@@ -619,12 +619,12 @@ Lemma check_coloring_1_correct:
coloring r1 <> coloring r2.
Proof.
unfold check_coloring_1. intros.
- assert (FSetInterface.compat_bool OrderedRegReg.eq
+ assert (compat_bool OrderedRegReg.eq
(fun r1r2 => if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2))
then false else true)).
red. unfold OrderedRegReg.eq. unfold OrderedReg.eq.
intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
- generalize (SetRegReg.for_all_2 _ _ H1 H _ H0).
+ generalize (SetRegReg.for_all_2 H1 H H0).
simpl. case (Loc.eq (coloring r1) (coloring r2)); intro.
intro; discriminate. auto.
Qed.
@@ -636,12 +636,12 @@ Lemma check_coloring_2_correct:
coloring r1 <> R mr2.
Proof.
unfold check_coloring_2. intros.
- assert (FSetInterface.compat_bool OrderedRegMreg.eq
+ assert (compat_bool OrderedRegMreg.eq
(fun r1r2 => if Loc.eq (coloring (fst r1r2)) (R (snd r1r2))
then false else true)).
red. unfold OrderedRegMreg.eq. unfold OrderedReg.eq.
intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto.
- generalize (SetRegMreg.for_all_2 _ _ H1 H _ H0).
+ generalize (SetRegMreg.for_all_2 H1 H H0).
simpl. case (Loc.eq (coloring r1) (R mr2)); intro.
intro; discriminate. auto.
Qed.
@@ -920,12 +920,12 @@ Proof.
intros. rewrite H2. unfold allregs.
elim (ordered_pair_charact x y); intro.
apply alloc_of_coloring_correct_1. auto.
- change OrderedReg.t with reg. rewrite <- H6.
+ change positive with reg. rewrite <- H6.
change (interfere x y g). unfold g.
apply interf_graph_correct_2; auto.
apply sym_not_equal.
apply alloc_of_coloring_correct_1. auto.
- change OrderedReg.t with reg. rewrite <- H6.
+ change positive with reg. rewrite <- H6.
change (interfere x y g). unfold g.
apply interf_graph_correct_2; auto.
Qed.
@@ -942,12 +942,12 @@ Proof.
rewrite H4; unfold allregs.
elim (ordered_pair_charact r1 r2); intro.
apply alloc_of_coloring_correct_1. auto.
- change OrderedReg.t with reg. rewrite <- H5.
+ change positive with reg. rewrite <- H5.
change (interfere r1 r2 g). unfold g.
apply interf_graph_correct_3; auto.
apply sym_not_equal.
apply alloc_of_coloring_correct_1. auto.
- change OrderedReg.t with reg. rewrite <- H5.
+ change positive with reg. rewrite <- H5.
change (interfere r1 r2 g). unfold g.
apply interf_graph_correct_3; auto.
Qed.
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
index 433c074d1..8a9dda67a 100644
--- a/backend/InterfGraph.v
+++ b/backend/InterfGraph.v
@@ -55,7 +55,7 @@ Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg).
Module SetRegReg := FSetAVL.Make(OrderedRegReg).
Module SetRegMreg := FSetAVL.Make(OrderedRegMreg).
-Record graph: Set := mkgraph {
+Record graph: Type := mkgraph {
interf_reg_reg: SetRegReg.t;
interf_reg_mreg: SetRegMreg.t;
pref_reg_reg: SetRegReg.t;
@@ -160,7 +160,7 @@ Lemma add_interf_correct:
interfere x y (add_interf x y g).
Proof.
intros. unfold interfere, add_interf; simpl.
- apply SetRegReg.add_1. red. apply OrderedRegReg.eq_refl.
+ apply SetRegReg.add_1. auto.
Qed.
Lemma add_interf_incl:
@@ -177,7 +177,7 @@ Lemma add_interf_mreg_correct:
interfere_mreg x y (add_interf_mreg x y g).
Proof.
intros. unfold interfere_mreg, add_interf_mreg; simpl.
- apply SetRegMreg.add_1. red. apply OrderedRegMreg.eq_refl.
+ apply SetRegMreg.add_1. auto.
Qed.
Lemma add_interf_mreg_incl:
@@ -214,17 +214,17 @@ Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t :=
Regset.add (fst r1m2) u.
Definition all_interf_regs (g: graph) : Regset.t :=
- SetRegReg.fold _ add_intf2
+ SetRegReg.fold add_intf2
g.(interf_reg_reg)
- (SetRegMreg.fold _ add_intf1
+ (SetRegMreg.fold add_intf1
g.(interf_reg_mreg)
Regset.empty).
Lemma in_setregreg_fold:
forall g r1 r2 u,
SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u ->
- Regset.In r1 (SetRegReg.fold _ add_intf2 g u) /\
- Regset.In r2 (SetRegReg.fold _ add_intf2 g u).
+ Regset.In r1 (SetRegReg.fold add_intf2 g u) /\
+ Regset.In r2 (SetRegReg.fold add_intf2 g u).
Proof.
set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u).
assert (forall l r1 r2 u,
@@ -235,7 +235,7 @@ Proof.
elim H; intro. inversion H0. auto.
apply IHl. destruct a as [a1 a2].
elim H; intro. inversion H0; subst.
- red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 r2.
+ red in H2. simpl in H2. destruct H2. subst r1 r2.
right; unfold add_intf2', add_intf2; simpl; split.
apply Regset.add_1. auto.
apply Regset.add_2. apply Regset.add_1. auto.
@@ -250,7 +250,7 @@ Qed.
Lemma in_setregreg_fold':
forall g r u,
Regset.In r u ->
- Regset.In r (SetRegReg.fold _ add_intf2 g u).
+ Regset.In r (SetRegReg.fold add_intf2 g u).
Proof.
intros. exploit in_setregreg_fold. eauto.
intros [A B]. eauto.
@@ -259,7 +259,7 @@ Qed.
Lemma in_setregmreg_fold:
forall g r1 mr2 u,
SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u ->
- Regset.In r1 (SetRegMreg.fold _ add_intf1 g u).
+ Regset.In r1 (SetRegMreg.fold add_intf1 g u).
Proof.
set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u).
assert (forall l r1 mr2 u,
@@ -269,7 +269,7 @@ Proof.
elim H; intro. inversion H0. auto.
apply IHl with mr2. destruct a as [a1 a2].
elim H; intro. inversion H0; subst.
- red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 mr2.
+ red in H2. simpl in H2. destruct H2. subst r1 mr2.
right; unfold add_intf1', add_intf1; simpl.
apply Regset.add_1; auto.
tauto.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index b4445aebd..188a23fdc 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -108,7 +108,7 @@ End DATAFLOW_SOLVER.
Module Type NODE_SET.
- Variable t: Set.
+ Variable t: Type.
Variable add: positive -> t -> t.
Variable pick: t -> option (positive * t).
Variable initial: positive -> t.
@@ -147,7 +147,7 @@ Variable entrypoints: list (positive * L.t).
- A worklist of program points that remain to be considered.
*)
-Record state : Set :=
+Record state : Type :=
mkstate { st_in: PMap.t L.t; st_wrk: NS.t }.
(** Kildall's algorithm, in pseudo-code, is as follows:
@@ -663,7 +663,7 @@ End Backward_Dataflow_Solver.
Module Type ORDERED_TYPE_WITH_TOP.
- Variable t: Set.
+ Variable t: Type.
Variable ge: t -> t -> Prop.
Variable top: t.
Hypothesis top_ge: forall x, ge top x.
@@ -736,7 +736,7 @@ Definition result := PMap.t L.t.
- A worklist of program points that remain to be considered.
*)
-Record state : Set := mkstate
+Record state : Type := mkstate
{ st_in: result; st_wrk: list positive }.
(** The ``extended basic block'' algorithm, in pseudo-code, is as follows:
@@ -1167,7 +1167,7 @@ Module NodeSetForward <: NODE_SET.
rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff.
elim (Plt_succ_inv _ _ H0); intro.
right. apply H. auto.
- left. red. red. auto.
+ left. auto.
Qed.
End NodeSetForward.
diff --git a/backend/LTL.v b/backend/LTL.v
index 0db5495e4..3a61e6d0f 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -34,7 +34,7 @@ Require Import Conventions.
Definition node := positive.
-Inductive instruction: Set :=
+Inductive instruction: Type :=
| Lnop: node -> instruction
| Lop: operation -> list loc -> loc -> node -> instruction
| Lload: memory_chunk -> addressing -> list loc -> loc -> node -> instruction
@@ -44,9 +44,9 @@ Inductive instruction: Set :=
| Lcond: condition -> list loc -> node -> node -> instruction
| Lreturn: option loc -> instruction.
-Definition code: Set := PTree.t instruction.
+Definition code: Type := PTree.t instruction.
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
fn_sig: signature;
fn_params: list loc;
fn_stacksize: Z;
@@ -103,7 +103,7 @@ Definition postcall_locs (ls: locset) : locset :=
(** LTL execution states. *)
-Inductive stackframe : Set :=
+Inductive stackframe : Type :=
| Stackframe:
forall (res: loc) (**r where to store the result *)
(f: function) (**r calling function *)
@@ -112,7 +112,7 @@ Inductive stackframe : Set :=
(pc: node), (**r program point in calling function *)
stackframe.
-Inductive state : Set :=
+Inductive state : Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(f: function) (**r function currently executing *)
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 4c87c0d68..10b7d8323 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -41,7 +41,7 @@ Definition label := positive.
transfer control to the given code label. Labels are explicitly
inserted in the instruction list as pseudo-instructions [Llabel]. *)
-Inductive instruction: Set :=
+Inductive instruction: Type :=
| Lop: operation -> list loc -> loc -> instruction
| Lload: memory_chunk -> addressing -> list loc -> loc -> instruction
| Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction
@@ -52,9 +52,9 @@ Inductive instruction: Set :=
| Lcond: condition -> list loc -> label -> instruction
| Lreturn: option loc -> instruction.
-Definition code: Set := list instruction.
+Definition code: Type := list instruction.
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
fn_sig: signature;
fn_params: list loc;
fn_stacksize: Z;
@@ -109,7 +109,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
code sequences [c] (suffixes of the code of the current function).
*)
-Inductive stackframe : Set :=
+Inductive stackframe : Type :=
| Stackframe:
forall (res: loc) (**r where to store the result *)
(f: function) (**r calling function *)
@@ -118,7 +118,7 @@ Inductive stackframe : Set :=
(c: code), (**r program point in calling function *)
stackframe.
-Inductive state : Set :=
+Inductive state : Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(f: function) (**r function currently executing *)
diff --git a/backend/Linear.v b/backend/Linear.v
index 34d6e5ce8..e025407a8 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -35,7 +35,7 @@ Require Import Conventions.
Definition label := positive.
-Inductive instruction: Set :=
+Inductive instruction: Type :=
| Lgetstack: slot -> mreg -> instruction
| Lsetstack: mreg -> slot -> instruction
| Lop: operation -> list mreg -> mreg -> instruction
@@ -48,9 +48,9 @@ Inductive instruction: Set :=
| Lcond: condition -> list mreg -> label -> instruction
| Lreturn: instruction.
-Definition code: Set := list instruction.
+Definition code: Type := list instruction.
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
fn_sig: signature;
fn_stacksize: Z;
fn_code: code
@@ -163,7 +163,7 @@ Definition return_regs (caller callee: locset) : locset :=
(** Linear execution states. *)
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
| Stackframe:
forall (f: function) (**r calling function *)
(sp: val) (**r stack pointer in calling function *)
@@ -171,7 +171,7 @@ Inductive stackframe: Set :=
(c: code), (**r program point in calling function *)
stackframe.
-Inductive state: Set :=
+Inductive state: Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(f: function) (**r function currently executing *)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index b38542917..c24d37042 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -193,7 +193,7 @@ Proof.
generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0.
exploit check_reachable_correct; eauto. intro.
exploit nodeset_of_list_correct; eauto. intros [A [B C]].
- rewrite B in H2. destruct H2. elim (Nodeset.empty_1 pc H2). auto.
+ rewrite B in H2. destruct H2. elim (Nodeset.empty_1 H2). auto.
Qed.
Lemma enumerate_norepet:
diff --git a/backend/Locations.v b/backend/Locations.v
index ca2f52725..295df281d 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -42,7 +42,7 @@ Require Export Machregs.
cannot reside in hardware registers, as determined by the
calling conventions. *)
-Inductive slot: Set :=
+Inductive slot: Type :=
| Local: Z -> typ -> slot
| Incoming: Z -> typ -> slot
| Outgoing: Z -> typ -> slot.
@@ -108,7 +108,7 @@ Qed.
(** Locations are just the disjoint union of machine registers and
activation record slots. *)
-Inductive loc : Set :=
+Inductive loc : Type :=
| R: mreg -> loc
| S: slot -> loc.
diff --git a/backend/Mach.v b/backend/Mach.v
index 3f251373d..0bb24428c 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -49,7 +49,7 @@ Require Import Locations.
Definition label := positive.
-Inductive instruction: Set :=
+Inductive instruction: Type :=
| Mgetstack: int -> typ -> mreg -> instruction
| Msetstack: mreg -> int -> typ -> instruction
| Mgetparam: int -> typ -> mreg -> instruction
@@ -65,7 +65,7 @@ Inductive instruction: Set :=
Definition code := list instruction.
-Record function: Set := mkfunction
+Record function: Type := mkfunction
{ fn_sig: signature;
fn_code: code;
fn_stacksize: Z;
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index 25819f720..aa17cd44b 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -51,7 +51,7 @@ Require Stacklayout.
values. Like location sets (see module [Locations]), overlap
can occur. *)
-Definition frame : Set := typ -> Z -> val.
+Definition frame : Type := typ -> Z -> val.
Definition typ_eq: forall (ty1 ty2: typ), {ty1=ty2} + {ty1<>ty2}.
Proof. decide equality. Defined.
@@ -154,7 +154,7 @@ End FRAME_ACCESSES.
(** Mach execution states. *)
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
| Stackframe:
forall (f: function) (**r calling function *)
(sp: val) (**r stack pointer in calling function *)
@@ -162,7 +162,7 @@ Inductive stackframe: Set :=
(fr: frame), (**r frame state in calling function *)
stackframe.
-Inductive state: Set :=
+Inductive state: Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(f: function) (**r function currently executing *)
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 4417cc6fc..876f558c8 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -86,7 +86,7 @@ Definition extcall_arguments
(** Mach execution states. *)
-Inductive stackframe: Set :=
+Inductive stackframe: Type :=
| Stackframe:
forall (f: block) (**r pointer to calling function *)
(sp: val) (**r stack pointer in calling function *)
@@ -94,7 +94,7 @@ Inductive stackframe: Set :=
(c: code), (**r program point in calling function *)
stackframe.
-Inductive state: Set :=
+Inductive state: Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(f: block) (**r pointer to current function *)
diff --git a/backend/RTL.v b/backend/RTL.v
index 5fad2f270..344d271f1 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -44,7 +44,7 @@ Require Import Registers.
Definition node := positive.
-Inductive instruction: Set :=
+Inductive instruction: Type :=
| Inop: node -> instruction
(** No operation -- just branch to the successor. *)
| Iop: operation -> list reg -> reg -> node -> instruction
@@ -80,9 +80,9 @@ Inductive instruction: Set :=
(it has no successor). It returns the value of the given
register, or [Vundef] if none is given. *)
-Definition code: Set := PTree.t instruction.
+Definition code: Type := PTree.t instruction.
-Record function: Set := mkfunction {
+Record function: Type := mkfunction {
fn_sig: signature;
fn_params: list reg;
fn_stacksize: Z;
@@ -152,7 +152,7 @@ a function call in progress.
[rs] is the state of registers in the calling function.
*)
-Inductive stackframe : Set :=
+Inductive stackframe : Type :=
| Stackframe:
forall (res: reg) (**r where to store the result *)
(c: code) (**r code of calling function *)
@@ -161,7 +161,7 @@ Inductive stackframe : Set :=
(rs: regset), (**r register state in calling function *)
stackframe.
-Inductive state : Set :=
+Inductive state : Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
(c: code) (**r current code *)
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 709dc78c7..65e873e84 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -36,7 +36,7 @@ Open Local Scope string_scope.
The mapping for let-bound variables is initially empty and updated
during translation of expressions, when crossing a [Elet] binding. *)
-Record mapping: Set := mkmapping {
+Record mapping: Type := mkmapping {
map_vars: PTree.t reg;
map_letvars: list reg
}.
@@ -45,7 +45,7 @@ Record mapping: Set := mkmapping {
current state of the control-flow graph for the function being translated,
as well as sources of fresh RTL registers and fresh CFG nodes. *)
-Record state: Set := mkstate {
+Record state: Type := mkstate {
st_nextreg: positive;
st_nextnode: positive;
st_code: code;
@@ -104,25 +104,25 @@ Qed.
We now define this monadic encoding -- the ``state and error'' monad --
as well as convenient syntax to express monadic computations. *)
-Inductive res (A: Set) (s: state): Set :=
+Inductive res (A: Type) (s: state): Type :=
| Error: Errors.errmsg -> res A s
| OK: A -> forall (s': state), state_incr s s' -> res A s.
Implicit Arguments OK [A s].
Implicit Arguments Error [A s].
-Definition mon (A: Set) : Set := forall (s: state), res A s.
+Definition mon (A: Type) : Type := forall (s: state), res A s.
-Definition ret (A: Set) (x: A) : mon A :=
+Definition ret (A: Type) (x: A) : mon A :=
fun (s: state) => OK x s (state_incr_refl s).
Implicit Arguments ret [A].
-Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
+Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg.
Implicit Arguments error [A].
-Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B :=
+Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B :=
fun (s: state) =>
match f s with
| Error msg => Error msg
@@ -135,7 +135,7 @@ Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B :=
Implicit Arguments bind [A B].
-Definition bind2 (A B C: Set) (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
+Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
bind f (fun xy => g (fst xy) (snd xy)).
Implicit Arguments bind2 [A B C].
@@ -145,7 +145,7 @@ Notation "'do' X <- A ; B" := (bind A (fun X => B))
Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
(at level 200, X ident, Y ident, A at level 100, B at level 200).
-Definition handle_error (A: Set) (f g: mon A) : mon A :=
+Definition handle_error (A: Type) (f g: mon A) : mon A :=
fun (s: state) =>
match f s with
| OK a s' i => OK a s' i
@@ -498,7 +498,7 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
[nlist] if it terminates by an [exit n] construct. [rret] is the
register where the return value of the function must be stored, if any. *)
-Definition labelmap : Set := PTree.t node.
+Definition labelmap : Type := PTree.t node.
Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
(nexits: list node) (ngoto: labelmap) (nret: node) (rret: option reg)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index e6adeb05f..8e6127171 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -47,7 +47,7 @@ Require Import RTLgen.
*)
Remark bind_inversion:
- forall (A B: Set) (f: mon A) (g: A -> mon B)
+ forall (A B: Type) (f: mon A) (g: A -> mon B)
(y: B) (s1 s3: state) (i: state_incr s1 s3),
bind f g s1 = OK y s3 i ->
exists x, exists s2, exists i1, exists i2,
@@ -61,7 +61,7 @@ Proof.
Qed.
Remark bind2_inversion:
- forall (A B C: Set) (f: mon (A*B)) (g: A -> B -> mon C)
+ forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C)
(z: C) (s1 s3: state) (i: state_incr s1 s3),
bind2 f g s1 = OK z s3 i ->
exists x, exists y, exists s2, exists i1, exists i2,
@@ -827,20 +827,6 @@ Inductive tr_function: CminorSel.function -> RTL.function -> Prop :=
(** We now show that the translation functions in module [RTLgen]
satisfy the specifications given above as inductive predicates. *)
-Scheme tr_expr_ind3 := Minimality for tr_expr Sort Prop
- with tr_condition_ind3 := Minimality for tr_condition Sort Prop
- with tr_exprlist_ind3 := Minimality for tr_exprlist Sort Prop.
-
-Definition tr_expr_condition_exprlist_ind3
- (c: code)
- (P : mapping -> list reg -> expr -> node -> node -> reg -> Prop)
- (P0 : mapping -> list reg -> condexpr -> node -> node -> node -> Prop)
- (P1 : mapping -> list reg -> exprlist -> node -> node -> list reg -> Prop) :=
- fun a b c' d e f g h i j k l =>
- conj (tr_expr_ind3 c P P0 P1 a b c' d e f g h i j k l)
- (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l)
- (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)).
-
Lemma tr_move_incr:
forall s1 s2, state_incr s1 s2 ->
forall ns rs nd rd,
@@ -850,69 +836,35 @@ Proof.
induction 2; econstructor; eauto with rtlg.
Qed.
-Lemma tr_expr_condition_exprlist_incr:
- forall s1 s2, state_incr s1 s2 ->
- (forall map pr a ns nd rd,
- tr_expr s1.(st_code) map pr a ns nd rd ->
- tr_expr s2.(st_code) map pr a ns nd rd)
-/\(forall map pr a ns ntrue nfalse,
- tr_condition s1.(st_code) map pr a ns ntrue nfalse ->
- tr_condition s2.(st_code) map pr a ns ntrue nfalse)
-/\(forall map pr al ns nd rl,
- tr_exprlist s1.(st_code) map pr al ns nd rl ->
- tr_exprlist s2.(st_code) map pr al ns nd rl).
-Proof.
- intros s1 s2 EXT.
- pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
- apply tr_expr_condition_exprlist_ind3; intros; econstructor; eauto.
- eapply tr_move_incr; eauto.
- eapply tr_move_incr; eauto.
-Qed.
-
Lemma tr_expr_incr:
forall s1 s2, state_incr s1 s2 ->
forall map pr a ns nd rd,
tr_expr s1.(st_code) map pr a ns nd rd ->
- tr_expr s2.(st_code) map pr a ns nd rd.
-Proof.
- intros.
- exploit tr_expr_condition_exprlist_incr; eauto.
- intros [A [B C]]. eauto.
-Qed.
-
-Lemma tr_condition_incr:
+ tr_expr s2.(st_code) map pr a ns nd rd
+with tr_condition_incr:
forall s1 s2, state_incr s1 s2 ->
forall map pr a ns ntrue nfalse,
tr_condition s1.(st_code) map pr a ns ntrue nfalse ->
- tr_condition s2.(st_code) map pr a ns ntrue nfalse.
-Proof.
- intros.
- exploit tr_expr_condition_exprlist_incr; eauto.
- intros [A [B C]]. eauto.
-Qed.
-
-Lemma tr_exprlist_incr:
+ tr_condition s2.(st_code) map pr a ns ntrue nfalse
+with tr_exprlist_incr:
forall s1 s2, state_incr s1 s2 ->
forall map pr al ns nd rl,
tr_exprlist s1.(st_code) map pr al ns nd rl ->
tr_exprlist s2.(st_code) map pr al ns nd rl.
Proof.
- intros.
- exploit tr_expr_condition_exprlist_incr; eauto.
- intros [A [B C]]. eauto.
+ intros s1 s2 EXT.
+ pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+ induction 1; econstructor; eauto.
+ eapply tr_move_incr; eauto.
+ eapply tr_move_incr; eauto.
+ intros s1 s2 EXT.
+ pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+ induction 1; econstructor; eauto.
+ intros s1 s2 EXT.
+ pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
+ induction 1; econstructor; eauto.
Qed.
-Scheme expr_ind3 := Induction for expr Sort Prop
- with condexpr_ind3 := Induction for condexpr Sort Prop
- with exprlist_ind3 := Induction for exprlist Sort Prop.
-
-Definition expr_condexpr_exprlist_ind
- (P1: expr -> Prop) (P2: condexpr -> Prop) (P3: exprlist -> Prop) :=
- fun a b c d e f g h i j k l =>
- conj (expr_ind3 P1 P2 P3 a b c d e f g h i j k l)
- (conj (condexpr_ind3 P1 P2 P3 a b c d e f g h i j k l)
- (exprlist_ind3 P1 P2 P3 a b c d e f g h i j k l)).
-
Lemma add_move_charact:
forall s ns rs nd rd s' i,
add_move rs rd nd s = OK ns s' i ->
@@ -923,30 +875,33 @@ Proof.
constructor. eauto with rtlg.
Qed.
-Lemma transl_expr_condexpr_list_charact:
- (forall a map rd nd s ns s' pr INCR
+Lemma transl_expr_charact:
+ forall a map rd nd s ns s' pr INCR
(TR: transl_expr map a rd nd s = OK ns s' INCR)
(WF: map_valid map s)
(OK: target_reg_ok map pr a rd)
(VALID: regs_valid pr s)
(VALID2: reg_valid rd s),
- tr_expr s'.(st_code) map pr a ns nd rd)
-/\
- (forall a map ntrue nfalse s ns s' pr INCR
+ tr_expr s'.(st_code) map pr a ns nd rd
+
+with transl_condexpr_charact:
+ forall a map ntrue nfalse s ns s' pr INCR
(TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
- (WF: map_valid map s)
- (VALID: regs_valid pr s),
- tr_condition s'.(st_code) map pr a ns ntrue nfalse)
-/\
- (forall al map rl nd s ns s' pr INCR
+ (VALID: regs_valid pr s)
+ (WF: map_valid map s),
+ tr_condition s'.(st_code) map pr a ns ntrue nfalse
+
+with transl_exprlist_charact:
+ forall al map rl nd s ns s' pr INCR
(TR: transl_exprlist map al rl nd s = OK ns s' INCR)
(WF: map_valid map s)
(OK: target_regs_ok map pr al rl)
(VALID1: regs_valid pr s)
(VALID2: regs_valid rl s),
- tr_exprlist s'.(st_code) map pr al ns nd rl).
+ tr_exprlist s'.(st_code) map pr al ns nd rl.
+
Proof.
- apply expr_condexpr_exprlist_ind; intros; try (monadInv TR).
+ induction a; intros; try (monadInv TR).
(* Evar *)
generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1.
econstructor; eauto.
@@ -955,31 +910,31 @@ Proof.
(* Eop *)
inv OK.
econstructor; eauto with rtlg.
- eapply H; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
(* Eload *)
inv OK.
econstructor; eauto with rtlg.
- eapply H; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
(* Econdition *)
inv OK.
econstructor; eauto with rtlg.
- eapply H; eauto with rtlg.
+ eapply transl_condexpr_charact; eauto with rtlg.
apply tr_expr_incr with s1; auto.
- eapply H0; eauto with rtlg. constructor; auto.
+ eapply transl_expr_charact; eauto with rtlg. constructor; auto.
apply tr_expr_incr with s0; auto.
- eapply H1; eauto with rtlg. constructor; auto.
+ eapply transl_expr_charact; eauto with rtlg. constructor; auto.
(* Elet *)
inv OK.
econstructor. eapply new_reg_not_in_map; eauto with rtlg.
- eapply H; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
apply tr_expr_incr with s1; auto.
- eapply H0. eauto.
+ eapply transl_expr_charact. eauto.
apply add_letvar_valid; eauto with rtlg.
constructor; auto.
red; unfold reg_in_map. simpl. intros [[id A] | [B | C]].
- elim H1. left; exists id; auto.
+ elim H. left; exists id; auto.
subst x. apply valid_fresh_absurd with rd s. auto. eauto with rtlg.
- elim H1. right; auto.
+ elim H. right; auto.
eauto with rtlg. eauto with rtlg.
(* Eletvar *)
generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0.
@@ -989,56 +944,41 @@ Proof.
eapply add_move_charact; eauto.
monadInv EQ1.
+(* Conditions *)
+ induction a; intros; try (monadInv TR).
+
(* CEtrue *)
constructor.
(* CEfalse *)
constructor.
(* CEcond *)
econstructor; eauto with rtlg.
- eapply H; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
(* CEcondition *)
econstructor.
- eapply H; eauto with rtlg.
+ eapply transl_condexpr_charact; eauto with rtlg.
apply tr_condition_incr with s1; auto.
- eapply H0; eauto with rtlg.
+ eapply transl_condexpr_charact; eauto with rtlg.
apply tr_condition_incr with s0; auto.
- eapply H1; eauto with rtlg.
+ eapply transl_condexpr_charact; eauto with rtlg.
+
+(* Lists *)
+
+ induction al; intros; try (monadInv TR).
(* Enil *)
destruct rl; inv TR. constructor.
(* Econs *)
destruct rl; simpl in TR; monadInv TR. inv OK.
econstructor.
- eapply H; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
generalize (VALID2 r (in_eq _ _)). eauto with rtlg.
apply tr_exprlist_incr with s0; auto.
- eapply H0; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
apply regs_valid_cons. apply VALID2. auto with coqlib. auto.
red; intros; apply VALID2; auto with coqlib.
Qed.
-Lemma transl_expr_charact:
- forall a map rd nd s ns s' INCR
- (TR: transl_expr map a rd nd s = OK ns s' INCR)
- (WF: map_valid map s)
- (OK: target_reg_ok map nil a rd)
- (VALID2: reg_valid rd s),
- tr_expr s'.(st_code) map nil a ns nd rd.
-Proof.
- destruct transl_expr_condexpr_list_charact as [A [B C]].
- intros. eapply A; eauto with rtlg.
-Qed.
-
-Lemma transl_condexpr_charact:
- forall a map ntrue nfalse s ns s' INCR
- (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR)
- (WF: map_valid map s),
- tr_condition s'.(st_code) map nil a ns ntrue nfalse.
-Proof.
- destruct transl_expr_condexpr_list_charact as [A [B C]].
- intros. eapply B; eauto with rtlg.
-Qed.
-
Lemma tr_store_var_incr:
forall s1 s2, state_incr s1 s2 ->
forall map rs id ns nd,
@@ -1076,7 +1016,7 @@ Lemma tr_stmt_incr:
tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret.
Proof.
intros s1 s2 EXT.
- destruct (tr_expr_condition_exprlist_incr s1 s2 EXT) as [A [B C]].
+ generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3.
pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
pose (STV := tr_store_var_incr s1 s2 EXT).
pose (STOV := tr_store_optvar_incr s1 s2 EXT).
@@ -1148,19 +1088,17 @@ Proof.
apply tr_store_var_incr with s1; auto with rtlg.
eapply store_var_charact; eauto.
(* Sstore *)
- destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
econstructor; eauto with rtlg.
- eapply P3; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
apply tr_expr_incr with s3; eauto with rtlg.
- eapply P1; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
(* Scall *)
- destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]].
assert (state_incr s0 s3) by eauto with rtlg.
assert (state_incr s3 s6) by eauto with rtlg.
econstructor; eauto with rtlg.
- eapply P1; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
apply tr_exprlist_incr with s6. auto.
- eapply P3; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg.
apply regs_valid_cons; eauto with rtlg.
apply regs_valid_incr with s1; eauto with rtlg.
@@ -1169,13 +1107,12 @@ Proof.
apply tr_store_optvar_incr with s4; eauto with rtlg.
eapply store_optvar_charact; eauto with rtlg.
(* Stailcall *)
- destruct transl_expr_condexpr_list_charact as [A [B C]].
assert (RV: regs_valid (x :: nil) s1).
apply regs_valid_cons; eauto with rtlg.
econstructor; eauto with rtlg.
- eapply A; eauto with rtlg.
+ eapply transl_expr_charact; eauto with rtlg.
apply tr_exprlist_incr with s4; auto.
- eapply C; eauto with rtlg.
+ eapply transl_exprlist_charact; eauto with rtlg.
(* Sseq *)
econstructor.
apply tr_stmt_incr with s0; auto.
diff --git a/backend/Registers.v b/backend/Registers.v
index c3d04d602..fceb7c240 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -24,7 +24,7 @@ Require Import Ordered.
Require Import FSets.
Require FSetAVL.
-Definition reg: Set := positive.
+Definition reg: Type := positive.
Module Reg.
@@ -41,14 +41,14 @@ Module Regmap := PMap.
Set Implicit Arguments.
Definition regmap_optget
- (A: Set) (or: option reg) (dfl: A) (rs: Regmap.t A) : A :=
+ (A: Type) (or: option reg) (dfl: A) (rs: Regmap.t A) : A :=
match or with
| None => dfl
| Some r => Regmap.get r rs
end.
Definition regmap_optset
- (A: Set) (or: option reg) (v: A) (rs: Regmap.t A) : Regmap.t A :=
+ (A: Type) (or: option reg) (v: A) (rs: Regmap.t A) : Regmap.t A :=
match or with
| None => rs
| Some r => Regmap.set r v rs
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 158af8f6e..182c32269 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -34,7 +34,7 @@ Require Import Stacklayout.
(** Computation the frame offset for the given component of the frame.
The component is expressed by the following [frame_index] sum type. *)
-Inductive frame_index: Set :=
+Inductive frame_index: Type :=
| FI_link: frame_index
| FI_retaddr: frame_index
| FI_local: Z -> typ -> frame_index
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index a7560d039..d5819f7ef 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -955,7 +955,7 @@ Proof.
exists ls'; exists rs'. split. assumption.
split. intros. elim H2; intros.
subst r. apply (agree_unused_reg _ _ _ _ _ D).
- rewrite <- number_within_bounds. auto. omega. auto.
+ rewrite <- number_within_bounds. auto. auto. auto.
split. intros. simpl in H2. apply C. tauto.
assumption.
Qed.
@@ -1051,7 +1051,7 @@ End FRAME_PROPERTIES.
Section LABELS.
Remark find_label_fold_right:
- forall (A: Set) (fn: A -> Mach.code -> Mach.code) lbl,
+ forall (A: Type) (fn: A -> Mach.code -> Mach.code) lbl,
(forall x k, Mach.find_label lbl (fn x k) = Mach.find_label lbl k) -> forall (args: list A) k,
Mach.find_label lbl (List.fold_right fn k args) = Mach.find_label lbl k.
Proof.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index b88dd50c7..1bafc35b1 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -51,7 +51,7 @@ Variable tf: Mach.function.
Hypothesis TRANSF_F: transf_function f = OK tf.
Lemma wt_fold_right:
- forall (A: Set) (f: A -> code -> code) (k: code) (l: list A),
+ forall (A: Type) (f: A -> code -> code) (k: code) (l: list A),
(forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) ->
wt_instrs k ->
wt_instrs (List.fold_right f k l).
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 8e97e1a47..791db3742 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -574,8 +574,8 @@ Proof.
exploit loadv_lessdef; eauto.
intros [v' [LOAD' VLD]].
left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split.
- eapply exec_Iload; eauto. rewrite <- ADDR'.
- apply eval_addressing_preserved. exact symbols_preserved.
+ eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'.
+ apply eval_addressing_preserved. exact symbols_preserved. eauto.
econstructor; eauto. apply regset_set; auto.
(* store *)
@@ -586,8 +586,8 @@ Proof.
exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD.
intros [m'1 [STORE' MLD']].
left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split.
- eapply exec_Istore; eauto. rewrite <- ADDR'.
- apply eval_addressing_preserved. exact symbols_preserved.
+ eapply exec_Istore with (a := a'). eauto. rewrite <- ADDR'.
+ apply eval_addressing_preserved. exact symbols_preserved. eauto.
destruct a; simpl in H1; try discriminate.
econstructor; eauto.
eapply match_stacksize_store; eauto.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 49bf89429..08f5f6ccb 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -268,16 +268,18 @@ Proof.
(* Lload *)
rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
left; econstructor; split.
- eapply exec_Lload; eauto.
+ eapply exec_Lload with (a := a).
rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+ eauto.
econstructor; eauto.
(* Lstore *)
rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
left; econstructor; split.
- eapply exec_Lstore; eauto.
+ eapply exec_Lstore with (a := a).
rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+ eauto.
econstructor; eauto.
(* Lcall *)
left; econstructor; split.
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index cc5e5ab34..1045d1a0d 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -108,7 +108,7 @@ Definition make_globaladdr (id: ident): expr :=
data block. [Var_global_scalar] and [Var_global_array] denote
global variables, stored in the global symbols with the same names. *)
-Inductive var_info: Set :=
+Inductive var_info: Type :=
| Var_local: memory_chunk -> var_info
| Var_stack_scalar: memory_chunk -> Z -> var_info
| Var_stack_array: Z -> var_info
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5615eabe4..f256bb26c 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -225,7 +225,7 @@ Record match_globalenvs (f: meminj) : Prop :=
collecting information on the current execution state of a Csharpminor
function and its Cminor translation. *)
-Record frame : Set :=
+Record frame : Type :=
mkframe {
fr_cenv: compilenv;
fr_e: Csharpminor.env;
@@ -235,7 +235,7 @@ Record frame : Set :=
fr_high: Z
}.
-Definition callstack : Set := list frame.
+Definition callstack : Type := list frame.
(** Matching of call stacks imply matching of environments for each of
the frames, plus matching of the global environments, plus disjointness
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 14b8053d8..248192cc7 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -426,7 +426,7 @@ Definition empty_env: env := (PTree.empty block).
how the execution terminated: either normally or prematurely
through the execution of a [break], [continue] or [return] statement. *)
-Inductive outcome: Set :=
+Inductive outcome: Type :=
| Out_break: outcome (**r terminated by [break] *)
| Out_continue: outcome (**r terminated by [continue] *)
| Out_normal: outcome (**r terminated normally *)
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 1aa536a14..942cfd75e 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -37,14 +37,14 @@ Require Import Smallstep.
be taken using [Eaddrof] expressions.
*)
-Inductive constant : Set :=
+Inductive constant : Type :=
| Ointconst: int -> constant (**r integer constant *)
| Ofloatconst: float -> constant. (**r floating-point constant *)
-Definition unary_operation : Set := Cminor.unary_operation.
-Definition binary_operation : Set := Cminor.binary_operation.
+Definition unary_operation : Type := Cminor.unary_operation.
+Definition binary_operation : Type := Cminor.binary_operation.
-Inductive expr : Set :=
+Inductive expr : Type :=
| Evar : ident -> expr (**r reading a scalar variable *)
| Eaddrof : ident -> expr (**r taking the address of a variable *)
| Econst : constant -> expr (**r constants *)
@@ -59,7 +59,7 @@ Inductive expr : Set :=
[Sexit n] terminates prematurely the execution of the [n+1] enclosing
[Sblock] statements. *)
-Inductive stmt : Set :=
+Inductive stmt : Type :=
| Sskip: stmt
| Sassign : ident -> expr -> stmt
| Sstore : memory_chunk -> expr -> expr -> stmt
@@ -77,7 +77,7 @@ Inductive stmt : Set :=
or array variables (of the indicated sizes). The only operation
permitted on an array variable is taking its address. *)
-Inductive var_kind : Set :=
+Inductive var_kind : Type :=
| Vscalar: memory_chunk -> var_kind
| Varray: Z -> var_kind.
@@ -86,7 +86,7 @@ Inductive var_kind : Set :=
local variables with associated [var_kind] description, and a
statement representing the function body. *)
-Record function : Set := mkfunction {
+Record function : Type := mkfunction {
fn_sig: signature;
fn_params: list (ident * memory_chunk);
fn_vars: list (ident * var_kind);
@@ -95,7 +95,7 @@ Record function : Set := mkfunction {
Definition fundef := AST.fundef function.
-Definition program : Set := AST.program fundef var_kind.
+Definition program : Type := AST.program fundef var_kind.
Definition funsig (fd: fundef) :=
match fd with
@@ -109,7 +109,7 @@ Definition funsig (fd: fundef) :=
style. Expressions evaluate to values, and statements evaluate to
``outcomes'' indicating how execution should proceed afterwards. *)
-Inductive outcome: Set :=
+Inductive outcome: Type :=
| Out_normal: outcome (**r continue in sequence *)
| Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *)
| Out_return: option val -> outcome. (**r return immediately to caller *)
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 2c010cb49..bd9cf2297 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -80,7 +80,7 @@ Qed.
(** * Properties of the translation functions *)
Lemma map_partial_names:
- forall (A B: Set) (f: A -> res B)
+ forall (A B: Type) (f: A -> res B)
(l: list (ident * A)) (tl: list (ident * B)),
map_partial prefix_var_name f l = OK tl ->
List.map (@fst ident B) tl = List.map (@fst ident A) l.
@@ -93,7 +93,7 @@ Proof.
Qed.
Lemma map_partial_append:
- forall (A B: Set) (f: A -> res B)
+ forall (A B: Type) (f: A -> res B)
(l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)),
map_partial prefix_var_name f l1 = OK tl1 ->
map_partial prefix_var_name f l2 = OK tl2 ->
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 75dbc145c..af6dc90af 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -865,7 +865,7 @@ Definition eval_funcall_prop
Csharpminor.eval_funcall tprog m1 tf params t m2 res.
(*
-Set Printing Depth 100.
+Type Printing Depth 100.
Check (Csem.eval_funcall_ind3 ge exec_stmt_prop exec_lblstmts_prop eval_funcall_prop).
*)
@@ -1592,19 +1592,18 @@ Lemma transl_funcall_divergence_correct:
Csem.evalinf_funcall ge m1 f params t ->
wt_fundef (global_typenv prog) f ->
transl_fundef f = OK tf ->
- Csharpminor.evalinf_funcall tprog m1 tf params t.
-Proof.
- cofix FUNCALL.
- assert (STMT:
- forall e m1 s t,
- Csem.execinf_stmt ge e m1 s t ->
- forall tyenv nbrk ncnt ts te
- (WT: wt_stmt tyenv s)
- (TR: transl_statement nbrk ncnt s = OK ts)
- (MENV: match_env tyenv e te),
- Csharpminor.execinf_stmt tprog te m1 ts t).
- cofix STMT.
- assert(LBLSTMT:
+ Csharpminor.evalinf_funcall tprog m1 tf params t
+
+with transl_stmt_divergence_correct:
+ forall e m1 s t,
+ Csem.execinf_stmt ge e m1 s t ->
+ forall tyenv nbrk ncnt ts te
+ (WT: wt_stmt tyenv s)
+ (TR: transl_statement nbrk ncnt s = OK ts)
+ (MENV: match_env tyenv e te),
+ Csharpminor.execinf_stmt tprog te m1 ts t
+
+with transl_lblstmt_divergence_correct:
forall s ncnt body ts tyenv e te m0 t0 m1 t1 n,
transl_lblstmts (lblstmts_length s)
(S (lblstmts_length s + ncnt))
@@ -1617,66 +1616,30 @@ Proof.
/\ execinf_lblstmts ge e m1 (select_switch n s) t1)
\/ (exec_stmt tprog te m0 body t0 m1 Out_normal
/\ execinf_lblstmts ge e m1 s t1) ->
- execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1)).
+ execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1).
- cofix LBLSTMT; intros.
- destruct s; simpl in *; monadInv H; inv H0.
- (* 1. LSdefault *)
- assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto.
- assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto.
- clear H2. inv H0.
- change (Sblock (Sseq body x))
- with ((fun z => Sblock z) (Sseq body x)).
- apply execinf_context.
- eapply execinf_Sseq_2. eauto. eapply STMT; eauto. auto.
- constructor.
- (* 2. LScase *)
- elim H2; clear H2.
- (* 2.1 searching for the case *)
- rewrite (Int.eq_sym i n).
- destruct (Int.eq n i).
- (* 2.1.1 found it! *)
- intros [A B]. inv B.
- (* 2.1.1.1 we diverge because of this case *)
- destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
- rewrite EQ1. apply execinf_context; auto.
- apply execinf_Sblock. eapply execinf_Sseq_2. eauto.
- eapply STMT; eauto. auto.
- (* 2.1.1.2 we diverge later, after falling through *)
- simpl. apply execinf_sleep.
- replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3).
- eapply LBLSTMT with (n := n); eauto. right. split.
- change Out_normal with (outcome_block Out_normal).
- apply exec_Sblock.
- eapply exec_Sseq_continue. eauto.
- change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
- eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
- auto. auto. traceEq.
- (* 2.1.2 still searching *)
- rewrite switch_target_table_shift. intros [A B].
- apply execinf_sleep.
- eapply LBLSTMT with (n := n); eauto. left. split.
- fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))).
- apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence.
- auto.
- (* 2.2 found the case already, falling through next cases *)
- intros [A B]. inv B.
- (* 2.2.1 we diverge because of this case *)
- destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
- rewrite EQ1. apply execinf_context; auto.
- apply execinf_Sblock. eapply execinf_Sseq_2. eauto.
- eapply STMT; eauto. auto.
- (* 2.2.2 we diverge later *)
- simpl. apply execinf_sleep.
- replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3).
- eapply LBLSTMT with (n := n); eauto. right. split.
- change Out_normal with (outcome_block Out_normal).
- apply exec_Sblock.
- eapply exec_Sseq_continue. eauto.
- change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
- eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
- auto. auto. traceEq.
+Proof.
+ (* Functions *)
+ intros. inv H.
+ (* Exploitation of typing hypothesis *)
+ inv H0. inv H6.
+ (* Exploitation of translation hypothesis *)
+ monadInv H1. monadInv EQ.
+ (* Allocation of variables *)
+ assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env).
+ apply match_globalenv_match_env_empty. apply match_global_typenv.
+ generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ).
+ intro.
+ destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5)
+ as [te [ALLOCVARS MATCHENV]].
+ (* Execution *)
+ econstructor; simpl.
+ eapply transl_names_norepet; eauto.
+ eexact ALLOCVARS.
+ eapply bind_parameters_match; eauto.
+ eapply transl_stmt_divergence_correct; eauto.
+(* Statements *)
intros. inv H; inv WT; try (generalize TR; intro TR'; monadInv TR').
(* Scall *)
@@ -1688,44 +1651,44 @@ Proof.
eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto.
eauto.
eapply transl_fundef_sig1; eauto. rewrite H3; auto.
- eapply FUNCALL; eauto.
+ eapply transl_funcall_divergence_correct; eauto.
eapply functions_well_typed; eauto.
(* Sseq 1 *)
- apply execinf_Sseq_1. eapply STMT; eauto.
+ apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto.
(* Sseq 2 *)
eapply execinf_Sseq_2.
change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto.
- eapply STMT; eauto. auto.
+ eapply transl_stmt_divergence_correct; eauto. auto.
(* Sifthenelse, true *)
assert (eval_expr tprog te m1 x v1).
eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
destruct (make_boolean_correct_true _ _ _ _ _ _ H H1) as [vb [A B]].
eapply execinf_Sifthenelse. eauto. apply Val.bool_of_true_val; eauto.
- auto. eapply STMT; eauto.
+ auto. eapply transl_stmt_divergence_correct; eauto.
(* Sifthenelse, false *)
assert (eval_expr tprog te m1 x v1).
eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
destruct (make_boolean_correct_false _ _ _ _ _ _ H H1) as [vb [A B]].
eapply execinf_Sifthenelse. eauto. apply Val.bool_of_false_val; eauto.
- auto. eapply STMT; eauto.
+ auto. eapply transl_stmt_divergence_correct; eauto.
(* Swhile, body *)
apply execinf_Sblock. apply execinf_Sloop_body.
eapply execinf_Sseq_2. eapply exit_if_false_true; eauto.
- apply execinf_Sblock. eapply STMT; eauto. traceEq.
+ apply execinf_Sblock. eapply transl_stmt_divergence_correct; eauto. traceEq.
(* Swhile, loop *)
apply execinf_Sblock. eapply execinf_Sloop_block.
eapply exec_Sseq_continue. eapply exit_if_false_true; eauto.
rewrite (transl_out_normal_or_continue out1 H3).
apply exec_Sblock.
eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. reflexivity.
- eapply STMT with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
+ eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
constructor; eauto.
traceEq.
(* Sdowhile, body *)
apply execinf_Sblock. apply execinf_Sloop_body.
apply execinf_Sseq_1. apply execinf_Sblock.
- eapply STMT; eauto.
+ eapply transl_stmt_divergence_correct; eauto.
(* Sdowhile, loop *)
apply execinf_Sblock. eapply execinf_Sloop_block.
eapply exec_Sseq_continue.
@@ -1733,21 +1696,21 @@ Proof.
apply exec_Sblock.
eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto.
eapply exit_if_false_true; eauto. reflexivity.
- eapply STMT with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
+ eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto.
constructor; auto.
traceEq.
(* Sfor start 1 *)
simpl in TR. destruct (is_Sskip a1).
subst a1. inv H0.
monadInv TR.
- apply execinf_Sseq_1. eapply STMT; eauto.
+ apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto.
(* Sfor start 2 *)
destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H0) as [ts1 [ts2 [EQ [TR1 TR2]]]].
subst ts.
eapply execinf_Sseq_2.
change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
eapply (transl_stmt_correct _ _ _ _ _ _ H1); eauto.
- eapply STMT; eauto.
+ eapply transl_stmt_divergence_correct; eauto.
constructor; auto. constructor.
auto.
(* Sfor_body *)
@@ -1756,7 +1719,7 @@ Proof.
eapply execinf_Sseq_2.
eapply exit_if_false_true; eauto.
apply execinf_Sseq_1. apply execinf_Sblock.
- eapply STMT; eauto.
+ eapply transl_stmt_divergence_correct; eauto.
traceEq.
(* Sfor next *)
rewrite transl_stmt_Sfor_not_start in TR; monadInv TR.
@@ -1767,7 +1730,7 @@ Proof.
rewrite (transl_out_normal_or_continue out1 H3).
apply exec_Sblock.
eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto.
- eapply STMT; eauto.
+ eapply transl_stmt_divergence_correct; eauto.
reflexivity. traceEq.
(* Sfor loop *)
generalize TR. rewrite transl_stmt_Sfor_not_start; intro TR'; monadInv TR'.
@@ -1781,7 +1744,7 @@ Proof.
change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal).
eapply (transl_stmt_correct _ _ _ _ _ _ H4); eauto.
reflexivity. reflexivity.
- eapply STMT; eauto.
+ eapply transl_stmt_divergence_correct; eauto.
constructor; auto.
traceEq.
(* Sswitch *)
@@ -1790,30 +1753,68 @@ Proof.
replace (ncnt + lblstmts_length sl + 1)%nat
with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega.
change t with (E0 *** t).
- eapply LBLSTMT; eauto.
+ eapply transl_lblstmt_divergence_correct; eauto.
left. split. apply exec_Sblock. constructor.
eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto.
- auto.
+ auto.
- (* Functions *)
- intros. inv H.
- (* Exploitation of typing hypothesis *)
- inv H0. inv H6.
- (* Exploitation of translation hypothesis *)
- monadInv H1. monadInv EQ.
- (* Allocation of variables *)
- assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env).
- apply match_globalenv_match_env_empty. apply match_global_typenv.
- generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ).
- intro.
- destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5)
- as [te [ALLOCVARS MATCHENV]].
- (* Execution *)
- econstructor; simpl.
- eapply transl_names_norepet; eauto.
- eexact ALLOCVARS.
- eapply bind_parameters_match; eauto.
- eapply STMT; eauto.
+(* Labeled statements *)
+ intros. destruct s; simpl in *; monadInv H; inv H0.
+ (* 1. LSdefault *)
+ assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto.
+ assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto.
+ clear H2. inv H0.
+ change (Sblock (Sseq body x))
+ with ((fun z => Sblock z) (Sseq body x)).
+ apply execinf_context.
+ eapply execinf_Sseq_2. eauto. eapply transl_stmt_divergence_correct; eauto. auto.
+ constructor.
+ (* 2. LScase *)
+ elim H2; clear H2.
+ (* 2.1 searching for the case *)
+ rewrite (Int.eq_sym i n).
+ destruct (Int.eq n i).
+ (* 2.1.1 found it! *)
+ intros [A B]. inv B.
+ (* 2.1.1.1 we diverge because of this case *)
+ destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
+ rewrite EQ1. apply execinf_context; auto.
+ apply execinf_Sblock. eapply execinf_Sseq_2. eauto.
+ eapply transl_stmt_divergence_correct; eauto. auto.
+ (* 2.1.1.2 we diverge later, after falling through *)
+ simpl. apply execinf_sleep.
+ replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3).
+ eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split.
+ change Out_normal with (outcome_block Out_normal).
+ apply exec_Sblock.
+ eapply exec_Sseq_continue. eauto.
+ change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
+ eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
+ auto. auto. traceEq.
+ (* 2.1.2 still searching *)
+ rewrite switch_target_table_shift. intros [A B].
+ apply execinf_sleep.
+ eapply transl_lblstmt_divergence_correct with (n := n); eauto. left. split.
+ fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))).
+ apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence.
+ auto.
+ (* 2.2 found the case already, falling through next cases *)
+ intros [A B]. inv B.
+ (* 2.2.1 we diverge because of this case *)
+ destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]].
+ rewrite EQ1. apply execinf_context; auto.
+ apply execinf_Sblock. eapply execinf_Sseq_2. eauto.
+ eapply transl_stmt_divergence_correct; eauto. auto.
+ (* 2.2.2 we diverge later *)
+ simpl. apply execinf_sleep.
+ replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3).
+ eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split.
+ change Out_normal with (outcome_block Out_normal).
+ apply exec_Sblock.
+ eapply exec_Sseq_continue. eauto.
+ change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal).
+ eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto.
+ auto. auto. traceEq.
Qed.
End CORRECTNESS.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ac7904700..b332e2160 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 *)
diff --git a/common/AST.v b/common/AST.v
index ec8053d4e..a8655c254 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 2c9bbc3fb..2165db367 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 c44da0138..011c454b2 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 f7209141d..1ce7bf5ee 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 e169dfc76..01c1975bf 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 a2634be13..f41fe4ed1 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 8124aea17..179d4d2ee 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 8182d7a5c..9645e8ac6 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
diff --git a/driver/Compiler.v b/driver/Compiler.v
index bce0dab03..97bc19b1e 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -80,10 +80,10 @@ Open Local Scope string_scope.
(** We first define useful monadic composition operators,
along with funny (but convenient) notations. *)
-Definition apply_total (A B: Set) (x: res A) (f: A -> B) : res B :=
+Definition apply_total (A B: Type) (x: res A) (f: A -> B) : res B :=
match x with Error msg => Error msg | OK x1 => OK (f x1) end.
-Definition apply_partial (A B: Set)
+Definition apply_partial (A B: Type)
(x: res A) (f: A -> res B) : res B :=
match x with Error msg => Error msg | OK x1 => f x1 end.
@@ -150,7 +150,7 @@ Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
(** The following lemmas help reason over compositions of passes. *)
Lemma map_partial_compose:
- forall (X A B C: Set)
+ forall (X A B C: Type)
(ctx: X -> errmsg)
(f1: A -> res B) (f2: B -> res C)
(pa: list (X * A)) (pc: list (X * C)),
@@ -168,7 +168,7 @@ Proof.
Qed.
Lemma transform_partial_program_compose:
- forall (A B C V: Set)
+ forall (A B C V: Type)
(f1: A -> res B) (f2: B -> res C)
(pa: program A V) (pc: program C V),
transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
@@ -183,7 +183,7 @@ Proof.
Qed.
Lemma transform_program_partial_program:
- forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V),
+ forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V),
transform_partial_program (fun x => OK (f x)) p = OK tp ->
transform_program f p = tp.
Proof.
@@ -192,7 +192,7 @@ Proof.
Qed.
Lemma transform_program_compose:
- forall (A B C V: Set)
+ forall (A B C V: Type)
(f1: A -> res B) (f2: B -> C)
(pa: program A V) (pc: program C V),
transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
@@ -209,7 +209,7 @@ Proof.
Qed.
Lemma transform_partial_program_identity:
- forall (A V: Set) (pa pb: program A V),
+ forall (A V: Type) (pa pb: program A V),
transform_partial_program (@OK A) pa = OK pb ->
pa = pb.
Proof.
diff --git a/driver/Complements.v b/driver/Complements.v
index 938c4888b..8ee70bdde 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -51,7 +51,7 @@ Require Import Errors.
that this external call succeeds, has result [r], and changes
the world to [w]. *)
-Inductive world: Set :=
+Inductive world: Type :=
World: (ident -> list eventval -> option (eventval * world)) -> world.
Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
diff --git a/extraction/Kildall.ml.patch b/extraction/Kildall.ml.patch
index 453d40ce8..b7e5b0bf1 100644
--- a/extraction/Kildall.ml.patch
+++ b/extraction/Kildall.ml.patch
@@ -1,38 +1,37 @@
-*** kildall.ml.orig 2006-09-11 13:50:56.266682206 +0200
---- kildall.ml 2006-09-11 14:29:50.392200227 +0200
+*** kildall.ml.orig 2009-06-03 11:32:52.297641897 +0200
+--- kildall.ml 2009-06-03 11:34:48.481516509 +0200
***************
-*** 163,171 ****
- Maps.PMap.t option **)
+*** 151,158 ****
+ -> (positive, LAT.t) prod list -> LAT.t PMap.t option **)
let fixpoint successors topnode transf entrypoints =
-! DS.fixpoint (fun s ->
-! Maps.PMap.get s (make_predecessors successors topnode)) topnode transf
-! entrypoints
+! DS.fixpoint (fun s -> PMap.get s (make_predecessors successors topnode))
+! topnode transf entrypoints
end
module type ORDERED_TYPE_WITH_TOP =
---- 163,170 ----
- Maps.PMap.t option **)
+--- 151,158 ----
+ -> (positive, LAT.t) prod list -> LAT.t PMap.t option **)
let fixpoint successors topnode transf entrypoints =
! let pred = make_predecessors successors topnode in
-! DS.fixpoint (fun s -> Maps.PMap.get s pred) topnode transf entrypoints
+! DS.fixpoint (fun s -> PMap.get s pred) topnode transf entrypoints
end
module type ORDERED_TYPE_WITH_TOP =
***************
-*** 264,271 ****
- (** val basic_block_map : (positive -> positive list) -> positive ->
- positive -> bbmap **)
+*** 248,255 ****
+ (** val basic_block_map :
+ (positive -> positive list) -> positive -> positive -> bbmap **)
! let basic_block_map successors topnode entrypoint x =
! is_basic_block_head entrypoint (make_predecessors successors topnode) x
(** val basic_block_list : positive -> bbmap -> positive list **)
---- 263,270 ----
- (** val basic_block_map : (positive -> positive list) -> positive ->
- positive -> bbmap **)
+--- 248,255 ----
+ (** val basic_block_map :
+ (positive -> positive list) -> positive -> positive -> bbmap **)
! let basic_block_map successors topnode entrypoint =
! is_basic_block_head entrypoint (make_predecessors successors topnode)
diff --git a/extraction/convert b/extraction/convert
index 879cfe50d..94ec38e85 100755
--- a/extraction/convert
+++ b/extraction/convert
@@ -2,8 +2,5 @@
s/\bList\b/CoqList/g;
s/\bString\b/CoqString/g;
-s/\bInt\.Z_as_Int\b/CoqInt.Z_as_Int/g;
-s/\bInt\.Int\b/CoqInt.Int/g;
-s/\bInt\.MoreInt\b/CoqInt.MoreInt/g;
-s/^open Int$//;
+s/^open Int$/open CoqInt/;
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index a79ea29cb..9e2199c12 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -31,7 +31,7 @@ Require Import Wf_nat.
that have identical contents are equal. *)
Axiom extensionality:
- forall (A B: Set) (f g : A -> B),
+ forall (A B: Type) (f g : A -> B),
(forall x, f x = g x) -> f = g.
Axiom proof_irrelevance:
@@ -114,7 +114,7 @@ Proof.
Qed.
Lemma peq_true:
- forall (A: Set) (x: positive) (a b: A), (if peq x x then a else b) = a.
+ forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a.
Proof.
intros. case (peq x x); intros.
auto.
@@ -122,7 +122,7 @@ Proof.
Qed.
Lemma peq_false:
- forall (A: Set) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
+ forall (A: Type) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
Proof.
intros. case (peq x y); intros.
elim H; auto.
@@ -223,7 +223,7 @@ Proof.
intros. apply nat_of_P_lt_Lt_compare_morphism. exact H.
Qed.
-Variable A: Set.
+Variable A: Type.
Variable v1: A.
Variable f: positive -> A -> A.
@@ -289,7 +289,7 @@ End POSITIVE_ITERATION.
Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec.
Lemma zeq_true:
- forall (A: Set) (x: Z) (a b: A), (if zeq x x then a else b) = a.
+ forall (A: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a.
Proof.
intros. case (zeq x x); intros.
auto.
@@ -297,7 +297,7 @@ Proof.
Qed.
Lemma zeq_false:
- forall (A: Set) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
+ forall (A: Type) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
Proof.
intros. case (zeq x y); intros.
elim H; auto.
@@ -309,7 +309,7 @@ Open Scope Z_scope.
Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec.
Lemma zlt_true:
- forall (A: Set) (x y: Z) (a b: A),
+ forall (A: Type) (x y: Z) (a b: A),
x < y -> (if zlt x y then a else b) = a.
Proof.
intros. case (zlt x y); intros.
@@ -318,7 +318,7 @@ Proof.
Qed.
Lemma zlt_false:
- forall (A: Set) (x y: Z) (a b: A),
+ forall (A: Type) (x y: Z) (a b: A),
x >= y -> (if zlt x y then a else b) = b.
Proof.
intros. case (zlt x y); intros.
@@ -329,7 +329,7 @@ Qed.
Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec.
Lemma zle_true:
- forall (A: Set) (x y: Z) (a b: A),
+ forall (A: Type) (x y: Z) (a b: A),
x <= y -> (if zle x y then a else b) = a.
Proof.
intros. case (zle x y); intros.
@@ -338,7 +338,7 @@ Proof.
Qed.
Lemma zle_false:
- forall (A: Set) (x y: Z) (a b: A),
+ forall (A: Type) (x y: Z) (a b: A),
x > y -> (if zle x y then a else b) = b.
Proof.
intros. case (zle x y); intros.
@@ -573,7 +573,7 @@ Set Implicit Arguments.
(** Mapping a function over an option type. *)
-Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B :=
+Definition option_map (A B: Type) (f: A -> B) (x: option A) : option B :=
match x with
| None => None
| Some y => Some (f y)
@@ -581,7 +581,7 @@ Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B :=
(** Mapping a function over a sum type. *)
-Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C :=
+Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C :=
match x with
| inl y => inl C (f y)
| inr z => inr B z
@@ -592,7 +592,7 @@ Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C :=
Hint Resolve in_eq in_cons: coqlib.
Lemma nth_error_in:
- forall (A: Set) (n: nat) (l: list A) (x: A),
+ forall (A: Type) (n: nat) (l: list A) (x: A),
List.nth_error l n = Some x -> In x l.
Proof.
induction n; simpl.
@@ -606,7 +606,7 @@ Qed.
Hint Resolve nth_error_in: coqlib.
Lemma nth_error_nil:
- forall (A: Set) (idx: nat), nth_error (@nil A) idx = None.
+ forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.
Proof.
induction idx; simpl; intros; reflexivity.
Qed.
@@ -615,7 +615,7 @@ Hint Resolve nth_error_nil: coqlib.
(** Properties of [List.incl] (list inclusion). *)
Lemma incl_cons_inv:
- forall (A: Set) (a: A) (b c: list A),
+ forall (A: Type) (a: A) (b c: list A),
incl (a :: b) c -> incl b c.
Proof.
unfold incl; intros. apply H. apply in_cons. auto.
@@ -623,14 +623,14 @@ Qed.
Hint Resolve incl_cons_inv: coqlib.
Lemma incl_app_inv_l:
- forall (A: Set) (l1 l2 m: list A),
+ forall (A: Type) (l1 l2 m: list A),
incl (l1 ++ l2) m -> incl l1 m.
Proof.
unfold incl; intros. apply H. apply in_or_app. left; assumption.
Qed.
Lemma incl_app_inv_r:
- forall (A: Set) (l1 l2 m: list A),
+ forall (A: Type) (l1 l2 m: list A),
incl (l1 ++ l2) m -> incl l2 m.
Proof.
unfold incl; intros. apply H. apply in_or_app. right; assumption.
@@ -639,7 +639,7 @@ Qed.
Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
Lemma incl_same_head:
- forall (A: Set) (x: A) (l1 l2: list A),
+ forall (A: Type) (x: A) (l1 l2: list A),
incl l1 l2 -> incl (x::l1) (x::l2).
Proof.
intros; red; simpl; intros. intuition.
@@ -648,7 +648,7 @@ Qed.
(** Properties of [List.map] (mapping a function over a list). *)
Lemma list_map_exten:
- forall (A B: Set) (f f': A -> B) (l: list A),
+ forall (A B: Type) (f f': A -> B) (l: list A),
(forall x, In x l -> f x = f' x) ->
List.map f' l = List.map f l.
Proof.
@@ -660,21 +660,21 @@ Proof.
Qed.
Lemma list_map_compose:
- forall (A B C: Set) (f: A -> B) (g: B -> C) (l: list A),
+ forall (A B C: Type) (f: A -> B) (g: B -> C) (l: list A),
List.map g (List.map f l) = List.map (fun x => g(f x)) l.
Proof.
induction l; simpl. reflexivity. rewrite IHl; reflexivity.
Qed.
Lemma list_map_identity:
- forall (A: Set) (l: list A),
+ forall (A: Type) (l: list A),
List.map (fun (x:A) => x) l = l.
Proof.
induction l; simpl; congruence.
Qed.
Lemma list_map_nth:
- forall (A B: Set) (f: A -> B) (l: list A) (n: nat),
+ forall (A B: Type) (f: A -> B) (l: list A) (n: nat),
nth_error (List.map f l) n = option_map f (nth_error l n).
Proof.
induction l; simpl; intros.
@@ -683,14 +683,14 @@ Proof.
Qed.
Lemma list_length_map:
- forall (A B: Set) (f: A -> B) (l: list A),
+ forall (A B: Type) (f: A -> B) (l: list A),
List.length (List.map f l) = List.length l.
Proof.
induction l; simpl; congruence.
Qed.
Lemma list_in_map_inv:
- forall (A B: Set) (f: A -> B) (l: list A) (y: B),
+ forall (A B: Type) (f: A -> B) (l: list A) (y: B),
In y (List.map f l) -> exists x:A, y = f x /\ In x l.
Proof.
induction l; simpl; intros.
@@ -702,7 +702,7 @@ Proof.
Qed.
Lemma list_append_map:
- forall (A B: Set) (f: A -> B) (l1 l2: list A),
+ forall (A B: Type) (f: A -> B) (l1 l2: list A),
List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.
Proof.
induction l1; simpl; intros.
@@ -712,19 +712,19 @@ Qed.
(** Properties of list membership. *)
Lemma in_cns:
- forall (A: Set) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
+ forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
Proof.
intros. simpl. tauto.
Qed.
Lemma in_app:
- forall (A: Set) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
+ forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
Proof.
intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
Qed.
Lemma list_in_insert:
- forall (A: Set) (x: A) (l1 l2: list A) (y: A),
+ forall (A: Type) (x: A) (l1 l2: list A) (y: A),
In x (l1 ++ l2) -> In x (l1 ++ y :: l2).
Proof.
intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto.
@@ -733,25 +733,25 @@ Qed.
(** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements
in common. *)
-Definition list_disjoint (A: Set) (l1 l2: list A) : Prop :=
+Definition list_disjoint (A: Type) (l1 l2: list A) : Prop :=
forall (x y: A), In x l1 -> In y l2 -> x <> y.
Lemma list_disjoint_cons_left:
- forall (A: Set) (a: A) (l1 l2: list A),
+ forall (A: Type) (a: A) (l1 l2: list A),
list_disjoint (a :: l1) l2 -> list_disjoint l1 l2.
Proof.
unfold list_disjoint; simpl; intros. apply H; tauto.
Qed.
Lemma list_disjoint_cons_right:
- forall (A: Set) (a: A) (l1 l2: list A),
+ forall (A: Type) (a: A) (l1 l2: list A),
list_disjoint l1 (a :: l2) -> list_disjoint l1 l2.
Proof.
unfold list_disjoint; simpl; intros. apply H; tauto.
Qed.
Lemma list_disjoint_notin:
- forall (A: Set) (l1 l2: list A) (a: A),
+ forall (A: Type) (l1 l2: list A) (a: A),
list_disjoint l1 l2 -> In a l1 -> ~(In a l2).
Proof.
unfold list_disjoint; intros; red; intros.
@@ -759,7 +759,7 @@ Proof.
Qed.
Lemma list_disjoint_sym:
- forall (A: Set) (l1 l2: list A),
+ forall (A: Type) (l1 l2: list A),
list_disjoint l1 l2 -> list_disjoint l2 l1.
Proof.
unfold list_disjoint; intros.
@@ -767,7 +767,7 @@ Proof.
Qed.
Lemma list_disjoint_dec:
- forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
+ forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
{list_disjoint l1 l2} + {~list_disjoint l1 l2}.
Proof.
induction l1; intros.
@@ -784,7 +784,7 @@ Defined.
(** [list_norepet l] holds iff the list [l] contains no repetitions,
i.e. no element occurs twice. *)
-Inductive list_norepet (A: Set) : list A -> Prop :=
+Inductive list_norepet (A: Type) : list A -> Prop :=
| list_norepet_nil:
list_norepet nil
| list_norepet_cons:
@@ -792,7 +792,7 @@ Inductive list_norepet (A: Set) : list A -> Prop :=
~(In hd tl) -> list_norepet tl -> list_norepet (hd :: tl).
Lemma list_norepet_dec:
- forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
+ forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
{list_norepet l} + {~list_norepet l}.
Proof.
induction l.
@@ -805,7 +805,7 @@ Proof.
Defined.
Lemma list_map_norepet:
- forall (A B: Set) (f: A -> B) (l: list A),
+ forall (A B: Type) (f: A -> B) (l: list A),
list_norepet l ->
(forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
list_norepet (List.map f l).
@@ -821,7 +821,7 @@ Proof.
Qed.
Remark list_norepet_append_commut:
- forall (A: Set) (a b: list A),
+ forall (A: Type) (a b: list A),
list_norepet (a ++ b) -> list_norepet (b ++ a).
Proof.
intro A.
@@ -844,7 +844,7 @@ Proof.
Qed.
Lemma list_norepet_app:
- forall (A: Set) (l1 l2: list A),
+ forall (A: Type) (l1 l2: list A),
list_norepet (l1 ++ l2) <->
list_norepet l1 /\ list_norepet l2 /\ list_disjoint l1 l2.
Proof.
@@ -860,7 +860,7 @@ Proof.
Qed.
Lemma list_norepet_append:
- forall (A: Set) (l1 l2: list A),
+ forall (A: Type) (l1 l2: list A),
list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
list_norepet (l1 ++ l2).
Proof.
@@ -868,14 +868,14 @@ Proof.
Qed.
Lemma list_norepet_append_right:
- forall (A: Set) (l1 l2: list A),
+ forall (A: Type) (l1 l2: list A),
list_norepet (l1 ++ l2) -> list_norepet l2.
Proof.
generalize list_norepet_app; firstorder.
Qed.
Lemma list_norepet_append_left:
- forall (A: Set) (l1 l2: list A),
+ forall (A: Type) (l1 l2: list A),
list_norepet (l1 ++ l2) -> list_norepet l1.
Proof.
generalize list_norepet_app; firstorder.
@@ -883,14 +883,14 @@ Qed.
(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
-Inductive is_tail (A: Set): list A -> list A -> Prop :=
+Inductive is_tail (A: Type): list A -> list A -> Prop :=
| is_tail_refl:
forall c, is_tail c c
| is_tail_cons:
forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).
Lemma is_tail_in:
- forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
+ forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
Proof.
induction c2; simpl; intros.
inversion H.
@@ -898,7 +898,7 @@ Proof.
Qed.
Lemma is_tail_cons_left:
- forall (A: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
+ forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
Proof.
induction c2; intros; inversion H.
constructor. constructor. constructor. auto.
@@ -907,13 +907,13 @@ Qed.
Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
Lemma is_tail_incl:
- forall (A: Set) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
+ forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
Proof.
induction 1; eauto with coqlib.
Qed.
Lemma is_tail_trans:
- forall (A: Set) (l1 l2: list A),
+ forall (A: Type) (l1 l2: list A),
is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3.
Proof.
induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
@@ -924,8 +924,8 @@ Qed.
Section FORALL2.
-Variable A: Set.
-Variable B: Set.
+Variable A: Type.
+Variable B: Type.
Variable P: A -> B -> Prop.
Inductive list_forall2: list A -> list B -> Prop :=
@@ -940,7 +940,7 @@ Inductive list_forall2: list A -> list B -> Prop :=
End FORALL2.
Lemma list_forall2_imply:
- forall (A B: Set) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
+ forall (A B: Type) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
list_forall2 P1 l1 l2 ->
forall (P2: A -> B -> Prop),
(forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) ->
@@ -954,45 +954,45 @@ Qed.
(** Dropping the first or first two elements of a list. *)
-Definition list_drop1 (A: Set) (x: list A) :=
+Definition list_drop1 (A: Type) (x: list A) :=
match x with nil => nil | hd :: tl => tl end.
-Definition list_drop2 (A: Set) (x: list A) :=
+Definition list_drop2 (A: Type) (x: list A) :=
match x with nil => nil | hd :: nil => nil | hd1 :: hd2 :: tl => tl end.
Lemma list_drop1_incl:
- forall (A: Set) (x: A) (l: list A), In x (list_drop1 l) -> In x l.
+ forall (A: Type) (x: A) (l: list A), In x (list_drop1 l) -> In x l.
Proof.
intros. destruct l. elim H. simpl in H. auto with coqlib.
Qed.
Lemma list_drop2_incl:
- forall (A: Set) (x: A) (l: list A), In x (list_drop2 l) -> In x l.
+ forall (A: Type) (x: A) (l: list A), In x (list_drop2 l) -> In x l.
Proof.
intros. destruct l. elim H. destruct l. elim H.
simpl in H. auto with coqlib.
Qed.
Lemma list_drop1_norepet:
- forall (A: Set) (l: list A), list_norepet l -> list_norepet (list_drop1 l).
+ forall (A: Type) (l: list A), list_norepet l -> list_norepet (list_drop1 l).
Proof.
intros. destruct l; simpl. constructor. inversion H. auto.
Qed.
Lemma list_drop2_norepet:
- forall (A: Set) (l: list A), list_norepet l -> list_norepet (list_drop2 l).
+ forall (A: Type) (l: list A), list_norepet l -> list_norepet (list_drop2 l).
Proof.
intros. destruct l; simpl. constructor.
destruct l; simpl. constructor. inversion H. inversion H3. auto.
Qed.
Lemma list_map_drop1:
- forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).
+ forall (A B: Type) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).
Proof.
intros; destruct l; reflexivity.
Qed.
Lemma list_map_drop2:
- forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).
+ forall (A B: Type) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).
Proof.
intros; destruct l. reflexivity. destruct l; reflexivity.
Qed.
@@ -1014,9 +1014,9 @@ Qed.
Section DECIDABLE_EQUALITY.
-Variable A: Set.
+Variable A: Type.
Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.
-Variable B: Set.
+Variable B: Type.
Lemma dec_eq_true:
forall (x: A) (ifso ifnot: B),
diff --git a/lib/Floats.v b/lib/Floats.v
index 6857236d3..2e60d73e0 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -23,7 +23,7 @@
Require Import Coqlib.
Require Import Integers.
-Parameter float: Set.
+Parameter float: Type.
Module Float.
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
index 728a7252b..77f5d8496 100644
--- a/lib/Inclusion.v
+++ b/lib/Inclusion.v
@@ -51,7 +51,7 @@ Ltac all_app e :=
(** This data type, [flatten], [insert_bin], [sort_bin] and a few theorem
are taken from the CoqArt book, chapt. 16. *)
-Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
+Inductive bin : Type := node : bin->bin->bin | leaf : nat->bin.
Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
match t with
@@ -91,7 +91,7 @@ Fixpoint sort_bin (t:bin) : bin :=
end.
Section assoc_eq.
- Variables (A : Set)(f : A->A->A).
+ Variables (A : Type)(f : A->A->A).
Hypothesis assoc : forall x y z:A, f x (f y z) = f (f x y) z.
Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
@@ -147,7 +147,7 @@ Ltac model_aux_app l v :=
end.
Theorem In_permute_app_head :
- forall A:Set, forall r:A, forall x y l:list A,
+ forall A:Type, forall r:A, forall x y l:list A,
In r (x++y++l) -> In r (y++x++l).
intros A r x y l; generalize r; change (incl (x++y++l)(y++x++l)).
repeat rewrite ass_app; auto with datatypes.
@@ -155,7 +155,7 @@ Qed.
Theorem insert_bin_included :
forall x:nat, forall t2:bin,
- forall (A:Set) (r:A) (l:list (list A))(def:list A),
+ forall (A:Type) (r:A) (l:list (list A))(def:list A),
In r (bin_A (list A) (app (A:=A)) l def (insert_bin x t2)) ->
In r (bin_A (list A) (app (A:=A)) l def (node (leaf x) t2)).
intros x t2; induction t2.
@@ -181,7 +181,7 @@ apply In_permute_app_head; assumption.
Qed.
Theorem in_or_insert_bin :
- forall (n:nat) (t2:bin) (A:Set)(r:A)(l:list (list A)) (def:list A),
+ forall (n:nat) (t2:bin) (A:Type)(r:A)(l:list (list A)) (def:list A),
In r (nth n l def) \/ In r (bin_A (list A)(app (A:=A)) l def t2) ->
In r (bin_A (list A)(app (A:=A)) l def (insert_bin n t2)).
intros n t2 A r l def; induction t2.
@@ -198,7 +198,7 @@ simpl; intros [H|H]; case (nat_le_bool n n0); simpl; apply in_or_app; auto.
Qed.
Theorem sort_included :
- forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+ forall t:bin, forall (A:Type)(r:A)(l:list(list A))(def:list A),
In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)) ->
In r (bin_A (list A) (app (A:=A)) l def t).
induction t.
@@ -213,7 +213,7 @@ simpl;intros;assumption.
Qed.
Theorem sort_included2 :
- forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+ forall t:bin, forall (A:Type)(r:A)(l:list(list A))(def:list A),
In r (bin_A (list A) (app (A:=A)) l def t) ->
In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)).
induction t.
@@ -226,7 +226,7 @@ simpl; auto.
Qed.
Theorem in_remove_head :
- forall (A:Set)(x:A)(l1 l2 l3:list A),
+ forall (A:Type)(x:A)(l1 l2 l3:list A),
In x (l1++l2) -> (In x l2 -> In x l3) -> In x (l1++l3).
intros A x l1 l2 l3 H H1.
elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
@@ -257,7 +257,7 @@ Fixpoint test_inclusion (t1 t2:bin) {struct t1} : bool :=
Theorem check_all_leaves_sound :
forall x t2,
check_all_leaves x t2 = true ->
- forall (A:Set)(r:A)(l:list(list A))(def:list A),
+ forall (A:Type)(r:A)(l:list(list A))(def:list A),
In r (bin_A (list A) (app (A:=A)) l def t2) ->
In r (nth x l def).
intros x t2; induction t2; simpl.
@@ -270,7 +270,7 @@ Qed.
Theorem remove_all_leaves_sound :
forall x t2,
- forall (A:Set)(r:A)(l:list(list A))(def:list A),
+ forall (A:Type)(r:A)(l:list(list A))(def:list A),
In r (bin_A (list A) (app(A:=A)) l def t2) ->
In r (bin_A (list A) (app(A:=A)) l def (remove_all_leaves x t2)) \/
In r (nth x l def).
@@ -293,7 +293,7 @@ Qed.
Theorem test_inclusion_sound :
forall t1 t2:bin,
test_inclusion t1 t2 = true ->
- forall (A:Set)(r:A)(l:list(list A))(def:list A),
+ forall (A:Type)(r:A)(l:list(list A))(def:list A),
In r (bin_A (list A)(app(A:=A)) l def t2) ->
In r (bin_A (list A)(app(A:=A)) l def t1).
intros t1; induction t1.
@@ -317,7 +317,7 @@ Qed.
Theorem inclusion_theorem :
forall t1 t2 : bin,
test_inclusion (sort_bin (flatten t1)) (sort_bin (flatten t2)) = true ->
- forall (A:Set)(r:A)(l:list(list A))(def:list A),
+ forall (A:Type)(r:A)(l:list(list A))(def:list A),
In r (bin_A (list A) (app(A:=A)) l def t2) ->
In r (bin_A (list A) (app(A:=A)) l def t1).
intros t1 t2 Heq A r l def H.
diff --git a/lib/Integers.v b/lib/Integers.v
index ceda85121..1eb59c5c5 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -23,7 +23,7 @@ Definition half_modulus : Z := modulus / 2.
(** * Comparisons *)
-Inductive comparison : Set :=
+Inductive comparison : Type :=
| Ceq : comparison (**r same *)
| Cne : comparison (**r different *)
| Clt : comparison (**r less than *)
@@ -57,7 +57,7 @@ Definition swap_comparison (c: comparison): comparison :=
integer (type [Z]) plus a proof that it is in the range 0 (included) to
[modulus] (excluded. *)
-Record int: Set := mkint { intval: Z; intrange: 0 <= intval < modulus }.
+Record int: Type := mkint { intval: Z; intrange: 0 <= intval < modulus }.
Module Int.
@@ -289,7 +289,7 @@ Definition is_power2 (x: int) : option int :=
>>
*)
-Inductive rlw_state: Set :=
+Inductive rlw_state: Type :=
| RLW_S0 : rlw_state
| RLW_S1 : rlw_state
| RLW_S2 : rlw_state
diff --git a/lib/Iteration.v b/lib/Iteration.v
index cabe5b825..24835da2b 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -18,9 +18,9 @@ Require Import Max.
Module Type ITER.
Variable iterate
- : forall A B : Set, (A -> B + A) -> A -> option B.
+ : forall A B : Type, (A -> B + A) -> A -> option B.
Hypothesis iterate_prop
- : forall (A B : Set) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
+ : forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop),
(forall a : A, P a ->
match step a with inl b => Q b | inr a' => P a' end) ->
forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b.
@@ -39,7 +39,7 @@ Module PrimIter: ITER.
Section ITERATION.
-Variables A B: Set.
+Variables A B: Type.
Variable step: A -> B + A.
(** The [step] parameter represents one step of the iteration. From a
@@ -174,7 +174,7 @@ Module GenIter: ITER.
Section ITERATION.
-Variables A B: Set.
+Variables A B: Type.
Variable step: A -> B + A.
Definition B_le (x y: option B) : Prop := x = None \/ y = x.
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 3c390069e..1d58ee5a9 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -25,7 +25,7 @@ Require Import FSets.
Module Type SEMILATTICE.
- Variable t: Set.
+ Variable t: Type.
Variable eq: t -> t -> Prop.
Hypothesis eq_refl: forall x, eq x x.
Hypothesis eq_sym: forall x y, eq x y -> eq y x.
@@ -49,24 +49,9 @@ End SEMILATTICE.
Module Type SEMILATTICE_WITH_TOP.
- Variable t: Set.
- Variable eq: t -> t -> Prop.
- Hypothesis eq_refl: forall x, eq x x.
- Hypothesis eq_sym: forall x y, eq x y -> eq y x.
- Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
- Variable beq: t -> t -> bool.
- Hypothesis beq_correct: forall x y, beq x y = true -> eq x y.
- Variable ge: t -> t -> Prop.
- Hypothesis ge_refl: forall x y, eq x y -> ge x y.
- Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
- Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
- Variable bot: t.
- Hypothesis ge_bot: forall x, ge x bot.
+ Include Type SEMILATTICE.
Variable top: t.
Hypothesis ge_top: forall x, ge top x.
- Variable lub: t -> t -> t.
- Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x).
- Hypothesis ge_lub_left: forall x y, ge (lub x y) x.
End SEMILATTICE_WITH_TOP.
@@ -78,11 +63,11 @@ End SEMILATTICE_WITH_TOP.
Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.
-Inductive t_ : Set :=
+Inductive t_ : Type :=
| Bot_except: PTree.t L.t -> t_
| Top_except: PTree.t L.t -> t_.
-Definition t: Set := t_.
+Definition t: Type := t_.
Definition get (p: positive) (x: t) : L.t :=
match x with
@@ -333,12 +318,12 @@ End LFSet.
Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP.
-Inductive t_ : Set :=
+Inductive t_ : Type :=
| Bot: t_
| Inj: X.t -> t_
| Top: t_.
-Definition t : Set := t_.
+Definition t : Type := t_.
Definition eq (x y: t) := (x = y).
Definition eq_refl: forall x, eq x x := (@refl_equal t).
diff --git a/lib/Maps.v b/lib/Maps.v
index 4209fe6ec..a277e6772 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -39,46 +39,46 @@ Set Implicit Arguments.
(** * The abstract signatures of trees *)
Module Type TREE.
- Variable elt: Set.
+ Variable elt: Type.
Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
- Variable t: Set -> Set.
- Variable eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+ Variable t: Type -> Type.
+ Variable eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
forall (a b: t A), {a = b} + {a <> b}.
- Variable empty: forall (A: Set), t A.
- Variable get: forall (A: Set), elt -> t A -> option A.
- Variable set: forall (A: Set), elt -> A -> t A -> t A.
- Variable remove: forall (A: Set), elt -> t A -> t A.
+ Variable empty: forall (A: Type), t A.
+ Variable get: forall (A: Type), elt -> t A -> option A.
+ Variable set: forall (A: Type), elt -> A -> t A -> t A.
+ Variable remove: forall (A: Type), elt -> t A -> t A.
(** The ``good variables'' properties for trees, expressing
commutations between [get], [set] and [remove]. *)
Hypothesis gempty:
- forall (A: Set) (i: elt), get i (empty A) = None.
+ forall (A: Type) (i: elt), get i (empty A) = None.
Hypothesis gss:
- forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
+ forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Hypothesis gso:
- forall (A: Set) (i j: elt) (x: A) (m: t A),
+ forall (A: Type) (i j: elt) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Hypothesis gsspec:
- forall (A: Set) (i j: elt) (x: A) (m: t A),
+ forall (A: Type) (i j: elt) (x: A) (m: t A),
get i (set j x m) = if elt_eq i j then Some x else get i m.
Hypothesis gsident:
- forall (A: Set) (i: elt) (m: t A) (v: A),
+ forall (A: Type) (i: elt) (m: t A) (v: A),
get i m = Some v -> set i v m = m.
(* We could implement the following, but it's not needed for the moment.
Hypothesis grident:
- forall (A: Set) (i: elt) (m: t A) (v: A),
+ forall (A: Type) (i: elt) (m: t A) (v: A),
get i m = None -> remove i m = m.
*)
Hypothesis grs:
- forall (A: Set) (i: elt) (m: t A), get i (remove i m) = None.
+ forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Hypothesis gro:
- forall (A: Set) (i j: elt) (m: t A),
+ forall (A: Type) (i j: elt) (m: t A),
i <> j -> get i (remove j m) = get i m.
(** Extensional equality between trees. *)
- Variable beq: forall (A: Set), (A -> A -> bool) -> t A -> t A -> bool.
+ Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
Hypothesis beq_correct:
- forall (A: Set) (P: A -> A -> Prop) (cmp: A -> A -> bool),
+ forall (A: Type) (P: A -> A -> Prop) (cmp: A -> A -> bool),
(forall (x y: A), cmp x y = true -> P x y) ->
forall (t1 t2: t A), beq cmp t1 t2 = true ->
forall (x: elt),
@@ -90,43 +90,43 @@ Module Type TREE.
(** Applying a function to all data of a tree. *)
Variable map:
- forall (A B: Set), (elt -> A -> B) -> t A -> t B.
+ forall (A B: Type), (elt -> A -> B) -> t A -> t B.
Hypothesis gmap:
- forall (A B: Set) (f: elt -> A -> B) (i: elt) (m: t A),
+ forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),
get i (map f m) = option_map (f i) (get i m).
(** Applying a function pairwise to all data of two trees. *)
Variable combine:
- forall (A: Set), (option A -> option A -> option A) -> t A -> t A -> t A.
+ forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A.
Hypothesis gcombine:
- forall (A: Set) (f: option A -> option A -> option A)
+ forall (A: Type) (f: option A -> option A -> option A)
(m1 m2: t A) (i: elt),
f None None = None ->
get i (combine f m1 m2) = f (get i m1) (get i m2).
Hypothesis combine_commut:
- forall (A: Set) (f g: option A -> option A -> option A),
+ forall (A: Type) (f g: option A -> option A -> option A),
(forall (i j: option A), f i j = g j i) ->
forall (m1 m2: t A),
combine f m1 m2 = combine g m2 m1.
(** Enumerating the bindings of a tree. *)
Variable elements:
- forall (A: Set), t A -> list (elt * A).
+ forall (A: Type), t A -> list (elt * A).
Hypothesis elements_correct:
- forall (A: Set) (m: t A) (i: elt) (v: A),
+ forall (A: Type) (m: t A) (i: elt) (v: A),
get i m = Some v -> In (i, v) (elements m).
Hypothesis elements_complete:
- forall (A: Set) (m: t A) (i: elt) (v: A),
+ forall (A: Type) (m: t A) (i: elt) (v: A),
In (i, v) (elements m) -> get i m = Some v.
Hypothesis elements_keys_norepet:
- forall (A: Set) (m: t A),
+ forall (A: Type) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).
(** Folding a function over all bindings of a tree. *)
Variable fold:
- forall (A B: Set), (B -> elt -> A -> B) -> t A -> B -> B.
+ forall (A B: Type), (B -> elt -> A -> B) -> t A -> B -> B.
Hypothesis fold_spec:
- forall (A B: Set) (f: B -> elt -> A -> B) (v: B) (m: t A),
+ forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A),
fold f m v =
List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
End TREE.
@@ -134,27 +134,27 @@ End TREE.
(** * The abstract signatures of maps *)
Module Type MAP.
- Variable elt: Set.
+ Variable elt: Type.
Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
- Variable t: Set -> Set.
- Variable init: forall (A: Set), A -> t A.
- Variable get: forall (A: Set), elt -> t A -> A.
- Variable set: forall (A: Set), elt -> A -> t A -> t A.
+ Variable t: Type -> Type.
+ Variable init: forall (A: Type), A -> t A.
+ Variable get: forall (A: Type), elt -> t A -> A.
+ Variable set: forall (A: Type), elt -> A -> t A -> t A.
Hypothesis gi:
- forall (A: Set) (i: elt) (x: A), get i (init x) = x.
+ forall (A: Type) (i: elt) (x: A), get i (init x) = x.
Hypothesis gss:
- forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
+ forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
Hypothesis gso:
- forall (A: Set) (i j: elt) (x: A) (m: t A),
+ forall (A: Type) (i j: elt) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Hypothesis gsspec:
- forall (A: Set) (i j: elt) (x: A) (m: t A),
+ forall (A: Type) (i j: elt) (x: A) (m: t A),
get i (set j x m) = if elt_eq i j then x else get i m.
Hypothesis gsident:
- forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
- Variable map: forall (A B: Set), (A -> B) -> t A -> t B.
+ forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+ Variable map: forall (A B: Type), (A -> B) -> t A -> t B.
Hypothesis gmap:
- forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
+ forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
get i (map f m) = f(get i m).
End MAP.
@@ -164,7 +164,7 @@ Module PTree <: TREE.
Definition elt := positive.
Definition elt_eq := peq.
- Inductive tree (A : Set) : Set :=
+ Inductive tree (A : Type) : Type :=
| Leaf : tree A
| Node : tree A -> option A -> tree A -> tree A
.
@@ -173,7 +173,7 @@ Module PTree <: TREE.
Definition t := tree.
- Theorem eq : forall (A : Set),
+ Theorem eq : forall (A : Type),
(forall (x y: A), {x=y} + {x<>y}) ->
forall (a b : t A), {a = b} + {a <> b}.
Proof.
@@ -182,9 +182,9 @@ Module PTree <: TREE.
generalize o o0; decide equality.
Qed.
- Definition empty (A : Set) := (Leaf : t A).
+ Definition empty (A : Type) := (Leaf : t A).
- Fixpoint get (A : Set) (i : positive) (m : t A) {struct i} : option A :=
+ Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
match m with
| Leaf => None
| Node l o r =>
@@ -195,7 +195,7 @@ Module PTree <: TREE.
end
end.
- Fixpoint set (A : Set) (i : positive) (v : A) (m : t A) {struct i} : t A :=
+ Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A :=
match m with
| Leaf =>
match i with
@@ -211,7 +211,7 @@ Module PTree <: TREE.
end
end.
- Fixpoint remove (A : Set) (i : positive) (m : t A) {struct i} : t A :=
+ Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A :=
match i with
| xH =>
match m with
@@ -242,22 +242,22 @@ Module PTree <: TREE.
end.
Theorem gempty:
- forall (A: Set) (i: positive), get i (empty A) = None.
+ forall (A: Type) (i: positive), get i (empty A) = None.
Proof.
induction i; simpl; auto.
Qed.
Theorem gss:
- forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
+ forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
Proof.
induction i; destruct m; simpl; auto.
Qed.
- Lemma gleaf : forall (A : Set) (i : positive), get i (Leaf : t A) = None.
+ Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None.
Proof. exact gempty. Qed.
Theorem gso:
- forall (A: Set) (i j: positive) (x: A) (m: t A),
+ forall (A: Type) (i j: positive) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Proof.
induction i; intros; destruct j; destruct m; simpl;
@@ -265,7 +265,7 @@ Module PTree <: TREE.
Qed.
Theorem gsspec:
- forall (A: Set) (i j: positive) (x: A) (m: t A),
+ forall (A: Type) (i j: positive) (x: A) (m: t A),
get i (set j x m) = if peq i j then Some x else get i m.
Proof.
intros.
@@ -273,7 +273,7 @@ Module PTree <: TREE.
Qed.
Theorem gsident:
- forall (A: Set) (i: positive) (m: t A) (v: A),
+ forall (A: Type) (i: positive) (m: t A) (v: A),
get i m = Some v -> set i v m = m.
Proof.
induction i; intros; destruct m; simpl; simpl in H; try congruence.
@@ -281,11 +281,11 @@ Module PTree <: TREE.
rewrite (IHi m1 v H); congruence.
Qed.
- Lemma rleaf : forall (A : Set) (i : positive), remove i (Leaf : t A) = Leaf.
+ Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf.
Proof. destruct i; simpl; auto. Qed.
Theorem grs:
- forall (A: Set) (i: positive) (m: t A), get i (remove i m) = None.
+ forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None.
Proof.
induction i; destruct m.
simpl; auto.
@@ -305,7 +305,7 @@ Module PTree <: TREE.
Qed.
Theorem gro:
- forall (A: Set) (i j: positive) (m: t A),
+ forall (A: Type) (i j: positive) (m: t A),
i <> j -> get i (remove j m) = get i m.
Proof.
induction i; intros; destruct j; destruct m;
@@ -335,7 +335,7 @@ Module PTree <: TREE.
Section EXTENSIONAL_EQUALITY.
- Variable A: Set.
+ Variable A: Type.
Variable eqA: A -> A -> Prop.
Variable beqA: A -> A -> bool.
Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
@@ -439,7 +439,7 @@ Module PTree <: TREE.
simpl; auto.
Qed.
- Fixpoint xmap (A B : Set) (f : positive -> A -> B) (m : t A) (i : positive)
+ Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive)
{struct m} : t B :=
match m with
| Leaf => Leaf
@@ -448,10 +448,10 @@ Module PTree <: TREE.
(xmap f r (append i (xI xH)))
end.
- Definition map (A B : Set) (f : positive -> A -> B) m := xmap f m xH.
+ Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH.
Lemma xgmap:
- forall (A B: Set) (f: positive -> A -> B) (i j : positive) (m: t A),
+ forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
get i (xmap f m j) = option_map (f (append j i)) (get i m).
Proof.
induction i; intros; destruct m; simpl; auto.
@@ -461,7 +461,7 @@ Module PTree <: TREE.
Qed.
Theorem gmap:
- forall (A B: Set) (f: positive -> A -> B) (i: positive) (m: t A),
+ forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
get i (map f m) = option_map (f i) (get i m).
Proof.
intros.
@@ -471,7 +471,7 @@ Module PTree <: TREE.
rewrite append_neutral_l; auto.
Qed.
- Fixpoint xcombine_l (A : Set) (f : option A -> option A -> option A)
+ Fixpoint xcombine_l (A : Type) (f : option A -> option A -> option A)
(m : t A) {struct m} : t A :=
match m with
| Leaf => Leaf
@@ -479,14 +479,14 @@ Module PTree <: TREE.
end.
Lemma xgcombine_l :
- forall (A : Set) (f : option A -> option A -> option A)
+ forall (A : Type) (f : option A -> option A -> option A)
(i : positive) (m : t A),
f None None = None -> get i (xcombine_l f m) = f (get i m) None.
Proof.
induction i; intros; destruct m; simpl; auto.
Qed.
- Fixpoint xcombine_r (A : Set) (f : option A -> option A -> option A)
+ Fixpoint xcombine_r (A : Type) (f : option A -> option A -> option A)
(m : t A) {struct m} : t A :=
match m with
| Leaf => Leaf
@@ -494,14 +494,14 @@ Module PTree <: TREE.
end.
Lemma xgcombine_r :
- forall (A : Set) (f : option A -> option A -> option A)
+ forall (A : Type) (f : option A -> option A -> option A)
(i : positive) (m : t A),
f None None = None -> get i (xcombine_r f m) = f None (get i m).
Proof.
induction i; intros; destruct m; simpl; auto.
Qed.
- Fixpoint combine (A : Set) (f : option A -> option A -> option A)
+ Fixpoint combine (A : Type) (f : option A -> option A -> option A)
(m1 m2 : t A) {struct m1} : t A :=
match m1 with
| Leaf => xcombine_r f m2
@@ -513,7 +513,7 @@ Module PTree <: TREE.
end.
Lemma xgcombine:
- forall (A: Set) (f: option A -> option A -> option A) (i: positive)
+ forall (A: Type) (f: option A -> option A -> option A) (i: positive)
(m1 m2: t A),
f None None = None ->
get i (combine f m1 m2) = f (get i m1) (get i m2).
@@ -523,7 +523,7 @@ Module PTree <: TREE.
Qed.
Theorem gcombine:
- forall (A: Set) (f: option A -> option A -> option A)
+ forall (A: Type) (f: option A -> option A -> option A)
(m1 m2: t A) (i: positive),
f None None = None ->
get i (combine f m1 m2) = f (get i m1) (get i m2).
@@ -532,7 +532,7 @@ Module PTree <: TREE.
Qed.
Lemma xcombine_lr :
- forall (A : Set) (f g : option A -> option A -> option A) (m : t A),
+ forall (A : Type) (f g : option A -> option A -> option A) (m : t A),
(forall (i j : option A), f i j = g j i) ->
xcombine_l f m = xcombine_r g m.
Proof.
@@ -543,7 +543,7 @@ Module PTree <: TREE.
Qed.
Theorem combine_commut:
- forall (A: Set) (f g: option A -> option A -> option A),
+ forall (A: Type) (f g: option A -> option A -> option A),
(forall (i j: option A), f i j = g j i) ->
forall (m1 m2: t A),
combine f m1 m2 = combine g m2 m1.
@@ -561,7 +561,7 @@ Module PTree <: TREE.
auto.
Qed.
- Fixpoint xelements (A : Set) (m : t A) (i : positive) {struct m}
+ Fixpoint xelements (A : Type) (m : t A) (i : positive) {struct m}
: list (positive * A) :=
match m with
| Leaf => nil
@@ -578,7 +578,7 @@ Module PTree <: TREE.
Definition elements A (m : t A) := xelements m xH.
Lemma xelements_correct:
- forall (A: Set) (m: t A) (i j : positive) (v: A),
+ forall (A: Type) (m: t A) (i j : positive) (v: A),
get i m = Some v -> In (append j i, v) (xelements m j).
Proof.
induction m; intros.
@@ -595,14 +595,14 @@ Module PTree <: TREE.
Qed.
Theorem elements_correct:
- forall (A: Set) (m: t A) (i: positive) (v: A),
+ forall (A: Type) (m: t A) (i: positive) (v: A),
get i m = Some v -> In (i, v) (elements m).
Proof.
intros A m i v H.
exact (xelements_correct m i xH H).
Qed.
- Fixpoint xget (A : Set) (i j : positive) (m : t A) {struct j} : option A :=
+ Fixpoint xget (A : Type) (i j : positive) (m : t A) {struct j} : option A :=
match i, j with
| _, xH => get i m
| xO ii, xO jj => xget ii jj m
@@ -611,7 +611,7 @@ Module PTree <: TREE.
end.
Lemma xget_left :
- forall (A : Set) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
+ forall (A : Type) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v.
Proof.
induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
@@ -619,7 +619,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_ii :
- forall (A: Set) (m: t A) (i j : positive) (v: A),
+ forall (A: Type) (m: t A) (i j : positive) (v: A),
In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j).
Proof.
induction m.
@@ -635,7 +635,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_io :
- forall (A: Set) (m: t A) (i j : positive) (v: A),
+ forall (A: Type) (m: t A) (i j : positive) (v: A),
~In (xI i, v) (xelements m (xO j)).
Proof.
induction m.
@@ -650,7 +650,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_oo :
- forall (A: Set) (m: t A) (i j : positive) (v: A),
+ forall (A: Type) (m: t A) (i j : positive) (v: A),
In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j).
Proof.
induction m.
@@ -666,7 +666,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_oi :
- forall (A: Set) (m: t A) (i j : positive) (v: A),
+ forall (A: Type) (m: t A) (i j : positive) (v: A),
~In (xO i, v) (xelements m (xI j)).
Proof.
induction m.
@@ -681,7 +681,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_ih :
- forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A),
+ forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),
In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH).
Proof.
destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -694,7 +694,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_oh :
- forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A),
+ forall (A: Type) (m1 m2: t A) (o: option A) (i : positive) (v: A),
In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH).
Proof.
destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -707,7 +707,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_hi :
- forall (A: Set) (m: t A) (i : positive) (v: A),
+ forall (A: Type) (m: t A) (i : positive) (v: A),
~In (xH, v) (xelements m (xI i)).
Proof.
induction m; intros.
@@ -722,7 +722,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_ho :
- forall (A: Set) (m: t A) (i : positive) (v: A),
+ forall (A: Type) (m: t A) (i : positive) (v: A),
~In (xH, v) (xelements m (xO i)).
Proof.
induction m; intros.
@@ -737,13 +737,13 @@ Module PTree <: TREE.
Qed.
Lemma get_xget_h :
- forall (A: Set) (m: t A) (i: positive), get i m = xget i xH m.
+ forall (A: Type) (m: t A) (i: positive), get i m = xget i xH m.
Proof.
destruct i; simpl; auto.
Qed.
Lemma xelements_complete:
- forall (A: Set) (i j : positive) (m: t A) (v: A),
+ forall (A: Type) (i j : positive) (m: t A) (v: A),
In (i, v) (xelements m j) -> xget i j m = Some v.
Proof.
induction i; simpl; intros; destruct j; simpl.
@@ -771,7 +771,7 @@ Module PTree <: TREE.
Qed.
Theorem elements_complete:
- forall (A: Set) (m: t A) (i: positive) (v: A),
+ forall (A: Type) (m: t A) (i: positive) (v: A),
In (i, v) (elements m) -> get i m = Some v.
Proof.
intros A m i v H.
@@ -781,7 +781,7 @@ Module PTree <: TREE.
Qed.
Lemma in_xelements:
- forall (A: Set) (m: t A) (i k: positive) (v: A),
+ forall (A: Type) (m: t A) (i k: positive) (v: A),
In (k, v) (xelements m i) ->
exists j, k = append i j.
Proof.
@@ -802,11 +802,11 @@ Module PTree <: TREE.
rewrite <- append_assoc_1. exists (xI k1); auto.
Qed.
- Definition xkeys (A: Set) (m: t A) (i: positive) :=
+ Definition xkeys (A: Type) (m: t A) (i: positive) :=
List.map (@fst positive A) (xelements m i).
Lemma in_xkeys:
- forall (A: Set) (m: t A) (i k: positive),
+ forall (A: Type) (m: t A) (i k: positive),
In k (xkeys m i) ->
exists j, k = append i j.
Proof.
@@ -816,7 +816,7 @@ Module PTree <: TREE.
Qed.
Remark list_append_cons_norepet:
- forall (A: Set) (l1 l2: list A) (x: A),
+ forall (A: Type) (l1 l2: list A) (x: A),
list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
~In x l1 -> ~In x l2 ->
list_norepet (l1 ++ x :: l2).
@@ -837,7 +837,7 @@ Module PTree <: TREE.
Qed.
Lemma xelements_keys_norepet:
- forall (A: Set) (m: t A) (i: positive),
+ forall (A: Type) (m: t A) (i: positive),
list_norepet (xkeys m i).
Proof.
induction m; unfold xkeys; simpl; fold xkeys; intros.
@@ -871,17 +871,17 @@ Module PTree <: TREE.
Qed.
Theorem elements_keys_norepet:
- forall (A: Set) (m: t A),
+ forall (A: Type) (m: t A),
list_norepet (List.map (@fst elt A) (elements m)).
Proof.
intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet.
Qed.
- Definition fold (A B : Set) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
+ Definition fold (A B : Type) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.
Theorem fold_spec:
- forall (A B: Set) (f: B -> positive -> A -> B) (v: B) (m: t A),
+ forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A),
fold f m v =
List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
Proof.
@@ -896,49 +896,49 @@ Module PMap <: MAP.
Definition elt := positive.
Definition elt_eq := peq.
- Definition t (A : Set) : Set := (A * PTree.t A)%type.
+ Definition t (A : Type) : Type := (A * PTree.t A)%type.
- Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+ Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
forall (a b: t A), {a = b} + {a <> b}.
Proof.
intros.
- generalize (PTree.eq H). intros.
+ generalize (PTree.eq X). intros.
decide equality.
Qed.
- Definition init (A : Set) (x : A) :=
+ Definition init (A : Type) (x : A) :=
(x, PTree.empty A).
- Definition get (A : Set) (i : positive) (m : t A) :=
+ Definition get (A : Type) (i : positive) (m : t A) :=
match PTree.get i (snd m) with
| Some x => x
| None => fst m
end.
- Definition set (A : Set) (i : positive) (x : A) (m : t A) :=
+ Definition set (A : Type) (i : positive) (x : A) (m : t A) :=
(fst m, PTree.set i x (snd m)).
Theorem gi:
- forall (A: Set) (i: positive) (x: A), get i (init x) = x.
+ forall (A: Type) (i: positive) (x: A), get i (init x) = x.
Proof.
intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto.
Qed.
Theorem gss:
- forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = x.
+ forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = x.
Proof.
intros. unfold get. unfold set. simpl. rewrite PTree.gss. auto.
Qed.
Theorem gso:
- forall (A: Set) (i j: positive) (x: A) (m: t A),
+ forall (A: Type) (i j: positive) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Proof.
intros. unfold get. unfold set. simpl. rewrite PTree.gso; auto.
Qed.
Theorem gsspec:
- forall (A: Set) (i j: positive) (x: A) (m: t A),
+ forall (A: Type) (i j: positive) (x: A) (m: t A),
get i (set j x m) = if peq i j then x else get i m.
Proof.
intros. destruct (peq i j).
@@ -947,7 +947,7 @@ Module PMap <: MAP.
Qed.
Theorem gsident:
- forall (A: Set) (i j: positive) (m: t A),
+ forall (A: Type) (i j: positive) (m: t A),
get j (set i (get i m) m) = get j m.
Proof.
intros. destruct (peq i j).
@@ -955,11 +955,11 @@ Module PMap <: MAP.
rewrite gso; auto.
Qed.
- Definition map (A B : Set) (f : A -> B) (m : t A) : t B :=
+ Definition map (A B : Type) (f : A -> B) (m : t A) : t B :=
(f (fst m), PTree.map (fun _ => f) (snd m)).
Theorem gmap:
- forall (A B: Set) (f: A -> B) (i: positive) (m: t A),
+ forall (A B: Type) (f: A -> B) (i: positive) (m: t A),
get i (map f m) = f(get i m).
Proof.
intros. unfold map. unfold get. simpl. rewrite PTree.gmap.
@@ -971,7 +971,7 @@ End PMap.
(** * An implementation of maps over any type that injects into type [positive] *)
Module Type INDEXED_TYPE.
- Variable t: Set.
+ Variable t: Type.
Variable index: t -> positive.
Hypothesis index_inj: forall (x y: t), index x = index y -> x = y.
Variable eq: forall (x y: t), {x = y} + {x <> y}.
@@ -981,28 +981,28 @@ Module IMap(X: INDEXED_TYPE).
Definition elt := X.t.
Definition elt_eq := X.eq.
- Definition t : Set -> Set := PMap.t.
- Definition eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+ Definition t : Type -> Type := PMap.t.
+ Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
forall (a b: t A), {a = b} + {a <> b} := PMap.eq.
- Definition init (A: Set) (x: A) := PMap.init x.
- Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m.
- Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
- Definition map (A B: Set) (f: A -> B) (m: t A) : t B := PMap.map f m.
+ Definition init (A: Type) (x: A) := PMap.init x.
+ Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m.
+ Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
+ Definition map (A B: Type) (f: A -> B) (m: t A) : t B := PMap.map f m.
Lemma gi:
- forall (A: Set) (x: A) (i: X.t), get i (init x) = x.
+ forall (A: Type) (x: A) (i: X.t), get i (init x) = x.
Proof.
intros. unfold get, init. apply PMap.gi.
Qed.
Lemma gss:
- forall (A: Set) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.
+ forall (A: Type) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.
Proof.
intros. unfold get, set. apply PMap.gss.
Qed.
Lemma gso:
- forall (A: Set) (i j: X.t) (x: A) (m: t A),
+ forall (A: Type) (i j: X.t) (x: A) (m: t A),
i <> j -> get i (set j x m) = get i m.
Proof.
intros. unfold get, set. apply PMap.gso.
@@ -1010,7 +1010,7 @@ Module IMap(X: INDEXED_TYPE).
Qed.
Lemma gsspec:
- forall (A: Set) (i j: X.t) (x: A) (m: t A),
+ forall (A: Type) (i j: X.t) (x: A) (m: t A),
get i (set j x m) = if X.eq i j then x else get i m.
Proof.
intros. unfold get, set.
@@ -1022,7 +1022,7 @@ Module IMap(X: INDEXED_TYPE).
Qed.
Lemma gmap:
- forall (A B: Set) (f: A -> B) (i: X.t) (m: t A),
+ forall (A B: Type) (f: A -> B) (i: X.t) (m: t A),
get i (map f m) = f(get i m).
Proof.
intros. unfold map, get. apply PMap.gmap.
@@ -1074,7 +1074,7 @@ Module NMap := IMap(NIndexed).
(** * An implementation of maps over any type with decidable equality *)
Module Type EQUALITY_TYPE.
- Variable t: Set.
+ Variable t: Type.
Variable eq: forall (x y: t), {x = y} + {x <> y}.
End EQUALITY_TYPE.
@@ -1082,45 +1082,45 @@ Module EMap(X: EQUALITY_TYPE) <: MAP.
Definition elt := X.t.
Definition elt_eq := X.eq.
- Definition t (A: Set) := X.t -> A.
- Definition init (A: Set) (v: A) := fun (_: X.t) => v.
- Definition get (A: Set) (x: X.t) (m: t A) := m x.
- Definition set (A: Set) (x: X.t) (v: A) (m: t A) :=
+ Definition t (A: Type) := X.t -> A.
+ Definition init (A: Type) (v: A) := fun (_: X.t) => v.
+ Definition get (A: Type) (x: X.t) (m: t A) := m x.
+ Definition set (A: Type) (x: X.t) (v: A) (m: t A) :=
fun (y: X.t) => if X.eq y x then v else m y.
Lemma gi:
- forall (A: Set) (i: elt) (x: A), init x i = x.
+ forall (A: Type) (i: elt) (x: A), init x i = x.
Proof.
intros. reflexivity.
Qed.
Lemma gss:
- forall (A: Set) (i: elt) (x: A) (m: t A), (set i x m) i = x.
+ forall (A: Type) (i: elt) (x: A) (m: t A), (set i x m) i = x.
Proof.
intros. unfold set. case (X.eq i i); intro.
reflexivity. tauto.
Qed.
Lemma gso:
- forall (A: Set) (i j: elt) (x: A) (m: t A),
+ forall (A: Type) (i j: elt) (x: A) (m: t A),
i <> j -> (set j x m) i = m i.
Proof.
intros. unfold set. case (X.eq i j); intro.
congruence. reflexivity.
Qed.
Lemma gsspec:
- forall (A: Set) (i j: elt) (x: A) (m: t A),
+ forall (A: Type) (i j: elt) (x: A) (m: t A),
get i (set j x m) = if elt_eq i j then x else get i m.
Proof.
intros. unfold get, set, elt_eq. reflexivity.
Qed.
Lemma gsident:
- forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+ forall (A: Type) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
Proof.
intros. unfold get, set. case (X.eq j i); intro.
congruence. reflexivity.
Qed.
- Definition map (A B: Set) (f: A -> B) (m: t A) :=
+ Definition map (A B: Type) (f: A -> B) (m: t A) :=
fun (x: X.t) => f(m x).
Lemma gmap:
- forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
+ forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
get i (map f m) = f(get i m).
Proof.
intros. unfold get, map. reflexivity.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index 4b1f4e0fe..eddc37213 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -45,6 +45,8 @@ Proof.
assert (Zpos x <> Zpos y). congruence. omega.
Qed.
+Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
+
End OrderedPositive.
(** Indexed types (those that inject into [positive]) are ordered. *)
@@ -81,6 +83,13 @@ Proof.
apply GT. exact l.
Qed.
+Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+Proof.
+ intros. case (peq (A.index x) (A.index y)); intros.
+ left. apply A.index_inj; auto.
+ right; red; unfold eq; intros; subst. congruence.
+Qed.
+
End OrderedIndexed.
(** The product of two ordered types is ordered. *)
@@ -164,5 +173,15 @@ Proof.
apply GT. red. left. auto.
Qed.
+Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+Proof.
+ unfold eq; intros.
+ case (A.eq_dec (fst x) (fst y)); intros.
+ case (B.eq_dec (snd x) (snd y)); intros.
+ left; auto.
+ right; intuition.
+ right; intuition.
+Qed.
+
End OrderedPair.
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 2c7b82a7b..edb267e46 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -63,7 +63,7 @@ Section PARMOV.
(** The development is parameterized by the type of registers,
equipped with a decidable equality. *)
-Variable reg: Set.
+Variable reg: Type.
Variable reg_eq : forall (r1 r2: reg), {r1=r2} + {r1<>r2}.
(** The [temp] function maps every register [r] to the register that
@@ -93,7 +93,7 @@ Definition dests (m: moves) := List.map (@snd reg reg) m.
(** The dynamic semantics of moves is given in terms of environments.
An environment is a mapping of registers to their current values. *)
-Variable val: Set.
+Variable val: Type.
Definition env := reg -> val.
Lemma env_ext:
@@ -186,7 +186,7 @@ Fixpoint exec_seq_rev (m: moves) (e: env) {struct m}: env :=
as an inductive predicate [transition] relating triples of moves,
and its reflexive transitive closure [transitions]. *)
-Inductive state: Set :=
+Inductive state: Type :=
State (mu: moves) (sigma: moves) (tau: moves) : state.
Definition no_read (mu: moves) (d: reg) : Prop :=
@@ -1331,7 +1331,7 @@ Qed.
Section REGISTER_CLASSES.
-Variable class: Set.
+Variable class: Type.
Variable regclass: reg -> class.
Hypothesis temp_preserves_class: forall r, regclass (temp r) = regclass r.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 63f0232ae..91de0b1eb 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -30,7 +30,7 @@ Require Conventions.
(** Integer registers, floating-point registers. *)
-Inductive ireg: Set :=
+Inductive ireg: Type :=
| GPR0: ireg | GPR1: ireg | GPR2: ireg | GPR3: ireg
| GPR4: ireg | GPR5: ireg | GPR6: ireg | GPR7: ireg
| GPR8: ireg | GPR9: ireg | GPR10: ireg | GPR11: ireg
@@ -40,7 +40,7 @@ Inductive ireg: Set :=
| GPR24: ireg | GPR25: ireg | GPR26: ireg | GPR27: ireg
| GPR28: ireg | GPR29: ireg | GPR30: ireg | GPR31: ireg.
-Inductive freg: Set :=
+Inductive freg: Type :=
| FPR0: freg | FPR1: freg | FPR2: freg | FPR3: freg
| FPR4: freg | FPR5: freg | FPR6: freg | FPR7: freg
| FPR8: freg | FPR9: freg | FPR10: freg | FPR11: freg
@@ -63,7 +63,7 @@ Proof. decide equality. Defined.
resolved later by the linker.
*)
-Inductive constant: Set :=
+Inductive constant: Type :=
| Cint: int -> constant
| Csymbol_low: ident -> int -> constant
| Csymbol_high: ident -> int -> constant.
@@ -80,7 +80,7 @@ Inductive constant: Set :=
(** Bits in the condition register. We are only interested in the
first 4 bits. *)
-Inductive crbit: Set :=
+Inductive crbit: Type :=
| CRbit_0: crbit
| CRbit_1: crbit
| CRbit_2: crbit
@@ -95,7 +95,7 @@ Inductive crbit: Set :=
Definition label := positive.
-Inductive instruction : Set :=
+Inductive instruction : Type :=
| Padd: ireg -> ireg -> ireg -> instruction (**r integer addition *)
| Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *)
| Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *)
@@ -303,7 +303,7 @@ Definition program := AST.program fundef unit.
(** The PowerPC has a great many registers, some general-purpose, some very
specific. We model only the following registers: *)
-Inductive preg: Set :=
+Inductive preg: Type :=
| IR: ireg -> preg (**r integer registers *)
| FR: freg -> preg (**r float registers *)
| PC: preg (**r program counter *)
@@ -441,7 +441,7 @@ Definition const_high (c: constant) :=
set and memory state after execution of the instruction at [rs#PC],
or [Error] if the processor is stuck. *)
-Inductive outcome: Set :=
+Inductive outcome: Type :=
| OK: regset -> mem -> outcome
| Error: outcome.
@@ -819,7 +819,7 @@ Definition loc_external_result (sg: signature) : preg :=
(** Execution of the instruction at [rs#PC]. *)
-Inductive state: Set :=
+Inductive state: Type :=
| State: regset -> mem -> state.
Inductive step: state -> trace -> state -> Prop :=
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 0c3ac75dc..5c37a570c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -225,7 +225,7 @@ Definition crbit_for_cond (cond: condition) :=
(** Recognition of comparisons [>= 0] and [< 0]. *)
-Inductive condition_class: condition -> list mreg -> Set :=
+Inductive condition_class: condition -> list mreg -> Type :=
| condition_ge0:
forall n r, n = Int.zero -> condition_class (Ccompimm Cge n) (r :: nil)
| condition_lt0:
diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v
index 6ec27a3f1..76ea153c3 100644
--- a/powerpc/Constprop.v
+++ b/powerpc/Constprop.v
@@ -32,7 +32,7 @@ Require Import Kildall.
(** To each pseudo-register at each program point, the static analysis
associates a compile-time approximation taken from the following set. *)
-Inductive approx : Set :=
+Inductive approx : Type :=
| Novalue: approx (** No value possible, code is unreachable. *)
| Unknown: approx (** All values are possible,
no compile-time information is available. *)
@@ -139,7 +139,7 @@ Definition eval_static_condition (cond: condition) (vl: list approx) :=
end.
*)
-Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Set :=
+Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type :=
| eval_static_condition_case1:
forall c n1 n2,
eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil)
@@ -271,7 +271,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
end.
*)
-Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Set :=
+Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type :=
| eval_static_operation_case1:
forall v1,
eval_static_operation_cases (Omove) (v1::nil)
@@ -696,7 +696,7 @@ Variable approx: D.t.
Definition intval (r: reg) : option int :=
match D.get r approx with I n => Some n | _ => None end.
-Inductive cond_strength_reduction_cases: condition -> list reg -> Set :=
+Inductive cond_strength_reduction_cases: condition -> list reg -> Type :=
| csr_case1:
forall c r1 r2,
cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil)
@@ -789,7 +789,7 @@ Definition make_xorimm (n: int) (r: reg) :=
then (Omove, r :: nil)
else (Oxorimm n, r :: nil).
-Inductive op_strength_reduction_cases: operation -> list reg -> Set :=
+Inductive op_strength_reduction_cases: operation -> list reg -> Type :=
| op_strength_reduction_case1:
forall (r1: reg) (r2: reg),
op_strength_reduction_cases Oadd (r1 :: r2 :: nil)
@@ -949,7 +949,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) :=
(op, args)
end.
-Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Set :=
+Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Type :=
| addr_strength_reduction_case1:
forall (r1: reg) (r2: reg),
addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil)
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index d0f7cf464..88b70c1d6 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -29,7 +29,7 @@ Require Import AST.
The type [mreg] does not include special-purpose or reserved
machine registers such as the stack pointer and the condition codes. *)
-Inductive mreg: Set :=
+Inductive mreg: Type :=
(** Allocatable integer regs *)
| R3: mreg | R4: mreg | R5: mreg | R6: mreg
| R7: mreg | R8: mreg | R9: mreg | R10: mreg
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 300a80438..27e12c2c7 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -36,7 +36,7 @@ Set Implicit Arguments.
(** Conditions (boolean-valued operators). *)
-Inductive condition : Set :=
+Inductive condition : Type :=
| Ccomp: comparison -> condition (**r signed integer comparison *)
| Ccompu: comparison -> condition (**r unsigned integer comparison *)
| Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *)
@@ -49,7 +49,7 @@ Inductive condition : Set :=
(** Arithmetic and logical operations. In the descriptions, [rd] is the
result of the operation and [r1], [r2], etc, are the arguments. *)
-Inductive operation : Set :=
+Inductive operation : Type :=
| Omove: operation (**r [rd = r1] *)
| Ointconst: int -> operation (**r [rd] is set to the given integer constant *)
| Ofloatconst: float -> operation (**r [rd] is set to the given float constant *)
@@ -104,7 +104,7 @@ Inductive operation : Set :=
(** Addressing modes. [r1], [r2], etc, are the arguments to the
addressing. *)
-Inductive addressing: Set :=
+Inductive addressing: Type :=
| Aindexed: int -> addressing (**r Address is [r1 + offset] *)
| Aindexed2: addressing (**r Address is [r1 + r2] *)
| Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *)
@@ -182,7 +182,7 @@ Definition offset_sp (sp: val) (delta: int) : option val :=
end.
Definition eval_operation
- (F: Set) (genv: Genv.t F) (sp: val)
+ (F: Type) (genv: Genv.t F) (sp: val)
(op: operation) (vl: list val): option val :=
match op, vl with
| Omove, v1::nil => Some v1
@@ -265,7 +265,7 @@ Definition eval_operation
end.
Definition eval_addressing
- (F: Set) (genv: Genv.t F) (sp: val)
+ (F: Type) (genv: Genv.t F) (sp: val)
(addr: addressing) (vl: list val) : option val :=
match addr, vl with
| Aindexed n, Vptr b1 n1 :: nil =>
@@ -360,7 +360,7 @@ Qed.
Section GENV_TRANSF.
-Variable F1 F2: Set.
+Variable F1 F2: Type.
Variable ge1: Genv.t F1.
Variable ge2: Genv.t F2.
Hypothesis agree_on_symbols:
@@ -389,14 +389,14 @@ End GENV_TRANSF.
(** Recognition of move operations. *)
Definition is_move_operation
- (A: Set) (op: operation) (args: list A) : option A :=
+ (A: Type) (op: operation) (args: list A) : option A :=
match op, args with
| Omove, arg :: nil => Some arg
| _, _ => None
end.
Lemma is_move_operation_correct:
- forall (A: Set) (op: operation) (args: list A) (a: A),
+ forall (A: Type) (op: operation) (args: list A) (a: A),
is_move_operation op args = Some a ->
op = Omove /\ args = a :: nil.
Proof.
@@ -497,7 +497,7 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
Section SOUNDNESS.
-Variable A: Set.
+Variable A: Type.
Variable genv: Genv.t A.
Lemma type_of_operation_sound:
@@ -560,7 +560,7 @@ End SOUNDNESS.
Section EVAL_OP_TOTAL.
-Variable F: Set.
+Variable F: Type.
Variable genv: Genv.t F.
Definition find_symbol_offset (id: ident) (ofs: int) : val :=
@@ -746,7 +746,7 @@ End EVAL_OP_TOTAL.
Section EVAL_LESSDEF.
-Variable F: Set.
+Variable F: Type.
Variable genv: Genv.t F.
Ltac InvLessdef :=
@@ -834,7 +834,7 @@ End EVAL_LESSDEF.
Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
Lemma eval_op_for_binary_addressing:
- forall (F: Set) (ge: Genv.t F) sp addr args v,
+ forall (F: Type) (ge: Genv.t F) sp addr args v,
(length args >= 2)%nat ->
eval_addressing ge sp addr args = Some v ->
eval_operation ge sp (op_for_binary_addressing addr) args = Some v.
diff --git a/powerpc/Selection.v b/powerpc/Selection.v
index 46d803907..286517ef0 100644
--- a/powerpc/Selection.v
+++ b/powerpc/Selection.v
@@ -118,7 +118,7 @@ Definition notint (e: expr) :=
characterizes the expressions that match each of the 4 cases of interest.
*)
-Inductive notint_cases: forall (e: expr), Set :=
+Inductive notint_cases: forall (e: expr), Type :=
| notint_case1:
forall (t1: expr) (t2: expr),
notint_cases (Eop Oand (t1:::t2:::Enil))
@@ -208,7 +208,7 @@ Definition addimm (n: int) (e: expr) :=
(** Addition of an integer constant. *)
-Inductive addimm_cases: forall (e: expr), Set :=
+Inductive addimm_cases: forall (e: expr), Type :=
| addimm_case1:
forall (m: int),
addimm_cases (Eop (Ointconst m) Enil)
@@ -268,7 +268,7 @@ Definition add (e1: expr) (e2: expr) :=
end.
*)
-Inductive add_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
| add_case1:
forall (n1: int) (t2: expr),
add_cases (Eop (Ointconst n1) Enil) (t2)
@@ -342,7 +342,7 @@ l))
end.
*)
-Inductive sub_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
| sub_case1:
forall (t1: expr) (n2: int),
sub_cases (t1) (Eop (Ointconst n2) Enil)
@@ -410,7 +410,7 @@ Definition rolm (e1: expr) :=
end
*)
-Inductive rolm_cases: forall (e1: expr), Set :=
+Inductive rolm_cases: forall (e1: expr), Type :=
| rolm_case1:
forall (n1: int),
rolm_cases (Eop (Ointconst n1) Enil)
@@ -488,7 +488,7 @@ Definition mulimm (n1: int) (e2: expr) :=
end.
*)
-Inductive mulimm_cases: forall (e2: expr), Set :=
+Inductive mulimm_cases: forall (e2: expr), Type :=
| mulimm_case1:
forall (n2: int),
mulimm_cases (Eop (Ointconst n2) Enil)
@@ -532,7 +532,7 @@ Definition mul (e1: expr) (e2: expr) :=
end.
*)
-Inductive mul_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive mul_cases: forall (e1: expr) (e2: expr), Type :=
| mul_case1:
forall (n1: int) (t2: expr),
mul_cases (Eop (Ointconst n1) Enil) (t2)
@@ -584,7 +584,7 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
Definition mods := mod_aux Odiv.
-Inductive divu_cases: forall (e2: expr), Set :=
+Inductive divu_cases: forall (e2: expr), Type :=
| divu_case1:
forall (n2: int),
divu_cases (Eop (Ointconst n2) Enil)
@@ -645,7 +645,7 @@ Definition same_expr_pure (e1 e2: expr) :=
| _, _ => false
end.
-Inductive or_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
| or_case1:
forall (amount1: int) (mask1: int) (t1: expr)
(amount2: int) (mask2: int) (t2: expr),
@@ -678,7 +678,7 @@ Definition or (e1: expr) (e2: expr) :=
(** ** General shifts *)
-Inductive shift_cases: forall (e1: expr), Set :=
+Inductive shift_cases: forall (e1: expr), Type :=
| shift_case1:
forall (n2: int),
shift_cases (Eop (Ointconst n2) Enil)
@@ -723,7 +723,7 @@ Definition addf (e1: expr) (e2: expr) :=
end.
*)
-Inductive addf_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive addf_cases: forall (e1: expr) (e2: expr), Type :=
| addf_case1:
forall (t1: expr) (t2: expr) (t3: expr),
addf_cases (Eop Omulf (t1:::t2:::Enil)) (t3)
@@ -770,7 +770,7 @@ Definition subf (e1: expr) (e2: expr) :=
end.
*)
-Inductive subf_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive subf_cases: forall (e1: expr) (e2: expr), Type :=
| subf_case1:
forall (t1: expr) (t2: expr) (t3: expr),
subf_cases (Eop Omulf (t1:::t2:::Enil)) (t3)
@@ -798,7 +798,7 @@ Definition subf (e1: expr) (e2: expr) :=
(** ** Truncations and sign extensions *)
-Inductive cast8signed_cases: forall (e1: expr), Set :=
+Inductive cast8signed_cases: forall (e1: expr), Type :=
| cast8signed_case1:
forall (e2: expr),
cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
@@ -826,7 +826,7 @@ Definition cast8signed (e: expr) :=
| cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil)
end.
-Inductive cast8unsigned_cases: forall (e1: expr), Set :=
+Inductive cast8unsigned_cases: forall (e1: expr), Type :=
| cast8unsigned_case1:
forall (e2: expr),
cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil))
@@ -854,7 +854,7 @@ Definition cast8unsigned (e: expr) :=
| cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil)
end.
-Inductive cast16signed_cases: forall (e1: expr), Set :=
+Inductive cast16signed_cases: forall (e1: expr), Type :=
| cast16signed_case1:
forall (e2: expr),
cast16signed_cases (Eop Ocast16signed (e2 ::: Enil))
@@ -882,7 +882,7 @@ Definition cast16signed (e: expr) :=
| cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil)
end.
-Inductive cast16unsigned_cases: forall (e1: expr), Set :=
+Inductive cast16unsigned_cases: forall (e1: expr), Type :=
| cast16unsigned_case1:
forall (e2: expr),
cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil))
@@ -910,7 +910,7 @@ Definition cast16unsigned (e: expr) :=
| cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil)
end.
-Inductive singleoffloat_cases: forall (e1: expr), Set :=
+Inductive singleoffloat_cases: forall (e1: expr), Type :=
| singleoffloat_case1:
forall (e2: expr),
singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil))
@@ -940,7 +940,7 @@ Definition singleoffloat (e: expr) :=
(** ** Comparisons *)
-Inductive comp_cases: forall (e1: expr) (e2: expr), Set :=
+Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
| comp_case1:
forall n1 t2,
comp_cases (Eop (Ointconst n1) Enil) (t2)
@@ -1043,7 +1043,7 @@ Definition addressing (e: expr) :=
end.
*)
-Inductive addressing_cases: forall (e: expr), Set :=
+Inductive addressing_cases: forall (e: expr), Type :=
| addressing_case1:
forall (s: ident) (n: int),
addressing_cases (Eop (Oaddrsymbol s n) Enil)
diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v
index 6ffffc18a..8a02c9975 100644
--- a/powerpc/Selectionproof.v
+++ b/powerpc/Selectionproof.v
@@ -1357,10 +1357,12 @@ Proof.
econstructor. destruct k; simpl in H; simpl; auto.
rewrite <- H0; reflexivity.
constructor; auto.
+(*
(* assign *)
exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split.
constructor. auto with evalexpr.
constructor; auto.
+*)
(* store *)
econstructor; split.
eapply eval_store; eauto with evalexpr.
diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v
index 48e26a760..0de1ccd64 100644
--- a/powerpc/eabi/Stacklayout.v
+++ b/powerpc/eabi/Stacklayout.v
@@ -45,7 +45,7 @@ the boundaries between areas in the frame part.
Definition fe_ofs_arg := 8.
-Record frame_env : Set := mk_frame_env {
+Record frame_env : Type := mk_frame_env {
fe_size: Z;
fe_ofs_link: Z;
fe_ofs_retaddr: Z;
diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v
index 0e9be2240..c57f3f920 100644
--- a/powerpc/macosx/Stacklayout.v
+++ b/powerpc/macosx/Stacklayout.v
@@ -42,7 +42,7 @@ the boundaries between areas in the frame part.
Definition fe_ofs_arg := 24.
-Record frame_env : Set := mk_frame_env {
+Record frame_env : Type := mk_frame_env {
fe_size: Z;
fe_ofs_link: Z;
fe_ofs_retaddr: Z;
--
GitLab