Skip to content

Instantly share code, notes, and snippets.

View yuga's full-sized avatar

s.murayama yuga

8 followers · 5 following
View GitHub Profile
@yuga
yuga / Logic_five_not_even.v
Last active August 29, 2015 14:03
Definition five_not_even' : ~ ev 5 :=
fun (Hev5 : ev 5) =>
(fun (P : nat -> Prop) (* evの帰納法の原理*)
(f : P 0)
(f0 : forall n : nat, ev n -> P n -> P (S (S n))) =>
fix F (n : nat) (e : ev n) {struct e} : P n := (* eについて減少 *)
match e in (ev n0) return (P n0) with
| ev_0 => f
| ev_SS n1 ev1 => f0 n1 ev1 (F n1 ev1)
end)
@yuga
yuga / cow.bash
Created August 12, 2014 08:59
cowbuilderのバッドノウハウ集
#!/bin/bash
PRG=$(readlink -f "$0")
PRGDIR=$(dirname "${PRG}")
set -x
set -e
list=(
haskell-names-th_0.0.1.0.dsc
@yuga
yuga / ChunkGroupBy.hs
Last active August 29, 2015 14:08
-- > chunkGroupBy (\x y -> x == y) 6 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
-- [[[0,0,0,0]],[[1,1,1]],[[2,2,2,2,2]],[[3,3,3,3]]]
--
-- > chunkGroupBy (\x y -> x == y) 7 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
-- [[[0,0,0,0],[1,1,1]],[[2,2,2,2,2]],[[3,3,3,3]]]
--
-- > chunkGroupBy (\x y -> x == y) 15 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
-- [[[0,0,0,0],[1,1,1],[2,2,2,2,2]],[[3,3,3,3]]]
--
-- > chunkGroupBy (\x y -> x == y) 16 [0,0,0,0,1,1,1,2,2,2,2,2,3,3,3,3]
@yuga
yuga / decimal.idr
Last active August 29, 2015 14:10
not deal with seriously
module decimal
record Decimal : Nat -> Type where
MkDecimal : (places : Nat) -> (mantissa : Integer) -> Decimal places
signum : Integer -> Integer
signum n = case compare n 0 of
LT => (-1)
EQ => 0
GT => 1
@yuga
yuga / gist:328a5bdf885f1599d28d
Created December 11, 2014 03:21
SQLite3用のモジュール名をどれにあわせるか？
HSQL
--------------------
DB.HSQL.SQLite3
HDBC
--------------------
Database.HDBC.Sqlite3
HDBI
--------------------
@yuga
yuga / exmaples.hs
Last active August 29, 2015 14:11
追加しようと思うexample
account1'' :: Relation () Account1
account1'' = relation $ do
a <- query account
wheres $ a ! Account.productCd' `in'` values ["CHK", "SAV", "CD", "MM"]
return $ Account1 |$| a ! Account.accountId'
|*| a ! Account.productCd'
|*| a ! Account.custId'
|*| a ! Account.availBalance'
data Account1 = Account1
@yuga
yuga / gist:c9f21ffbc7c5bd2cc3d9
Last active August 29, 2015 14:11
SQL: date time literals
@yuga
yuga / query_orderby_sql-99.bnf.md
Last active August 29, 2015 14:11

UNIONとORDER BYの組み合わせ

relational-record-examples の sql/6.4.1a.sh に対応するHaskellコードの説明を書いていて、何だか嘘を書いている気分になったので調査してみた。ちなみに書いていた説明は以下のようなもの。英語は雰囲気です。

-- | sql/6.4.1a.sh
--
-- MySQL allows the syntax of UNION that has an order clause at the
-- last of query. SQLite does not.
@yuga
yuga / read.hs
Created February 28, 2015 16:08
ByteString -> Double
toRealFloat . either error id . parseOnly Data.Attoparsec.ByteString.Char8.scientific :: ByteString -> Double
@yuga
yuga / hackagedocs
Created April 16, 2015 15:19
maoeさんのを手元環境で動くようにしたバージョン。
#!/bin/bash
cabal configure && cabal build && cabal haddock --hyperlink-source \
--html-location='http://hackage.haskell.org/package/$pkg/docs' \
--contents-location='http://hackage.haskell.org/package/$pkg'
S=$?
if [ "${S}" -eq "0" ]; then
cd "dist/doc/html"
DDIR="${1}-${2}-docs"
cp -r "${1}" "${DDIR}" && tar -cvz --format=ustar -f "${DDIR}.tar.gz" "${DDIR}"
CS=$?