diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
| commit | 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 (patch) | |
| tree | ec5f45b6546e19519f59b1ee0f42955616ca1b98 | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
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
71 files changed, 795 insertions, 852 deletions
@@ -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 ======================= @@ -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 b51d974..5bd84b6 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 3466c0b..2e422d2 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 @@ -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 d04a4ca..12cc1b2 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 10f93f3..967e229 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 dd3c6a1..b374bfd 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 3971fb6..e2387b5 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 d1ed28d..8c5f536 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 13e9be8..cad3503 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 35bf391..b48db2d 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 bfe92a4..1e798b5 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 7204bc7..67824ae 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 c86652a..92ac067 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 433c074..8a9dda6 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 b4445ae..188a23f 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 0db5495..3a61e6d 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 4c87c0d..10b7d83 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 34d6e5c..e025407 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 b385429..c24d370 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 ca2f527..295df28 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 3f25137..0bb2442 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 25819f7..aa17cd4 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 4417cc6..876f558 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 5fad2f2..344d271 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 709dc78..65e873e 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 e6adeb0..8e61271 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 c3d04d6..fceb7c2 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 158af8f..182c322 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 a7560d0..d5819f7 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 b88dd50..1bafc35 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 8e97e1a..791db37 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 49bf894..08f5f6c 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 cc5e5ab..1045d1a 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 5615eab..f256bb2 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 14b8053..248192c 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 1aa536a..942cfd7 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 2c010cb..bd9cf22 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 75dbc14..af6dc90 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 ac79047..b332e21 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 ec8053d..a8655c2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -36,7 +36,7 @@ Definition ident_eq := peq. [Tint] for integers and pointers, and [Tfloat] for floating-point numbers. *) -Inductive typ : Set := +Inductive typ : Type := | Tint : typ | Tfloat : typ. @@ -58,7 +58,7 @@ Proof. decide equality. apply typ_eq. Qed. are used in particular to determine appropriate calling conventions for the function. *) -Record signature : Set := mksignature { +Record signature : Type := mksignature { sig_args: list typ; sig_res: option typ }. @@ -73,7 +73,7 @@ Definition proj_sig_res (s: signature) : typ := a ``memory chunk'' indicating the type, size and signedness of the chunk of memory being accessed. *) -Inductive memory_chunk : Set := +Inductive memory_chunk : Type := | Mint8signed : memory_chunk (**r 8-bit signed integer *) | Mint8unsigned : memory_chunk (**r 8-bit unsigned integer *) | Mint16signed : memory_chunk (**r 16-bit signed integer *) @@ -84,7 +84,7 @@ Inductive memory_chunk : Set := (** Initialization data for global variables. *) -Inductive init_data: Set := +Inductive init_data: Type := | Init_int8: int -> init_data | Init_int16: int -> init_data | Init_int32: int -> init_data @@ -104,16 +104,16 @@ for variables vary among the various intermediate languages and are taken as parameters to the [program] type. The other parts of whole programs are common to all languages. *) -Record program (F V: Set) : Set := mkprogram { +Record program (F V: Type) : Type := mkprogram { prog_funct: list (ident * F); prog_main: ident; prog_vars: list (ident * list init_data * V) }. -Definition prog_funct_names (F V: Set) (p: program F V) : list ident := +Definition prog_funct_names (F V: Type) (p: program F V) : list ident := map (@fst ident F) p.(prog_funct). -Definition prog_var_names (F V: Set) (p: program F V) : list ident := +Definition prog_var_names (F V: Type) (p: program F V) : list ident := map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars). (** * Generic transformations over programs *) @@ -124,7 +124,7 @@ Definition prog_var_names (F V: Set) (p: program F V) : list ident := Section TRANSF_PROGRAM. -Variable A B V: Set. +Variable A B V: Type. Variable transf: A -> B. Definition transf_program (l: list (ident * A)) : list (ident * B) := @@ -158,7 +158,7 @@ Open Local Scope string_scope. Section MAP_PARTIAL. -Variable A B C: Set. +Variable A B C: Type. Variable prefix_errmsg: A -> errmsg. Variable f: B -> res C. @@ -207,7 +207,7 @@ Qed. End MAP_PARTIAL. Remark map_partial_total: - forall (A B C: Set) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), + forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)), map_partial prefix (fun b => OK (f b)) l = OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l). Proof. @@ -217,7 +217,7 @@ Proof. Qed. Remark map_partial_identity: - forall (A B: Set) (prefix: A -> errmsg) (l: list (A * B)), + forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)), map_partial prefix (fun b => OK b) l = OK l. Proof. induction l; simpl. @@ -227,7 +227,7 @@ Qed. Section TRANSF_PARTIAL_PROGRAM. -Variable A B V: Set. +Variable A B V: Type. Variable transf_partial: A -> res B. Definition prefix_funct_name (id: ident) : errmsg := @@ -271,7 +271,7 @@ End TRANSF_PARTIAL_PROGRAM. Section TRANSF_PARTIAL_PROGRAM2. -Variable A B V W: Set. +Variable A B V W: Type. Variable transf_partial_function: A -> res B. Variable transf_partial_variable: V -> res W. @@ -322,7 +322,7 @@ End TRANSF_PARTIAL_PROGRAM2. Section MATCH_PROGRAM. -Variable A B V W: Set. +Variable A B V W: Type. Variable match_fundef: A -> B -> Prop. Variable match_varinfo: V -> W -> Prop. @@ -344,7 +344,7 @@ Definition match_program (p1: program A V) (p2: program B W) : Prop := End MATCH_PROGRAM. Remark transform_partial_program2_match: - forall (A B V W: Set) + forall (A B V W: Type) (transf_partial_function: A -> res B) (transf_partial_variable: V -> res W) (p: program A V) (tp: program B W), @@ -375,12 +375,12 @@ Qed. (a.k.a. system calls) that emit an event when applied. We define a type for such functions and some generic transformation functions. *) -Record external_function : Set := mkextfun { +Record external_function : Type := mkextfun { ef_id: ident; ef_sig: signature }. -Inductive fundef (F: Set): Set := +Inductive fundef (F: Type): Type := | Internal: F -> fundef F | External: external_function -> fundef F. @@ -388,7 +388,7 @@ Implicit Arguments External [F]. Section TRANSF_FUNDEF. -Variable A B: Set. +Variable A B: Type. Variable transf: A -> B. Definition transf_fundef (fd: fundef A): fundef B := @@ -401,7 +401,7 @@ End TRANSF_FUNDEF. Section TRANSF_PARTIAL_FUNDEF. -Variable A B: Set. +Variable A B: Type. Variable transf_partial: A -> res B. Definition transf_partial_fundef (fd: fundef A): res (fundef B) := diff --git a/common/Errors.v b/common/Errors.v index 2c9bbc3..2165db3 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -28,11 +28,11 @@ Set Implicit Arguments. as a list of either substrings or positive numbers encoding a source-level identifier (see module AST). *) -Inductive errcode: Set := +Inductive errcode: Type := | MSG: string -> errcode | CTX: positive -> errcode. -Definition errmsg: Set := list errcode. +Definition errmsg: Type := list errcode. Definition msg (s: string) : errmsg := MSG s :: nil. @@ -42,7 +42,7 @@ Definition msg (s: string) : errmsg := MSG s :: nil. The return value is either [OK res] to indicate success, or [Error msg] to indicate failure. *) -Inductive res (A: Set) : Set := +Inductive res (A: Type) : Type := | OK: A -> res A | Error: errmsg -> res A. @@ -51,13 +51,13 @@ Implicit Arguments Error [A]. (** To automate the propagation of errors, we use a monadic style with the following [bind] operation. *) -Definition bind (A B: Set) (f: res A) (g: A -> res B) : res B := +Definition bind (A B: Type) (f: res A) (g: A -> res B) : res B := match f with | OK x => g x | Error msg => Error msg end. -Definition bind2 (A B C: Set) (f: res (A * B)) (g: A -> B -> res C) : res C := +Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C := match f with | OK (x, y) => g x y | Error msg => Error msg @@ -74,7 +74,7 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) : error_monad_scope. Remark bind_inversion: - forall (A B: Set) (f: res A) (g: A -> res B) (y: B), + forall (A B: Type) (f: res A) (g: A -> res B) (y: B), bind f g = OK y -> exists x, f = OK x /\ g x = OK y. Proof. @@ -84,7 +84,7 @@ Proof. Qed. Remark bind2_inversion: - forall (A B C: Set) (f: res (A*B)) (g: A -> B -> res C) (z: C), + forall (A B C: Type) (f: res (A*B)) (g: A -> B -> res C) (z: C), bind2 f g = OK z -> exists x, exists y, f = OK (x, y) /\ g x y = OK z. Proof. @@ -97,14 +97,14 @@ Open Local Scope error_monad_scope. (** This is the familiar monadic map iterator. *) -Fixpoint mmap (A B: Set) (f: A -> res B) (l: list A) {struct l} : res (list B) := +Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) := match l with | nil => OK nil | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl') end. Remark mmap_inversion: - forall (A B: Set) (f: A -> res B) (l: list A) (l': list B), + forall (A B: Type) (f: A -> res B) (l: list A) (l': list B), mmap f l = OK l' -> list_forall2 (fun x y => f x = OK y) l l'. Proof. diff --git a/common/Events.v b/common/Events.v index c44da01..011c454 100644 --- a/common/Events.v +++ b/common/Events.v @@ -32,11 +32,11 @@ Require Import Values. allow pointers to be exchanged between the program and the outside world. *) -Inductive eventval: Set := +Inductive eventval: Type := | EVint: int -> eventval | EVfloat: float -> eventval. -Record event : Set := mkevent { +Record event : Type := mkevent { ev_name: ident; ev_args: list eventval; ev_res: eventval @@ -56,7 +56,7 @@ Definition Eextcall Definition Eapp (t1 t2: trace) : trace := t1 ++ t2. -CoInductive traceinf : Set := +CoInductive traceinf : Type := | Enilinf: traceinf | Econsinf: event -> traceinf -> traceinf. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index f720914..1ce7bf5 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -47,43 +47,43 @@ Module Type GENV. (** ** Types and operations *) - Variable t: Set -> Set. + Variable t: Type -> Type. (** The type of global environments. The parameter [F] is the type of function descriptions. *) - Variable globalenv: forall (F V: Set), program F V -> t F. + Variable globalenv: forall (F V: Type), program F V -> t F. (** Return the global environment for the given program. *) - Variable init_mem: forall (F V: Set), program F V -> mem. + Variable init_mem: forall (F V: Type), program F V -> mem. (** Return the initial memory state for the given program. *) - Variable find_funct_ptr: forall (F: Set), t F -> block -> option F. + Variable find_funct_ptr: forall (F: Type), t F -> block -> option F. (** Return the function description associated with the given address, if any. *) - Variable find_funct: forall (F: Set), t F -> val -> option F. + Variable find_funct: forall (F: Type), t F -> val -> option F. (** Same as [find_funct_ptr] but the function address is given as a value, which must be a pointer with offset 0. *) - Variable find_symbol: forall (F: Set), t F -> ident -> option block. + Variable find_symbol: forall (F: Type), t F -> ident -> option block. (** Return the address of the given global symbol, if any. *) (** ** Properties of the operations. *) Hypothesis find_funct_inv: - forall (F: Set) (ge: t F) (v: val) (f: F), + forall (F: Type) (ge: t F) (v: val) (f: F), find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. Hypothesis find_funct_find_funct_ptr: - forall (F: Set) (ge: t F) (b: block), + forall (F: Type) (ge: t F) (b: block), find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b. Hypothesis find_symbol_exists: - forall (F V: Set) (p: program F V) + forall (F V: Type) (p: program F V) (id: ident) (init: list init_data) (v: V), In (id, init, v) (prog_vars p) -> exists b, find_symbol (globalenv p) id = Some b. Hypothesis find_funct_ptr_exists: - forall (F V: Set) (p: program F V) (id: ident) (f: F), + forall (F V: Type) (p: program F V) (id: ident) (f: F), list_norepet (prog_funct_names p) -> list_disjoint (prog_funct_names p) (prog_var_names p) -> In (id, f) (prog_funct p) -> @@ -91,49 +91,49 @@ Module Type GENV. /\ find_funct_ptr (globalenv p) b = Some f. Hypothesis find_funct_ptr_inversion: - forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> exists id, In (id, f) (prog_funct p). Hypothesis find_funct_inversion: - forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F), find_funct (globalenv p) v = Some f -> exists id, In (id, f) (prog_funct p). Hypothesis find_funct_ptr_symbol_inversion: - forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F), + forall (F V: Type) (p: program F V) (id: ident) (b: block) (f: F), find_symbol (globalenv p) id = Some b -> find_funct_ptr (globalenv p) b = Some f -> In (id, f) p.(prog_funct). Hypothesis find_funct_ptr_prop: - forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (b: block) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct_ptr (globalenv p) b = Some f -> P f. Hypothesis find_funct_prop: - forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + forall (F V: Type) (P: F -> Prop) (p: program F V) (v: val) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct (globalenv p) v = Some f -> P f. Hypothesis initmem_nullptr: - forall (F V: Set) (p: program F V), + forall (F V: Type) (p: program F V), let m := init_mem p in valid_block m nullptr /\ m.(blocks) nullptr = empty_block 0 0. Hypothesis initmem_inject_neutral: - forall (F V: Set) (p: program F V), + forall (F V: Type) (p: program F V), mem_inject_neutral (init_mem p). Hypothesis find_funct_ptr_negative: - forall (F V: Set) (p: program F V) (b: block) (f: F), + forall (F V: Type) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> b < 0. Hypothesis find_symbol_not_fresh: - forall (F V: Set) (p: program F V) (id: ident) (b: block), + forall (F V: Type) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). Hypothesis find_symbol_not_nullptr: - forall (F V: Set) (p: program F V) (id: ident) (b: block), + forall (F V: Type) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b <> nullptr. Hypothesis global_addresses_distinct: - forall (F V: Set) (p: program F V) id1 id2 b1 b2, + forall (F V: Type) (p: program F V) id1 id2 b1 b2, id1<>id2 -> find_symbol (globalenv p) id1 = Some b1 -> find_symbol (globalenv p) id2 = Some b2 -> @@ -143,30 +143,30 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f). Hypothesis find_funct_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> find_funct (globalenv (transform_program transf p)) v = Some (transf f). Hypothesis find_symbol_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (s: ident), find_symbol (globalenv (transform_program transf p)) s = find_symbol (globalenv p) s. Hypothesis init_mem_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), init_mem (transform_program transf p) = init_mem p. Hypothesis find_funct_ptr_rev_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (b : block) (tf : B), find_funct_ptr (globalenv (transform_program transf p)) b = Some tf -> exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = tf. Hypothesis find_funct_rev_transf: - forall (A B V: Set) (transf: A -> B) (p: program A V), + forall (A B V: Type) (transf: A -> B) (p: program A V), forall (v : val) (tf : B), find_funct (globalenv (transform_program transf p)) v = Some tf -> exists f : A, find_funct (globalenv p) v = Some f /\ transf f = tf. @@ -175,37 +175,37 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (b: block) (f: A), find_funct_ptr (globalenv p) b = Some f -> exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf f = OK f'. Hypothesis find_funct_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (v: val) (f: A), find_funct (globalenv p) v = Some f -> exists f', find_funct (globalenv p') v = Some f' /\ transf f = OK f'. Hypothesis find_symbol_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> init_mem p' = init_mem p. Hypothesis find_funct_ptr_rev_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (b : block) (tf : B), find_funct_ptr (globalenv p') b = Some tf -> exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf f = OK tf. Hypothesis find_funct_rev_transf_partial: - forall (A B V: Set) (transf: A -> res B) (p: program A V) (p': program B V), + forall (A B V: Type) (transf: A -> res B) (p: program A V) (p': program B V), transform_partial_program transf p = OK p' -> forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> @@ -213,7 +213,7 @@ Module Type GENV. find_funct (globalenv p) v = Some f /\ transf f = OK tf. Hypothesis find_funct_ptr_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (b: block) (f: A), @@ -221,7 +221,7 @@ Module Type GENV. exists f', find_funct_ptr (globalenv p') b = Some f' /\ transf_fun f = OK f'. Hypothesis find_funct_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (v: val) (f: A), @@ -229,18 +229,18 @@ Module Type GENV. exists f', find_funct (globalenv p') v = Some f' /\ transf_fun f = OK f'. Hypothesis find_symbol_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (s: ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> init_mem p' = init_mem p. Hypothesis find_funct_ptr_rev_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (b : block) (tf : B), @@ -248,7 +248,7 @@ Module Type GENV. exists f : A, find_funct_ptr (globalenv p) b = Some f /\ transf_fun f = OK tf. Hypothesis find_funct_rev_transf_partial2: - forall (A B V W: Set) (transf_fun: A -> res B) (transf_var: V -> res W) + forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) (p: program A V) (p': program B W), transform_partial_program2 transf_fun transf_var p = OK p' -> forall (v : val) (tf : B), @@ -260,7 +260,7 @@ Module Type GENV. and operations over global environments. *) Hypothesis find_funct_ptr_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (b : block) (f : A), @@ -268,7 +268,7 @@ Module Type GENV. exists tf : B, find_funct_ptr (globalenv p') b = Some tf /\ match_fun f tf. Hypothesis find_funct_ptr_rev_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (b : block) (tf : B), @@ -276,27 +276,27 @@ Module Type GENV. exists f : A, find_funct_ptr (globalenv p) b = Some f /\ match_fun f tf. Hypothesis find_funct_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (v : val) (f : A), find_funct (globalenv p) v = Some f -> exists tf : B, find_funct (globalenv p') v = Some tf /\ match_fun f tf. Hypothesis find_funct_rev_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (v : val) (tf : B), find_funct (globalenv p') v = Some tf -> exists f : A, find_funct (globalenv p) v = Some f /\ match_fun f tf. Hypothesis find_symbol_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> forall (s : ident), find_symbol (globalenv p') s = find_symbol (globalenv p) s. Hypothesis init_mem_match: - forall (A B V W: Set) (match_fun: A -> B -> Prop) + forall (A B V W: Type) (match_fun: A -> B -> Prop) (match_var: V -> W -> Prop) (p: program A V) (p': program B W), match_program match_fun match_var p p' -> init_mem p' = init_mem p. @@ -310,10 +310,10 @@ Module Genv: GENV. Section GENV. -Variable F: Set. (* The type of functions *) -Variable V: Set. (* The type of information over variables *) +Variable F: Type. (* The type of functions *) +Variable V: Type. (* The type of information over variables *) -Record genv : Set := mkgenv { +Record genv : Type := mkgenv { functions: ZMap.t (option F); (* mapping function ptr -> function *) nextfunction: Z; symbols: PTree.t block (* mapping symbol -> block *) @@ -588,7 +588,7 @@ Proof. generalize (find_symbol_above_nextfunction _ _ X). unfold block; unfold ZIndexed.t; intro; omega. - intros. exploit H; eauto. assumption. intros [b [X Y]]. + intros. exploit H; eauto. intros [b [X Y]]. exists b; split. unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. @@ -770,7 +770,7 @@ End GENV. Section MATCH_PROGRAM. -Variable A B V W: Set. +Variable A B V W: Type. Variable match_fun: A -> B -> Prop. Variable match_var: V -> W -> Prop. Variable p: program A V. @@ -950,7 +950,7 @@ End MATCH_PROGRAM. Section TRANSF_PROGRAM_PARTIAL2. -Variable A B V W: Set. +Variable A B V W: Type. Variable transf_fun: A -> res B. Variable transf_var: V -> res W. Variable p: program A V. @@ -1024,7 +1024,7 @@ End TRANSF_PROGRAM_PARTIAL2. Section TRANSF_PROGRAM_PARTIAL. -Variable A B V: Set. +Variable A B V: Type. Variable transf: A -> res B. Variable p: program A V. Variable p': program B V. @@ -1089,7 +1089,7 @@ End TRANSF_PROGRAM_PARTIAL. Section TRANSF_PROGRAM. -Variable A B V: Set. +Variable A B V: Type. Variable transf: A -> B. Variable p: program A V. Let tp := transform_program transf p. diff --git a/common/Mem.v b/common/Mem.v index e169dfc..01c1975 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -31,20 +31,20 @@ Require Import Integers. Require Import Floats. Require Import Values. -Definition update (A: Set) (x: Z) (v: A) (f: Z -> A) : Z -> A := +Definition update (A: Type) (x: Z) (v: A) (f: Z -> A) : Z -> A := fun y => if zeq y x then v else f y. Implicit Arguments update [A]. Lemma update_s: - forall (A: Set) (x: Z) (v: A) (f: Z -> A), + forall (A: Type) (x: Z) (v: A) (f: Z -> A), update x v f x = v. Proof. intros; unfold update. apply zeq_true. Qed. Lemma update_o: - forall (A: Set) (x: Z) (v: A) (f: Z -> A) (y: Z), + forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z), x <> y -> update x v f y = f y. Proof. intros; unfold update. apply zeq_false; auto. @@ -62,17 +62,17 @@ Qed. [d+2] and [d+3]. The [Cont] contents enable detecting future writes that would partially overlap the 4-byte value. *) -Inductive content : Set := +Inductive content : Type := | Undef: content (**r undefined contents *) | Datum: nat -> val -> content (**r first byte of a value *) | Cont: content. (**r continuation bytes for a multi-byte value *) -Definition contentmap : Set := Z -> content. +Definition contentmap : Type := Z -> content. (** A memory block comprises the dimensions of the block (low and high bounds) plus a mapping from byte offsets to contents. *) -Record block_contents : Set := mkblock { +Record block_contents : Type := mkblock { low: Z; high: Z; contents: contentmap @@ -82,7 +82,7 @@ Record block_contents : Set := mkblock { integers) to blocks. We also maintain the address of the next unallocated block, and a proof that this address is positive. *) -Record mem : Set := mkmem { +Record mem : Type := mkmem { blocks: Z -> block_contents; nextblock: block; nextblock_pos: nextblock > 0 @@ -455,7 +455,7 @@ Proof. Defined. Lemma in_bounds_true: - forall m chunk b ofs (A: Set) (a1 a2: A), + forall m chunk b ofs (A: Type) (a1 a2: A), valid_access m chunk b ofs -> (if in_bounds m chunk b ofs then a1 else a2) = a1. Proof. @@ -858,7 +858,7 @@ Qed. Inductive load_store_cases (chunk1: memory_chunk) (b1: block) (ofs1: Z) - (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Set := + (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type := | lsc_similar: b1 = b2 -> ofs1 = ofs2 -> size_chunk chunk1 = size_chunk chunk2 -> load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 @@ -1277,7 +1277,7 @@ Qed. Section GENERIC_INJECT. -Definition meminj : Set := block -> option (block * Z). +Definition meminj : Type := block -> option (block * Z). Variable val_inj: meminj -> val -> val -> Prop. @@ -2838,7 +2838,7 @@ Qed. (** Signed 8- and 16-bit stores can be performed like unsigned stores. *) Remark in_bounds_equiv: - forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A), + forall chunk1 chunk2 m b ofs (A: Type) (a1 a2: A), size_chunk chunk1 = size_chunk chunk2 -> (if in_bounds m chunk1 b ofs then a1 else a2) = (if in_bounds m chunk2 b ofs then a1 else a2). diff --git a/common/Smallstep.v b/common/Smallstep.v index a2634be..f41fe4e 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -33,8 +33,8 @@ Set Implicit Arguments. Section CLOSURES. -Variable genv: Set. -Variable state: Set. +Variable genv: Type. +Variable state: Type. (** A one-step transition relation has the following signature. It is parameterized by a global environment, which does not @@ -197,7 +197,7 @@ Qed. (** An alternate, equivalent definition of [forever] that is useful for coinductive reasoning. *) -Variable A: Set. +Variable A: Type. Variable order: A -> A -> Prop. CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := @@ -290,7 +290,7 @@ Qed. finite prefix of this trace, or the whole trace.) *) -Inductive program_behavior: Set := +Inductive program_behavior: Type := | Terminates: trace -> int -> program_behavior | Diverges: traceinf -> program_behavior. @@ -326,8 +326,8 @@ Section SIMULATION. (** The first small-step semantics is axiomatized as follows. *) -Variable genv1: Set. -Variable state1: Set. +Variable genv1: Type. +Variable state1: Type. Variable step1: genv1 -> state1 -> trace -> state1 -> Prop. Variable initial_state1: state1 -> Prop. Variable final_state1: state1 -> int -> Prop. @@ -335,8 +335,8 @@ Variable ge1: genv1. (** The second small-step semantics is also axiomatized. *) -Variable genv2: Set. -Variable state2: Set. +Variable genv2: Type. +Variable state2: Type. Variable step2: genv2 -> state2 -> trace -> state2 -> Prop. Variable initial_state2: state2 -> Prop. Variable final_state2: state2 -> int -> Prop. diff --git a/common/Switch.v b/common/Switch.v index 8124aea..179d4d2 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -23,7 +23,7 @@ Require Import Integers. (** A multi-way branch is composed of a list of (key, action) pairs, plus a default action. *) -Definition table : Set := list (int * nat). +Definition table : Type := list (int * nat). Fixpoint switch_target (n: int) (dfl: nat) (cases: table) {struct cases} : nat := @@ -37,7 +37,7 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table) Each node of the tree performs an equality test or a less-than test against one of the keys. *) -Inductive comptree : Set := +Inductive comptree : Type := | CTaction: nat -> comptree | CTifeq: int -> nat -> comptree -> comptree | CTiflt: int -> comptree -> comptree -> comptree. diff --git a/common/Values.v b/common/Values.v index 8182d7a..9645e8a 100644 --- a/common/Values.v +++ b/common/Values.v @@ -21,7 +21,7 @@ Require Import AST. Require Import Integers. Require Import Floats. -Definition block : Set := Z. +Definition block : Type := Z. Definition eq_block := zeq. (** A value is either: @@ -33,7 +33,7 @@ Definition eq_block := zeq. value of an uninitialized variable. *) -Inductive val: Set := +Inductive val: Type := | Vundef: val | Vint: int -> val | Vfloat: float -> val diff --git a/driver/Compiler.v b/driver/Compiler.v index bce0dab..97bc19b 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 938c488..8ee70bd 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 453d40c..b7e5b0b 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 879cfe5..94ec38e 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 a79ea29..9e2199c 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 6857236..2e60d73 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 728a725..77f5d84 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 ceda851..1eb59c5 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 cabe5b8..24835da 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 3c39006..1d58ee5 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). @@ -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 4b1f4e0..eddc372 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 2c7b82a..edb267e 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 63f0232..91de0b1 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 0c3ac75..5c37a57 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 6ec27a3..76ea153 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 d0f7cf4..88b70c1 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 300a804..27e12c2 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 46d8039..286517e 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 6ffffc1..8a02c99 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 48e26a7..0de1ccd 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 0e9be22..c57f3f9 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; |