Skip to content

Instantly share code, notes, and snippets.

@maxkrieger
Created Mar 29, 2021
Embed
What would you like to do?
Synapse Act 4: a trio from https://penrose.ink
type Set
type Point
type Map
constructor Singleton : Point p -> Set
function Intersection : Set a * Set b -> Set
function Union : Set a * Set b -> Set
function Subtraction : Set a * Set b -> Set
function CartesianProduct : Set a * Set b -> Set
function Difference : Set a * Set b -> Set
function Subset : Set a * Set b -> Set
function AddPoint : Point p * Set s1 -> Set
predicate Not : Prop p1
predicate From : Map f * Set domain * Set codomain
predicate Empty : Set s
predicate Intersecting : Set s1 * Set s2
predicate IsSubset : Set s1 * Set s2
predicate PointIn : Set s * Point p
predicate In : Point p * Set s
predicate Injection : Map m
predicate Surjection : Map m
predicate Bijection : Map m
predicate PairIn : Point * Point * Map
notation "A ⊂ B" ~ "IsSubset(A, B)"
notation "p ∈ A" ~ "PointIn(A, p)"
notation "p ∉ A" ~ "PointNotIn(A, p)"
notation "A ∩ B = ∅" ~ "Not(Intersecting(A, B))"
notation "f: A -> B" ~ "Map f; From(f, A, B)"
Set x {
x.shape = Circle {
strokeWidth : 0.
}
x.shading = Image {
center : x.shape.center
w : x.shape.r * 2.0
h : x.shape.r * 2.0
path : "shading.svg"
}
x.shadow = Image {
path : "shadow.svg"
w : x.shape.r * 2.15
h : x.shape.r * 2.22
center : (x.shape.center[0] + 0.03 * x.shading.w, x.shape.center[1] - 0.051 * x.shading.h)
}
x.text = Text {
string : x.label
color: rgba(1.0, 1.0, 1.0, 1.0)
w: 0.5 * x.shape.r
h: 0.5 * x.shape.r
}
ensure contains(x.shape, x.text)
ensure minSize(x.shape)
ensure maxSize(x.shape)
encourage sameCenter(x.text, x.shape)
x.shape below x.text
x.shading below x.shape
x.shadow below x.shading
}
forall Set x; Set y
where IsSubset(x, y) {
ensure smallerThan(x.shape, y.shape)
ensure outsideOf(y.text, x.shape)
ensure contains(y.shape, x.shape, 5.0)
x.shape above y.shape
y.text below x.shape
x.shadow above y.shape
}
Set x; Set y
where Not(Intersecting(x, y)) {
ensure disjoint(x.shape, y.shape)
}
Set x; Set y
where Intersecting(x, y) {
ensure overlapping(x.shape, y.shape)
ensure outsideOf(y.text, x.shape)
ensure outsideOf(x.text, y.shape)
}
Set A
Set B
Set C
Set D
Set E
Set F
Set G
IsSubset(B, A)
IsSubset(C, B)
IsSubset(D, C)
IsSubset(E, D)
IsSubset(F, E)
IsSubset(G, F)
AutoLabel All
{"authorship":{"madeBy":"maxkrieger","name":"Synapse Act 4","avatar":"https://avatars.githubusercontent.com/u/2660634?v=4"}}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment