lylek

import Control.Monad
import Data.Char
import Text.Parsec
import Text.Parsec.String

data SExpr =
    SSym { getSym :: String } |
    SInt !Integer |
    SBool !Bool |
    SList [SExpr] |

lylek

module SchemeParser where

import Text.Parsec
import Text.Parsec.String

(<>) :: Parser [a] -> Parser [a] -> Parser [a]
p1 <> p2 = do r1 <- p1; r2 <- p2; return (r1 ++ r2)

one :: Parser a -> Parser [a]
one = fmap (:[])

lylek

#!/usr/bin/env stack
-- stack --resolver lts-5.5 --install-ghc runghc

-- Pizza Hut solution for Pi Day problem 1
-- http://blog.pizzahut.com/flavor-news/national-pi-day-math-contest-problems-are-here-2/

import Data.List (permutations)

main = putStrLn $ head solutions

lylek

-- Semigroups and monoids

-- On Maybe:

-- Nothing disappears, left wins
instance Monoid (Maybe a) where
	mempty = Nothing
    Nothing `mappend` y = y
    x `mappend` _ = x

lylek

#!/usr/bin/env stack
-- stack --install-ghc runghc --package=criterion

import Criterion.Main
import Data.Char (intToDigit)
import Data.List (intercalate)

type Expression = [Term]
type Term = [Factor]
type Factor = [Digit]

lylek

#!/usr/bin/env stack
-- stack --install-ghc runghc --package=containers --package=pretty-tree --package=criterion --package=QuickCheck

-- Pearls of Functional Algorithm Design, Chap. 7
-- Building a tree of minimum height

{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}

import Control.DeepSeq (NFData, deepseq)
import Criterion.Main

lylek

#!/usr/bin/env stack
-- stack --install-ghc runghc --package=criterion --package=QuickCheck --package=deepseq

-- Pearls of Functional Algorithm Design, Chap. 8
-- Unravelling greedy algorithms

{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}

import Control.DeepSeq (deepseq)
import Criterion.Main

lylek

-- Exercise 1

section
    variable A : Type
    variable f : A → A
    variable P : A → Prop
    variable h : ∀ x, P x → P (f x)
    -- Show the following:
    example : ∀ y, P y → P (f (f y)) :=
    assume y,

lylek

hub ws (x : xs)
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits ws]
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits (us ++ vs)]
= minimum [is ++ nub ((x : xs) \\ is) | is <- inits us ++ map (us ++) (inits+ vs)]
= minimum ([is ++ nub ((x : xs) \\ is) | is <- inits us] ++ [is ++ nub ((x : xs) \\ is) | is <- map (us ++) (inits+ vs)])
= minimum ([is ++ nub ((x : xs) \\ is) | is <- inits us] ++ [us ++ is ++ nub ((x : xs) \\ (us ++ is)) | is <- inits+ vs])
= min (minimum [is ++ nub ((x : xs) \\ is) | is <- inits us]) (minimum [us ++ is ++ nub ((x : xs) \\ (us ++ is)) | is <- inits+ vs])
= min A B

A, when x not in xs

lylek

-- Logic and Proof Chapter 14 Exercises

-- Exercise 1

section
parameters {A : Type} {R : A → A → Prop}
parameter (irreflR : irreflexive R)
parameter (transR : transitive R)

local infix < := R