Poppen's Lab
This is Markdown editor.
{-# LANGUAGE BangPatterns #-} | |
import Control.Monad | |
import Control.Monad.ST | |
import Control.Applicative | |
import qualified Data.Vector.Unboxed as V | |
import Data.Vector.Unboxed ((!)) | |
import qualified Data.Vector.Algorithms.Intro as Intro | |
isort v = runST $ do |
import Criterion.Main | |
import Data.List | |
f :: Int -> Int | |
f n = foldl1' (+) $ zipWith (+) [1..n] [1..n] | |
main = defaultMain | |
[ bgroup "map" | |
[ bench "map" $ whnf f 1000000 | |
] |
module Tree where | |
data Tree a | |
= Tip | |
| Node (Tree a) a (Tree a) | |
mirror :: Tree a -> Tree a | |
mirror Tip = Tip | |
mirror (Node l v r) = Node (mirror r) v (mirror l) |
{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} | |
module Sorts where { | |
import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**), | |
(>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq, | |
error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse, | |
zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod, | |
String, Bool(True, False), Maybe(Nothing, Just)); | |
import qualified Prelude; |
theory Sorts | |
imports Main | |
begin | |
primrec insert :: "int => int list => int list" where | |
"insert v [] = [v]" | | |
"insert v (x # xs) = | |
(if v <= x then v # x # xs else x # insert v xs)" | |
primrec insert_sort :: "int list => int list" where |
theory Scratch | |
imports Main | |
begin | |
primrec ins :: "int => int list => int list" where | |
"ins x [] = [x]" | | |
"ins x (y # ys) = (if x <= y then (x # y # ys) else (y # ins x ys))" | |
primrec sort :: "int list => int list" where | |
"sort [] = []" | |
#include <vcc.h> | |
_(logic \bool sorted(int *buf, unsigned len) = | |
\forall unsigned i, j; i < j && j < len ==> buf[i] <= buf[j]) | |
_(typedef unsigned perm_t[unsigned];) | |
_(logic \bool is_permutation(perm_t perm, unsigned len) = | |
(\forall unsigned i, j; | |
i < j && j < len ==> perm[i] != perm[j])) |
#include <vcc.h> | |
_(logic \bool sorted(int *buf, unsigned len) = | |
\forall unsigned i, j; i < j && j < len ==> buf[i] <= buf[j]) | |
_(logic \bool is_minimum(int *buf, unsigned l, unsigned r, unsigned x) = | |
\forall unsigned i; l <= i && i < r ==> buf[x] <= buf[i]) | |
unsigned find_min(int *v, unsigned l, unsigned r) | |
_(requires \thread_local_array(v, r)) |
import Data.SBV | |
godNumber :: Int | |
godNumber = 50 | |
p1 :: [[SInteger]] | |
p1 = | |
[ [11, 2, 8, 5] | |
, [13, 14, 10, 12] | |
, [4, 3, 1, 7] |