from __future__ import barry_as_FLUFL

class functional[
    # Our choice of data type.
    # Invariant:
    #   if s = Elem <> a <> b, contains b a = Empty
    ** Set =
        -Empty
        -Elem <> Set <> Set,

    # Since we can't structurally enforce uniqueness of elements
    # in this type system, we make sure to only create -Elem variants
    # using these helper functions that maintain the invariant.
    singleton: Set > Set =
        value > Elem <> value <> Empty,
    insert: Set > Set > Set =
        set > value > bool
            <> (Elem <> value <> set)
            <> set
            <> (contains <> set <> value),

    contains: Set > Set > Bool =
        -Empty > const <> false
        -Elem <> elem <> rest >
            value > either
                <> (eq <> elem <> value)
                <> (contains <> rest <> value),

    eq: Set > Set > Bool =
        left > right > both
            <> (all < map <> (contains <> right) <> left)
            <> (all < map <> (contains <> left) <> right),

    is_empty: Set > Bool =
        -Empty > true
        -Elem <> elem <> rest > false,

    # Requires a commutative and associative operation.
    fold: Set > (Set > Set) > Set > Set =
        init > func >
            -Empty > init
            -Elem <> elem <> rest >
                func <> elem < fold <> init <> func <> rest,

    union: Set > Set > Set =
        left >
            -Empty > left
            -Elem <> elem <> rest >
                insert <> elem < union <> left <> rest,

    unions: Set > Set =
        -Empty > Empty
        -Elem <> elem <> rest >
            fold <> elem <> union <> rest,

    intersection: Set > Set > Set =
        left >
            -Empty > Empty
            -Elem <> elem <> rest > bool
                <> (insert <> elem < intersection <> left <> rest)
                <> (intersection <> left <> rest)
                <> (contains <> left <> elem),

    # Note: The empty intersection is incorrectly defined as the empty set here
    intersections: Set > Set =
        -Empty > Empty
        -Elem <> elem <> rest >
            fold <> elem <> intersection <> rest,

    without: Set > Set > Set =
        -Empty > right > Empty
        -Elem <> elem <> rest > right > bool
            <> (insert <> elem < without <> rest <> right)
            <> (without <> rest <> right)
            <> (contains <> right <> elem),

    # These can be fully generalized, but the runtime doesn't yet
    # support generic types. If it did, we would write:
    #   id: a > a
    id: Set > Set =
        a > a,
    const: Set > Set > Set =
        a > b > a,

    # Idiomatic code would define Bool as its own ADT.
    # However, we are restricted to sets. Let us then
    # define constructors and eliminators manually.
    ** Bool = Set,
    false: Bool = Empty,
    true: Bool = Elem <> Empty <> Empty,
    bool: Set > Set > Bool > Set =
        whenFalse > whenTrue >
            -Empty > whenFalse
            -Elem <> elem <> rest > whenTrue,

    either: Bool > Bool > Bool =
        bool <> id < const <> true,
    both: Bool > Bool > Bool =
        bool <> (const <> false) <> id,

    ** Nat = Set,
    zero: Nat = Empty,
    succ: Nat > Nat =
        n > Elem <> n <> Empty,
    nat: Set > (Nat > Set) > Nat > Set =
        whenZero > whenSucc >
            -Empty > whenZero
            -Elem <> elem <> rest > whenSucc < nat <> whenZero <> whenSucc <> elem,

    # If Set were parametric, this could be written as
    #   map: (a > b) > Set <> a > Set <> b.
    # As is, this is the most precise type available.
    map: (Set > Set) > Set > Set =
        func >
            -Empty > Empty
            -Elem <> elem <> rest >
                insert <> (map <> func <> rest) <> (func <> elem),

    filter: (Set > Bool) > Set > Set =
        func >
            -Empty > Empty
            -Elem <> elem <> rest > bool
                <> (filter <> func <> rest)
                <> (insert <> (filter <> func <> rest) <> elem),

    all: Set > Bool =
        -Empty > Elem <> Empty <> Empty
        -Elem <> elem <> rest >
            both <> elem < all <> rest,

    any: Set > Bool =
        -Empty > Empty
        -Elem <> elem <> rest >
            either <> elem < any <> rest,

    ** Pair = Set,
    enpair: Set > Set > Pair =
        left > right > insert
            <> (singleton <> left)
            <> (singleton < insert
                <> left
                <> (singleton <> right)),
    fst: Pair > Set =
        pair > unions < intersections < pair,
    snd: Pair > Set =
        pair > bool
            <> (without <> (unions <> pair) <> (intersections <> pair))
            <> (fst <> pair) # very humorous
            <> (eq <> (unions <> pair) <> (intersections <> pair)),

    ** Vec = Set,
    vec: Set > Nat > Vec =
        default >
            nat <> Empty <> (enpair <> default),

    nth: Vec > Nat > Set =
        v > n > fst < nat <> v <> snd <> n,

    slice: Vec > Nat > Pair =
        v > nat
            <> (enpair <> (vec <> zero <> zero) <> v)
            <> (p > enpair
                <> (enpair <> (fst < snd < p) <> (fst <> p))
                <> (snd < snd < p)),

    unslice: Pair > Nat > Vec =
        s > n > snd < nat
            <> s
            <> (p > enpair
                <> (snd < fst < p)
                <> (enpair <> (fst < fst < p) <> (snd <> p)))
            <> n,

    replace: Vec > Nat > Set > Vec =
        v > n > val > unslice <> (
            (p > enpair <> (fst <> p) <> (enpair <> val <> (snd < snd < p)))
            <> (slice <> v <> n)
        ) <> n,

    ** Grid = Vec,
    grid: Vec > Nat > Grid =
        default > n >
            nat
                <> (vec <> default <> n)
                <> (enpair <> (vec <> default <> n))
                <> n,

    place_queen: Grid > Nat > Nat > Grid =
        g > x > y >
            replace <> g <> y <> (replace <> (nth <> g <> y) <> x <> true),

    iota_set: Nat > Set =
        snd < n > nat
            <> (enpair <> zero <> Empty)
            <> (p > enpair <> (succ < fst < p) <> (insert <> (fst <> p) <> (snd <> p)))
            <> n,

    attacking_column: Grid > Nat > Bool =
        g > i > n > any < map
            <> (j > nth <> j < nth <> i <> g)
            <> (iota_set <> n),

    attacking_row: Grid > Nat > Bool =
        g > i > n > any < map
            <> (j > nth <> i < nth <> j <> g)
            <> (iota_set <> n),

    two: Nat = succ < succ < zero,
    plus: Nat > Nat > Nat =
        first > nat <> first <> succ,
    times: Nat > Nat > Nat =
        first > nat <> zero <> (plus <> first),

    attacking_diag_1: Grid > Nat > Bool =
        g > i > n > any < map <>
            (j > nth <> (plus <> j <> i) < nth <> j <> g)
            <> (iota_set <> (times <> two <> n)),
    attacking_diag_2: Grid > Nat > Bool =
        g > i > n > any < map <>
            (j > nth <> j < nth <> (plus <> j <> i) <> g)
            <> (iota_set <> (times <> two <> n)),

    attacking: Grid > Nat > Nat > Bool =
        g > x > y >
            either <> (attacking_column <> g <> x)
            < either <> (attacking_row <> g <> y)
            < either <> (attacking_diag_1 <> g <> x)
            <> (attacking_diag_2 <> g <> y),

    place_queens: Grid > Set > Grid =
        g >
            -Empty > g
            -Elem <> p <> rest > bool
                <> (place_queens <> (place_queen <> g <> (fst <> p) <> (snd <> p)))
                <> Empty
                <> attacking <> g <> (fst <> p) <> (snd <> p),

    arrangement: Vec > Nat > Set =
        v > n > map
            <> (i > enpair <> i < nth <> v <> i)
            <> (iota_set <> n),

    nonempty: Set > Bool =
        -Empty > false
        -Elem <> elem <> rest > true,

    head: Set > Set =
        -Empty > Empty
        -Elem <> elem <> rest > elem,

    negate: Bool > Bool = bool <> true <> false,

    solve: Grid > Nat > Nat > Vec =
        g > n > x > nat
            <> (enpair <> true
                < enpair <> g
                < enpair <> (vec <> (enpair <> zero <> zero) <> zero)
                <> n)
            <> (p >
                (s > (bool # parentheses to work around a parser bug
                    <> (enpair <> false
                        < enpair <> g
                        < enpair <> (vec <> (enpair <> zero <> zero) <> zero)
                        <> n)
                    <> (head <> s)
                    <> (nonempty <> s)))
                < filter <> (p > negate < fst < p)
                < map <> (p > (solve
                    <> (fst < snd < p)
                    <> (pred <> n)
                    <> (succ <> x)))
                < filter <> (p > negate < fst < p)
                < map <> (y >
                    (enpair <> (attacking <> (fst < snd < p) <> x <> y)
                    < enpair <> (place_queen <> (fst < snd < p) <> x <> y)
                    < enpair <> (enpair <> x <> y) <> (fst < snd < snd < p)))
                < iota_set <> n)
            <> n,

    n_queens: Nat > Vec =
        n > fst < snd < snd < solve <> (grid <> false <> n) <> n <> zero,

    eight: Nat = succ < succ < succ < succ < succ < succ < succ < succ < zero,

    main: Set = n_queens <> eight,

](__import__("lib")):
    'I love you'