This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(ℬ (tree) … ((tree ↦ tree_₂))) | |
↦ | |
;;;;; ok cases | |
;; `tree` is either a number, in which case `vertices` returns 1 | |
;; or `tree` is a pair, in which case `vertices`returns an exact positive integer | |
;; Looking up path-condition tails `γ₁` and `γ₂` recursively tell facts | |
;; about `(car tree)` and `(cdr tree)` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
#| | |
let app = 5;; | |
let app = 2;; | |
let z = 3;; | |
let z = 2;; | |
let app = 3 in app + z;; | |
app * z | |
|# |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
(let* ([try (λ (f) (or (f #f) (f #t)))] | |
[p (λ (x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀) | |
(and x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀))] | |
[solve | |
(λ (q) | |
(try (λ (n₁) | |
(try (λ (n₂) | |
(try (λ (n₃) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mkdir -p out | |
cp 01-intro.tex out/01-intro.tex | |
sed -f latex-unicode-pre.sed -i.bak out/01-intro.tex | |
sed -f latex-unicode-escape.sed -i.bak out/01-intro.tex | |
sed -f latex-unicode.sed -i.bak out/01-intro.tex | |
sed -f latex-unicode-unescape.sed -i.bak out/01-intro.tex | |
sed -f latex-unicode-post.sed -i.bak out/01-intro.tex | |
mkdir -p out | |
cp 14-conclusions.tex out/14-conclusions.tex | |
sed -f latex-unicode-pre.sed -i.bak out/14-conclusions.tex |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import pyvw | |
from nltk.corpus import wordnet as wn | |
valid_labels = {'n.act': 0, | |
'n.animal': 1, | |
'n.artifact': 2, | |
'n.attribute': 3, | |
'n.body': 4, | |
'n.cognition': 5, | |
'n.communication': 6, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import sys | |
import random | |
# Given file name, make an iterator returning random line batches, each of which is also randomized | |
def iterRandomLines(filename): | |
batches = readBatches(filename) | |
random.shuffle(batches) | |
for lines in batches: | |
random.shuffle(lines) #FIXME: we don't want to randomize lines within each batch | |
for line in lines: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import leon.lang._ | |
import leon.lang.synthesis._ | |
import leon.annotation._ | |
object Test { | |
/** Compute n's reciprocal, requiring n != 0 */ | |
def recip (n: Int): Int = { | |
require (n != 0) | |
1 / n |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import leon.lang._ | |
import leon.lang.synthesis._ | |
import leon.annotation._ | |
object BraunTree { | |
sealed abstract class Tree | |
case object Leaf extends Tree | |
case class Node(l: Tree, n: Int, r: Tree) extends Tree | |
def size(t: Tree): Int = t match { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import scala.language.experimental.macros | |
import scala.reflect.macros.blackbox.Context | |
import scala.annotation.StaticAnnotation | |
import scala.annotation.compileTimeOnly | |
/** | |
This annotation turns a simple class declaration into a type-safe and unboxed Enum. | |
It does not attempt to be compatible with Java, because I have no respect for Java. | |
There is an example usage at the end of the file. | |
*/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang typed/racket | |
(define ∅ : (Setof Nothing) {set}) | |
(define ∪ set-union) | |
(define ∩ set-intersect) | |
(define ∋ set-member?) | |
(: fix : (∀ (X) (X → X) X → X)) | |
;; Compute `f`'s fixpoint starting from `x` | |
(define (fix f x) |