moea

;; ============================================================================
;; JSON parser, built on algebraic effects + multi-shot continuations,
;; with a homegrown combinator DSL on top of `defmacro`.
;;
;; The bottom of the file (the actual grammar) reads close to BNF:
;;
;;   (deftoken null  "null"  (JNull))
;;   (deftoken true  "true"  (JBool true))
;;   (defparser json-array
;;     (JArr (between! "[" (sep! json-value ",") "]")))

moea

(effect Rand
  (rand-int :: (-> int int))
  (rand     :: (-> float)))

(define with-rng :: (forall [A e] (-> int (-> A ! <Rand ...e>) A ! <...e>))
  (fn [seed thunk]
    (let [_ (_rng-seed seed)]
      ((handler
        (return v -> v)
        ((rand-int n) k -> (resume k (_rand-int n)))

moea

;; AVL Tree

(deftype-alias AVLL [A X] (AVL (refine v A (< v X))))
(deftype-alias AVLR [A X] (AVL (refine v A (> v X))))

;; ---- Data declaration (every Node verifies BST + balance + height) ----

(deftype AVL [A]
  (Leaf)
  (Node :key    A

moea

;; Invariants are baked into the data definition. Each Node construction
;; verifies the AVL invariant locally; the smart constructor `mk-node`
;; both verifies its inputs and certifies its output.

(deftype AVL [A]
  (Leaf)
  (Node :key    A
        :left   (AVL A)
        :right  (refine right (AVL A)
                  (<= (abs (- (avl-height left) (avl-height right))) 1))

moea

package main

import (
	"errors"
	"fmt"
	"io"
	"os"

	"github.com/consensys/gnark-crypto/ecc/bn254"
	"github.com/consensys/gnark-crypto/ecc/bn254/fr"

moea

(ns thebes.gadt
  (:require [clojure.string :as str]
            [clojure.walk   :as walk]))

(defrecord TypeVar [name])
(defrecord Variant [name tag params ret-type])
(defrecord TypeApp [name args])

(defn type-var?    [t] (instance? TypeVar t))
(defn variant?     [t] (instance? Variant t))

moea

(ns assistant.reader
  (:import [java.io PushbackReader StringReader]))

(defprotocol Reader
  (read-char   [this])
  (peek-char   [this])
  (unread-char [this ch])
  (eof?        [this]))

(extend-type PushbackReader

moea

#lang turnstile/base

(provide (type-out →) λ #%app ann #%module-begin #%top-interaction require)

(require (for-syntax "util/filter-maximal.rkt"))

(define-binding-type ∀)

(define-typed-syntax (Λ (tv:id ...) e) ≫
  [[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ]

moea

;; NB there is a bug when switching between circles/ellipses.  Anyone spot it?

(ns perturb.arcs
  (:require [perturb.util
             :refer [cos
                     sin
                     PI
                     TAU
                     avg
                     rad

moea

(ns perturb.interp)

(defn pts->path [pts]
  (flatten
   (into [(into ["M"] (first pts))]
     (for [pt (rest pts)]
       (into ["L"] pt)))))

(let [v 6
      c (fn cubic [[x0 y0] [x1 y1] [x2 y2] [x3 y3]]