data Term
___ = Lazy Term Env -- lazy evaluation
___ | IVar Int -- de bruijn index
___ | ICon String -- data constructor
___ | IApp Term Term -- term application
___ | IAbs Term -- term abstraction
___ deriving (Eq)
data Env = Env {
___ getScope :: Int, -- current scope
___ getBindings :: [(Int, Maybe Term)] -- list of pairs of scope and ptr
} deriving (Eq)
전역 범위는 0에 대응되는 스코프이고,
람다 안으로 들어갈 때랑 let binding 안으로 갈 때 스코프의 값이 1씩 증가하도록 하고 싶은데,
아무리 고민해도 함수 rewrite :: Term -> Env -> Term를 못 짜겠음.
ptr은 변수가 바인딩된 항을 가르킴


- dc official App