as-capabl

Require Import Relation_Definitions.
Require Import SetoidClass.
Require Import VectorDef.
Require Import Morphisms.
Require Import COC.Base.Main.


Set Implicit Arguments.

as-capabl

(* やりたいこと：Coq上でReaderTを実装し、
 Haskellコードに変換してHaskell側から使う *)
Require Import Coq.Logic.FunctionalExtensionality.

Section Monad_Definition.
  (* Reserved Notation "c >>= f"
           (at level 42, left associativity). *)

  (* Monadの宣言 *)
  Class Monad {T : Type -> Type} (returns : forall {A : Type}, A -> T A)

as-capabl

{-# LANGUAGE Arrows #-}

module Main where

import Prelude hiding (filter, id, (.), unzip, mapM_)
import Control.Category
import Control.Arrow
import Criterion
import Criterion.Main (defaultMain)
import Data.Time

as-capabl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}


module
    Main
where

as-capabl

Require Import List.

Section Monoid.
  Class Monoid {A:Type} (dot : A -> A -> A) (unit : A) : Prop :=
    {
      dot_assoc :
        forall x y z:A,
          dot x (dot y z) = dot (dot x y) z;
      unit_left :
        forall x, dot unit x = x;

as-capabl

{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language TypeOperators #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}
{-# Language LambdaCase #-}

module
    Main

as-capabl

{-# Language Arrows #-}

import Control.Arrow
import Control.Monad (forever)
import Control.Monad.Trans (lift)
import qualified Control.Arrow.Machine as P
import qualified Data.Machine as Mc
import Data.Machine ((<~))