Denotation of open cfgs in presence of function calls

_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

theories/Basics/Applicative.v

@@ -0,0 +1,9 @@
+Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
+{ pure : forall {A : Type@{d}}, A -> T A
+; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
+}.
+
+Module ApplicativeNotation.
+  Notation "f <*> x" := (ap f x) (at level 52, left associativity).
+End ApplicativeNotation.
+

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. *)

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.
+

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

theories/Basics/Functor.v

@@ -0,0 +1,7 @@
+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.
+