// 05. move / affinity 검사기가 거부해야 하는 코드
//
// 09, 10과 같은 이유로 외부 타입이 하나도 없다. affinity의 뿌리는 capability라
// 자원 타입을 이 파일에서 정의해야 검사기가 affine임을 알 수 있다.
// 외부 타입은 affine임을 증명할 수 없으므로 copyable로 취급된다.

pub capability File {
    fn size() -> Int
}

pub capability Gateway {
    fn refund(id: Int) effects {Gateway.refund}
}

pub capability Registry {
    fn add(h: fn()) effects {Registry.add}
}

// 파일을 소비하는 함수: own 유표기
pub fn close(own f: File) effects {File.close}

// 빌리기만 하는 함수: 무표기
pub fn size_of(f: File) -> Int {
    f.size()
}

// --- 통과해야 하는 것 ---

pub fn use_then_close(own f: File) effects {File.close} -> Int {
    let n = size_of(f)
    close(f)
    n
}

// 양쪽 분기에서 소비하면 통과한다
pub fn both_branches_close(own f: File, c: Bool) effects {File.close} {
    if c {
        close(f)
    } else {
        close(f)
    }
}

// 빌린 값을 다른 빌림 자리로 넘기는 것은 복제가 아니다
pub fn borrow_twice(f: File) -> Int {
    size_of(f) + size_of(f)
}

// affine 값을 capture한 클로저는 affine fn이다
pub fn deferred_close(own f: File) -> affine fn() effects {File.close} {
    fn() { close(f) }
}

// --- 여기서부터 전부 오류다 ---

// [E-move-after-move] affine 값의 이중 소비
pub fn double_close(own f: File) effects {File.close} {
    close(f)
    close(f)
}

// [E-move-join] 분기 병합은 보수적 합집합
pub fn conditional_close(own f: File, c: Bool) effects {File.close} {
    if c {
        close(f)
    }
    close(f)
}

// [E-use-escape] 빌린 값의 반환
pub fn leak_capability(pay: Gateway) -> Gateway {
    pay
}

// [E-use-escape] 빌린 값의 저장
pub struct Holder {
    pay: Gateway,
}

pub fn store_capability(pay: Gateway) -> Holder {
    Holder { pay: pay }
}

// [E-use-escape] 빌린 값을 다른 함수에 소유로 넘긴다
pub fn give_away(f: File) effects {File.close} {
    close(f)
}

// [E-use-escape] 빌린 값을 capture한 클로저를 own 자리에 넘긴다
pub fn register(own h: fn() effects {Gateway.refund}) effects {Registry.add}

pub fn escape_via_closure(pay: Gateway) effects {Registry.add} {
    register(fn() { pay.refund(1) })
}

// [E-affinity-transitive] affine 필드를 가진 타입을 copyable로 선언
pub copyable struct Box {
    f: File,
}

// [E-callable-affinity] affine 값을 capture한 클로저를 fn 위치에 반환
pub fn misuse_affine_closure(own f: File) -> fn() effects {File.close} {
    fn() { close(f) }
}

// [E-closure-mut-capture] 클로저는 mut 바인딩을 capture할 수 없다
pub fn capture_mut(own f: File, pay: Gateway)
    effects {File.close, Registry.add, Gateway.refund} {
    let mut counter = 0
    register(fn() {
        counter = counter + 1
        pay.refund(counter)
    })
    close(f)
}