Skip to content

Instantly share code, notes, and snippets.

View eduardoleon's full-sized avatar

eduardoleon

View GitHub Profile
create table male
( male_id int not null
, name varchar(100) not null
, primary key (male_id) );
create table female
( female_id int not null
, name varchar(100) not null
, primary key (female_id) );
@eduardoleon
eduardoleon / Queue.sml
Last active July 5, 2016 09:01
Okasaki's real-time queues
infixr 5 :::
datatype 'a stream = Nil | ::: of 'a * 'a stream lazy
signature QUEUE =
sig
type 'a queue
val empty : 'a queue
val snoc : 'a queue * 'a -> 'a queue
@eduardoleon
eduardoleon / mtc-elab.sml
Created July 11, 2016 16:11
Modular type classes are defined by elaboration
using IntOrd
(* `Heap` elaborates to `Heap(IntOrd)`,
* so `val xs : Heap(IntOrd).t` *)
val xs = Heap.fromList [1,2,3];
(* shadows previous `using` declaration *)
using Backwards(IntOrd)
(* `Heap` elaborates to `Heap(Backwards(IntOrd))`,
@eduardoleon
eduardoleon / Unsound.hs
Created August 4, 2016 18:43
Haskell is logically unsound
import Control.Monad
newtype Mu a = Mu { unMu :: Mu a -> a }
bottom :: a
bottom = id <*> Mu $ join unMu
@eduardoleon
eduardoleon / specs-1
Last active August 13, 2017 00:31
dmidecode's output
# dmidecode 3.0
Getting SMBIOS data from sysfs.
SMBIOS 3.0 present.
87 structures occupying 4071 bytes.
Table at 0x8B256000.
Handle 0x0000, DMI type 0, 24 bytes
BIOS Information
Vendor: American Megatrends Inc.
Version: 3.40
@eduardoleon
eduardoleon / blass.hs
Last active February 20, 2017 04:23
“Seven Trees in One” by Andreas Blass
import Test.QuickCheck
data Tree = L | N Tree Tree deriving (Eq, Show)
data Herp
= H0
| H1 Tree
| H2 Tree Tree
| H3 Tree Tree Tree
| H4 Tree Tree Tree Tree
In file included from /usr/include/c++/7.2.1/cstdlib:75:0,
from /usr/include/c++/7.2.1/bits/stl_algo.h:59,
from /usr/include/c++/7.2.1/algorithm:62,
from ../win32xx/include/wxx_appcore0.h:110,
from ../win32xx/include/wxx_appcore.h:57,
from ../win32xx/include/wxx_wincore.h:96,
from frame.cpp:1:
/usr/include/stdlib.h:310:5: error: ‘int32_t’ does not name a type; did you mean ‘wint_t’?
int32_t *fptr; /* Front pointer. */
^~~~~~~
@eduardoleon
eduardoleon / series.wl
Created June 3, 2018 00:12
Problem 4.1.(ii) from Teschl's book
w[0] := a
w[1] := -a^2
w[2] := a^3
w[3] := -a^4 + 1/3
w[k_] := w[k] = -Sum[ w[i-1] * w[k-i] / k, {i, k} ] // Simplify
init {
int x = 123;
int y = 456;
int max;
if
:: x >= y -> max = x
:: y >= x -> max = y
fi
}
@eduardoleon
eduardoleon / bridge.pml
Created September 1, 2018 04:26
Promela model for the problem about people crossing a bridge or a river or whatever
mtype = { left, right }
inline shift(source, target) {
/* select who goes */
if
:: side[0] == source -> pick = 0
:: side[1] == source -> pick = 1
:: side[2] == source -> pick = 2
:: side[3] == source -> pick = 3
fi