khibino

-- Example implementation for Meta-Theory à la Carte

-- data Fix (f : Set -> Set) : Set where
--   inF : f (Fix f) -> Fix f

open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_)
import Data.Nat as Nat

khibino

f1029 = [7, 123229502148636]

f1030 = [2, 7]

f1031 = [4, 21855]

f1032 = [7, 560803991675135]

f1034 = [5, 33554431]

khibino

import Numeric.Natural (Natural)

type Nat = Natural

data NatListF a = Nil | Cons (Nat, a) deriving Show
newtype NatList = In (NatListF NatList) deriving Show

out :: NatList -> NatListF NatList
out (In x) = x

khibino

module CoYoneda where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Data.Product using (_×_; proj₁; proj₂; ∃; _,_)


pattern _⊢_⊗_ a k x = (a , k , x) --  ∃ (λ a → (a → r) × f a)

module CovariantMap

khibino

module Yoneda where

open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

{- specialized Morphism to Haskell function,
   specialized Functor to Haskell Functor,
   Proof of Yoneda Lemma -}
{- 射を Haskell の関数に、
   関手を Haskell の Functor に限定した場合の

khibino

{-# LANGUAGE FlexibleInstances #-}

import Data.DList
import Control.Monad.Trans.Writer (Writer)
import Data.Functor.ProductIsomorphic

data PH a = PH

newtype WithPhT r a =
  WithPhT { runWithPhT :: Writer (DList Int) (r a)  }

khibino

open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import RSC

-- Basic data-types

khibino

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}

module Position where

import GHC.Generics (Generic)
import Foreign.Ptr (Ptr )
import Data.Word (Word8)

khibino

Debian sid 上の groonga 8.0.2 および Debian jessie 上の groonga 8.0.1 で実験しました。
groonga に投入するクライアントプログラムを中断すると、
それとは関係のない別のクライアントで、JSON の解釈エラーが返ることがある問題があるようです。

問題を再現するスクリプト run.sh を作ることに成功したのでここに貼ります。
( 後輩の前角さんが協力してくれました。ありがとうございます。 )
実行に必要な Debian package は、
groonga, curl です。

run.sh を実行すると、

khibino

import Language.Haskell.TH (nameBase)
import Language.Haskell.TH.Name.CamelCase (varCamelcaseName, varName)
import Database.Record.TH

customConfig :: NameConfig
customConfig =
  defaultNameConfig
  { columnName = \tbl col -> varCamelcaseName $ tbl ++ "_" ++ col }

main :: IO ()