Skip to content

Instantly share code, notes, and snippets.

@tangentstorm
tangentstorm / ed.ijs
Last active Jul 29, 2021
A tiny editor in J
View ed.ijs
NB. Core logic for a tiny editor in J.
NB. No select/copy/paste (in this gist), but it does support multiple cursors.
NB. This started as the code for editing a single line of text, but I'm now
NB. using three copies simultaneously: one for a single token, one for
NB. boxed tokens on a line, and one for boxed lines in a buffer.
coclass 'ed'
init =: {{
B =: '' NB. the buffer to edit.
C =: 0 NB. cursor position(s)
@tangentstorm
tangentstorm / parsers.ijs
Last active Jul 7, 2021
parser combinators for J
View parsers.ijs
clear''
NB. Parser Combinators for J
NB.
NB. The semantics here are heavily inspired by
NB. Allesandro Warth's ometa system:
NB.
NB. http://tinlizzie.org/ometa/
NB.
NB. but implemented as parser combinators rather than a standalone language.
NB.
@tangentstorm
tangentstorm / asmvm.js
Last active Jul 2, 2021
ASM vm... This started as an attempt at a bootstrapping virtual machine, then I got caught up with the idea that bytecode could be human readable, and it probably got a bit out of hand.
View asmvm.js
const DATA=0, CALL=1, WORK=2, TEMP=3
class Worker {
vm = null // virtual machine
w = 0 // worker number
f = 0 // function pointer
e = 0 // execution pointer
t = 0 // current token in function
@tangentstorm
tangentstorm / meld.js
Created Dec 2, 2020
meld a list of dictionaries into a smaller list of dictionaries
View meld.js
glue = (x,y) => x === undefined ? y : Array.isArray(x) ? x.concat(y) : [x,y]
function meld(xs) {
let idx = {}, res = [], it
for (x of xs) {
if (x.id in idx) it = res[idx[x.id]]
else { it = {id: x.id}; idx[x.id] = res.length; res.push(it) }
for (k of Object.keys(x)) if (k!=='id') it[k] = glue(it[k], x[k]) }
return res }
View catalan-1-filter.ijs
c =: '01' ([: +/ =)"0 _ ] NB. count 0 and 1
t =: {{(*/ <:/"1 c\ y) *. =/c y }} NB. the two rules
g =: {{'01' {~ #:i.2^2*y}} NB. generate the numbers
f =: {{y {~ I.t"1 y}} NB. filter by t
f g 3
@tangentstorm
tangentstorm / animation.ijs
Created Aug 12, 2019
Basic animation in J
View animation.ijs
NB. Code from the "Basic Animation In J" video
NB. https://www.youtube.com/watch?v=uL-70fMTVnw
NB. ------------------------------------------------------------------------
NB. animation demo
load 'viewmat'
coinsert'jgl2'
wd 'pc w0 closeok' NB. parent control (window) named 'w0'
View collatz.ijs
C =: -:`(1+3&*)@.(2&|)"0
R =: -:^:(-.@(2&|))^:_
S =: 1 + 3&*
T =: R@([`S@.(2&|))"0
T i. 10
@tangentstorm
tangentstorm / failure.thy
Created Aug 1, 2018
how do i do this in isabelle?
View failure.thy
(* how do i do this?? *)
function simplex_count :: "int⇒int⇒int" where
"simplex_count 0 0 = 1" |
"simplex_count 0 1 = 0" |
"simplex_count 1 0 = 2" |
"simplex_count n k = (simplex_count (n-1) k + simplex_count n (k-1))"
sorry
lemma simplex_count_lemma:
@tangentstorm
tangentstorm / Poly100.thy
Last active Aug 9, 2018
start on a proof of the polyhedron formula
View Poly100.thy
(* Isar Proofs (eventually) for three theorems from http://www.cs.ru.nl/~freek/100/
#13 Polyhedron Formula (F + V - E = 2)
#50 The Number of Platonic Solids
#92 Pick's theorem
*)
theory Poly100
imports Main "HOL.Binomial" "HOL-Analysis.Polytope"
begin
View TopSpace.thy
(* Topological Spaces
Based on "A Bridge to Advanced Mathematics" by Dennis Sentilles
Translated to Isar by Michal J Wallace *)
theory TopSpace
imports Main
begin
textA topological space (X,T) is a pair where X is a set whose elements
are called the "points" of the topological space, and T is a fixed collection of
subsets of X called neighborhoods, with the following properties: