packages feed

comonad-transformers 2.1.2 → 4.0

raw patch · 16 files changed

Files

+ .ghci view
@@ -0,0 +1,1 @@+:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h
+ .gitignore view
@@ -0,0 +1,13 @@+dist+docs+wiki+TAGS+tags+wip+.DS_Store+.*.swp+.*.swo+*.o+*.hi+*~+*#
.travis.yml view
@@ -1,1 +1,8 @@ language: haskell+notifications:+  irc:+    channels:+      - "irc.freenode.org#haskell-lens"+    skip_join: true+    template:+      - "\x0313comonad-transformers\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
+ .vim.custom view
@@ -0,0 +1,31 @@+" Add the following to your .vimrc to automatically load this on startup++" if filereadable(".vim.custom")+"     so .vim.custom+" endif++function StripTrailingWhitespace()+  let myline=line(".")+  let mycolumn = col(".")+  silent %s/  *$//+  call cursor(myline, mycolumn)+endfunction++" enable syntax highlighting+syntax on++" search for the tags file anywhere between here and /+set tags=TAGS;/++" highlight tabs and trailing spaces+set listchars=tab:‗‗,trail:‗+set list++" f2 runs hasktags+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>++" strip trailing whitespace before saving+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()++" rebuild hasktags after saving+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"
− CHANGELOG 
@@ -1,4 +0,0 @@-2.1:- * Removed Discont- * Switched to mkTyCon3- * Upgraded to transformers 0.3
− Control/Comonad/Hoist/Class.hs 
@@ -1,29 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Hoist.Class--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------------------------------------------------------------------------------module Control.Comonad.Hoist.Class (ComonadHoist(..)) where--import Control.Comonad-import Control.Monad.Trans.Identity-import Data.Functor.Identity--class ComonadHoist t where-  -- | Ideally we would offer a way to lift comonad homomorphisms-  -- but this isn't Haskell 98, so we settle for the most common case-  -- here.-  ---  -- > liftTrans :: (forall a. w a -> v a) -> t w a -> t v a -  -- > cohoist = liftTrans (Identity . extract)-  cohoist :: Comonad w => t w a -> t Identity a---- avoiding orphans--instance ComonadHoist IdentityT where-  cohoist = IdentityT . Identity . extract . runIdentityT
− Control/Comonad/Trans/Class.hs 
@@ -1,22 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Class--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------------------------------------------------------------------------------module Control.Comonad.Trans.Class -  ( ComonadTrans(..) ) where--import Control.Comonad-import Control.Monad.Trans.Identity--class ComonadTrans t where-  lower :: Extend w => t w a -> w a ---- avoiding orphans-instance ComonadTrans IdentityT where-  lower = runIdentityT
− Control/Comonad/Trans/Env.hs 
@@ -1,134 +0,0 @@-{-# LANGUAGE CPP, FlexibleContexts #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Env--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The environment comonad transformer (aka coreader).--- This adds an extra value that can be accessed in the environment.------ Left adjoint to the reader comonad.------------------------------------------------------------------------------module Control.Comonad.Trans.Env-  (-  -- * The strict environment comonad-    Env-  , env-  , runEnv-  -- * The strict environment comonad transformer-  , EnvT(..)-  , runEnvT-  , lowerEnvT-  -- * Combinators-  , ask-  , asks-  , local-  ) where--import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Foldable-import Data.Traversable-import Data.Functor.Apply-import Data.Functor.Identity-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Data--instance (Typeable s, Typeable1 w) => Typeable1 (EnvT s w) where-  typeOf1 dswa = mkTyConApp envTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: EnvT s w a -> s-      s = undefined-      w :: EnvT s w a -> w a-      w = undefined--envTTyCon :: TyCon-#if __GLASGOW_HASKELL__ < 704-envTTyCon = mkTyCon "Control.Comonad.Trans.Env.EnvT"-#else-envTTyCon = mkTyCon3 "comonad-transformers" "Control.Comonad.Trans.Env" "EnvT"-#endif-{-# NOINLINE envTTyCon #-}--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (EnvT s w a) where-  typeOf = typeOfDefault--instance-  ( Data e-  , Typeable1 w, Data (w a)-  , Data a-  ) => Data (EnvT e w a) where-    gfoldl f z (EnvT e wa) = z EnvT `f` e `f` wa-    toConstr _ = envTConstr-    gunfold k z c = case constrIndex c of-        1 -> k (k (z EnvT))-        _ -> error "gunfold"-    dataTypeOf _ = envTDataType-    dataCast1 f = gcast1 f--envTConstr :: Constr-envTConstr = mkConstr envTDataType "EnvT" [] Prefix-{-# NOINLINE envTConstr #-}--envTDataType :: DataType-envTDataType = mkDataType "Control.Comonad.Trans.Env.EnvT" [envTConstr]-{-# NOINLINE envTDataType #-}--#endif--type Env e = EnvT e Identity-data EnvT e w a = EnvT e (w a)--env :: e -> a -> Env e a-env e a = EnvT e (Identity a)--runEnv :: Env e a -> (e, a)-runEnv (EnvT e (Identity a)) = (e, a)--runEnvT :: EnvT e w a -> (e, w a)-runEnvT (EnvT e wa) = (e, wa)--instance Functor w => Functor (EnvT e w) where-  fmap g (EnvT e wa) = EnvT e (fmap g wa)--instance Extend w => Extend (EnvT e w) where-  duplicate (EnvT e wa) = EnvT e (extend (EnvT e) wa)--instance Comonad w => Comonad (EnvT e w) where-  extract (EnvT _ wa) = extract wa--instance ComonadTrans (EnvT e) where-  lower (EnvT _ wa) = wa--lowerEnvT :: EnvT e w a -> w a-lowerEnvT (EnvT _ wa) = wa--instance ComonadHoist (EnvT e) where-  cohoist (EnvT e wa) = EnvT e (Identity (extract wa))--instance (Semigroup e, Apply w) => Apply (EnvT e w) where-  EnvT ef wf <.> EnvT ea wa = EnvT (ef <> ea) (wf <.> wa)--instance Foldable w => Foldable (EnvT e w) where-  foldMap f (EnvT _ w) = foldMap f w--instance Traversable w => Traversable (EnvT e w) where-  traverse f (EnvT e w) = EnvT e <$> traverse f w--ask :: EnvT e w a -> e-ask (EnvT e _) = e--asks :: (e -> f) -> EnvT e w a -> f-asks f (EnvT e _) = f e--local :: (e -> e) -> EnvT e w a -> EnvT e w a-local f (EnvT e wa) = EnvT (f e) wa-
− Control/Comonad/Trans/Identity.hs 
@@ -1,16 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Identity--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable--- ------------------------------------------------------------------------------module Control.Comonad.Trans.Identity-  ( IdentityT(..)-  ) where--import Control.Monad.Trans.Identity
− Control/Comonad/Trans/Store.hs 
@@ -1,128 +0,0 @@-{-# LANGUAGE CPP #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Store--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The strict store (state-in-context/costate) comonad transformer is subject to the laws:------ > x = seek (pos x) x--- > y = pos (seek y x)--- > seek y x = seek y (seek z x)------ Thanks go to Russell O'Connor and Daniel Peebles for their help formulating--- and proving the laws for this comonad transformer.------------------------------------------------------------------------------module Control.Comonad.Trans.Store-  (-  -- * The Store comonad-    Store, store, runStore-  -- * The Store comonad transformer-  , StoreT(..), runStoreT-  -- * Operations-  , pos-  , seek, seeks-  , peek, peeks-  , experiment-  ) where--import Control.Applicative-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Functor.Identity-import Data.Functor.Apply-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Typeable-instance (Typeable s, Typeable1 w) => Typeable1 (StoreT s w) where-  typeOf1 dswa = mkTyConApp storeTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: StoreT s w a -> s-      s = undefined-      w :: StoreT s w a -> w a-      w = undefined--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (StoreT s w a) where-  typeOf = typeOfDefault--storeTTyCon :: TyCon-#if __GLASGOW_HASKELL__ < 704-storeTTyCon = mkTyCon "Control.Comonad.Trans.Store.StoreT"-#else-storeTTyCon = mkTyCon3 "comonad-transformers" "Control.Comonad.Trans.Store" "StoreT"-#endif-{-# NOINLINE storeTTyCon #-}-#endif--type Store s = StoreT s Identity--store :: (s -> a) -> s -> Store s a-store f s = StoreT (Identity f) s--runStore :: Store s a -> (s -> a, s)-runStore (StoreT (Identity f) s) = (f, s)--data StoreT s w a = StoreT (w (s -> a)) s--runStoreT :: StoreT s w a -> (w (s -> a), s)-runStoreT (StoreT wf s) = (wf, s)--experiment :: (Comonad w, Functor f) => (s -> f s) -> StoreT s w a -> f a-experiment f (StoreT wf s) = extract wf <$> f s--instance Functor w => Functor (StoreT s w) where-  fmap f (StoreT wf s) = StoreT (fmap (f .) wf) s--instance (Apply w, Semigroup s) => Apply (StoreT s w) where-  StoreT ff m <.> StoreT fa n = StoreT ((<*>) <$> ff <.> fa) (m <> n)--instance (Applicative w, Semigroup s, Monoid s) => Applicative (StoreT s w) where-  pure a = StoreT (pure (const a)) mempty-  StoreT ff m <*> StoreT fa n = StoreT ((<*>) <$> ff <*> fa) (m `mappend` n)--instance Extend w => Extend (StoreT s w) where-  duplicate (StoreT wf s) = StoreT (extend StoreT wf) s-  extend f (StoreT wf s) = StoreT (extend (\wf' s' -> f (StoreT wf' s')) wf) s--instance Comonad w => Comonad (StoreT s w) where-  extract (StoreT wf s) = extract wf s--instance ComonadTrans (StoreT s) where-  lower (StoreT f s) = fmap ($s) f--instance ComonadHoist (StoreT s) where-  cohoist (StoreT f s) = StoreT (Identity (extract f)) s---- | Read the current position-pos :: StoreT s w a -> s-pos (StoreT _ s) = s---- | Seek to an absolute location------ > seek s = peek s . duplicate-seek :: Comonad w => s -> StoreT s w a -> StoreT s w a-seek s ~(StoreT f _) = StoreT f s---- | Seek to a relative location------ > seeks f = peeks f . duplicate-seeks :: Comonad w => (s -> s) -> StoreT s w a -> StoreT s w a-seeks f ~(StoreT g s) = StoreT g (f s)---- | Peek at a value at a given absolute location------ > peek x . extend (peek y) = peek y-peek :: Comonad w => s -> StoreT s w a -> a-peek s (StoreT g _) = extract g s---- | Peek at a value at a given relative location-peeks :: Comonad w => (s -> s) -> StoreT s w a -> a-peeks f ~(StoreT g s) = extract g (f s)-
− Control/Comonad/Trans/Traced.hs 
@@ -1,106 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Traced--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The trace comonad transformer (aka the cowriter or exponential comonad transformer).---------------------------------------------------------------------------------module Control.Comonad.Trans.Traced-  (-  -- * Traced comonad-    Traced-  , traced-  , runTraced-  -- * Traced comonad transformer-  , TracedT(..)-  -- * Operations-  , trace-  , listen-  , listens-  , censor-  ) where--import Control.Applicative-import Control.Monad.Instances ()-import Control.Monad (ap)-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Distributive-import Data.Functor.Apply-import Data.Functor.Identity-import Data.Semigroup-import Data.Typeable--type Traced m = TracedT m Identity--traced :: (m -> a) -> Traced m a-traced f = TracedT (Identity f)--runTraced :: Traced m a -> m -> a-runTraced (TracedT (Identity f)) = f--newtype TracedT m w a = TracedT { runTracedT :: w (m -> a) }--instance Functor w => Functor (TracedT m w) where-  fmap g = TracedT . fmap (g .) . runTracedT--instance Apply w => Apply (TracedT m w) where-  TracedT wf <.> TracedT wa = TracedT (ap <$> wf <.> wa)--instance Applicative w => Applicative (TracedT m w) where-  pure = TracedT . pure . const-  TracedT wf <*> TracedT wa = TracedT (ap <$> wf <*> wa)--instance (Extend w, Semigroup m) => Extend (TracedT m w) where-  extend f = TracedT . extend (\wf m -> f (TracedT (fmap (. (<>) m) wf))) . runTracedT--instance (Comonad w, Semigroup m, Monoid m) => Comonad (TracedT m w) where-  extract (TracedT wf) = extract wf mempty--instance (Semigroup m, Monoid m) => ComonadTrans (TracedT m) where-  lower = fmap ($mempty) . runTracedT--instance (Semigroup m, Monoid m) => ComonadHoist (TracedT m) where-  cohoist = traced . extract . runTracedT--instance Distributive w => Distributive (TracedT m w) where-  distribute = TracedT . fmap (\tma m -> fmap ($m) tma) . collect runTracedT--trace :: (Comonad w, Monoid m) => m -> TracedT m w a -> a-trace m (TracedT wf) = extract wf m--listen :: Functor w => TracedT m w a -> TracedT m w (a, m)-listen = TracedT . fmap (\f m -> (f m, m)) . runTracedT--listens :: Functor w => (m -> b) -> TracedT m w a -> TracedT m w (a, b)-listens g = TracedT . fmap (\f m -> (f m, g m)) . runTracedT--censor :: Functor w => (m -> m) -> TracedT m w a -> TracedT m w a-censor g = TracedT . fmap (. g) . runTracedT--#ifdef __GLASGOW_HASKELL__--instance (Typeable s, Typeable1 w) => Typeable1 (TracedT s w) where-  typeOf1 dswa = mkTyConApp tracedTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: TracedT s w a -> s-      s = undefined-      w :: TracedT s w a -> w a-      w = undefined--tracedTTyCon :: TyCon-#if __GLASGOW_HASKELL__ < 704-tracedTTyCon = mkTyCon "Control.Comonad.Trans.Traced.TracedT"-#else-tracedTTyCon = mkTyCon3 "comonad-transformers" "Control.Comonad.Trans.Traced" "TracedT"-#endif-{-# NOINLINE tracedTTyCon #-}--#endif
− Data/Functor/Composition.hs 
@@ -1,14 +0,0 @@-module Data.Functor.Composition-  ( Composition(..) ) where--import Data.Functor.Compose---- | We often need to distinguish between various forms of Functor-like composition in Haskell in order to please the type system.--- This lets us work with these representations uniformly.-class Composition o where-  decompose :: o f g x -> f (g x)-  compose :: f (g x) -> o f g x--instance Composition Compose where-  decompose = getCompose-  compose = Compose
− Data/Functor/Coproduct.hs 
@@ -1,64 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Data.Functor.Coproduct--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------------------------------------------------------------------------------module Data.Functor.Coproduct-  ( Coproduct(..)-  , left-  , right-  , coproduct-  ) where--import Control.Comonad-import Data.Functor.Contravariant-import Data.Foldable-import Data.Traversable-import Data.Semigroup.Foldable-import Data.Semigroup.Traversable--newtype Coproduct f g a = Coproduct { getCoproduct :: Either (f a) (g a) }--left :: f a -> Coproduct f g a-left = Coproduct . Left--right :: g a -> Coproduct f g a-right = Coproduct . Right--coproduct :: (f a -> b) -> (g a -> b) -> Coproduct f g a -> b-coproduct f g = either f g . getCoproduct--instance (Functor f, Functor g) => Functor (Coproduct f g) where-  fmap f = Coproduct . coproduct (Left . fmap f) (Right . fmap f)--instance (Foldable f, Foldable g) => Foldable (Coproduct f g) where-  foldMap f = coproduct (foldMap f) (foldMap f)--instance (Foldable1 f, Foldable1 g) => Foldable1 (Coproduct f g) where-  foldMap1 f = coproduct (foldMap1 f) (foldMap1 f)--instance (Traversable f, Traversable g) => Traversable (Coproduct f g) where-  traverse f = coproduct-    (fmap (Coproduct . Left) . traverse f)-    (fmap (Coproduct . Right) . traverse f)--instance (Traversable1 f, Traversable1 g) => Traversable1 (Coproduct f g) where-  traverse1 f = coproduct-    (fmap (Coproduct . Left) . traverse1 f)-    (fmap (Coproduct . Right) . traverse1 f)--instance (Extend f, Extend g) => Extend (Coproduct f g) where-  extend f = Coproduct . coproduct-    (Left . extend (f . Coproduct . Left))-    (Right . extend (f . Coproduct . Right))--instance (Comonad f, Comonad g) => Comonad (Coproduct f g) where-  extract = coproduct extract extract--instance (Contravariant f, Contravariant g) => Contravariant (Coproduct f g) where-  contramap f = Coproduct . coproduct (Left . contramap f) (Right . contramap f)
+ README.markdown view
@@ -0,0 +1,19 @@+comonad-transformers+==========++[![Build Status](https://secure.travis-ci.org/ekmett/comonad-transformers.png?branch=master)](http://travis-ci.org/ekmett/comonad-transformers)++This package provides a standard set of comonad transformers for Haskell.++Like the `transformers` package this package is `Haskell 98`.++Clases for these types are provided by the [`comonads-fd`](/ekmett/comonads-fd) package.++Contact Information+-------------------++Contributions and bug reports are welcome!++Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.++-Edward Kmett
comonad-transformers.cabal view
@@ -1,6 +1,6 @@ name:          comonad-transformers category:      Control, Comonads-version:       2.1.2+version:       4.0 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -9,37 +9,20 @@ stability:     provisional homepage:      http://github.com/ekmett/comonad-transformers/ bug-reports:   http://github.com/ekmett/comonad-transformers/issues-copyright:     Copyright (C) 2008-2012 Edward A. Kmett-synopsis:      Comonad transformers-description:   Comonad transformers+copyright:     Copyright (C) 2008-2013 Edward A. Kmett+synopsis:      This package has been merged into comonad 4.0+description:   This package has been merged into comonad 4.0 build-type:    Simple-extra-source-files: coq/Store.v CHANGELOG .travis.yml+extra-source-files:+  README.markdown+  .travis.yml+  .ghci+  .gitignore+  .vim.custom  source-repository head   type: git   location: git://github.com/ekmett/comonad-transformers.git  library-  build-depends:-    base          >= 4       && < 5,-    comonad       >= 1.1.1.5 && < 1.2,-    containers    >= 0.3     && < 0.6,-    contravariant >= 0.2.0.1 && < 0.3,-    distributive  >= 0.2.2   && < 0.3,-    semigroupoids >= 1.3.1.2 && < 1.4,-    semigroups    >= 0.8.3.1 && < 0.9,-    transformers  >= 0.2     && < 0.4--  extensions: CPP--  exposed-modules:-    Control.Comonad.Hoist.Class-    Control.Comonad.Trans.Class-    Control.Comonad.Trans.Env-    Control.Comonad.Trans.Identity-    Control.Comonad.Trans.Store-    Control.Comonad.Trans.Traced-    Data.Functor.Coproduct-    Data.Functor.Composition--  ghc-options:      -Wall+  build-depends: base >= 4 && < 5, comonad >= 4
− coq/Store.v 
@@ -1,96 +0,0 @@-(* Proof StoreT forms a comonad -- Russell O'Connor *)--Set Implict Arguments.-Unset Strict Implicit.--Require Import FunctionalExtensionality.--Record Comonad (w : Type -> Type) : Type :=- { extract : forall a, w a -> a- ; extend : forall a b, (w a -> b) -> w a -> w b- ; law1 : forall a x, extend _ _ (extract a) x = x- ; law2 : forall a b f x, extract b (extend a _ f x) = f x- ; law3 : forall a b c f g x, extend b c f (extend a b g x) = extend a c (fun y => f (extend a b g y)) x- }.--Section StoreT.--Variables (s : Type) (w:Type -> Type).-Hypothesis wH : Comonad w.--Definition map a b f x := extend _ wH a b (fun y => f (extract _ wH _ y)) x.--Lemma map_extend : forall a b c f g x, map b c f (extend _ wH a b g x) = extend _ wH _ _ (fun y => f (g y)) x.-Proof.-intros a b c f g x.-unfold map.-rewrite law3.-apply equal_f.-apply f_equal.-extensionality y.-rewrite law2.-reflexivity.-Qed.--Record StoreT (a:Type): Type := mkStoreT-  {store : w (s -> a)-  ;loc   : s}.--Definition extractST a (x:StoreT a) : a := - extract _ wH _ (store _ x) (loc _ x).--Definition mapST a b (f:a -> b) (x:StoreT a) : StoreT b :=- mkStoreT _ (map _ _ (fun g x => f (g x)) (store _ x)) (loc _ x).--Definition duplicateST a (x:StoreT a) : StoreT (StoreT a) :=- mkStoreT _ (extend _ wH _ _ (mkStoreT _) (store _ x)) (loc _ x).--Let extendST := fun a b f x => mapST _ b f (duplicateST a x).--Lemma law1ST : forall a x, extendST _ _ (extractST a) x = x.-Proof.-intros a [v b].-unfold extractST, extendST, duplicateST, mapST.-simpl.-rewrite map_extend.-simpl.-replace (fun (y : w (s -> a)) (x : s) => extract w wH (s -> a) y x)- with (extract w wH (s -> a)).- rewrite law1.- reflexivity.-extensionality y.-extensionality x.-reflexivity.-Qed.--Lemma law2ST : forall a b f x, extractST b (extendST a _ f x) = f x.-Proof.-intros a b f [v c].-unfold extendST, mapST, extractST.-simpl.-rewrite map_extend.-rewrite law2.-reflexivity.-Qed.--Lemma law3ST : forall a b c f g x, extendST b c f (extendST a b g x) = extendST a c (fun y => f (extendST a b g y)) x.-Proof.-intros a b c f g [v d].-unfold extendST, mapST, extractST.-simpl.-repeat rewrite map_extend.-rewrite law3.-repeat (apply equal_f||apply f_equal).-extensionality y.-extensionality x.-rewrite map_extend.-reflexivity.-Qed.--Definition StoreTComonad : Comonad StoreT :=- Build_Comonad _ _ _ law1ST law2ST law3ST.--End StoreT.--Check StoreTComonad.-