ROSCOQ.shim.Haskell.RoshaskTopic
Require Import String.
Require Import ExtrHaskellString.
Require Import RoshaskNodeMonad.
Definition TopicName : Type := string.
Axiom RTopic : Type → Type.
Require Import ExtrHaskellString.
Require Import RoshaskNodeMonad.
Definition TopicName : Type := string.
Axiom RTopic : Type → Type.
TODO: generalize over the IO monad.
Extract Constant RTopic "a" ⇒ "Ros.Node.Topic GHC.Base.IO a".
TODO: make it an instance of Functor
Axiom tmap : ∀ {A B :Type}, (A→B) → RTopic A → RTopic B.
Extract Constant tmap ⇒ "GHC.Base.fmap".
Axiom tfilter : ∀ {A B: Type} (f: A → bool)
(g: ∀ (a:A) {pr: f a = true}, B), RTopic A → RTopic B.
Extract Constant tfilter ⇒ "\f g l -> GHC.Base.fmap (\x -> g x ()) (Ros.Topic.filter f l)".
Axiom asapMerge : ∀ {A:Type}, (RTopic A) → (RTopic A) → (RTopic A).
Extract Constant asapMerge ⇒ "Ros.Topic.Util.merge".
Axiom flattenTL : ∀ {A:Type}, (RTopic (list A)) → (RTopic A).
Extract Constant flattenTL ⇒ "Ros.ROSCoqUtil.flattenTL".
Axiom foldMapL : ∀ {s a b :Type}, s → (s → a → (b × s)) → RTopic a → RTopic b.
Extract Constant foldMapL ⇒ "Ros.ROSCoqUtil.foldMapL".
Extract Constant tmap ⇒ "GHC.Base.fmap".
Axiom tfilter : ∀ {A B: Type} (f: A → bool)
(g: ∀ (a:A) {pr: f a = true}, B), RTopic A → RTopic B.
Extract Constant tfilter ⇒ "\f g l -> GHC.Base.fmap (\x -> g x ()) (Ros.Topic.filter f l)".
Axiom asapMerge : ∀ {A:Type}, (RTopic A) → (RTopic A) → (RTopic A).
Extract Constant asapMerge ⇒ "Ros.Topic.Util.merge".
Axiom flattenTL : ∀ {A:Type}, (RTopic (list A)) → (RTopic A).
Extract Constant flattenTL ⇒ "Ros.ROSCoqUtil.flattenTL".
Axiom foldMapL : ∀ {s a b :Type}, s → (s → a → (b × s)) → RTopic a → RTopic b.
Extract Constant foldMapL ⇒ "Ros.ROSCoqUtil.foldMapL".