tanakh

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

tanakh

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
    ]

tanakh

Markdown Editor

Poppen's Lab

##What

This is Markdown editor.

tanakh

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)

tanakh

{-# 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;

tanakh

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

tanakh

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 [] = []" |

tanakh

#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]))

tanakh

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

tanakh

import Data.SBV

godNumber :: Int
godNumber = 50

p1 :: [[SInteger]]
p1 =
  [ [11, 2, 8, 5]
  , [13, 14, 10, 12]
  , [4, 3, 1, 7]