TakashiHarada

## script for experiments

#! /bin/bash -                                                                                                                                              

n=5
m=10

for (( i = 1; i <= n; i += 1))
do
    for ((j = 1; j <= m; j += 1))

TakashiHarada

-- もっと効率の良い実装があるはず．．．

import Data.Char

main :: IO ()
main = putStrLn "Enter a length of element: "
  >> (readLn :: IO Int)
  >>= \d -> putStrLn ("graph Lattice" ++ show d ++ " {")
  >> putStr "\n  graph [\n   rankdir = BT\n  ]\n\n"
  >> putStrLn ((unlines . concatMap piyo . reverse . mkLattice) d ++ "}")

TakashiHarada

import System.Random.Shuffle
import System.Random
import System.Environment
import Data.List

main :: IO ()
main =
  getArgs >>=
  \args -> if 3 /= (length args)
           then putStrLn "Usage: $ ./mkC1Pmatrix 100 32 randomC1Pmatrix"

TakashiHarada

#include "list.h"
#include <math.h>

struct MATRIX {
  unsigned m;
  unsigned n;
  char**   b;
};
typedef struct MATRIX matrix;

TakashiHarada

fact :: Integer -> Integer
fact n = product [1..n]

comb :: Integer -> Integer -> Integer
comb n k = product [(n-k+1)..n] `div` (fact k)

f :: Integer -> Integer
f w = sum [(comb (3^w) k) * (fact k) * 2^k | k <- [1..3^w]]

TakashiHarada

import Parser
import BNF2Props
import System.IO
import System.Environment
import Data.Maybe
import Data.List

main =
  putStr "Input a grammar file: " >>       -- grammar.txt
  getLine >>= \filename ->

TakashiHarada

module BNF2Props where

import Parser
import Control.Applicative
import Data.Char
import Data.Maybe
--import Text.Parsec.String.Parsec (parse)

{-

TakashiHarada

module Parser where

-- for Text.Parsec
-- https://github.com/JakeWheat/intro_to_parsing/blob/master/FunctionsAndTypesForParsing.lhs

-- I refered to the "Programming in Haskell 2nd edition" for implemeting this module.

import Control.Applicative
import Data.Char
import Data.List

TakashiHarada

-- https://en.wikibooks.org/wiki/Haskell/Monad_transformers

import Data.Char
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.Maybe

-- getPassphrase :: IO (Maybe String)
-- getPassphrase =
--   getLine >>=

TakashiHarada

module ex7-1-1 where

data Bool : Set where
  t : Bool
  f : Bool

not : Bool → Bool
not t = f
not f = t