From 7cd2d3b1365e3fecf72a7f6c705f9057e8769698 Mon Sep 17 00:00:00 2001 From: Yannick Date: Thu, 20 Feb 2020 21:46:24 -0500 Subject: [PATCH 1/8] The Either monad transformer lifts the iterative structure over its kleisli category --- theories/Basics/MonadEither.v | 260 ++++++++++++++++++++++++++++++++++ 1 file changed, 260 insertions(+) create mode 100644 theories/Basics/MonadEither.v diff --git a/theories/Basics/MonadEither.v b/theories/Basics/MonadEither.v new file mode 100644 index 00000000..2f725a82 --- /dev/null +++ b/theories/Basics/MonadEither.v @@ -0,0 +1,260 @@ +From Coq Require Import + Setoid + Morphisms. + +From ExtLib Require Import + Structures.Monad + EitherMonad. + +From ITree Require Import + Basics.Basics + Basics.Category + Basics.CategoryKleisli + Basics.CategoryKleisliFacts + Basics.Monad. + +Import ITree.Basics.Basics.Monads. +Import CatNotations. +Local Open Scope cat_scope. +Local Open Scope cat. + +Section Either. + Variable M : Type -> Type. + Variable A : Type. + Context {EQM : EqM M}. + Context {HM: Monad M}. + Context {HEQP: @EqMProps M _ EQM}. + Context {ML: @MonadLaws M _ HM}. + + Global Instance EqM_eitherTM : EqM (eitherT A M). + Proof. + intros ? [a] [b]. + exact (eqm a b). + Defined. + + Global Instance EqMProps_eitherTM : @EqMProps (eitherT A M) _ EqM_eitherTM. + Proof. + constructor. + - intros [x]; cbn; reflexivity. + - intros [x] [y]; cbn; symmetry; auto. + - intros [x] [y] [z]; cbn; etransitivity; eauto. + Qed. + + Instance MonadLaws_eitherTM : @MonadLaws (eitherT A M) _ _. + Proof. + constructor. + - cbn. intros a b f x; destruct (f x) eqn:EQ. + repeat red. + rewrite bind_ret_l, EQ; cbn. + reflexivity. + - cbn. intros a [x]; cbn. + match goal with + |- _ ≈ ?h => rewrite <- (bind_ret_r _ h) at 2 + end. + apply Proper_bind; [reflexivity | intros [b | m]; reflexivity]. + - cbn. intros a b c [x] f g; cbn. + rewrite bind_bind. + apply Proper_bind; [reflexivity | intros [? | m]]. + + rewrite bind_ret_l; reflexivity. + + reflexivity. + - cbn; intros a b [x] [y] EQ x' y' H'; cbn in *. + apply Proper_bind; [auto | intros [? | ?]]; [reflexivity |]. + specialize (H' a0). + destruct (x' a0), (y' a0); cbn in *; auto. + Qed. + + Context {IM: Iter (Kleisli M) sum}. + Context {CM: Iterative (Kleisli M) sum}. + + Definition iso {a b:Type} (Aab : A + (a + b)) : (a + (A + b)) := + match Aab with + | inl A => inr (inl A) + | inr (inl a) => inl a + | inr (inr b) => inr (inr b) + end. + + (* Definition iso_inv {a b:Type} (sab : (S * a) + (S * b)) : S * (a + b) := *) + (* match sab with *) + (* | inl (s, a) => (s, inl a) *) + (* | inr (s, b) => (s, inr b) *) + (* end. *) + + (* Definition internalize {a b:Type} (f : Kleisli (eitherT S M) a b) : Kleisli M (S * a) (S * b) := *) + (* fun (sa : S * a) => f (snd sa) (fst sa). *) + + (* Lemma internalize_eq {a b:Type} (f g : Kleisli (eitherT S M) a b) : *) + (* eq2 f g <-> eq2 (internalize f) (internalize g). *) + (* Proof. *) + (* split. *) + (* - intros. *) + (* repeat red. destruct a0. *) + (* unfold internalize. cbn. apply H. *) + (* - intros. *) + (* repeat red. intros. *) + (* unfold internalize in H. *) + (* specialize (H (a1, a0)). *) + (* apply H. *) + (* Qed. *) + + + (* Lemma internalize_pure {a b c} (f : Kleisli (eitherT S M) a b) (g : S * b -> S * c) : *) + (* internalize f >>> pure g ⩯ (internalize (f >>> (fun b s => ret (g (s,b))))). *) + (* Proof. *) + (* repeat red. *) + (* destruct a0. *) + (* unfold internalize, cat, Cat_Kleisli. cbn. *) + (* apply Proper_bind; auto. *) + (* - reflexivity. *) + (* - repeat red. *) + (* destruct a1. *) + (* unfold pure. reflexivity. *) + (* Qed. *) + + Definition internalize {a b:Type} (f : Kleisli (eitherT A M) a b) : Kleisli M a (A + b) := + fun x => let '(mkEitherT y) := f x in y. + + Global Instance Iter_eitherTM : Iter (Kleisli (eitherT A M)) sum := + fun (a b: Type) (f: a -> (eitherT A M (a + b))) x => + mkEitherT (iter ((internalize f) >>> (pure iso)) x). + + (* Instance proper_internalize: Proper (eqm ==> eq2) internalize. *) + + Instance proper_internalize {a b}: Proper (eq2 ==> eq2) (@internalize a b). + intros x y H o; specialize (H o). + unfold internalize; destruct (x o), (y o). + apply H. + Qed. + + (* Lemma internalize_cat {a b c} (f : Kleisli (eitherT A M) a b) (g : Kleisli (eitherT A M) b c) : *) + (* (internalize (f >>> g)) ⩯ ((internalize f) >>> (internalize g)). *) + (* Proof. *) + (* repeat red. *) + (* destruct a0. *) + (* cbn. *) + (* unfold internalize. *) + (* unfold cat, Cat_Kleisli. *) + (* cbn. *) + (* reflexivity. *) + (* Qed. *) + + Global Instance Proper_Iter_eitherTM : forall a b, @Proper (Kleisli (eitherT A M) a (a + b) -> (Kleisli (eitherT A M) a b)) (eq2 ==> eq2) iter. + Proof. + destruct CM. + intros a b x y H a0. + apply iterative_proper_iter. + apply cat_eq2_r. + rewrite H; reflexivity. + Qed. + + Global Instance IterUnfold_eitherTM : IterUnfold (Kleisli (eitherT A M)) sum. + Proof. + destruct CM. + intros a b f o. + cbn; destruct (f o) as [e] eqn:EQ; cbn. + unfold cat, Cat_Kleisli. + unfold iter, Iter_eitherTM. + rewrite iterative_unfold. + unfold cat, Cat_Kleisli. + rewrite bind_bind. + apply Proper_bind. + + unfold internalize; rewrite EQ; reflexivity. + + intros [xA | [xa | xb]]; unfold pure; rewrite bind_ret_l; reflexivity. + Qed. + + Global Instance IterNatural_eitherTM : IterNatural (Kleisli (eitherT A M)) sum. + Proof. + destruct CM. + intros a b c f g o. + cbn; destruct (f o) as [e] eqn:EQf; cbn. + setoid_rewrite iterative_natural. + apply iterative_proper_iter; intros a'. + unfold cat, Cat_Kleisli. + unfold internalize; destruct (f a') eqn:EQf'; cbn. + rewrite! bind_bind. + apply Proper_bind; [reflexivity |]. + intros [xA | [xa | xb]]; unfold pure; cbn; rewrite !bind_ret_l; cbn; unfold cat, Cat_Kleisli; cbn. + - rewrite bind_ret_l; cbn; reflexivity. + - unfold id_, Id_Kleisli, pure; rewrite bind_ret_l; reflexivity. + - destruct (g xb); cbn; rewrite bind_bind. + apply Proper_bind; [reflexivity |]. + intros [? | ?]; rewrite bind_ret_l; reflexivity. + Qed. + + Lemma iter_dinatural_helper: + forall (a b c : Type) (f : Kleisli (eitherT A M) a (b + c)) (g : Kleisli (eitherT A M) b (a + c)), + internalize (f >>> case_ g inr_) >>> pure iso ⩯ internalize f >>> pure iso >>> case_ (internalize g >>> pure iso) inr_. + Proof. + destruct CM. + intros a b c f g o. + unfold cat, Cat_Kleisli, internalize; cbn. + repeat rewrite bind_bind. + destruct (f o) as [fo] eqn: EQ; cbn. + unfold pure; cbn. + apply Proper_bind; [reflexivity | intros [xA | [xa | xb]]]; cbn. + - rewrite !bind_ret_l; reflexivity. + - destruct (g xa) as [gxa] eqn:EQ'; cbn. + rewrite bind_ret_l; cbn; rewrite EQ'; reflexivity. + - rewrite !bind_ret_l; reflexivity. + Qed. + + Global Instance IterDinatural_eitherTM : IterDinatural (Kleisli (eitherT A M)) sum. + Proof. + destruct CM. + unfold IterDinatural. + intros a b c f g o. + unfold iter, Iter_eitherTM. cbn. + eapply transitivity. + eapply iterative_proper_iter. + apply iter_dinatural_helper. + rewrite iterative_dinatural. + cbn. + unfold cat, Cat_Kleisli. + rewrite bind_bind. + unfold internalize. cbn. + apply Proper_bind. + - reflexivity. + - unfold pure; cbn; intros [xA | [xa | xb]]; cbn. + + rewrite bind_ret_l; cbn; reflexivity. + + rewrite bind_ret_l; cbn. + eapply iterative_proper_iter. + intros ?; rewrite !bind_bind. + destruct (g a0) eqn:EQ; cbn. + apply Proper_bind; [reflexivity | intros [|[|]]]; cbn; rewrite !bind_ret_l; try reflexivity. + + rewrite bind_ret_l; cbn. + reflexivity. + Qed. + + Global Instance IterCodiagonal_eitherTM : IterCodiagonal (Kleisli (eitherT A M)) sum. + Proof. + destruct CM. + unfold IterCodiagonal. + intros a b f o. + unfold iter, Iter_eitherTM. + cbn. + eapply transitivity. + eapply iterative_proper_iter. + eapply Proper_cat_Kleisli; [| reflexivity]. + unfold internalize; cbn. reflexivity. + eapply transitivity. + + eapply iterative_proper_iter. + apply iterative_natural. + rewrite iterative_codiagonal. + eapply iterative_proper_iter. + rewrite cat_assoc, bimap_case, cat_id_l, cat_id_r. + unfold internalize. + intros o'; cbn. + unfold cat, Cat_Kleisli; rewrite !bind_bind; destruct (f o'); cbn. + apply Proper_bind; [reflexivity | intros [| [|]]]. + unfold pure; rewrite !bind_ret_l; reflexivity. + unfold pure; cbn; rewrite !bind_ret_l; reflexivity. + unfold pure; cbn; rewrite !bind_ret_l; reflexivity. + Qed. + + Global Instance Iterative_eitherTM : Iterative (Kleisli (eitherT A M)) sum. + Proof. + constructor; + typeclasses eauto. + Qed. + +End Either. From 8dd5316d141cc957330553af083e9f60e58f0742 Mon Sep 17 00:00:00 2001 From: Yannick Date: Fri, 21 Feb 2020 16:41:26 -0500 Subject: [PATCH 2/8] Generalized Fin over any Kleisli Category --- theories/Basics/MonadEither.v | 51 ----------------------------------- tutorial/Fin.v | 47 +++++++++++++++++++++----------- 2 files changed, 32 insertions(+), 66 deletions(-) diff --git a/theories/Basics/MonadEither.v b/theories/Basics/MonadEither.v index 2f725a82..01295d06 100644 --- a/theories/Basics/MonadEither.v +++ b/theories/Basics/MonadEither.v @@ -73,43 +73,6 @@ Section Either. | inr (inr b) => inr (inr b) end. - (* Definition iso_inv {a b:Type} (sab : (S * a) + (S * b)) : S * (a + b) := *) - (* match sab with *) - (* | inl (s, a) => (s, inl a) *) - (* | inr (s, b) => (s, inr b) *) - (* end. *) - - (* Definition internalize {a b:Type} (f : Kleisli (eitherT S M) a b) : Kleisli M (S * a) (S * b) := *) - (* fun (sa : S * a) => f (snd sa) (fst sa). *) - - (* Lemma internalize_eq {a b:Type} (f g : Kleisli (eitherT S M) a b) : *) - (* eq2 f g <-> eq2 (internalize f) (internalize g). *) - (* Proof. *) - (* split. *) - (* - intros. *) - (* repeat red. destruct a0. *) - (* unfold internalize. cbn. apply H. *) - (* - intros. *) - (* repeat red. intros. *) - (* unfold internalize in H. *) - (* specialize (H (a1, a0)). *) - (* apply H. *) - (* Qed. *) - - - (* Lemma internalize_pure {a b c} (f : Kleisli (eitherT S M) a b) (g : S * b -> S * c) : *) - (* internalize f >>> pure g ⩯ (internalize (f >>> (fun b s => ret (g (s,b))))). *) - (* Proof. *) - (* repeat red. *) - (* destruct a0. *) - (* unfold internalize, cat, Cat_Kleisli. cbn. *) - (* apply Proper_bind; auto. *) - (* - reflexivity. *) - (* - repeat red. *) - (* destruct a1. *) - (* unfold pure. reflexivity. *) - (* Qed. *) - Definition internalize {a b:Type} (f : Kleisli (eitherT A M) a b) : Kleisli M a (A + b) := fun x => let '(mkEitherT y) := f x in y. @@ -117,26 +80,12 @@ Section Either. fun (a b: Type) (f: a -> (eitherT A M (a + b))) x => mkEitherT (iter ((internalize f) >>> (pure iso)) x). - (* Instance proper_internalize: Proper (eqm ==> eq2) internalize. *) - Instance proper_internalize {a b}: Proper (eq2 ==> eq2) (@internalize a b). intros x y H o; specialize (H o). unfold internalize; destruct (x o), (y o). apply H. Qed. - (* Lemma internalize_cat {a b c} (f : Kleisli (eitherT A M) a b) (g : Kleisli (eitherT A M) b c) : *) - (* (internalize (f >>> g)) ⩯ ((internalize f) >>> (internalize g)). *) - (* Proof. *) - (* repeat red. *) - (* destruct a0. *) - (* cbn. *) - (* unfold internalize. *) - (* unfold cat, Cat_Kleisli. *) - (* cbn. *) - (* reflexivity. *) - (* Qed. *) - Global Instance Proper_Iter_eitherTM : forall a b, @Proper (Kleisli (eitherT A M) a (a + b) -> (Kleisli (eitherT A M) a b)) (eq2 ==> eq2) iter. Proof. destruct CM. diff --git a/tutorial/Fin.v b/tutorial/Fin.v index 6132615c..433eb3c5 100644 --- a/tutorial/Fin.v +++ b/tutorial/Fin.v @@ -22,7 +22,12 @@ From ITree Require Import ITree ITreeFacts Basics.Category - Basics.CategorySub. + Basics.CategorySub + Basics.MonadEither + Basics.Monad. +From ExtLib Require Import + EitherMonad. + (* end hide *) (* Type with [n] inhabitants. *) @@ -60,7 +65,17 @@ Proof. contradiction. Qed. -Instance FinInitial {E} : Initial (sub (ktree E) fin) 0 := fun _ => fin_0. +Section WithMonad. + +Variable M: Type -> Type. +Context {EQM : EqM M}. +Context {HM: Monad M}. +Context {HEQP: @EqMProps M _ EQM}. +Context {ML: @MonadLaws M _ HM}. + +Notation ktree := (Kleisli M). + +Global Instance FinInitial : Initial (sub ktree fin) 0 := fun _ => fin_0. Lemma split_fin_helper: forall n m x : nat, x < n + m -> ~ x < n -> x - n < m. @@ -82,7 +97,7 @@ Defined. Program Definition L {n} (m : nat) (a : fin n) : fin (n + m) := _. Next Obligation. destruct a. - exists x. apply PeanoNat.Nat.lt_lt_add_r. assumption. + exists x. apply PeanoNat.Nat.lt_lt_add_r. assumption. Defined. Program Definition R {m} (n:nat) (a:fin m) : fin (n + m) := _. @@ -187,30 +202,30 @@ Proof. try contradiction + exfalso; lia. Qed. -Instance ToBifunctor_ktree_fin {E} : ToBifunctor (ktree E) fin sum Nat.add := - fun n m y => Ret (split_fin_sum n m y). +Global Instance ToBifunctor_ktree_fin : ToBifunctor ktree fin sum Nat.add := + fun n m y => ret (split_fin_sum n m y). -Instance FromBifunctor_ktree_fin {E} : FromBifunctor (ktree E) fin sum Nat.add := - fun n m y => Ret (merge_fin_sum n m y). +Global Instance FromBifunctor_ktree_fin : FromBifunctor ktree fin sum Nat.add := + fun n m y => ret (merge_fin_sum n m y). -Instance IsoBif_ktree_fin {E} - : forall a b, Iso (ktree E) (a := fin (Nat.add a b)) to_bif from_bif. +Global Instance IsoBif_ktree_fin + : forall a b, Iso ktree (a := fin (Nat.add a b)) to_bif from_bif. Proof. unfold to_bif, ToBifunctor_ktree_fin, from_bif, FromBifunctor_ktree_fin. constructor; intros x. - unfold cat, Cat_sub, Cat_Kleisli. cbn. rewrite bind_ret_l. - apply eqit_Ret, merge_split. + rewrite merge_split; reflexivity. - unfold cat, Cat_sub, Cat_Kleisli. cbn. rewrite bind_ret_l. - apply eqit_Ret, split_merge. + rewrite split_merge; reflexivity. Qed. -Instance ToBifunctor_Fun_fin : ToBifunctor Fun fin sum Nat.add := +Global Instance ToBifunctor_Fun_fin : ToBifunctor Fun fin sum Nat.add := fun n m y => split_fin_sum n m y. -Instance FromBifunctor_Fun_fin : FromBifunctor Fun fin sum Nat.add := +Global Instance FromBifunctor_Fun_fin : FromBifunctor Fun fin sum Nat.add := fun n m y => merge_fin_sum n m y. -Instance IsoBif_Fun_fin +Global Instance IsoBif_Fun_fin : forall a b, Iso Fun (a := fin (Nat.add a b)) to_bif from_bif. Proof. constructor; intros x. @@ -218,7 +233,9 @@ Proof. - apply split_merge. Qed. -Instance InitialObject_ktree_fin {E} : InitialObject (sub (ktree E) fin) 0. +Global Instance InitialObject_ktree_fin : InitialObject (sub ktree fin) 0. Proof. intros n f x; apply fin_0; auto. Qed. + +End WithMonad. From c34cddf9ea9df52e34a8f7d29cc2acbbc5954867 Mon Sep 17 00:00:00 2001 From: Yannick Date: Fri, 21 Feb 2020 16:42:08 -0500 Subject: [PATCH 3/8] Denotation of asm over the (Kleisli (EitherM value (itree E))) --- tutorial/Asm.v | 35 +++++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 14 deletions(-) diff --git a/tutorial/Asm.v b/tutorial/Asm.v index 2522b92c..c85e8165 100644 --- a/tutorial/Asm.v +++ b/tutorial/Asm.v @@ -13,7 +13,10 @@ From Coq Require Import Setoid RelationClasses. -Require Import ExtLib.Structures.Monad. +From ExtLib Require Import + Structures.Monad + EitherMonad + MonadTrans. (* SAZ: Should we add ITreeMonad to ITree? *) From ITree Require Import @@ -21,6 +24,7 @@ From ITree Require Import ITreeFacts ITreeMonad Basics.Monad + Basics.MonadEither Basics.CategorySub Events.State Events.StateFacts. @@ -61,6 +65,7 @@ Variant instr : Set := Variant branch {label : Type} : Type := | Bjmp (_ : label) (* jump to label *) | Bbrz (_ : reg) (yes no : label) (* conditional jump *) +| Bret (_: reg) | Bhalt . Global Arguments branch _ : clear implicits. @@ -123,7 +128,6 @@ Inductive Memory : Type -> Type := | Load (a : addr) : Memory value | Store (a : addr) (val : value) : Memory unit. - (* SAZ: Move Exit to the itrees library? *) (** We also introduce a special event to model termination of the computation. Note that it expects _actively_ no answer from the environment: [Done] is @@ -136,7 +140,6 @@ Inductive Exit : Type -> Type := Definition exit {E A} `{Exit -< E} : itree E A := vis Done (fun v => match v : void with end). - Section Denote. (** Once again, [asm] programs shall be denoted as [itree]s. *) @@ -147,7 +150,6 @@ Section Denote. Local Open Scope monad_scope. (* end hide *) - Section with_event. (** As with _Imp_, we parameterize our semantics by a universe of events @@ -190,26 +192,31 @@ Section Denote. trigger (Store addr val) end. + Definition returns {B} r: eitherT value (itree E) B := mkEitherT (val <- trigger (GetReg r);; ret (inl val)). + + Notation tree_ret := (eitherT value (itree E)). + (** A [branch] returns the computed label whose set of possible values [B] is carried by the type of the branch. If the computation halts instead of branching, we return the [exit] tree. *) - Definition denote_br {B} (b : branch B) : itree E B := + Definition denote_br {B} (b : branch B) : tree_ret B := match b with | Bjmp l => ret l | Bbrz v y n => - val <- trigger (GetReg v) ;; - if val:nat then ret y else ret n - | Bhalt => exit + lift + (val <- trigger (GetReg v) ;; + if val:nat then ret y else ret n) + | Bret r => returns r + | Bhalt => lift exit end. - (** The denotation of a basic [block] shares the same type, returning the [label] of the next [block] it shall jump to. It recursively denote its instruction before that. *) - Fixpoint denote_bk {B} (b : block B) : itree E B := + Fixpoint denote_bk {B} (b : block B) : tree_ret B := match b with | bbi i b => - denote_instr i ;; denote_bk b + lift (denote_instr i) ;; denote_bk b | bbb b => denote_br b end. @@ -225,10 +232,10 @@ Section Denote. They have a nice algebraic structure, supported by the library, including a [loop] combinator that we can use to link collections of basic blocks. (See below.) *) - Definition denote_bks {A B : nat} (bs: bks A B): sub (ktree E) fin A B := + Definition denote_bks {A B : nat} (bs: bks A B): sub (Kleisli tree_ret) fin A B := fun a => denote_bk (bs a). - (** One can think of an [asm] program as a circuit/diagram where wires + (** One can think of an [asm] program as a circuit/diagram where wires correspond to jumps/program links. [denote_bks] computes the meaning of each basic block as an [itree] that returns the label of the next block to jump to, laying down all our elementary wires. In order to denote an [asm @@ -238,7 +245,7 @@ Section Denote. accomplish this with the same [loop] combinator we used to denote _Imp_'s [while] loop. It directly takes our [denote_bks (code s): ktree E (I + A) (I + B)] and hides [I] as desired. *) - Definition denote_asm {A B} : asm A B -> sub (ktree E) fin A B := + Definition denote_asm {A B} : asm A B -> sub (Kleisli tree_ret) fin A B := fun s => loop (denote_bks (code s)). End with_event. From 918e994fb9f0c88fa719a1276fbb3582a90ef5b0 Mon Sep 17 00:00:00 2001 From: Yannick Date: Mon, 24 Feb 2020 16:45:34 -0500 Subject: [PATCH 4/8] Added an interpreter for [eitherM A (itree E)]. I don't think we want to go this road on such a specialized instance, but it's kinda insightful if we want to generalize --- theories/Interp/InterpEither.v | 91 ++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 theories/Interp/InterpEither.v diff --git a/theories/Interp/InterpEither.v b/theories/Interp/InterpEither.v new file mode 100644 index 00000000..f4bc10fa --- /dev/null +++ b/theories/Interp/InterpEither.v @@ -0,0 +1,91 @@ +(** * Monadic interpretations of interaction trees *) + +(** We can derive semantics for an interaction tree [itree E ~> M] + from semantics given for every individual event [E ~> M], + when [M] is a monad (actually, with some more structure). + + We define the following terminology for this library. + Other sources may have different usages for the same or related + words. + + The notation [E ~> F] stands for [forall T, E T -> F T] + (in [ITree.Basics]). + It can mean many things, including the following: + + - The semantics of itrees are given as monad morphisms + [itree E ~> M], also called "interpreters". + + - "ITree interpreters" (or "itree morphisms") are monad morphisms + where the codomain is made of ITrees: [itree E ~> itree F]. + + Interpreters can be obtained from handlers: + + - In general, "event handlers" are functions [E ~> M] where + [M] is a monad. + + - "ITree event handlers" are functions [E ~> itree F]. + + Categorically, this boils down to saying that [itree] is a free + monad (not quite, but close enough). + *) + +(* begin hide *) +From ExtLib Require Import + Structures.Functor + EitherMonad + Structures.Monad. + +From ITree Require Import + Basics.Basics + Core.ITreeDefinition + Indexed.Relation. +(* end hide *) + +(** ** Translate *) + +(** An event morphism [E ~> F] lifts to an itree morphism [itree E ~> itree F] + by applying the event morphism to every visible event. We call this + process _event translation_. + + Translation is a special case of interpretation: +[[ + translate h t ≈ interp (trigger ∘ h) t +]] + However this definition of [translate] yields strong bisimulations + more often than [interp]. + For example, [translate (id_ E) t ≅ id_ (itree E)]. +*) + +(** A plain event morphism [E ~> F] defines an itree morphism + [itree E ~> itree F]. *) +(* Definition translateF {E F R} (h : E ~> F) (rec: itree E R -> itree F R) (t : itreeF E R _) : itree F R := *) +(* match t with *) +(* | RetF x => Ret x *) +(* | TauF t => Tau (rec t) *) +(* | VisF e k => Vis (h _ e) (fun x => rec (k x)) *) +(* end. *) + +(* Definition translate {E F} (h : E ~> F) *) +(* : itree E ~> itree F *) +(* := fun R => cofix translate_ t := translateF h translate_ (observe t). *) + +(* Arguments translate {E F} h [T]. *) + +(** ** Interpret *) + +(** An event handler [E ~> M] defines a monad morphism + [itree E ~> M] for any monad [M] with a loop operator. *) + +Definition interp_either {E M : Type -> Type} {A: Type} + {FM : Functor M} {MM : Monad M} {IM : MonadIter M} + (h : E ~> eitherT A M) : + eitherT A (itree E) ~> eitherT A M := + fun R => iter (fun t => + match observe (unEitherT t) with + | RetF (inl a) => mkEitherT (ret (inl a)) + | RetF (inr r) => ret (inr r) + | TauF t => ret (inl (mkEitherT t)) + | VisF e k => fmap (fun x => inl (mkEitherT (k x))) (h _ e) + end). + +Arguments interp_either {E M A FM MM IM} h [T]. From e2eb95edf1c21000032f5f1a6c6e4abb11d40ad1 Mon Sep 17 00:00:00 2001 From: Yannick Date: Fri, 3 Apr 2020 11:42:35 -0400 Subject: [PATCH 5/8] Interpreter for asm --- theories/Interp/InterpEither.v | 12 ++++++ tutorial/Asm.v | 71 +++++++++++++++++++++++----------- 2 files changed, 60 insertions(+), 23 deletions(-) diff --git a/theories/Interp/InterpEither.v b/theories/Interp/InterpEither.v index f4bc10fa..70e7e820 100644 --- a/theories/Interp/InterpEither.v +++ b/theories/Interp/InterpEither.v @@ -88,4 +88,16 @@ Definition interp_either {E M : Type -> Type} {A: Type} | VisF e k => fmap (fun x => inl (mkEitherT (k x))) (h _ e) end). +Definition interp_either' {E M : Type -> Type} {A: Type} + {FM : Functor M} {MM : Monad M} {IM : MonadIter M} + (h : E ~> M) : + eitherT A (itree E) ~> eitherT A M := + fun R => iter (fun t => + match observe (unEitherT t) with + | RetF (inl a) => mkEitherT (ret (inl a)) + | RetF (inr r) => ret (inr r) + | TauF t => ret (inl (mkEitherT t)) + | VisF e k => fmap (fun x => inl (mkEitherT (k x))) (MonadTrans.lift (h _ e)) + end). + Arguments interp_either {E M A FM MM IM} h [T]. diff --git a/tutorial/Asm.v b/tutorial/Asm.v index c85e8165..528ec2da 100644 --- a/tutorial/Asm.v +++ b/tutorial/Asm.v @@ -308,18 +308,43 @@ Definition registers := alist reg value. Definition memory := alist addr value. +(* Definition eitherT_stateT_commute {S A M R}: *) +(* (stateT S (eitherT A M) R) -> (eitherT A (stateT S M) R). *) +(* intros ?. *) + +From ITree Require Import Interp.InterpEither. (** The _asm_ interpreter takes as inputs a starting heap [mem] and register state [reg] and interprets an itree in two nested instances of the [map] variant of the state monad. To get this type to work out, we have to do a bit of post-processing to swap the order of the "state components" introduced by the interpretation. -*) -Definition interp_asm {E A} (t : itree (Reg +' Memory +' E) A) : - memory -> registers -> itree E (memory * (registers * A)) := - let h := bimap h_reg (bimap h_memory (id_ _)) in - let t' := interp h t in - fun mem regs => interp_map (interp_map t' regs) mem. + *) +(* Should [eitherT] be on top of [itree E] or on the outside? *) + +Definition distribute {A B C: Type}: A * (B + C) -> A * B + A * C := + fun '(a,bc) => match bc with + | inl b => inl (a,b) + | inr c => inr (a,c) + end. +Definition interp_either_map {E K V Exc d map} `{M : Map K V map} : + eitherT Exc (itree (@mapE K V d +' E)) ~> + stateT map (eitherT (map * Exc) (itree E)) := + fun T t s => + let '(mkEitherT t') := + interp_either' (M := stateT _ _) (case_ (@handle_map K V _ _ E d) pure_state) _ t in + mkEitherT (ITree.map distribute (t' s)). + +(* +Definition MAS {m: Type -> Type} (S: Type) (Exc: Type): Type -> Type := + fun (A: Type) => m ((Exc * S) + (A * S)). + *) +Definition interp_asm {E A} + (t : eitherT value (itree (Reg +' Memory +' E)) A) : + stateT registers (stateT memory (eitherT (memory * (registers * value)) (itree E))) A := + let h := bimap h_reg (bimap h_memory (id_ E)) in + let t' := interp_either' h _ t in + fun mem regs => interp_either_map _ (interp_either_map _ t' mem) regs. (** We can then define an evaluator for closed assembly programs by interpreting both store and heap events into two instances of [mapE], and running them @@ -331,7 +356,7 @@ Definition run_asm (p: asm 1 0) := interp_asm (denote_asm p Fin.f0) empty empty. *) (** The definition [interp_asm] also induces a notion of equivalence (open) _asm_ programs, which is just the equivalence of the ktree category *) -Definition eq_asm_denotations {E A B} (t1 t2 : Kleisli (itree (Reg +' Memory +' E)) A B) : Prop := +Definition eq_asm_denotations {E A B} (t1 t2 : Kleisli (eitherT value (itree (Reg +' Memory +' E))) A B) : Prop := forall a mem regs, interp_asm (t1 a) mem regs ≈ interp_asm (t2 a) mem regs. Definition eq_asm {A B} (p1 p2 : asm A B) : Prop := @@ -343,33 +368,33 @@ Section InterpAsmProperties. Notation E := (Reg +' Memory +' E'). (** This interpreter is compatible with the equivalence-up-to-tau. *) - Global Instance eutt_interp_asm {R}: - Proper (@eutt E R R eq ==> eq ==> eq ==> @eutt E' (prod memory (prod registers R)) (prod _ (prod _ R)) eq) interp_asm. - Proof. - repeat intro. - unfold interp_asm. - unfold interp_map. - rewrite H0. - rewrite H. - rewrite H1. - reflexivity. - Qed. + (* Global Instance eutt_interp_asm {R}: *) + (* Proper (@eutt E R R eq ==> eq ==> eq ==> @eutt E' (prod memory (prod registers R)) (prod _ (prod _ R)) eq) interp_asm. *) + (* Proof. *) + (* repeat intro. *) + (* unfold interp_asm. *) + (* unfold interp_map. *) + (* rewrite H0. *) + (* rewrite H. *) + (* rewrite H1. *) + (* reflexivity. *) + (* Qed. *) (** [interp_asm] commutes with [Ret]. *) Lemma interp_asm_ret: forall {R} (r: R) (regs : registers) (mem: memory), - @eutt E' _ _ eq (interp_asm (ret r) mem regs) - (ret (mem, (regs, r))). + @eutt E' _ _ eq (interp_asm (ret (m:= eitherT _ _) r) mem regs) + (ret (mem, (regs, inr r))). Proof. unfold interp_asm, interp_map. intros. unfold ret at 1, Monad_itree. - rewrite interp_ret, 2 interp_state_ret. + cbn. rewrite interp_ret, 2 interp_state_ret. reflexivity. Qed. (** [interp_asm] commutes with [bind]. *) - Lemma interp_asm_bind: forall {R S} (t: itree E R) (k: R -> itree _ S) (regs : registers) (mem: memory), - @eutt E' _ _ eq (interp_asm (ITree.bind t k) mem regs) + Lemma interp_asm_bind: forall {R S} (t: eitherT value (itree E) R) (k: R -> eitherT value (itree _) S) (regs : registers) (mem: memory), + @eutt E' _ _ eq (interp_asm (bind t k) mem regs) (ITree.bind (interp_asm t mem regs) (fun '(mem', (regs', x)) => interp_asm (k x) mem' regs')). Proof. From 3c3f44f5950daba11d72e35899a8d8fc038f7599 Mon Sep 17 00:00:00 2001 From: Yannick Date: Mon, 6 Apr 2020 23:36:28 -0400 Subject: [PATCH 6/8] Work in progress to cut some dependency on extlib, use a shallower eitherT monad transformer, clean up/ think a bit more about the monad infrastructure we are building and draft an Interpretable type class --- theories/Basics/Basics.v | 225 +++++++++++++------------ theories/Basics/CategoryKleisli.v | 16 +- theories/Basics/CategoryKleisliFacts.v | 3 - theories/Basics/Monad.v | 191 +++++++++++++++++++-- theories/Basics/MonadEither.v | 189 ++++++++++++--------- theories/Basics/MonadState.v | 102 ++++++----- theories/Events/State.v | 1 + tutorial/Asm.v | 38 ++++- 8 files changed, 515 insertions(+), 250 deletions(-) diff --git a/theories/Basics/Basics.v b/theories/Basics/Basics.v index 5503df06..2b3a1177 100644 --- a/theories/Basics/Basics.v +++ b/theories/Basics/Basics.v @@ -9,16 +9,6 @@ From Coq Require From Coq Require Import RelationClasses. -From ExtLib Require Import - Structures.Functor - Structures.Monad - Data.Monads.StateMonad - Data.Monads.ReaderMonad - Data.Monads.OptionMonad - Data.Monads.EitherMonad. - -Import MonadNotation. -Local Open Scope monad. (* end hide *) (** ** Parametric functions *) @@ -103,48 +93,63 @@ Section ProdRelInstances. End ProdRelInstances. - (** ** Common monads and transformers. *) -Module Monads. - -Definition identity (a : Type) : Type := a. - -Definition stateT (s : Type) (m : Type -> Type) (a : Type) : Type := - s -> m (prod s a). -Definition state (s a : Type) := s -> prod s a. - -Definition readerT (r : Type) (m : Type -> Type) (a : Type) : Type := - r -> m a. -Definition reader (r a : Type) := r -> a. - -Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type := - m (prod w a). -Definition writer := prod. - -Instance Functor_stateT {m s} {Fm : Functor m} : Functor (stateT s m) - := {| - fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s) - |}. - -Instance Monad_stateT {m s} {Fm : Monad m} : Monad (stateT s m) - := {| - ret _ a := fun s => ret (s, a) - ; bind _ _ t k := fun s => - sa <- t s ;; - k (snd sa) (fst sa) - |}. - -End Monads. - -(** ** Loop operator *) - -(** [iter]: A primitive for general recursion. - Iterate a function updating an accumulator [I], until it produces - an output [R]. - *) -Polymorphic Class MonadIter (M : Type -> Type) : Type := - iter : forall {R I: Type}, (I -> M (I + R)%type) -> I -> M R. +(* Module Monads. *) + +(* Definition identity (a : Type) : Type := a. *) + +(* Definition eitherT (exc : Type) (m: Type -> Type) (a: Type) : Type := *) +(* m (sum exc a). *) +(* Definition either (exc : Type) (a : Type) : Type := *) +(* sum exc a. *) + +(* Definition stateT (s : Type) (m : Type -> Type) (a : Type) : Type := *) +(* s -> m (prod s a). *) +(* Definition state (s a : Type) := s -> prod s a. *) + +(* Definition readerT (r : Type) (m : Type -> Type) (a : Type) : Type := *) +(* r -> m a. *) +(* Definition reader (r a : Type) := r -> a. *) + +(* Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type := *) +(* m (prod w a). *) +(* Definition writer := prod. *) + +(* Instance Functor_stateT {m s} {Fm : Functor m} : Functor (stateT s m) *) +(* := {| *) +(* fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s) *) +(* |}. *) + +(* Instance Monad_stateT {m s} {Fm : Monad m} : Monad (stateT s m) *) +(* := {| *) +(* ret _ a := fun s => ret (s, a) *) +(* ; bind _ _ t k := fun s => *) +(* sa <- t s ;; *) +(* k (snd sa) (fst sa) *) +(* |}. *) + +(* Instance Functor_eitherT {m exc} {Fm : Functor m} : Functor (eitherT exc m) *) +(* := {| *) +(* fmap _ _ f := fmap (fun ma => match ma with *) +(* | inl e => inl e *) +(* | inr a => inr (f a) *) +(* end) *) +(* |}. *) + +(* Program Instance Monad_eitherT {m exc} {Fm : Monad m} : Monad (eitherT exc m) *) +(* := {| *) +(* ret _ a := ret (inr a) *) +(* ; bind _ _ t k := *) +(* bind (m := m) t *) +(* (fun ma => *) +(* match ma with *) +(* | inl e => ret (inl e) *) +(* | inr a => k a *) +(* end) *) +(* |}. *) + +(* End Monads. *) (** *** Transformer instances *) @@ -153,66 +158,66 @@ Polymorphic Class MonadIter (M : Type -> Type) : Type := Quite easily in fact, no [Monad] assumption needed. *) -Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M} - : MonadIter (stateT S M) := - fun _ _ step i => mkStateT (fun s => - iter (fun is => - let i := fst is in - let s := snd is in - is' <- runStateT (step i) s ;; - ret match fst is' with - | inl i' => inl (i', snd is') - | inr r => inr (r, snd is') - end) (i, s)). - -Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M} - : MonadIter (Monads.stateT S M) := - fun _ _ step i s => - iter (fun si => - let s := fst si in - let i := snd si in - si' <- step i s;; - ret match snd si' with - | inl i' => inl (fst si', i') - | inr r => inr (fst si', r) - end) (s, i). - -Instance MonadIter_readerT {M S} {AM : MonadIter M} : MonadIter (readerT S M) := - fun _ _ step i => mkReaderT (fun s => - iter (fun i => runReaderT (step i) s) i). - -Instance MonadIter_optionT {M} {MM : Monad M} {AM : MonadIter M} - : MonadIter (optionT M) := - fun _ _ step i => mkOptionT ( - iter (fun i => - oi <- unOptionT (step i) ;; - ret match oi with - | None => inr None - | Some (inl i) => inl i - | Some (inr r) => inr (Some r) - end) i). - -Instance MonadIter_eitherT {M E} {MM : Monad M} {AM : MonadIter M} - : MonadIter (eitherT E M) := - fun _ _ step i => mkEitherT ( - iter (fun i => - ei <- unEitherT (step i) ;; - ret match ei with - | inl e => inr (inl e) - | inr (inl i) => inl i - | inr (inr r) => inr (inr r) - end) i). +(* Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M} *) +(* : MonadIter (stateT S M) := *) +(* fun _ _ step i => mkStateT (fun s => *) +(* iter (fun is => *) +(* let i := fst is in *) +(* let s := snd is in *) +(* is' <- runStateT (step i) s ;; *) +(* ret match fst is' with *) +(* | inl i' => inl (i', snd is') *) +(* | inr r => inr (r, snd is') *) +(* end) (i, s)). *) + +(* Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M} *) +(* : MonadIter (Monads.stateT S M) := *) +(* fun _ _ step i s => *) +(* iter (fun si => *) +(* let s := fst si in *) +(* let i := snd si in *) +(* si' <- step i s;; *) +(* ret match snd si' with *) +(* | inl i' => inl (fst si', i') *) +(* | inr r => inr (fst si', r) *) +(* end) (s, i). *) + +(* Instance MonadIter_readerT {M S} {AM : MonadIter M} : MonadIter (readerT S M) := *) +(* fun _ _ step i => mkReaderT (fun s => *) +(* iter (fun i => runReaderT (step i) s) i). *) + +(* Instance MonadIter_optionT {M} {MM : Monad M} {AM : MonadIter M} *) +(* : MonadIter (optionT M) := *) +(* fun _ _ step i => mkOptionT ( *) +(* iter (fun i => *) +(* oi <- unOptionT (step i) ;; *) +(* ret match oi with *) +(* | None => inr None *) +(* | Some (inl i) => inl i *) +(* | Some (inr r) => inr (Some r) *) +(* end) i). *) + +(* Instance MonadIter_eitherT {M E} {MM : Monad M} {AM : MonadIter M} *) +(* : MonadIter (eitherT E M) := *) +(* fun _ _ step i => mkEitherT ( *) +(* iter (fun i => *) +(* ei <- unEitherT (step i) ;; *) +(* ret match ei with *) +(* | inl e => inr (inl e) *) +(* | inr (inl i) => inl i *) +(* | inr (inr r) => inr (inr r) *) +(* end) i). *) (** And the nondeterminism monad [_ -> Prop] also has one. *) -Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R) - : Prop := -| iter_done - : step i (inr r) -> iter_Prop step i r -| iter_step i' - : step i (inl i') -> - iter_Prop step i' r -> - iter_Prop step i r -. - -Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop. +(* Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R) *) +(* : Prop := *) +(* | iter_done *) +(* : step i (inr r) -> iter_Prop step i r *) +(* | iter_step i' *) +(* : step i (inl i') -> *) +(* iter_Prop step i' r -> *) +(* iter_Prop step i r *) +(* . *) + +(* Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop. *) diff --git a/theories/Basics/CategoryKleisli.v b/theories/Basics/CategoryKleisli.v index 2ec6daec..bcd56126 100644 --- a/theories/Basics/CategoryKleisli.v +++ b/theories/Basics/CategoryKleisli.v @@ -18,9 +18,6 @@ From Coq Require Import Morphisms. -From ExtLib Require Import - Structures.Monad. - From ITree Require Import Basics.Basics Basics.CategoryOps @@ -56,7 +53,7 @@ Section Instances. Definition map {a b c} (g:b -> c) (ab : Kleisli m a b) : Kleisli m a c := cat ab (pure g). - + Global Instance Initial_Kleisli : Initial (Kleisli m) void := fun _ v => match v : void with end. @@ -73,6 +70,15 @@ Section Instances. fun _ _ => pure inr. Global Instance Iter_Kleisli `{MonadIter m} : Iter (Kleisli m) sum := - fun a b => Basics.iter. + fun a b => iter. End Instances. + +(* Convenient equation to switch perspective between the monadic and categorical view. *) +Lemma iter_monad_to_cat: + forall {M} {IM: MonadIter M} a b, + @Monad.iter M IM a b = @CategoryOps.iter Type (Kleisli M) sum _ b a. +Proof. + reflexivity. +Qed. + diff --git a/theories/Basics/CategoryKleisliFacts.v b/theories/Basics/CategoryKleisliFacts.v index b312e277..52771a64 100644 --- a/theories/Basics/CategoryKleisliFacts.v +++ b/theories/Basics/CategoryKleisliFacts.v @@ -6,9 +6,6 @@ From Coq Require Import Morphisms RelationClasses. -From ExtLib Require Import - Structures.Monad. - From ITree Require Import Basics.Basics Basics.Category diff --git a/theories/Basics/Monad.v b/theories/Basics/Monad.v index d05f16f9..46757ee3 100644 --- a/theories/Basics/Monad.v +++ b/theories/Basics/Monad.v @@ -4,9 +4,6 @@ From Coq Require Import Morphisms. -From ExtLib Require Export - Structures.Monad. - From ITree Require Import Basics.Basics Basics.CategoryOps @@ -14,6 +11,24 @@ From ITree Require Import (* end hide *) Set Primitive Projections. +(* Set Implicit Arguments. *) +(* Set Strict Implicit. *) +(* Set Universe Polymorphism. *) + +Set Implicit Arguments. +Set Strict Implicit. + +Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type := + { fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }. + +Module FunctorNotation. + Notation "f <$> x" := (@fmap _ _ _ _ f x) (at level 52, left associativity). +End FunctorNotation. + +Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := +{ ret : forall {t : Type@{d}}, t -> m t +; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u +}. Class EqM (m:Type -> Type) : Type := eqm : forall a, m a -> m a -> Prop. @@ -24,7 +39,65 @@ Class EqMProps (m:Type -> Type) `{Monad m} `{EqM m} := Arguments eqm {m _ _}. Infix "≈" := eqm (at level 70) : monad_scope. -Section Laws. +Section monadic. + + Definition liftM@{d c} + {m : Type@{d} -> Type@{c}} + {M : Monad m} + {T U : Type@{d}} (f : T -> U) : m T -> m U := + fun x => bind x (fun x => ret (f x)). + + Definition liftM2@{d c} + {m : Type@{d} -> Type@{c}} + {M : Monad m} + {T U V : Type@{d}} (f : T -> U -> V) : m T -> m U -> m V := + Eval cbv beta iota zeta delta [ liftM ] in + fun x y => bind x (fun x => liftM (f x) y). + + Definition liftM3@{d c} + {m : Type@{d} -> Type@{c}} + {M : Monad m} + {T U V W : Type@{d}} (f : T -> U -> V -> W) : m T -> m U -> m V -> m W := + Eval cbv beta iota zeta delta [ liftM2 ] in + fun x y z => bind x (fun x => liftM2 (f x) y z). + + Definition apM@{d c} + {m : Type@{d} -> Type@{c}} + {M : Monad m} + {A B : Type@{d}} (fM:m (A -> B)) (aM:m A) : m B := + bind fM (fun f => liftM f aM). + + (* Left-to-right composition of Kleisli arrows. *) + Definition mcompose@{c d} + {m:Type@{d}->Type@{c}} + {M: Monad m} + {T U V:Type@{d}} + (f: T -> m U) (g: U -> m V): (T -> m V) := + fun x => bind (f x) g. + +End monadic. + +Module MonadNotation. + + Delimit Scope monad_scope with monad. + + Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 58, left associativity) : monad_scope. + Notation "f =<< c" := (@bind _ _ _ _ c f) (at level 61, right associativity) : monad_scope. + Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope. + + Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2)) + (at level 61, c1 at next level, right associativity) : monad_scope. + + Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad + (at level 61, right associativity) : monad_scope. + + Notation "' pat <- c1 ;; c2" := + (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end)) + (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope. + +End MonadNotation. + +Section MonadLaws. Context (m : Type -> Type). Context {EqM : @EqM m}. @@ -32,21 +105,119 @@ Section Laws. Context {EqMP : @EqMProps m _ EqM}. Local Open Scope monad_scope. - - (* This should go coq-ext-lib. *) + Class MonadLaws := - { bind_ret_l :> forall a b (f : a -> m b) (x : a), bind (ret x) f ≈ f x - ; bind_ret_r :> forall a (x : m a), bind x (fun y => ret y) ≈ x - ; bind_bind :> forall a b c (x : m a) (f : a -> m b) (g : b -> m c), bind (bind x f) g ≈ bind x (fun y => bind (f y) g) + { bind_ret_l : forall a b (f : a -> m b) (x : a), bind (ret x) f ≈ f x + ; bind_ret_r : forall a (x : m a), bind x (fun y => ret y) ≈ x + ; bind_bind : forall a b c (x : m a) (f : a -> m b) (g : b -> m c), bind (bind x f) g ≈ bind x (fun y => bind (f y) g) ; Proper_bind :> forall {a b}, (@Proper (m a%type -> (a -> m b) -> m b) (eqm ==> pointwise_relation _ eqm ==> eqm) bind) }. -End Laws. +End MonadLaws. Arguments bind_ret_l {m _ _ _}. Arguments bind_ret_r {m _ _ _}. Arguments bind_bind {m _ _ _}. Arguments Proper_bind {m _ _ _}. + +(** ** Loop operator *) + +(** [iter]: A primitive for general recursion. + Iterate a function updating an accumulator [I], until it produces + an output [R]. + *) +Polymorphic Class MonadIter (M : Type -> Type) : Type := + iter : forall {R I: Type}, (I -> M (I + R)%type) -> I -> M R. + +(* Its laws are defined by its [Kleisli] category forming an [Iterative] category *) + +Section MonadHomomorphism. + + Local Open Scope monad_scope. + + Variable M M': Type -> Type. + Context {MM: Monad M}. + Context {MM': Monad M'}. + Context {IM: MonadIter M}. + Context {IM': MonadIter M'}. + Context {EqMM': @EqM M'}. + Variable F: M ~> M'. + + Class MonadHom: Prop := + { + resp_ret : forall A (a: A), F (ret a) ≈ ret a; + resp_bind: forall A B (m: M A) (k: A -> M B), + F (bind m k) ≈ bind (F m) (fun x => F (k x)) + }. + + Class IterHom: Prop := + { + resp_iter: forall (I R: Type) (body: I -> M (I + R)%type) i, + F (iter body i) ≈ iter (fun x => F (body x)) i + }. + +End MonadHomomorphism. + +Section MonadTriggerable. + + Local Open Scope monad_scope. + + Variable M M': Type -> Type. + Context {MM: Monad M}. + Context {MM': Monad M'}. + Context {EqMM': @EqM M'}. + Context {IM: MonadIter M}. + Context {IM': MonadIter M'}. + + (** + Monads that allow for the embedding of an effect as a minimal + monadic effectful computation are dubbed "Triggerable". + *) + + Class Triggerable := trigger: forall (E: Type -> Type), E ~> M. + + (* The correctness of this operation, i.e. its minimality, is expressed + with respect to a notion of interpretation of monads. + A monad [M] is said to be "Interpretable" into a monad [M'] if there + is a family of monad monomorphisms for each handler [h: E ~> M']. + *) + + Class Interpretable := + interp: forall (E: Type -> Type) (h: E ~> M'), M ~> M'. + + Class InterpCorrect {InterpMM': Interpretable} {TrigM: Triggerable}: Prop := + { + interp_monad_hom E h :> MonadHom (interp E h); + interp_iter_hom E h :> IterHom (interp E h); + interp_trigger E h T (e: E T): interp E h (trigger _ _ e) ≈ h _ e + }. + +End MonadTriggerable. + +Import CatNotations. +Local Open Scope cat_scope. +Local Open Scope monad_scope. + +Ltac rw_pointed_l H := + match goal with + |- ?f ?x ≈ _ => + let tmp := fresh "H" in + assert (tmp: f ⩯ f) by reflexivity; + setoid_rewrite H in tmp at 1; + specialize (tmp x); + setoid_rewrite <- tmp + end. + +Ltac rw_pointed_r H := + match goal with + |- _ ≈ ?f ?x => + let tmp := fresh "H" in + assert (tmp: f ⩯ f) by reflexivity; + setoid_rewrite H in tmp at 1; + specialize (tmp x); + setoid_rewrite <- tmp + end. + diff --git a/theories/Basics/MonadEither.v b/theories/Basics/MonadEither.v index 01295d06..6eb834ce 100644 --- a/theories/Basics/MonadEither.v +++ b/theories/Basics/MonadEither.v @@ -2,10 +2,6 @@ From Coq Require Import Setoid Morphisms. -From ExtLib Require Import - Structures.Monad - EitherMonad. - From ITree Require Import Basics.Basics Basics.Category @@ -13,144 +9,171 @@ From ITree Require Import Basics.CategoryKleisliFacts Basics.Monad. -Import ITree.Basics.Basics.Monads. Import CatNotations. +Import MonadNotation. Local Open Scope cat_scope. Local Open Scope cat. +Local Open Scope monad_scope. + +Definition eitherT (exn: Type) (M: Type -> Type) (a: Type) : Type := + M (sum exn a). +Definition either (exn a : Type) : Type := + sum exn a. + +Section Functor_Either. + Global Instance Functor_eitherT {M} {Fm : Functor M} (exn: Type) : Functor (eitherT exn M) + := {| + fmap _ _ f := fmap (fun ma => match ma with + | inl e => inl e + | inr a => inr (f a) + end) + |}. + +End Functor_Either. -Section Either. +Section Monad_Either. Variable M : Type -> Type. - Variable A : Type. + Variable exn : Type. Context {EQM : EqM M}. Context {HM: Monad M}. Context {HEQP: @EqMProps M _ EQM}. Context {ML: @MonadLaws M _ HM}. - Global Instance EqM_eitherTM : EqM (eitherT A M). - Proof. - intros ? [a] [b]. - exact (eqm a b). - Defined. - - Global Instance EqMProps_eitherTM : @EqMProps (eitherT A M) _ EqM_eitherTM. + Global Instance Monad_eitherT : Monad (eitherT exn M) + := {| + ret _ a := ret (inr a) + ; bind _ _ t k := + bind (m := M) t + (fun ma => + match ma with + | inl e => ret (inl e) + | inr a => k a + end) + |}. + + Global Instance EqM_eitherTM : EqM (eitherT exn M) := fun _ => eqm (m := M). + + Global Instance EqMProps_eitherTM : @EqMProps _ _ EqM_eitherTM. Proof. constructor. - - intros [x]; cbn; reflexivity. - - intros [x] [y]; cbn; symmetry; auto. - - intros [x] [y] [z]; cbn; etransitivity; eauto. + - repeat red; reflexivity. + - repeat red; intros x y; cbn; symmetry; auto. + - repeat red; intros x y z; cbn; etransitivity; eauto. Qed. - Instance MonadLaws_eitherTM : @MonadLaws (eitherT A M) _ _. + Instance MonadLaws_eitherTM : @MonadLaws (eitherT exn M) _ _. Proof. constructor. - - cbn. intros a b f x; destruct (f x) eqn:EQ. + - cbn. intros a b f x. repeat red. - rewrite bind_ret_l, EQ; cbn. + rewrite bind_ret_l; cbn. reflexivity. - - cbn. intros a [x]; cbn. + - cbn; intros a x. unfold eitherT in x. + unfold eqm, EqM_eitherTM. match goal with |- _ ≈ ?h => rewrite <- (bind_ret_r _ h) at 2 end. apply Proper_bind; [reflexivity | intros [b | m]; reflexivity]. - - cbn. intros a b c [x] f g; cbn. - rewrite bind_bind. + - cbn. intros a b c x f g; cbn. + rewrite bind_bind. do 2 red. apply Proper_bind; [reflexivity | intros [? | m]]. + rewrite bind_ret_l; reflexivity. + reflexivity. - - cbn; intros a b [x] [y] EQ x' y' H'; cbn in *. - apply Proper_bind; [auto | intros [? | ?]]; [reflexivity |]. - specialize (H' a0). - destruct (x' a0), (y' a0); cbn in *; auto. + - cbn; intros a b x y EQ x' y' H'; cbn in *. + do 2 red; apply Proper_bind; [auto | intros [? | ?]]; [reflexivity | apply H']. Qed. - Context {IM: Iter (Kleisli M) sum}. +End Monad_Either. + +Section Iter_Either. + + Variable M : Type -> Type. + Variable exn : Type. + Context {EQM : EqM M}. + Context {HM: Monad M}. + Context {HEQP: @EqMProps M _ EQM}. + Context {ML: @MonadLaws M _ HM}. + Context {IM: MonadIter M}. Context {CM: Iterative (Kleisli M) sum}. - Definition iso {a b:Type} (Aab : A + (a + b)) : (a + (A + b)) := + Definition iso {a b:Type} (Aab : exn + (a + b)) : (a + (exn + b)) := match Aab with | inl A => inr (inl A) | inr (inl a) => inl a | inr (inr b) => inr (inr b) end. - Definition internalize {a b:Type} (f : Kleisli (eitherT A M) a b) : Kleisli M a (A + b) := - fun x => let '(mkEitherT y) := f x in y. + Definition internalize {a b:Type} (f : Kleisli (eitherT exn M) a b) : Kleisli M a (exn + b) := f. - Global Instance Iter_eitherTM : Iter (Kleisli (eitherT A M)) sum := - fun (a b: Type) (f: a -> (eitherT A M (a + b))) x => - mkEitherT (iter ((internalize f) >>> (pure iso)) x). + Global Instance Iter_eitherTM : MonadIter (eitherT exn M) := + fun (b a: Type) (f: a -> M (exn + (a + b))) x => + iter ((internalize f) >>> (pure iso)) x. Instance proper_internalize {a b}: Proper (eq2 ==> eq2) (@internalize a b). - intros x y H o; specialize (H o). - unfold internalize; destruct (x o), (y o). - apply H. + intros x y H o; apply H. Qed. - Global Instance Proper_Iter_eitherTM : forall a b, @Proper (Kleisli (eitherT A M) a (a + b) -> (Kleisli (eitherT A M) a b)) (eq2 ==> eq2) iter. + Global Instance Proper_Iter_eitherTM : forall a b, @Proper (Kleisli (eitherT exn M) a (a + b) -> (Kleisli (eitherT exn M) a b)) (eq2 ==> eq2) iter. Proof. destruct CM. - intros a b x y H a0. + intros A B x y H a. apply iterative_proper_iter. apply cat_eq2_r. rewrite H; reflexivity. - Qed. + Qed. - Global Instance IterUnfold_eitherTM : IterUnfold (Kleisli (eitherT A M)) sum. + Global Instance IterUnfold_eitherTM : IterUnfold (Kleisli (eitherT exn M)) sum. Proof. - destruct CM. - intros a b f o. - cbn; destruct (f o) as [e] eqn:EQ; cbn. - unfold cat, Cat_Kleisli. - unfold iter, Iter_eitherTM. - rewrite iterative_unfold. + intros A B f a; cbn. + unfold CategoryOps.iter, Iter_Kleisli. + rewrite iter_monad_to_cat. + rw_pointed_l iter_unfold. unfold cat, Cat_Kleisli. + do 2 red. rewrite bind_bind. apply Proper_bind. - + unfold internalize; rewrite EQ; reflexivity. + + reflexivity. + intros [xA | [xa | xb]]; unfold pure; rewrite bind_ret_l; reflexivity. Qed. - Global Instance IterNatural_eitherTM : IterNatural (Kleisli (eitherT A M)) sum. + Global Instance IterNatural_eitherTM : IterNatural (Kleisli (eitherT exn M)) sum. Proof. destruct CM. - intros a b c f g o. - cbn; destruct (f o) as [e] eqn:EQf; cbn. + intros A B C f g a; cbn. setoid_rewrite iterative_natural. apply iterative_proper_iter; intros a'. unfold cat, Cat_Kleisli. - unfold internalize; destruct (f a') eqn:EQf'; cbn. + unfold internalize; cbn. rewrite! bind_bind. apply Proper_bind; [reflexivity |]. intros [xA | [xa | xb]]; unfold pure; cbn; rewrite !bind_ret_l; cbn; unfold cat, Cat_Kleisli; cbn. - rewrite bind_ret_l; cbn; reflexivity. - - unfold id_, Id_Kleisli, pure; rewrite bind_ret_l; reflexivity. - - destruct (g xb); cbn; rewrite bind_bind. + - unfold id_, Id_Kleisli, pure; rewrite bind_bind, !bind_ret_l; reflexivity. + - cbn; rewrite bind_bind. apply Proper_bind; [reflexivity |]. intros [? | ?]; rewrite bind_ret_l; reflexivity. Qed. Lemma iter_dinatural_helper: - forall (a b c : Type) (f : Kleisli (eitherT A M) a (b + c)) (g : Kleisli (eitherT A M) b (a + c)), + forall (a b c : Type) (f : Kleisli (eitherT exn M) a (b + c)) (g : Kleisli (eitherT exn M) b (a + c)), internalize (f >>> case_ g inr_) >>> pure iso ⩯ internalize f >>> pure iso >>> case_ (internalize g >>> pure iso) inr_. Proof. destruct CM. intros a b c f g o. unfold cat, Cat_Kleisli, internalize; cbn. - repeat rewrite bind_bind. - destruct (f o) as [fo] eqn: EQ; cbn. + repeat rewrite bind_bind; cbn. unfold pure; cbn. apply Proper_bind; [reflexivity | intros [xA | [xa | xb]]]; cbn. - rewrite !bind_ret_l; reflexivity. - - destruct (g xa) as [gxa] eqn:EQ'; cbn. - rewrite bind_ret_l; cbn; rewrite EQ'; reflexivity. + - rewrite bind_ret_l; reflexivity. - rewrite !bind_ret_l; reflexivity. Qed. - Global Instance IterDinatural_eitherTM : IterDinatural (Kleisli (eitherT A M)) sum. + Global Instance IterDinatural_eitherTM : IterDinatural (Kleisli (eitherT exn M)) sum. Proof. destruct CM. unfold IterDinatural. - intros a b c f g o. + intros A B C f g a. unfold iter, Iter_eitherTM. cbn. eapply transitivity. eapply iterative_proper_iter. @@ -160,6 +183,7 @@ Section Either. unfold cat, Cat_Kleisli. rewrite bind_bind. unfold internalize. cbn. + do 2 red. apply Proper_bind. - reflexivity. - unfold pure; cbn; intros [xA | [xa | xb]]; cbn. @@ -167,13 +191,12 @@ Section Either. + rewrite bind_ret_l; cbn. eapply iterative_proper_iter. intros ?; rewrite !bind_bind. - destruct (g a0) eqn:EQ; cbn. apply Proper_bind; [reflexivity | intros [|[|]]]; cbn; rewrite !bind_ret_l; try reflexivity. + rewrite bind_ret_l; cbn. reflexivity. Qed. - Global Instance IterCodiagonal_eitherTM : IterCodiagonal (Kleisli (eitherT A M)) sum. + Global Instance IterCodiagonal_eitherTM : IterCodiagonal (Kleisli (eitherT exn M)) sum. Proof. destruct CM. unfold IterCodiagonal. @@ -186,24 +209,36 @@ Section Either. unfold internalize; cbn. reflexivity. eapply transitivity. - eapply iterative_proper_iter. - apply iterative_natural. - rewrite iterative_codiagonal. - eapply iterative_proper_iter. - rewrite cat_assoc, bimap_case, cat_id_l, cat_id_r. - unfold internalize. - intros o'; cbn. - unfold cat, Cat_Kleisli; rewrite !bind_bind; destruct (f o'); cbn. - apply Proper_bind; [reflexivity | intros [| [|]]]. - unfold pure; rewrite !bind_ret_l; reflexivity. - unfold pure; cbn; rewrite !bind_ret_l; reflexivity. - unfold pure; cbn; rewrite !bind_ret_l; reflexivity. + eapply iterative_proper_iter. + apply iterative_natural. + rewrite iterative_codiagonal. + eapply iterative_proper_iter. + rewrite cat_assoc, bimap_case, cat_id_l, cat_id_r. + unfold internalize. + intros o'; cbn. + unfold cat, Cat_Kleisli; cbn; rewrite !bind_bind; cbn. + apply Proper_bind; [reflexivity | intros [| [|]]]. + unfold pure; rewrite !bind_ret_l; reflexivity. + unfold pure; cbn; rewrite !bind_ret_l; reflexivity. + unfold pure; cbn; rewrite !bind_ret_l; reflexivity. Qed. - Global Instance Iterative_eitherTM : Iterative (Kleisli (eitherT A M)) sum. + Global Instance Iterative_eitherTM : Iterative (Kleisli (eitherT exn M)) sum. Proof. constructor; typeclasses eauto. Qed. -End Either. +End Iter_Either. + +(* Section Interpretable_Either. *) + +(* Variable M : Type -> Type. *) +(* Variable exn : Type. *) +(* Context {EQM : EqM M}. *) +(* Context {HM: Monad M}. *) +(* Context {HEQP: @EqMProps M _ EQM}. *) +(* Context {ML: @MonadLaws M _ HM}. *) +(* Context {IM: MonadIter M}. *) +(* Context {CM: Iterative (Kleisli M) sum}. *) + diff --git a/theories/Basics/MonadState.v b/theories/Basics/MonadState.v index 921658e7..2e73e933 100644 --- a/theories/Basics/MonadState.v +++ b/theories/Basics/MonadState.v @@ -3,9 +3,6 @@ From Coq Require Import Setoid Morphisms. -From ExtLib Require Import - Structures.Monad. - From ITree Require Import Basics.Basics Basics.Category @@ -13,12 +10,27 @@ From ITree Require Import Basics.CategoryKleisliFacts Basics.Monad. -Import ITree.Basics.Basics.Monads. Import CatNotations. +Import MonadNotation. Local Open Scope cat_scope. Local Open Scope cat. +Local Open Scope monad_scope. + +Definition stateT (S: Type) (M: Type -> Type) (A : Type) : Type := + S -> M (prod S A). +Definition state (S A : Type) := S -> prod S A. + +Section Functor_State. + + Global Instance Functor_stateT {M} {Fm : Functor M} {S} : Functor (stateT S M) + := {| + fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s) + |}. + +End Functor_State. + +Section Monad_State. -Section State. Variable M : Type -> Type. Variable S : Type. Context {EQM : EqM M}. @@ -26,6 +38,14 @@ Section State. Context {HEQP: @EqMProps M _ EQM}. Context {ML: @MonadLaws M _ HM}. + Global Instance Monad_stateT : Monad (stateT S M) + := {| + ret _ a := fun s => ret (s, a) + ; bind _ _ t k := fun s => + sa <- t s ;; + k (snd sa) (fst sa) + |}. + Global Instance EqM_stateTM : EqM (stateT S M). Proof. exact (fun a => pointwise_relation _ eqm). @@ -40,7 +60,7 @@ Section State. - repeat red. intros. etransitivity; eauto. apply H. apply H0. Qed. - Instance MonadLaws_stateTM : @MonadLaws (stateT S M) _ _. + Global Instance MonadLaws_stateTM : @MonadLaws (stateT S M) _ _. Proof. constructor. - cbn. intros a b f x. @@ -66,7 +86,17 @@ Section State. apply H0. Qed. - Context {IM: Iter (Kleisli M) sum}. +End Monad_State. + +Section Iter_State. + + Variable M : Type -> Type. + Variable S : Type. + Context {EQM : EqM M}. + Context {HM: Monad M}. + Context {HEQP: @EqMProps M _ EQM}. + Context {ML: @MonadLaws M _ HM}. + Context {IM: MonadIter M}. Context {CM: Iterative (Kleisli M) sum}. Definition iso {a b:Type} (sab : S * (a + b)) : (S * a) + (S * b) := @@ -111,7 +141,6 @@ Section State. reflexivity. Qed. - Lemma internalize_pure {a b c} (f : Kleisli (stateT S M) a b) (g : S * b -> S * c) : internalize f >>> pure g ⩯ (internalize (f >>> (fun b s => ret (g (s,b))))). Proof. @@ -125,13 +154,9 @@ Section State. unfold pure. reflexivity. Qed. - - Global Instance Iter_stateTM : Iter (Kleisli (stateT S M)) sum. - Proof. - exact - (fun (a b : Type) (f : a -> S -> M (S * (a + b))) (x:a) (s:S) => - iter ((internalize f) >>> (pure iso)) (s, x)). - Defined. + Global Instance Iter_stateTM : MonadIter (stateT S M) := + fun a b (body: b -> S -> M (S * (b + a))) x s => + iter ((internalize body) >>> (pure iso)) (s, x). Global Instance Proper_Iter_stateTM : forall a b, @Proper (Kleisli (stateT S M) a (a + b) -> (Kleisli (stateT S M) a b)) (eq2 ==> eq2) iter. Proof. @@ -149,43 +174,38 @@ Section State. Global Instance IterUnfold_stateTM : IterUnfold (Kleisli (stateT S M)) sum. Proof. - destruct CM. - unfold IterUnfold. - intros a b f. - repeat red. - intros a0 s. - unfold cat, Cat_Kleisli. - unfold iter, Iter_stateTM. - rewrite iterative_unfold. (* SAZ: why isn't iter_unfold exposed here? *) - unfold cat, Cat_Kleisli. - simpl. - rewrite bind_bind. - apply Proper_bind. - + reflexivity. - + repeat red. destruct a1 as [s' [x | y]]; simpl. - * unfold pure. rewrite bind_ret_l. - reflexivity. - * unfold pure. rewrite bind_ret_l. - reflexivity. + (* destruct CM. *) + unfold IterUnfold, CategoryOps.iter, Iter_Kleisli, iter, Iter_stateTM. + intros A B f a s. + rewrite iter_monad_to_cat. + rw_pointed_l iter_unfold. + unfold cat, Cat_Kleisli. + simpl. + rewrite bind_bind. + apply Proper_bind. + + reflexivity. + + intros [? [? | ?]]; simpl. + * unfold pure. rewrite bind_ret_l. + reflexivity. + * unfold pure. rewrite bind_ret_l. + reflexivity. Qed. Global Instance IterNatural_stateTM : IterNatural (Kleisli (stateT S M)) sum. Proof. destruct CM. - unfold IterNatural. - intros a b c f g. - repeat red. - intros a0 s. + intros A B C f g a s. + unfold CategoryOps.iter, Iter_Kleisli, iter, Iter_stateTM. setoid_rewrite iterative_natural. apply iterative_proper_iter. repeat red. - destruct a1. + intros []. unfold cat, Cat_Kleisli. cbn. rewrite! bind_bind. apply Proper_bind. - reflexivity. - - repeat red. destruct a2 as [s' [x | y]]; simpl. + - repeat red. intros [s' [x | y]]; simpl. + unfold pure. rewrite bind_ret_l. cbn. unfold cat, Cat_Kleisli. cbn. rewrite bind_bind. @@ -198,7 +218,7 @@ Section State. rewrite bind_bind. apply Proper_bind. * reflexivity. - * repeat red. destruct a2. + * repeat red. intros []. cbn. rewrite bind_ret_l. reflexivity. Qed. @@ -357,4 +377,4 @@ Section State. typeclasses eauto. Qed. -End State. +End Iter_State. diff --git a/theories/Events/State.v b/theories/Events/State.v index ca262519..414153a5 100644 --- a/theories/Events/State.v +++ b/theories/Events/State.v @@ -9,6 +9,7 @@ From ExtLib Require Import From ITree Require Import Basics.Basics + Basics.MonadState Basics.CategoryOps Basics.CategoryKleisli Core.ITreeDefinition diff --git a/tutorial/Asm.v b/tutorial/Asm.v index 528ec2da..edbd95e0 100644 --- a/tutorial/Asm.v +++ b/tutorial/Asm.v @@ -25,6 +25,7 @@ From ITree Require Import ITreeMonad Basics.Monad Basics.MonadEither + Basics.MonadState Basics.CategorySub Events.State Events.StateFacts. @@ -78,8 +79,6 @@ Inductive block {label : Type} : Type := | bbb (_ : branch label). Global Arguments block _ : clear implicits. - - (** A piece of code should expose the set of labels allowing to enter into it, as well as the set of outer labels it might jump to. To this end, [bks] represents a collection of blocks labeled by [F A], with branches in [F B]. @@ -354,10 +353,28 @@ Definition run_asm (p: asm 1 0) := interp_asm (denote_asm p Fin.f0) empty empty. (* SAZ: Should some of thes notions of equivalence be put into the library? SAZ: Should this be stated in terms of ktree ? *) + +Axiom fold: forall E (r b: Type), (itree E r -> b -> b) -> itree E r -> b -> b. + +Definition interp {E M : Type -> Type} + {FM : Functor M} {MM : Monad M} {IM : MonadIter M} + (h : E ~> M) : + itree E ~> M. := fun R => + iter (fun t => + match observe t with + | RetF r => ret (inr r) + | TauF t => ret (inl t) + | VisF e k => fmap (fun x => inl (k x)) (h _ e) + end). +(* TODO: this does a map, and aloop does a bind. We could fuse those + by giving aloop a continuation to compose its bind with. + (coyoneda...) *) + + (** The definition [interp_asm] also induces a notion of equivalence (open) _asm_ programs, which is just the equivalence of the ktree category *) Definition eq_asm_denotations {E A B} (t1 t2 : Kleisli (eitherT value (itree (Reg +' Memory +' E))) A B) : Prop := - forall a mem regs, interp_asm (t1 a) mem regs ≈ interp_asm (t2 a) mem regs. + forall a, eqm (interp_asm (t1 a)) (interp_asm (t2 a)). Definition eq_asm {A B} (p1 p2 : asm A B) : Prop := eq_asm_denotations (denote_asm p1) (denote_asm p2). @@ -381,8 +398,21 @@ Section InterpAsmProperties. (* Qed. *) (** [interp_asm] commutes with [Ret]. *) + Lemma interp_asm_ret: forall {R} (r: R), + eqm (interp_asm (E := E') (ret (m:= eitherT _ _) r)) + (ret (m := stateT _ _) r). + Proof. + unfold interp_asm, interp_either_map. + intros R r regs mem. + unfold ret at 1, Monad_eitherT. + unfold eqm. unfold EqM_eitherTM. + replace {| unEitherT := ret (m := itree E) (inr r) |} with (ret (m := eitherT _ _) r). + rewrite interp_ret, 2 interp_state_ret. + reflexivity. + Qed. + Lemma interp_asm_ret: forall {R} (r: R) (regs : registers) (mem: memory), - @eutt E' _ _ eq (interp_asm (ret (m:= eitherT _ _) r) mem regs) + @eutt E' _ _ eq (interp_asm (ret (m:= eitherT _ _) r) regs mem) (ret (mem, (regs, inr r))). Proof. unfold interp_asm, interp_map. From 2c9ae4035fe174c2b7150a456eaa6043bcf265d3 Mon Sep 17 00:00:00 2001 From: Yannick Date: Tue, 7 Apr 2020 20:26:08 -0400 Subject: [PATCH 7/8] Getting back to being able to work in Asm.v --- _CoqConfig | 5 ++++ theories/Basics/Monad.v | 26 +++++++------------ theories/Basics/MonadEither.v | 5 ++-- theories/Basics/MonadState.v | 1 + theories/Core/ITreeDefinition.v | 6 ++--- theories/Core/KTreeFacts.v | 2 +- theories/Events/Dependent.v | 3 ++- theories/Events/Map.v | 7 ++---- theories/Events/MapDefault.v | 14 ++++++----- theories/Events/MapDefaultFacts.v | 32 ++++++++++++----------- theories/Events/State.v | 7 ++---- theories/Events/StateFacts.v | 39 ++++++++++++++-------------- theories/Events/Writer.v | 11 +++++--- theories/Interp/Handler.v | 2 +- theories/Interp/HandlerFacts.v | 2 +- theories/Interp/Interp.v | 6 ++--- theories/Interp/InterpEither.v | 42 ++----------------------------- theories/Interp/InterpFacts.v | 4 +-- theories/Interp/Recursion.v | 2 +- theories/Interp/TranslateFacts.v | 4 +-- tutorial/Asm.v | 9 +------ 21 files changed, 91 insertions(+), 138 deletions(-) diff --git a/_CoqConfig b/_CoqConfig index 112ca51d..9db2ee8f 100644 --- a/_CoqConfig +++ b/_CoqConfig @@ -11,8 +11,13 @@ theories/Basics/CategoryTheory.v theories/Basics/CategoryFacts.v theories/Basics/CategorySub.v theories/Basics/CategoryFunctor.v +theories/Basics/Applicative.v +theories/Basics/Functor.v theories/Basics/Monad.v +theories/Basics/MonadId.v theories/Basics/MonadState.v +theories/Basics/MonadEither.v +theories/Basics/MonadWriter.v theories/Basics/CategoryKleisli.v theories/Basics/CategoryKleisliFacts.v theories/Basics/Function.v diff --git a/theories/Basics/Monad.v b/theories/Basics/Monad.v index 46757ee3..82435678 100644 --- a/theories/Basics/Monad.v +++ b/theories/Basics/Monad.v @@ -11,20 +11,11 @@ From ITree Require Import (* end hide *) Set Primitive Projections. -(* Set Implicit Arguments. *) -(* Set Strict Implicit. *) -(* Set Universe Polymorphism. *) +Set Universe Polymorphism. Set Implicit Arguments. Set Strict Implicit. -Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type := - { fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }. - -Module FunctorNotation. - Notation "f <$> x" := (@fmap _ _ _ _ f x) (at level 52, left associativity). -End FunctorNotation. - Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := { ret : forall {t : Type@{d}}, t -> m t ; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u @@ -35,7 +26,7 @@ Class EqM (m:Type -> Type) : Type := Class EqMProps (m:Type -> Type) `{Monad m} `{EqM m} := eqm_equiv :> forall a, Equivalence (eqm a). - +Arguments EqMProps m {_ _}. Arguments eqm {m _ _}. Infix "≈" := eqm (at level 70) : monad_scope. @@ -118,6 +109,7 @@ Section MonadLaws. End MonadLaws. +Arguments MonadLaws m {_ _}. Arguments bind_ret_l {m _ _ _}. Arguments bind_ret_r {m _ _ _}. Arguments bind_bind {m _ _ _}. @@ -169,7 +161,7 @@ Section MonadTriggerable. Context {MM: Monad M}. Context {MM': Monad M'}. Context {EqMM': @EqM M'}. - Context {IM: MonadIter M}. + Context {IM: MonadIter M}. Context {IM': MonadIter M'}. (** @@ -177,7 +169,7 @@ Section MonadTriggerable. monadic effectful computation are dubbed "Triggerable". *) - Class Triggerable := trigger: forall (E: Type -> Type), E ~> M. + Class Triggerable (E: Type -> Type) := trigger: E ~> M. (* The correctness of this operation, i.e. its minimality, is expressed with respect to a notion of interpretation of monads. @@ -188,11 +180,11 @@ Section MonadTriggerable. Class Interpretable := interp: forall (E: Type -> Type) (h: E ~> M'), M ~> M'. - Class InterpCorrect {InterpMM': Interpretable} {TrigM: Triggerable}: Prop := + Class InterpCorrect E {InterpMM': Interpretable} {TrigM: Triggerable E}: Prop := { - interp_monad_hom E h :> MonadHom (interp E h); - interp_iter_hom E h :> IterHom (interp E h); - interp_trigger E h T (e: E T): interp E h (trigger _ _ e) ≈ h _ e + interp_monad_hom h :> MonadHom (interp E h); + interp_iter_hom h :> IterHom (interp E h); + interp_trigger h T (e: E T): interp E h (trigger _ e) ≈ h _ e }. End MonadTriggerable. diff --git a/theories/Basics/MonadEither.v b/theories/Basics/MonadEither.v index 6eb834ce..4d0f8952 100644 --- a/theories/Basics/MonadEither.v +++ b/theories/Basics/MonadEither.v @@ -7,6 +7,7 @@ From ITree Require Import Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts + Basics.Functor Basics.Monad. Import CatNotations. @@ -91,8 +92,8 @@ Section Iter_Either. Variable exn : Type. Context {EQM : EqM M}. Context {HM: Monad M}. - Context {HEQP: @EqMProps M _ EQM}. - Context {ML: @MonadLaws M _ HM}. + Context {HEQP: @EqMProps M HM EQM}. + Context {ML: @MonadLaws M EQM HM}. Context {IM: MonadIter M}. Context {CM: Iterative (Kleisli M) sum}. diff --git a/theories/Basics/MonadState.v b/theories/Basics/MonadState.v index 2e73e933..6a32f83d 100644 --- a/theories/Basics/MonadState.v +++ b/theories/Basics/MonadState.v @@ -8,6 +8,7 @@ From ITree Require Import Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts + Basics.Functor Basics.Monad. Import CatNotations. diff --git a/theories/Core/ITreeDefinition.v b/theories/Core/ITreeDefinition.v index d551b351..67061f88 100644 --- a/theories/Core/ITreeDefinition.v +++ b/theories/Core/ITreeDefinition.v @@ -1,12 +1,9 @@ (** * Interaction trees: core definitions *) (* begin hide *) -Require Import ExtLib.Structures.Functor. -Require Import ExtLib.Structures.Applicative. -Require Import ExtLib.Structures.Monad. Require Import Program.Tactics. -From ITree Require Import Basics. +From ITree Require Import Basics Monad Applicative Functor. Set Implicit Arguments. Set Contextual Implicit. @@ -212,6 +209,7 @@ Definition map {E R S} (f : R -> S) (t : itree E R) : itree E S := (** Atomic itrees triggering a single event. *) Definition trigger {E : Type -> Type} : E ~> itree E := fun R e => Vis e (fun x => Ret x). +Instance trigger_itree {E: Type -> Type} : Triggerable (itree E) E := trigger. (** Ignore the result of a tree. *) Definition ignore {E R} : itree E R -> itree E unit := diff --git a/theories/Core/KTreeFacts.v b/theories/Core/KTreeFacts.v index 031eecf9..8d78e1ba 100644 --- a/theories/Core/KTreeFacts.v +++ b/theories/Core/KTreeFacts.v @@ -152,7 +152,7 @@ Lemma unfold_iter_ktree {E A B} (f : ktree E A (A + B)) (a0 : A) : | inr b => Ret b end. Proof. - unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree, cat. + unfold iter, Iter_Kleisli, Monad.iter, MonadIter_itree, cat. rewrite unfold_iter; cbn. eapply eqit_bind; try reflexivity. Qed. diff --git a/theories/Events/Dependent.v b/theories/Events/Dependent.v index 3c6b5fe4..764de262 100644 --- a/theories/Events/Dependent.v +++ b/theories/Events/Dependent.v @@ -16,11 +16,12 @@ (* begin hide *) From ITree Require Import Basics.Basics + Basics.Monad + Basics.MonadId Core.ITreeDefinition Indexed.Sum Core.Subevent. -Import Basics.Basics.Monads. (* end hide *) Variant depE {I : Type} (F : I -> Type) : Type -> Type := diff --git a/theories/Events/Map.v b/theories/Events/Map.v index d6dbade3..fcc58f6f 100644 --- a/theories/Events/Map.v +++ b/theories/Events/Map.v @@ -8,14 +8,12 @@ From Coq Require Import String List. Import ListNotations. -From ExtLib Require Import - Core.RelDec. - From ExtLib.Structures Require - Functor Monoid Maps. + Monoid Maps. From ITree Require Import Basics.Basics + Basics.MonadState Basics.CategoryOps Core.ITreeDefinition Indexed.Sum @@ -23,7 +21,6 @@ From ITree Require Import Interp.Interp Events.State. -Import ITree.Basics.Basics.Monads. (* end hide *) Section Map. diff --git a/theories/Events/MapDefault.v b/theories/Events/MapDefault.v index ab55564d..09e0f37c 100644 --- a/theories/Events/MapDefault.v +++ b/theories/Events/MapDefault.v @@ -8,10 +8,13 @@ From ExtLib Require Import Core.RelDec. From ExtLib.Structures Require - Functor Monoid Maps. + Monoid Maps. From ITree Require Import Basics.Basics + Basics.Functor + Basics.Monad + Basics.MonadState Basics.CategoryOps Core.ITreeDefinition Indexed.Sum @@ -19,7 +22,6 @@ From ITree Require Import Interp.Interp Events.State. -Import ITree.Basics.Basics.Monads. (* end hide *) Section Map. @@ -35,7 +37,7 @@ Section Map. Arguments Insert {d}. Arguments LookupDef {d}. Arguments Remove {d}. - + Definition insert {E d} `{(mapE d) -< E} : K -> V -> itree E unit := embed Insert. Definition lookup_def {E d} `{(mapE d) -< E} : K -> itree E V := embed LookupDef. Definition remove {E d} `{(mapE d) -< E} : K -> itree E unit := embed Remove. @@ -50,7 +52,7 @@ Section Map. | Some v' => v' | None => d end. - + Definition handle_map {E d} : mapE d ~> stateT map (itree E) := fun _ e env => match e with @@ -60,7 +62,7 @@ Section Map. end. (* SAZ: I think that all of these [run_foo] functions should be renamed - [interp_foo]. That would be more consistent with the idea that + [interp_foo]. That would be more consistent with the idea that we define semantics by nested interpretation. Also, it seems a bit strange to define [interp_map] in terms of [interp_state]. *) @@ -73,7 +75,7 @@ Section Map. answers under [lookup_default] *) Definition eq_map (d:V) (m1 m2 : map) : Prop := forall k, lookup_default k d m1 = lookup_default k d m2. - + End Map. Arguments insert {K V E d _}. diff --git a/theories/Events/MapDefaultFacts.v b/theories/Events/MapDefaultFacts.v index 529866d5..c0c0f1da 100644 --- a/theories/Events/MapDefaultFacts.v +++ b/theories/Events/MapDefaultFacts.v @@ -13,12 +13,15 @@ From ExtLib Require Import Core.RelDec. From ExtLib.Structures Require - Functor Monoid Maps. + Monoid Maps. From Paco Require Import paco. From ITree Require Import Basics.Basics + Basics.Monad + Basics.Functor + Basics.MonadState Basics.CategoryOps ITree ITreeFacts @@ -28,7 +31,6 @@ From ITree Require Import Events.StateFacts Events.MapDefault. -Import ITree.Basics.Basics.Monads. Import Structures.Maps. (* end hide *) @@ -45,7 +47,7 @@ Section MapFacts. Lemma lookup_add_eq: forall k v s, lookup k (add k v s) = Some v. Proof. intros. - rewrite mapsto_lookup; apply mapsto_add_eq. + rewrite mapsto_lookup; apply mapsto_add_eq. Unshelve. 2: typeclasses eauto. Qed. @@ -101,7 +103,7 @@ Section MapFacts. Global Instance eq_map_refl {d} : Reflexive (@eq_map _ _ _ _ d). Proof. red. intros. unfold eq_map. tauto. - Qed. + Qed. Global Instance eq_map_sym {d} : Symmetric (@eq_map _ _ _ _ d). Proof. @@ -113,7 +115,7 @@ Section MapFacts. Global Instance eq_map_trans {d} : Transitive (@eq_map _ _ _ _ d). Proof. - repeat intro. + repeat intro. unfold eq_map in *. rewrite H. rewrite H0. reflexivity. Qed. @@ -123,7 +125,7 @@ Section MapFacts. Context {R1 R2 : Type}. Variable RR : R1 -> R2 -> Prop. - Definition map_default_eq d {E} + Definition map_default_eq d {E} : (stateT map (itree E) R1) -> (stateT map (itree E) R2) -> Prop := fun t1 t2 => forall s1 s2, (@eq_map _ _ _ _ d) s1 s2 -> eutt (prod_rel (@eq_map _ _ _ _ d) RR) (t1 s1) (t2 s2). @@ -141,7 +143,7 @@ Section MapFacts. rewrite 2 lookup_add_eq; reflexivity. - unfold lookup_default in *. rewrite 2 lookup_add_neq; auto. - Qed. + Qed. Lemma eq_map_remove: forall (d : V) (s1 s2 : map) (k : K), (@eq_map _ _ _ _ d) s1 s2 -> (@eq_map _ _ _ _ d) (remove k s1) (remove k s2). @@ -154,8 +156,8 @@ Section MapFacts. - rewrite 2 lookup_remove_neq; auto. apply H. Qed. - - Lemma handle_map_eq : + + Lemma handle_map_eq : forall d E X (s1 s2 : map) (m : mapE K d X), (@eq_map _ _ _ _ d) s1 s2 -> eutt (prod_rel (@eq_map _ _ _ _ d) eq) (handle_map m s1) ((handle_map m s2) : itree E (map * X)). @@ -175,8 +177,8 @@ Section MapFacts. apply handle_map_eq. assumption. Qed. - - + + (* This lemma states that the operations provided by [handle_map] respect the equivalence on the underlying map interface *) Lemma interp_map_id d {E X} (t : itree (mapE K d +' E) X) : @@ -202,7 +204,7 @@ Section MapFacts. gstep; constructor. gbase. apply CH. assumption. Qed. - + Global Instance interp_map_proper {R E d} {RR : R -> R -> Prop} : Proper ((eutt RR) ==> (@map_default_eq _ _ RR d E)) (@interp_map _ _ _ _ E d R). Proof. @@ -212,7 +214,7 @@ Section MapFacts. einit. ecofix CH. intros. - rewrite! unfold_interp_state. + rewrite! unfold_interp_state. punfold H0. red in H0. revert s1 s2 H1. induction H0; intros; subst; simpl; pclearbot. @@ -225,7 +227,7 @@ Section MapFacts. destruct e. apply handle_map_eq. assumption. unfold pure_state. pstep. econstructor. intros. constructor. pfold. econstructor. constructor; auto. - } + } intros. inversion H. subst. estep; constructor. ebase. @@ -234,5 +236,5 @@ Section MapFacts. - rewrite tau_euttge, unfold_interp_state. eauto. Qed. - + End MapFacts. diff --git a/theories/Events/State.v b/theories/Events/State.v index 414153a5..52a7e409 100644 --- a/theories/Events/State.v +++ b/theories/Events/State.v @@ -3,12 +3,10 @@ (** Events to read and update global state. *) (* begin hide *) -From ExtLib Require Import - Structures.Functor - Structures.Monad. - From ITree Require Import Basics.Basics + Basics.Functor + Basics.Monad Basics.MonadState Basics.CategoryOps Basics.CategoryKleisli @@ -18,7 +16,6 @@ From ITree Require Import Core.Subevent Interp.Interp. -Import ITree.Basics.Basics.Monads. Import ITreeNotations. Open Scope itree_scope. diff --git a/theories/Events/StateFacts.v b/theories/Events/StateFacts.v index db612636..192347d2 100644 --- a/theories/Events/StateFacts.v +++ b/theories/Events/StateFacts.v @@ -11,6 +11,8 @@ From Paco Require Import paco. From ITree Require Import Basics.Basics + Basics.Monad + Basics.MonadState Basics.Category Basics.CategoryKleisli Basics.Monad @@ -25,12 +27,10 @@ From ITree Require Import Interp.RecursionFacts Events.State. -Import ITree.Basics.Basics.Monads. Import ITreeNotations. Open Scope itree_scope. -Import Monads. (* end hide *) Definition _interp_state {E F S R} @@ -42,23 +42,24 @@ Definition _interp_state {E F S R} | VisF e k => f _ e s >>= (fun sx => Tau (interp_state f (k (snd sx)) (fst sx))) end. -Lemma unfold_interp_state {E F S R} (h : E ~> Monads.stateT S (itree F)) +Lemma unfold_interp_state {E F S R} (h : E ~> stateT S (itree F)) (t : itree E R) s : eq_itree eq (interp_state h t s) (_interp_state h (observe t) s). Proof. - unfold interp_state, interp, Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree; cbn. + unfold interp_state, interp, iter, Iter_stateTM, iter, MonadIter_itree, internalize; cbn. rewrite unfold_iter; cbn. + rewrite bind_bind. destruct observe; cbn. - rewrite 2 bind_ret_l. reflexivity. - rewrite 2 bind_ret_l. reflexivity. - - rewrite bind_map, bind_bind; cbn. setoid_rewrite bind_ret_l. + - rewrite bind_map. cbn. setoid_rewrite bind_ret_l. apply eqit_bind; reflexivity. Qed. -Instance eq_itree_interp_state {E F S R} (h : E ~> Monads.stateT S (itree F)) : +Instance eq_itree_interp_state {E F S R} (h : E ~> stateT S (itree F)) : Proper (eq_itree eq ==> eq ==> eq_itree eq) (@interp_state _ _ _ _ _ _ h R). Proof. @@ -83,7 +84,7 @@ Proof. Qed. Lemma interp_state_vis {E F : Type -> Type} {S T U : Type} - (e : E T) (k : T -> itree E U) (h : E ~> Monads.stateT S (itree F)) (s : S) + (e : E T) (k : T -> itree E U) (h : E ~> stateT S (itree F)) (s : S) : interp_state h (Vis e k) s ≅ h T e s >>= fun sx => Tau (interp_state h (k (snd sx)) (fst sx)). Proof. @@ -91,14 +92,14 @@ Proof. Qed. Lemma interp_state_tau {E F : Type -> Type} S {T : Type} - (t : itree E T) (h : E ~> Monads.stateT S (itree F)) (s : S) + (t : itree E T) (h : E ~> stateT S (itree F)) (s : S) : interp_state h (Tau t) s ≅ Tau (interp_state h t s). Proof. rewrite unfold_interp_state; reflexivity. Qed. Lemma interp_state_trigger {E F : Type -> Type} {R S : Type} - (e : E R) (f : E ~> Monads.stateT S (itree F)) (s : S) + (e : E R) (f : E ~> stateT S (itree F)) (s : S) : (interp_state f (ITree.trigger e) s) ≅ (f _ e s >>= fun x => Tau (Ret x)). Proof. unfold ITree.trigger. rewrite interp_state_vis. @@ -134,7 +135,7 @@ Proof. Qed. Instance eutt_interp_state {E F: Type -> Type} {S : Type} - (h : E ~> Monads.stateT S (itree F)) R RR : + (h : E ~> stateT S (itree F)) R RR : Proper (eutt RR ==> eq ==> eutt (prod_rel eq RR)) (@interp_state E (itree F) S _ _ _ h R). Proof. repeat intro. subst. revert_until R. @@ -152,7 +153,7 @@ Proof. Qed. Instance eutt_interp_state_eq {E F: Type -> Type} {S : Type} - (h : E ~> Monads.stateT S (itree F)) R : + (h : E ~> stateT S (itree F)) R : Proper (eutt eq ==> eq ==> eutt eq) (@interp_state E (itree F) S _ _ _ h R). Proof. repeat intro. subst. revert_until R. @@ -173,7 +174,7 @@ Qed. Lemma eutt_interp_state_aloop {E F S I I' A A'} (RA : A -> A' -> Prop) (RI : I -> I' -> Prop) (RS : S -> S -> Prop) - (h : E ~> Monads.stateT S (itree F)) + (h : E ~> stateT S (itree F)) (t1 : I -> itree E (I + A)) (t2 : I' -> itree E (I' + A')): (forall i i' s1 s2, RS s1 s2 -> RI i i' -> @@ -199,7 +200,7 @@ Qed. Lemma eutt_interp_state_iter {E F S A A' B B'} (RA : A -> A' -> Prop) (RB : B -> B' -> Prop) (RS : S -> S -> Prop) - (h : E ~> Monads.stateT S (itree F)) + (h : E ~> stateT S (itree F)) (t1 : A -> itree E (A + B)) (t2 : A' -> itree E (A' + B')) : (forall ca ca' s1 s2, RS s1 s2 -> @@ -209,14 +210,14 @@ Lemma eutt_interp_state_iter {E F S A A' B B'} (interp_state h (t2 ca') s2)) -> (forall a a' s1 s2, RS s1 s2 -> RA a a' -> eutt (fun a b => RS (fst a) (fst b) /\ RB (snd a) (snd b)) - (interp_state h (iter (C := ktree _) t1 a) s1) - (interp_state h (iter (C := ktree _) t2 a') s2)). + (interp_state h (CategoryOps.iter (C := ktree _) t1 a) s1) + (interp_state h (CategoryOps.iter (C := ktree _) t2 a') s2)). Proof. apply eutt_interp_state_aloop. Qed. Lemma eutt_interp_state_loop {E F S A B C} (RS : S -> S -> Prop) - (h : E ~> Monads.stateT S (itree F)) + (h : E ~> stateT S (itree F)) (t1 t2 : C + A -> itree E (C + B)) : (forall ca s1 s2, RS s1 s2 -> eutt (fun a b => RS (fst a) (fst b) /\ snd a = snd b) @@ -255,9 +256,9 @@ Lemma interp_state_iter {E F } S (f : E ~> stateT S (itree F)) {I A} (t' : I -> stateT S (itree F) (I + A)) (EQ_t : forall i, state_eq (State.interp_state f (t i)) (t' i)) : forall i, state_eq (State.interp_state f (ITree.iter t i)) - (Basics.iter t' i). + (iter t' i). Proof. - unfold Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree in *; cbn. + unfold iter, Iter_stateTM, iter, MonadIter_itree in *; cbn. ginit. gcofix CIH; intros i s. rewrite 2 unfold_iter; cbn. rewrite !bind_bind. @@ -275,7 +276,7 @@ Qed. Lemma interp_state_iter' {E F } S (f : E ~> stateT S (itree F)) {I A} (t : I -> itree E (I + A)) : forall i, state_eq (State.interp_state f (ITree.iter t i)) - (Basics.iter (fun i => State.interp_state f (t i)) i). + (iter (fun i => State.interp_state f (t i)) i). Proof. eapply interp_state_iter. intros i. diff --git a/theories/Events/Writer.v b/theories/Events/Writer.v index 1f2e208f..328b3005 100644 --- a/theories/Events/Writer.v +++ b/theories/Events/Writer.v @@ -11,13 +11,17 @@ From Coq Require Import Import ListNotations. From ExtLib Require Import - Structures.Functor - Structures.Monad +(* Structures.Functor *) +(* Structures.Monad *) Structures.Monoid. From ITree Require Import Basics.Basics Basics.CategoryOps + Basics.Functor + Basics.Monad + Basics.MonadState + Basics.MonadWriter Core.ITreeDefinition Indexed.Sum Core.Subevent @@ -25,7 +29,6 @@ From ITree Require Import Interp.Handler Events.State. -Import Basics.Basics.Monads. (* end hide *) (** Event to output values of type [W]. *) @@ -68,7 +71,7 @@ Definition handle_writer {W E} (Monoid_W : Monoid W) : writerE W ~> stateT W (itree E) := fun _ e s => match e with - | Tell w => Ret (monoid_plus Monoid_W s w, tt) + | Tell w => Ret (monoid_plus Monoid_W s w, tt) end. Definition run_writer {W E} (Monoid_W : Monoid W) diff --git a/theories/Interp/Handler.v b/theories/Interp/Handler.v index 3084fbb8..f8195788 100644 --- a/theories/Interp/Handler.v +++ b/theories/Interp/Handler.v @@ -9,6 +9,7 @@ From Coq Require Import From ITree Require Import Basics.Basics + Basics.Monad Basics.Category Core.ITreeDefinition Eq.Eq @@ -18,7 +19,6 @@ From ITree Require Import Interp.Interp Interp.Recursion. -Import ITree.Basics.Basics.Monads. Import ITreeNotations. Open Scope itree_scope. diff --git a/theories/Interp/HandlerFacts.v b/theories/Interp/HandlerFacts.v index 7071d10e..0e70703b 100644 --- a/theories/Interp/HandlerFacts.v +++ b/theories/Interp/HandlerFacts.v @@ -10,6 +10,7 @@ From Paco Require Import paco. From ITree Require Import Basics.Basics + Basics.Monad Basics.Category Core.ITreeDefinition Eq.Eq @@ -21,7 +22,6 @@ From ITree Require Import Interp.InterpFacts Interp.RecursionFacts. -Import ITree.Basics.Basics.Monads. Import ITreeNotations. Open Scope itree_scope. diff --git a/theories/Interp/Interp.v b/theories/Interp/Interp.v index cd59dde8..defc14d1 100644 --- a/theories/Interp/Interp.v +++ b/theories/Interp/Interp.v @@ -30,12 +30,10 @@ *) (* begin hide *) -From ExtLib Require Import - Structures.Functor - Structures.Monad. - From ITree Require Import Basics.Basics + Basics.Monad + Basics.Functor Core.ITreeDefinition Indexed.Relation. (* end hide *) diff --git a/theories/Interp/InterpEither.v b/theories/Interp/InterpEither.v index 70e7e820..5cb967c0 100644 --- a/theories/Interp/InterpEither.v +++ b/theories/Interp/InterpEither.v @@ -30,52 +30,14 @@ *) (* begin hide *) -From ExtLib Require Import - Structures.Functor - EitherMonad - Structures.Monad. - From ITree Require Import Basics.Basics + Basics.Monad + Basics.MonadEither Core.ITreeDefinition Indexed.Relation. (* end hide *) -(** ** Translate *) - -(** An event morphism [E ~> F] lifts to an itree morphism [itree E ~> itree F] - by applying the event morphism to every visible event. We call this - process _event translation_. - - Translation is a special case of interpretation: -[[ - translate h t ≈ interp (trigger ∘ h) t -]] - However this definition of [translate] yields strong bisimulations - more often than [interp]. - For example, [translate (id_ E) t ≅ id_ (itree E)]. -*) - -(** A plain event morphism [E ~> F] defines an itree morphism - [itree E ~> itree F]. *) -(* Definition translateF {E F R} (h : E ~> F) (rec: itree E R -> itree F R) (t : itreeF E R _) : itree F R := *) -(* match t with *) -(* | RetF x => Ret x *) -(* | TauF t => Tau (rec t) *) -(* | VisF e k => Vis (h _ e) (fun x => rec (k x)) *) -(* end. *) - -(* Definition translate {E F} (h : E ~> F) *) -(* : itree E ~> itree F *) -(* := fun R => cofix translate_ t := translateF h translate_ (observe t). *) - -(* Arguments translate {E F} h [T]. *) - -(** ** Interpret *) - -(** An event handler [E ~> M] defines a monad morphism - [itree E ~> M] for any monad [M] with a loop operator. *) - Definition interp_either {E M : Type -> Type} {A: Type} {FM : Functor M} {MM : Monad M} {IM : MonadIter M} (h : E ~> eitherT A M) : diff --git a/theories/Interp/InterpFacts.v b/theories/Interp/InterpFacts.v index 361984bd..898b5cd6 100644 --- a/theories/Interp/InterpFacts.v +++ b/theories/Interp/InterpFacts.v @@ -68,7 +68,7 @@ Definition _interp {E F R} (f : E ~> itree F) (ot : itreeF E R _) Lemma unfold_interp {E F R} {f : E ~> itree F} (t : itree E R) : interp f t ≅ (_interp f (observe t)). Proof. - unfold interp. unfold Basics.iter, MonadIter_itree. rewrite unfold_iter. + unfold interp. unfold Monad.iter, MonadIter_itree. rewrite unfold_iter. destruct (observe t); cbn; rewrite ?bind_ret_l, ?bind_map; reflexivity. Qed. @@ -349,7 +349,7 @@ Lemma interp_iter {E F} (f : E ~> itree F) {A B} (t : A -> itree E (A + B)) a0 : interp f (iter t a0) ≅ iter (C := ktree _) (fun a => interp f (t a)) a0. Proof. - unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree. + unfold iter, Iter_Kleisli, Monad.iter, MonadIter_itree. apply interp_iter'. reflexivity. Qed. diff --git a/theories/Interp/Recursion.v b/theories/Interp/Recursion.v index c6affc57..c4d7e1d6 100644 --- a/theories/Interp/Recursion.v +++ b/theories/Interp/Recursion.v @@ -5,7 +5,7 @@ From ITree Require Import Core.ITreeDefinition Indexed.Sum. -Import ITree.Basics.Basics.Monads. +Import ITree.Basics.Monad. Import ITreeNotations. Open Scope itree_scope. diff --git a/theories/Interp/TranslateFacts.v b/theories/Interp/TranslateFacts.v index 1e1e1b73..471e8b56 100644 --- a/theories/Interp/TranslateFacts.v +++ b/theories/Interp/TranslateFacts.v @@ -1,8 +1,8 @@ (** * Theorems about [Interp.translate] *) (* begin hide *) -From ExtLib Require - Structures.Monoid. +(* From ExtLib Require *) +(* Structures.Monoid. *) From ITree Require Import Basics.Basics diff --git a/tutorial/Asm.v b/tutorial/Asm.v index edbd95e0..6ffe270a 100644 --- a/tutorial/Asm.v +++ b/tutorial/Asm.v @@ -13,12 +13,6 @@ From Coq Require Import Setoid RelationClasses. -From ExtLib Require Import - Structures.Monad - EitherMonad - MonadTrans. - - (* SAZ: Should we add ITreeMonad to ITree? *) From ITree Require Import ITree ITreeFacts @@ -144,7 +138,6 @@ Section Denote. (** Once again, [asm] programs shall be denoted as [itree]s. *) (* begin hide *) - Import ExtLib.Structures.Monad. Import MonadNotation. Local Open Scope monad_scope. (* end hide *) @@ -162,7 +155,7 @@ Section Denote. Definition denote_operand (o : operand) : itree E value := match o with | Oimm v => Ret v - | Oreg v => trigger (GetReg v) + | Oreg v => ITree.trigger (GetReg v) end. (** Instructions offer no suprises either. *) From 0897a7c828808bd3991fd1dffaa6990c50cc8da3 Mon Sep 17 00:00:00 2001 From: Yannick Date: Sun, 12 Apr 2020 19:37:34 -0400 Subject: [PATCH 8/8] Maybe I went mad and we can use the old interp? --- theories/Basics/Monad.v | 4 ++ theories/Core/ITreeDefinition.v | 2 +- tutorial/Asm.v | 75 +++++++++++++-------------------- 3 files changed, 34 insertions(+), 47 deletions(-) diff --git a/theories/Basics/Monad.v b/theories/Basics/Monad.v index 51d388a7..098cb985 100644 --- a/theories/Basics/Monad.v +++ b/theories/Basics/Monad.v @@ -154,6 +154,8 @@ Section MonadHomomorphism. End MonadHomomorphism. +(* TO PLUG IN WHENEVER + Section MonadTriggerable. Local Open Scope monad_scope. @@ -190,6 +192,8 @@ Section MonadTriggerable. End MonadTriggerable. + *) + Import CatNotations. Local Open Scope cat_scope. Local Open Scope monad_scope. diff --git a/theories/Core/ITreeDefinition.v b/theories/Core/ITreeDefinition.v index 4d967ba3..6b4ba660 100644 --- a/theories/Core/ITreeDefinition.v +++ b/theories/Core/ITreeDefinition.v @@ -210,7 +210,7 @@ Definition map {E R S} (f : R -> S) (t : itree E R) : itree E S := (** Atomic itrees triggering a single event. *) Definition trigger {E : Type -> Type} : E ~> itree E := fun R e => Vis e (fun x => Ret x). -Instance trigger_itree {E: Type -> Type} : Triggerable (itree E) E := trigger. +(* Instance trigger_itree {E: Type -> Type} : Triggerable (itree E) E := trigger. *) (** Ignore the result of a tree. *) Definition ignore {E R} : itree E R -> itree E unit := diff --git a/tutorial/Asm.v b/tutorial/Asm.v index 6ffe270a..3c94be23 100644 --- a/tutorial/Asm.v +++ b/tutorial/Asm.v @@ -26,7 +26,6 @@ From ITree Require Import Require Import Fin Utils_tutorial. -Import Monads. (* end hide *) (** ** Syntax *) @@ -133,6 +132,10 @@ Inductive Exit : Type -> Type := Definition exit {E A} `{Exit -< E} : itree E A := vis Done (fun v => match v : void with end). +(* TO MOVE *) +(* Instance trigger' {E F: Type -> Type} `{E -< F} : Triggerable (eitherT value (itree F)) E := *) + (* fun _ e => Vis (subevent _ e) (fun x => ret (inr x)). *) + Section Denote. (** Once again, [asm] programs shall be denoted as [itree]s. *) @@ -155,10 +158,11 @@ Section Denote. Definition denote_operand (o : operand) : itree E value := match o with | Oimm v => Ret v - | Oreg v => ITree.trigger (GetReg v) + | Oreg v => trigger (GetReg v) end. (** Instructions offer no suprises either. *) + Print Instances Monad. Definition denote_instr (i : instr) : itree E unit := match i with | Imov d s => @@ -184,10 +188,14 @@ Section Denote. trigger (Store addr val) end. - Definition returns {B} r: eitherT value (itree E) B := mkEitherT (val <- trigger (GetReg r);; ret (inl val)). + Definition returns {B} r: eitherT value (itree E) B := val <- trigger (GetReg r);; ret (inl val). Notation tree_ret := (eitherT value (itree E)). + (* TO MOVE *) + Definition lift {m T} `{Monad m} {V} (c: m T): eitherT V m T := + bind c (fun x => ret (inr x)). + (** A [branch] returns the computed label whose set of possible values [B] is carried by the type of the branch. If the computation halts instead of branching, we return the [exit] tree. *) @@ -195,11 +203,10 @@ Section Denote. match b with | Bjmp l => ret l | Bbrz v y n => - lift - (val <- trigger (GetReg v) ;; - if val:nat then ret y else ret n) + val <- trigger (GetReg v) ;; + if val:nat then ret (inr y) else ret (inr n) | Bret r => returns r - | Bhalt => lift exit + | Bhalt => exit end. (** The denotation of a basic [block] shares the same type, returning the @@ -299,12 +306,11 @@ Definition h_memory {E : Type -> Type} `{mapE addr 0 -< E} : Definition registers := alist reg value. Definition memory := alist addr value. - (* Definition eitherT_stateT_commute {S A M R}: *) (* (stateT S (eitherT A M) R) -> (eitherT A (stateT S M) R). *) (* intros ?. *) -From ITree Require Import Interp.InterpEither. +(* From ITree Require Import Interp.InterpEither. *) (** The _asm_ interpreter takes as inputs a starting heap [mem] and register state [reg] and interprets an itree in two nested instances of the [map] variant of the state monad. To get this type to work out, we have to @@ -313,11 +319,14 @@ From ITree Require Import Interp.InterpEither. *) (* Should [eitherT] be on top of [itree E] or on the outside? *) +(* + Definition distribute {A B C: Type}: A * (B + C) -> A * B + A * C := fun '(a,bc) => match bc with | inl b => inl (a,b) | inr c => inr (a,c) end. + Definition interp_either_map {E K V Exc d map} `{M : Map K V map} : eitherT Exc (itree (@mapE K V d +' E)) ~> stateT map (eitherT (map * Exc) (itree E)) := @@ -337,6 +346,13 @@ Definition interp_asm {E A} let h := bimap h_reg (bimap h_memory (id_ E)) in let t' := interp_either' h _ t in fun mem regs => interp_either_map _ (interp_either_map _ t' mem) regs. + *) + +Definition interp_asm {E A} (t : itree (Reg +' Memory +' E) A) : + stateT registers (stateT memory (itree E)) A := + let h := bimap h_reg (bimap h_memory (id_ _)) in + let t' := interp h t in + fun mem regs => interp_map (interp_map t' mem) regs. (** We can then define an evaluator for closed assembly programs by interpreting both store and heap events into two instances of [mapE], and running them @@ -347,27 +363,10 @@ Definition run_asm (p: asm 1 0) := interp_asm (denote_asm p Fin.f0) empty empty. SAZ: Should this be stated in terms of ktree ? *) -Axiom fold: forall E (r b: Type), (itree E r -> b -> b) -> itree E r -> b -> b. - -Definition interp {E M : Type -> Type} - {FM : Functor M} {MM : Monad M} {IM : MonadIter M} - (h : E ~> M) : - itree E ~> M. := fun R => - iter (fun t => - match observe t with - | RetF r => ret (inr r) - | TauF t => ret (inl t) - | VisF e k => fmap (fun x => inl (k x)) (h _ e) - end). -(* TODO: this does a map, and aloop does a bind. We could fuse those - by giving aloop a continuation to compose its bind with. - (coyoneda...) *) - - (** The definition [interp_asm] also induces a notion of equivalence (open) _asm_ programs, which is just the equivalence of the ktree category *) Definition eq_asm_denotations {E A B} (t1 t2 : Kleisli (eitherT value (itree (Reg +' Memory +' E))) A B) : Prop := - forall a, eqm (interp_asm (t1 a)) (interp_asm (t2 a)). + forall (a: A), eqm (interp_asm (t1 a)) (interp_asm (t2 a)). Definition eq_asm {A B} (p1 p2 : asm A B) : Prop := eq_asm_denotations (denote_asm p1) (denote_asm p2). @@ -392,34 +391,18 @@ Section InterpAsmProperties. (** [interp_asm] commutes with [Ret]. *) Lemma interp_asm_ret: forall {R} (r: R), - eqm (interp_asm (E := E') (ret (m:= eitherT _ _) r)) - (ret (m := stateT _ _) r). + eqm (interp_asm (E := E') (ret r)) (ret r). Proof. - unfold interp_asm, interp_either_map. intros R r regs mem. - unfold ret at 1, Monad_eitherT. - unfold eqm. unfold EqM_eitherTM. - replace {| unEitherT := ret (m := itree E) (inr r) |} with (ret (m := eitherT _ _) r). + unfold interp_asm, interp_map. cbn. rewrite interp_ret, 2 interp_state_ret. reflexivity. Qed. - Lemma interp_asm_ret: forall {R} (r: R) (regs : registers) (mem: memory), - @eutt E' _ _ eq (interp_asm (ret (m:= eitherT _ _) r) regs mem) - (ret (mem, (regs, inr r))). - Proof. - unfold interp_asm, interp_map. - intros. - unfold ret at 1, Monad_itree. - cbn. rewrite interp_ret, 2 interp_state_ret. - reflexivity. - Qed. - (** [interp_asm] commutes with [bind]. *) - Lemma interp_asm_bind: forall {R S} (t: eitherT value (itree E) R) (k: R -> eitherT value (itree _) S) (regs : registers) (mem: memory), + Lemma interp_asm_bind: forall {R S} (t: eitherT value (itree E) R) (k: R -> eitherT value (itree _) S) mem regs, @eutt E' _ _ eq (interp_asm (bind t k) mem regs) (ITree.bind (interp_asm t mem regs) (fun '(mem', (regs', x)) => interp_asm (k x) mem' regs')). - Proof. intros. unfold interp_asm.