Skip to content

Instantly share code, notes, and snippets.

View tangentstorm's full-sized avatar

tangentstorm tangentstorm

171 followers · 137 following
View GitHub Profile
@tangentstorm
tangentstorm / IntListAsNum.hs
Last active August 29, 2015 14:08
{-# Language FlexibleInstances, ConstraintKinds #-}
module IntListAsNum where
-- IntList :: Num implementation
--
-- At the GHCi prompt the expression "take 5 10" yields
-- the strange error message:
--
-- No instance for (Num [a0]) arising from a use of ‘it’
-- In a stmt of an interactive GHCi command: print it
@tangentstorm
tangentstorm / proof
Last active August 29, 2015 14:09
a proof language (embedded in nial)
r0 := ("^^>^* (ph 'exponent rule')
(("$x "^ "$y) "^ "$z)
"= (("$x "^ ("$y "* "$z))))
r1 := ("xy>yx (ph 'commutative rule for *')
("x "* "y)
"= ("y "* "x))
@tangentstorm
tangentstorm / paging.md
Created November 14, 2014 13:47
(probably not paging) a wild guess about what i think paging might be

Most modern operating systems allow running many programs simultaneously.

There's no way to know how much ram a particular program will need, since this might depend on user actions (like opening a file). This means there's no way for the operating system to allocate a fixed chunk of ram for each process.

Since the amount of ram required by a process may change over time, you might want to leave lots of room for each process to grow.

On the other hand, RAM is a limited resource on a computer, so you want to pack the processes together tightly in ram.

@tangentstorm
tangentstorm / program-composition.org
Last active August 29, 2015 14:09

“Here’s an example. In one integer variable x , the specification x′=x ∨ x′=x+1 says that the final value of x is either the same as the initial value or one greater. Let’s compose it with itself.

   x′=x ∨ x′=x+1 . x′=x ∨ x′=x+1
= ∃x′′· (x′′=x ∨ x′′=x+1) ∧ (x′=x′′ ∨ x′=x′′+1) 
 distribute ∧ over ∨
= ∃x′′· x′′=x ∧ x′=x′′ ∨ x′′=x+1 ∧ x′=x′′ ∨ x′′=x ∧ x′=x′′+1 ∨ x′′=x+1 ∧ x′=x′′+1   
 distribute ∃ over ∨
= (∃x′′· x′′=x ∧ x′=x′′) ∨ (∃x′′· x′′=x+1 ∧ x′=x′′) ∨ (∃x′′· x′′=x ∧ x′=x′′+1) ∨ (∃x′′· x′′=x+1 ∧ x′=x′′+1) 
 One Point, 4 times
@tangentstorm
tangentstorm / doctest.ijs
Created November 29, 2014 10:03
NB. doctest
NB. unicode box chars. (j magically translates these to unicode for display)
uboxch=: [: (9!:7) (a.{~16 17 18 19 20 21 22 23 24 25 26)"_
aboxch =: 16 26 17 18 25 22 23 24 19 20 21
NB. ┌ ─ ┬ ┐ │ └ ┴ ┘ ├ ┼ ┤
uboxch =: 9484 9472 9516 9488 9474 9492 9524 9496 9500 9532 9508
forcerank =: ,@] $~ -@[ {.!.1 [: $ ]
@tangentstorm
tangentstorm / exponents.thy
Created December 23, 2014 05:45
theory Exponents
imports Main
begin
lemma rMulComm: "(a*b ::int) = (b*a ::int)"
by (rule Groups.ab_semigroup_mult_class.mult.commute)
lemma rExpMul: "((a^b)^c ::int) = (a^(b*c) ::int)"
by (rule Int.zpower_zpower)
@tangentstorm
tangentstorm / gist:3449f2372fc4843c8313
Created December 29, 2014 02:32
blit ~:/\^:(<32) ]32$1
▛▛▛▛▛▛▛▛▛▛▛▛▛▛▛▛
▛ ▛ ▛ ▛ ▛ ▛ ▛ ▛
▛▛ ▛▛ ▛▛ ▛▛
▛ ▛ ▛ ▛
▛▛▛▛ ▛▛▛▛
▛ ▛ ▛ ▛
▛▛ ▛▛
▛ ▛
▛▛▛▛▛▛▛▛
@tangentstorm
tangentstorm / gist:0c4052c492db4061a96e
Created December 31, 2014 06:01
23:51:07 j-bot tangentstorm: |▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟▝▟|
23:51:07 j-bot tangentstorm: | ▝▄▟ ▝▄▟ ▝▄▟ ▝▄▟ ▝▄▟ ▝▄▟ ▝▄▟ ▝▄▟|
23:51:07 j-bot tangentstorm: | ▝▟ ▝▟ ▝▟ ▝▟ ▝▟ ▝▟ ▝▟ ▝▟|
23:51:07 j-bot tangentstorm: | ▝▄▄▄▟ ▝▄▄▄▟ ▝▄▄▄▟ ▝▄▄▄▟|
23:51:28 tangentstorm neat, huh?
23:52:21 tangentstorm the sierpinski pattern continues until it makes a 64x64 grid.
23:52:32 tangentstorm if i'd used 7 variables, it would be 128*128.. and so on.
23:52:58 tangentstorm here is the derivative of each line.
23:53:04 tangentstorm oh that sucks. :/
23:53:18 tangentstorm [ pb bd a,b,(a and b),c,(c and a),(c and b),(c and b and a),d
@tangentstorm
tangentstorm / minij.js
Created January 7, 2015 12:36
var ometajs_ = require("ometajs");var AbstractGrammar = ometajs_.grammars.AbstractGrammar;var BSJSParser = ometajs_.grammars.BSJSParser;var BSJSIdentity = ometajs_.grammars.BSJSIdentity;var BSJSTranslator = ometajs_.grammars.BSJSTranslator;// mini-j interpreter
// just enough j to handle simple boolean expressions
int = function (s) { return parseInt(s,10); }
ints = function (s) { return s.split(" ").map(int); }
var minij = function minij(source, opts) {AbstractGrammar.call(this, source, opts)};minij.grammarName = "minij";minij.match = AbstractGrammar.match;minij.matchAll = AbstractGrammar.matchAll;exports.minij = minij;require("util").inherits(minij, AbstractGrammar);minij.prototype["j"] = function $j() {return (this._rule("bits",false,[],null,this["bits"]))};
minij.prototype["bits"] = function $bits() {return (this._atomic(function() {var bs;return this._list(function() {return this._rule("bit",false,[],null,this["bit"]) && this._many(function() { return this._atomic(function() { return (this._many(funct
@tangentstorm
tangentstorm / idrislog.txt
Created February 5, 2015 23:57
Resolving dependencies...
[1 of 1] Compiling Main ( /tmp/haskeline-0.7.1.3-55923/haskeline-0.7.1.3/dist/setup/setup.hs, /tmp/haskeline-0.7.1.3-55923/haskeline-0.7.1.3/dist/setup/Main.o )
Linking /tmp/haskeline-0.7.1.3-55923/haskeline-0.7.1.3/dist/setup/setup ...
Configuring haskeline-0.7.1.3...
Building haskeline-0.7.1.3...
Preprocessing library haskeline-0.7.1.3...
[ 1 of 27] Compiling System.Console.Haskeline.Recover ( System/Console/Haskeline/Recover.hs, dist/build/System/Console/Haskeline/Recover.o )
[ 2 of 27] Compiling System.Console.Haskeline.Directory ( dist/build/System/Console/Haskeline/Directory.hs, dist/build/System/Console/Haskeline/Directory.o )
[ 3 of 27] Compiling System.Console.Haskeline.Key ( System/Console/Haskeline/Key.hs, dist/build/System/Console/Haskeline/Key.o )
[ 4 of 27] Compiling System.Console.Haskeline.History ( System/Console/Haskeline/History.hs, dist/build/System/Console/Haskeline/History.o )