cbiffle

fs = require 'fs'
path = require 'path'
events = require 'events'

# Recursively walks a filesystem tree, emitting what it finds.
# The EventEmitter produces the following events:
#  ('file', pathname) for each file discovered.
#  ('dir',  pathname) for each directory discovered.
#  ('end') when traversal is complete.
walk = (pathname) ->

cbiffle

crypto = require 'crypto'

hash = crypto.createHash('sha256')

x = hash.update
x("foo")

cbiffle

#!/usr/bin/env coffee
#
# This simulates a common pattern for deriving encryption keys
# from passwords.  It's somewhat alarming how fast computers
# have become.  You may have to try round counts over 100k to
# get a useful measurement!
#
# To use:
#  coffee hash-benchmark.coffee <algo> <rounds>
#

cbiffle

// A simple program to help me learn Rust.  This is a functional clone
// of cat circa 6th Edition Unix, before it grew all the options and
// stuff.

use std::env;
use std::io;
use std::fs::File;
use std::io::Write;
use std::io::BufRead;

cbiffle

   Compiling warn v0.1.0 (file:///home/cbiffle/proj/rs/warn)
src/lib.rs:2:3: 2:31 warning: function is never used: `tested`, #[warn(dead_code)] on by default
src/lib.rs:2   pub fn tested() -> i32 { 0 }
               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
src/lib.rs:5:3: 5:33 warning: function is never used: `untested`, #[warn(dead_code)] on by default
src/lib.rs:5   pub fn untested() -> i32 { 0 }
               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     Running target/debug/warn-fef74f9367799b2e

running 1 test

cbiffle

-- This is a reduction of code that I wrote last night.
-- I can use this code to produce a `Void`.

-- Because I'm new to Idris I may have simply misinterpreted
-- what's going on here, so I've tried to specify my
-- understanding in comments.

%default total

data Color = Red | Blue

cbiffle

%default total

data KnownSet : Type where
  Control : KnownSet
  Data : KnownSet

dataNotControl : Not (Data = Control)
dataNotControl Refl impossible

data RState : Type where

cbiffle

||| Demonstration of length preservation during vector concatenation.
||| Derived from Guillaume Allais's Agda original.
|||
||| Ignore the fact that functions here are named "reverse" -- they are really
||| concatenation.
module ConcatVec

import Data.Vect

%default total

cbiffle

module ProofWith

--------------------------------------------------------------------------------
-- Some lemmas used in the proofs below.  I've proposed these for inclusion in
-- the prelude, with cases like this in mind.
--
-- Together, these prove that we can predict the shape of the output of `decEq`
-- if we can either demonstrate propositional equality of its arguments, or
-- show that such equality is ridiculous.

cbiffle

||| Church numerals using explicit lambdas, vs. equational style.  This is
||| a somewhat contrived example to demonstrate how proofs of function
||| equality can succeed for lambdas and fail for equational functions, even
||| though (to a casual observer) there isn't really a difference between the
||| two.
module ChurchLambda

-- Because I like the same names as the Prelude.  I admit I don't really
-- understand why names defined in this module don't just "win", but that's
-- not the point of this gist.  Keep scrolling.