tangentstorm

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

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

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 }

tangentstorm

   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

var b4 = (new function() { var EOF='\0',self = {

    d:[], a:[],                             // data and auxiliary/return stack
    defs:[],core:[],scope:[],               // dictionary
    base:10,                                // numbers
    cp:-1, ch:'\x01',ibuf:[],wd:'',         // lexer state
    compiling:false,state:[],target:[],     // compiler state

    def : function (k,v){
        var res=self.defs.length; self.defs.push(v); self.scope[0].push([k,res]); return res },

tangentstorm

C =: -:`(1+3&*)@.(2&|)"0
R =: -:^:(-.@(2&|))^:_
S =: 1 + 3&*
T =: R@([`S@.(2&|))"0
T i. 10

tangentstorm

(* 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

tangentstorm

(* 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

(* Topological Spaces
   Based on "A Bridge to Advanced Mathematics" by Dennis Sentilles
   Translated to Isar by Michal J Wallace *)
theory TopSpace
  imports Main
begin

text ‹A 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:›

tangentstorm

(* Simple Group Theory from Scratch *)
theory MJWGroups
  imports Pure
begin

locale group =
  fixes op :: "'g ⇒ 'g ⇒ 'g" (infixl "∘" 65)
  fixes id :: "'g" ("𝔦")
  fixes inv :: "'g ⇒ 'g"
  assumes assoc: "(a ∘ b) ∘ c == a ∘ (b ∘ c)"