diff options
| -rw-r--r-- | backend/RTLgen.v | 21 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 18 | ||||
| -rw-r--r-- | lib/Coqlib.v | 8 |
3 files changed, 14 insertions, 33 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 49d79fb2..11da630b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -23,7 +23,7 @@ Require Import Registers. Require Import CminorSel. Require Import RTL. -Open Local Scope string_scope. +Local Open Scope string_scope. (** * Translation environments and state *) @@ -112,16 +112,13 @@ Implicit Arguments Error [A s]. Definition mon (A: Type) : Type := forall (s: state), res A s. -Definition ret (A: Type) (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: Type) (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: Type) (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 @@ -132,27 +129,21 @@ Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (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]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). 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: Type) (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 | Error _ => g s end. -Implicit Arguments handle_error [A]. - (** ** Operations on state *) (** The initial state (empty CFG). *) diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index bfdd8ab9..71b67f67 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -25,7 +25,7 @@ Require Import Cop. Require Import Csyntax. Require Import Clight. -Open Local Scope string_scope. +Local Open Scope string_scope. (** State and error monad for generating fresh identifiers. *) @@ -43,17 +43,13 @@ Implicit Arguments Res [A g]. Definition mon (A: Type) := forall (g: generator), result A g. -Definition ret (A: Type) (x: A) : mon A := +Definition ret {A: Type} (x: A) : mon A := fun g => Res x g (Ple_refl (gen_next g)). -Implicit Arguments ret [A]. - -Definition error (A: Type) (msg: Errors.errmsg) : mon A := +Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun g => Err msg. -Implicit Arguments error [A]. - -Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B := +Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B := fun g => match x g with | Err msg => Err msg @@ -64,13 +60,9 @@ Definition bind (A B: Type) (x: mon A) (f: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (x: mon (A * B)) (f: A -> B -> mon C) : mon C := +Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C := bind x (fun p => f (fst p) (snd p)). -Implicit Arguments bind2 [A B C]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200) : gensym_monad_scope. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 6fa82492..18d4d7e1 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1200,7 +1200,7 @@ Proof. subst; exists b1; auto. exploit IHlist_forall2; eauto. intros (x2 & U & V); exists x2; auto. Qed. - + Lemma list_forall2_in_right: forall x2 l1 l2, list_forall2 l1 l2 -> In x2 l2 -> exists x1, In x1 l1 /\ P x1 x2. @@ -1209,7 +1209,7 @@ Proof. subst; exists a1; auto. exploit IHlist_forall2; eauto. intros (x1 & U & V); exists x1; auto. Qed. - + End FORALL2. Lemma list_forall2_imply: @@ -1277,11 +1277,9 @@ Qed. (** * Definitions and theorems over boolean types *) -Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := +Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool := if a then true else false. -Implicit Arguments proj_sumbool [P Q]. - Coercion proj_sumbool: sumbool >-> bool. Lemma proj_sumbool_true: |