// 10. effect 검사기가 거부해야 하는 코드
//
// 09와 같은 이유로 외부 타입이 하나도 없다. capability를 이 파일에서 정의해야
// 메서드의 effect가 알려지고, 검사기가 실제로 판정할 수 있다.

pub capability Db {
    fn read(id: Int) effects {Db.read} -> Int
    fn write(id: Int, v: Int) effects {Db.write}
}

pub capability Log {
    fn write(msg: String) effects {Log.write}
}

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

pub fn get(db: Db, id: Int) effects {Db.read} -> Int {
    db.read(id)
}

pub fn copy(db: Db, from: Int, to: Int) effects {Db.read, Db.write} {
    db.write(to, db.read(from))
}

// 헬퍼를 부르면 헬퍼의 effect를 물려받는다
pub fn get_twice(db: Db, id: Int) effects {Db.read} -> Int {
    get(db, id) + get(db, id)
}

// effect 변수: 결정 위치의 변수가 인자의 effect로 묶인다
pub fn twice[e: effects](f: fn() effects e) effects e {
    f()
    f()
}

pub fn log_twice(log: Log) effects {Log.write} {
    twice(fn() { log.write("hi") })
}

// effect 없는 함수는 effects 절이 없다
pub fn pure_add(a: Int, b: Int) -> Int {
    a + b
}

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

// [E-effect-undeclared] 선언 없이 capability 메서드를 부른다
pub fn silent_read(db: Db) -> Int {
    db.read(1)
}

// [E-effect-undeclared] 일부만 선언했다
pub fn partial(db: Db, id: Int) effects {Db.read} {
    db.write(id, db.read(id))
}

// [E-effect-undeclared] 헬퍼가 수행하는 effect도 물려받아야 한다
pub fn via_helper(db: Db, id: Int) -> Int {
    get(db, id)
}

// [E-effect-undeclared] 클로저를 통해 새어 나오는 effect
pub fn via_closure(log: Log) {
    twice(fn() { log.write("hi") })
}

// [E-effect-closure-annotated] 클로저가 선언한 것보다 많이 수행한다
pub fn closure_lies(log: Log) effects {Log.write} {
    twice(fn() effects {} { log.write("hi") })
}

// [E-effect-param] 파라미터가 허용한 effect를 넘는 함수를 넘긴다
pub fn takes_pure(f: fn() effects {}) {
    f()
}

pub fn pass_impure(log: Log) effects {Log.write} {
    takes_pure(fn() { log.write("hi") })
}

// [E-capability-static] capability 메서드를 타입 이름으로 부른다.
// 이것이 허용되면 capability 없이 effect를 수행할 수 있게 되어
// "capability 없이는 effect를 수행할 수 없다"는 정리가 무너진다.
pub fn no_instance() effects {Db.read} -> Int {
    Db.read(1)
}