lylek

{-# LANGUAGE BangPatterns, CPP #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing -fwarn-unused-imports #-}
-- -Wall 

-- This is a rate-limiting version of https://github.com/simonmar/parconc-examples/blob/master/Stream.hs,
-- as per the exercise on page 69 of Parallel and Concurrent Programming in Haskell.

-- A module for stream processing built on top of Control.Monad.Par

-- (In the future may want to look into the stream interface used by

lylek

-- Logic & Proof Chapter 18 Exercises

namespace hidden

open nat

-- From 17.4

theorem mul_add (m n k : nat) : m * (n + k) = (m * n) + (m * k) :=
nat.rec_on k

lylek

-- Logic & Proof Chapter 18 Exercises

namespace hidden

open nat

-- From 17.4

theorem mul_add (m n k : nat) : m * (n + k) = (m * n) + (m * k) :=
nat.rec_on k

lylek

-- Logic and Proof Exercise 17.19
-- Finds an increasing list of Fibonacci numbers that sum to the given natural number.
-- The algorithm is linear in the input number, and tail recursive.

main = mapM_ print $ map fibsSummingTo [0..100]

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

fibsSummingTo :: Integer -> [Integer]
fibsSummingTo n = loop n ltFibs []

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

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

-- 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

#!/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

#!/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

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

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