From d3abe2547c8921d2b324da67370822b7fb89b6c0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 26 Sep 2022 13:13:51 +0100 Subject: Add global monad notation using Instances This was mostly inspired by the std++ library. --- src/common/Errormonad.v | 9 ++- src/common/Monad.v | 61 +++++++++++++++-- src/common/Optionmonad.v | 10 ++- src/common/Statemonad.v | 9 ++- src/common/Vericertlib.v | 3 + src/hls/GiblePargen.v | 8 +-- src/hls/GiblePargenproof.v | 158 +++++++++++++++++++++------------------------ src/hls/HTLgen.v | 2 +- src/hls/HTLgenspec.v | 11 ++-- src/hls/Predicate.v | 2 +- 10 files changed, 169 insertions(+), 104 deletions(-) diff --git a/src/common/Errormonad.v b/src/common/Errormonad.v index 09c5c1c..201a101 100644 --- a/src/common/Errormonad.v +++ b/src/common/Errormonad.v @@ -26,13 +26,13 @@ Module ErrorMonad <: Monad. | Error m => Error m end. - Definition bind {A B : Type} (f : mon A) (g : A -> mon B) : mon B := + Definition bind {A B : Type} (g : A -> mon B) (f : mon A) : mon B := match f with | OK a => g a | Error m => Error m end. - Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> mon C) : mon C := + Definition bind2 {A B C : Type} (g : A -> B -> mon C) (f : mon (A * B)) : mon C := match f with | OK (a, b) => g a b | Error m => Error m @@ -44,6 +44,11 @@ Module ErrorMonad <: Monad. | OK a' => a' end. + #[global] Instance error_ret : MRet res := @ret. + #[global] Instance error_bind : MBind res := @bind. + #[global] Instance error_join : MJoin res := @join. + #[global] Instance error_map : FMap res := @map. + End ErrorMonad. Module ErrorMonadExtra := MonadExtra(ErrorMonad). diff --git a/src/common/Monad.v b/src/common/Monad.v index b7d97a1..cf3180b 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -18,6 +18,9 @@ From Coq Require Import Lists.List. +Declare Scope vericert_scope. +#[local] Open Scope vericert_scope. + Declare Scope monad_scope. Module Type Monad. @@ -27,10 +30,10 @@ Module Type Monad. Parameter ret : forall (A : Type) (x : A), mon A. Arguments ret [A]. - Parameter bind : forall (A B : Type) (f : mon A) (g : A -> mon B), mon B. + Parameter bind : forall (A B : Type) (g : A -> mon B) (f : mon A), mon B. Arguments bind [A B]. - Parameter bind2 : forall (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C), mon C. + Parameter bind2 : forall (A B C: Type) (g: A -> B -> mon C) (f: mon (A * B)), mon C. Arguments bind2 [A B C]. End Monad. @@ -41,10 +44,10 @@ Module MonadExtra(M : Monad). Module Import MonadNotation. Notation "'do' X <- A ; B" := - (bind A (fun X => B)) + (bind (fun X => B) A) (at level 200, X name, A at level 100, B at level 200) : monad_scope. Notation "'do' ( X , Y ) <- A ; B" := - (bind2 A (fun X Y => B)) + (bind2 (fun X Y => B) A) (at level 200, X name, Y name, A at level 100, B at level 200) : monad_scope. End MonadNotation. @@ -70,3 +73,53 @@ Module MonadExtra(M : Monad). fold_left (fun a b => do a' <- a; f a' b) l s. End MonadExtra. + +(** A [Params f n] instance forces the setoid rewriting mechanism not to +rewrite in the first [n] arguments of the function [f]. We will declare such +instances for all operational type classes in this development. *) +From Coq Require Export Morphisms RelationClasses. + +From Coq Require Setoid. + +Global Instance: Params (@Relation_Definitions.equiv) 2 := {}. + +Class MRet (M : Type -> Type) := mret: forall {A}, A -> M A. +Global Arguments mret {_ _ _} _ : assert. +Global Instance: Params (@mret) 3 := {}. +Global Hint Mode MRet ! : typeclass_instances. + +Class MBind (M : Type -> Type) := mbind : forall {A B}, (A -> M B) -> M A -> M B. +Global Arguments mbind {_ _ _ _} _ !_ / : assert. +Global Instance: Params (@mbind) 4 := {}. +Global Hint Mode MBind ! : typeclass_instances. + +Class MJoin (M : Type -> Type) := mjoin: forall {A}, M (M A) -> M A. +Global Arguments mjoin {_ _ _} !_ / : assert. +Global Instance: Params (@mjoin) 3 := {}. +Global Hint Mode MJoin ! : typeclass_instances. + +Class FMap (M : Type -> Type) := fmap : forall {A B}, (A -> B) -> M A -> M B. +Global Arguments fmap {_ _ _ _} _ !_ / : assert. +Global Instance: Params (@fmap) 4 := {}. +Global Hint Mode FMap ! : typeclass_instances. + +Class OMap (M : Type -> Type) := omap: forall {A B}, (A -> option B) -> M A -> M B. +Global Arguments omap {_ _ _ _} _ !_ / : assert. +Global Instance: Params (@omap) 4 := {}. +Global Hint Mode OMap ! : typeclass_instances. + +Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : vericert_scope. +Notation "( m ≫=.)" := (fun f => mbind f m) (only parsing) : vericert_scope. +Notation "(.≫= f )" := (mbind f) (only parsing) : vericert_scope. +Notation "(≫=)" := (fun m f => mbind f m) (only parsing) : vericert_scope. + +Notation "x ← y ; z" := (y ≫= (fun x : _ => z)) + (at level 20, y at level 100, z at level 200, only parsing) : vericert_scope. + +Notation "' x ← y ; z" := (y ≫= (fun x : _ => z)) + (at level 20, x pattern, y at level 100, z at level 200, only parsing) : vericert_scope. + +Infix "<$>" := fmap (at level 61, left associativity) : vericert_scope. + +Notation "x ;; z" := (x ≫= fun _ => z) + (at level 100, z at level 200, only parsing, right associativity): vericert_scope. diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v index 4a80ff8..037dd83 100644 --- a/src/common/Optionmonad.v +++ b/src/common/Optionmonad.v @@ -43,13 +43,13 @@ Module Option <: Monad. | _ => None end. - Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := + Definition bind {A B : Type} (g : A -> option B) (f : option A) : option B := match f with | Some a => g a | _ => None end. - Definition bind2 {A B C : Type} (f : mon (A * B)) (g : A -> B -> option C) : option C := + Definition bind2 {A B C : Type} (g : A -> B -> option C) (f : mon (A * B)) : option C := match f with | Some (a, b) => g a b | _ => None @@ -61,6 +61,12 @@ Module Option <: Monad. | Some a' => a' end. + #[global] Instance option_ret : MRet option := @ret. + #[global] Instance option_bind : MBind option := @bind. + #[global] Instance option_join : MJoin option := @join. + #[global] Instance option_map : FMap option := @map. + #[global] Instance option_omap : OMap option := @bind. + End Option. Module OptionExtra. diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index 16dcbbf..c667fd9 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -42,7 +42,7 @@ Module Statemonad(S : State) <: Monad. Definition ret {A: Type} (x: A) : mon A := fun (s : S.st) => OK x s (S.st_refl s). - Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := + Definition bind {A B: Type} (g: A -> mon B) (f: mon A) : mon B := fun (s : S.st) => match f s with | Error msg => Error msg @@ -53,8 +53,8 @@ Module Statemonad(S : State) <: Monad. end end. - 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)). + Definition bind2 {A B C: Type} (g: A -> B -> mon C) (f: mon (A * B)) : mon C := + bind (fun xy => g (fst xy) (snd xy)) (f: mon (A * B)). Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s : S.st) => @@ -76,4 +76,7 @@ Module Statemonad(S : State) <: Monad. | Error err => Errors.Error err end. + #[global] Instance statemonad_ret : MRet mon := @ret. + #[global] Instance statemonad_bind : MBind mon := @bind. + End Statemonad. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 24abece..6f602fc 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -31,8 +31,11 @@ Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import vericert.common.Show. +Require Export vericert.common.Monad. Require Export vericert.common.Optionmonad. +#[global] Open Scope vericert_scope. + (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 0ca7ead..af09ee6 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -241,10 +241,10 @@ Definition is_initial_pred (f: forest) (p: positive) := | _ => None end. -Definition update (fop : option (pred_op * forest)) (i : instr): option (pred_op * forest) := - do (pred, f) <- fop; +Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest) := + let (pred, f) := fop in match i with - | RBnop => fop + | RBnop => Some fop | RBop p op rl r => do pruned <- prune_predicated @@ -298,7 +298,7 @@ Get a sequence from the basic block. |*) Definition abstract_sequence (b : list instr) : option forest := - Option.map snd (fold_left update b (Some (Ptrue, empty))). + Option.map snd (mfold_left update b (Some (Ptrue, empty))). (*| Check equivalence of control flow instructions. As none of the basic blocks diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index eae309b..bcc3fd0 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -32,6 +32,10 @@ Require Import vericert.hls.Gible. Require Import vericert.hls.GiblePargen. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. +Require Import vericert.common.Monad. + +Module OptionExtra := MonadExtra(Option). +Import OptionExtra. #[local] Open Scope positive. #[local] Open Scope forest. @@ -1160,18 +1164,20 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. forall f i' i'' a sp p i p' f', sem (mk_ctx i sp ge) f (i', None) -> step_instr ge sp (Iexec i') a (Iexec i'') -> - update (Some (p, f)) a = Some (p', f') -> + update (p, f) a = Some (p', f') -> sem (mk_ctx i sp ge) f' (i'', None). Proof. Admitted. - (* Lemma sem_update_instr_term : *) - (* forall f i' i'' a sp i cf p p' p'' f', *) - (* sem (mk_ctx i sp ge) f (i', None) -> *) - (* step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) -> *) - (* update (Some (p', f)) a = Some (p'', f') -> *) - (* sem (mk_ctx i sp ge) f' (i'', Some cf) *) - (* /\ eval_apred (mk_ctx i sp ge) p'' false. *) - (* Proof. Admitted. *) + + Lemma sem_update_instr_term : + forall f i' i'' a sp i cf p p' p'' f', + sem (mk_ctx i sp ge) f (i', None) -> + step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) -> + update (p', f) a = Some (p'', f') -> + sem (mk_ctx i sp ge) f' (i'', Some cf) + /\ eval_predf (is_ps i) p'' = false. + Proof. + Admitted. (* Lemma step_instr_lessdef : *) (* forall sp a i i' ti, *) @@ -1180,12 +1186,12 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. (* exists ti', step_instr ge sp (Iexec ti) a (Iexec ti') /\ state_lessdef i' ti'. *) (* Proof. Admitted. *) - (* Lemma step_instr_lessdef_term : *) - (* forall sp a i i' ti cf, *) - (* step_instr ge sp (Iexec i) a (Iterm i' cf) -> *) - (* state_lessdef i ti -> *) - (* exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'. *) - (* Proof. Admitted. *) + Lemma step_instr_lessdef_term : + forall sp a i i' ti cf, + step_instr ge sp (Iexec i) a (Iterm i' cf) -> + state_lessdef i ti -> + exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'. + Proof. Admitted. (* Lemma app_predicated_semregset : forall A ctx o f res r y, @@ -1320,75 +1326,62 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. (* (* now apply falsy_update. *) *) (* (* Qed. *) Admitted. *) - (* Lemma state_lessdef_sem : *) - (* forall i sp f i' ti cf, *) - (* sem (mk_ctx i sp ge) f (i', cf) -> *) - (* state_lessdef i ti -> *) - (* exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'. *) - (* Proof. Admitted. *) - - (* Lemma update_Some : *) - (* forall x n y, *) - (* fold_left update x n = Some y -> *) - (* exists n', n = Some n'. *) - (* Proof. *) - (* induction x; crush. *) - (* econstructor; eauto. *) - (* exploit IHx; eauto; simplify. *) - (* unfold update, Option.bind2, Option.bind in H1. *) - (* repeat (destruct_match; try discriminate); econstructor; eauto. *) - (* Qed. *) + Lemma state_lessdef_sem : + forall i sp f i' ti cf, + sem (mk_ctx i sp ge) f (i', cf) -> + state_lessdef i ti -> + exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ state_lessdef i' ti'. + Proof. Admitted. (* #[local] Opaque update. *) - (* Lemma abstr_fold_correct : *) - (* forall sp x i i' i'' cf f p f', *) - (* SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> *) - (* sem (mk_ctx i sp ge) (snd f) (i', None) -> *) - (* fold_left update x (Some f) = Some (p, f') -> *) - (* forall ti, *) - (* state_lessdef i ti -> *) - (* exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) *) - (* /\ state_lessdef i'' ti'. *) - (* Proof. *) - (* induction x; simplify; inv H. *) - (* - destruct f. exploit update_Some; eauto; intros. simplify. *) - (* rewrite H3 in H1. destruct x0. *) - (* exploit IHx; eauto. eapply sem_update_instr; eauto. *) - (* - destruct f. *) - (* exploit state_lessdef_sem; eauto; intros. simplify. *) - (* exploit step_instr_lessdef_term; eauto; intros. simplify. *) - (* inv H6. exploit update_Some; eauto; simplify. destruct x2. *) - (* exploit sem_update_instr_term; eauto; simplify. *) - (* eexists; split. *) - (* eapply abstr_fold_falsy; eauto. *) - (* rewrite H6 in H1. eauto. auto. *) - (* Qed. *) - - (* Lemma sem_regset_empty : *) - (* forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). *) - (* Proof. *) - (* intros; constructor; intros. *) - (* constructor; auto. constructor. *) - (* constructor. *) - (* Qed. *) + Lemma abstr_fold_correct : + forall sp x i i' i'' cf f p f', + SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) -> + sem (mk_ctx i sp ge) (snd f) (i', None) -> + mfold_left update x (Some f) = Some (p, f') -> + forall ti, + state_lessdef i ti -> + exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf) + /\ state_lessdef i'' ti'. + Proof. + induction x; simplify; inv H. + - destruct f. (* exploit update_Some; eauto; intros. simplify. *) + (* rewrite H3 in H1. destruct x0. *) + (* exploit IHx; eauto. eapply sem_update_instr; eauto. *) + (* - destruct f. *) + (* exploit state_lessdef_sem; eauto; intros. simplify. *) + (* exploit step_instr_lessdef_term; eauto; intros. simplify. *) + (* inv H6. exploit update_Some; eauto; simplify. destruct x2. *) + (* exploit sem_update_instr_term; eauto; simplify. *) + (* eexists; split. *) + (* eapply abstr_fold_falsy; eauto. *) + (* rewrite H6 in H1. eauto. auto. *) + (* Qed. *) Admitted. + + Lemma sem_regset_empty : + forall A ctx, @sem_regset A ctx empty (ctx_rs ctx). + Proof using. + intros; constructor; intros. + constructor; auto. constructor. + constructor. + Qed. - (* Lemma sem_predset_empty : *) - (* forall A ctx, @sem_predset A ctx empty (ctx_ps ctx). *) - (* Proof. *) - (* intros; constructor; intros. *) - (* constructor; auto. constructor. *) - (* constructor. *) - (* Qed. *) + Lemma sem_predset_empty : + forall A ctx, @sem_predset A ctx empty (ctx_ps ctx). + Proof using. + intros; constructor; intros. + constructor; auto. constructor. + Qed. - (* Lemma sem_empty : *) - (* forall A ctx, @sem A ctx empty (ctx_is ctx, None). *) - (* Proof. *) - (* intros. destruct ctx. destruct ctx_is. *) - (* constructor; try solve [constructor; constructor; crush]. *) - (* eapply sem_regset_empty. *) - (* eapply sem_predset_empty. *) - (* Qed. *) + Lemma sem_empty : + forall A ctx, @sem A ctx empty (ctx_is ctx, None). + Proof using. + intros. destruct ctx. destruct ctx_is. + constructor; try solve [constructor; constructor; crush]. + eapply sem_regset_empty. + eapply sem_predset_empty. + Qed. Lemma abstr_sequence_correct : forall sp x i i'' cf x', @@ -1402,10 +1395,9 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. unfold abstract_sequence. intros. unfold Option.map in H0. destruct_match; try easy. destruct p; simplify. - (* eapply abstr_fold_correct; eauto. *) - (* simplify. eapply sem_empty. *) - (* Qed. *) - Admitted. + eapply abstr_fold_correct; eauto. + simplify. eapply sem_empty. + Qed. Lemma abstr_check_correct : forall sp i i' a b cf ti, diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index bff68a2..6e632b8 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -385,7 +385,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => do tc <- translate_condition c rl; - ret (Vternary tc (Vvar r1) (Vvar r2)) + mret (Vternary tc (Vvar r1) (Vvar r2)) | Op.Olea a, _ => translate_eff_addressing a args | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 165fa91..0259be9 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -39,7 +39,7 @@ Require Import vericert.hls.FunctionalUnits. Remark bind_inversion: forall (A B: Type) (f: mon A) (g: A -> mon B) (y: B) (s1 s3: st) (i: st_incr s1 s3), - bind f g s1 = OK y s3 i -> + bind g f s1 = OK y s3 i -> exists x, exists s2, exists i1, exists i2, f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2. Proof. @@ -53,7 +53,7 @@ Qed. Remark bind2_inversion: forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) (z: C) (s1 s3: st) (i: st_incr s1 s3), - bind2 f g s1 = OK z s3 i -> + bind2 g f s1 = OK z s3 i -> exists x, exists y, exists s2, exists i1, exists i2, f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2. Proof. @@ -71,9 +71,11 @@ Ltac monadInv1 H := discriminate | (ret _ _ = OK _ _ _) => inversion H; clear H; try subst + | (mret _ _ = OK _ _ _) => + inversion H; clear H; try subst | (error _ _ = OK _ _ _) => discriminate - | (bind ?F ?G ?S = OK ?X ?S' ?I) => + | (bind ?G ?F ?S = OK ?X ?S' ?I) => let x := fresh "x" in ( let s := fresh "s" in ( let i1 := fresh "INCR" in ( @@ -83,7 +85,7 @@ Ltac monadInv1 H := destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]]; clear H; try (monadInv1 EQ2))))))) - | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => + | (bind2 ?G ?F ?S = OK ?X ?S' ?I) => let x1 := fresh "x" in ( let x2 := fresh "x" in ( let s := fresh "s" in ( @@ -99,6 +101,7 @@ Ltac monadInv1 H := Ltac monadInv H := match type of H with | (ret _ _ = OK _ _ _) => monadInv1 H + | (mret _ _ = OK _ _ _) => monadInv1 H | (error _ _ = OK _ _ _) => monadInv1 H | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 8dbd0f6..6067719 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -178,7 +178,7 @@ Proof. crush. Qed. { equiv := sat_equiv; }. #[global] - Instance PandProper : Proper (equiv ==> equiv ==> equiv) Pand. + Instance PandProper : Proper (SetoidClass.equiv ==> SetoidClass.equiv ==> SetoidClass.equiv) Pand. Proof. unfold Proper. simplify. unfold "==>". intros. -- cgit