module Quox.Scoped

import public Quox.Var
import public Quox.Context

import Derive.Prelude

%language ElabReflection
%default total


public export
data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
  Y : (body : f (s + n)) -> ScopedBody s f n
  N : (body : f n)       -> ScopedBody s f n
%name ScopedBody body

export %inline %hint
EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n)
EqScopedBody = deriveEq

export %inline %hint
ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
ShowScopedBody = deriveShow

||| a scoped term with names
public export
record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
  constructor S
  names : BContext s
  body  : ScopedBody s f n
%name Scoped body

export %inline
(forall n. Eq (f n)) => Eq (Scoped s f n) where
  s == t = s.body == t.body

export %inline %hint
ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
ShowScoped = deriveShow


||| scope which ignores all its binders
public export %inline
SN : Located1 f => {s : Nat} -> f n -> Scoped s f n
SN body = S (replicate s $ BN Unused body.loc) $ N body

||| scope which uses its binders
public export %inline
SY : BContext s -> f (s + n) -> Scoped s f n
SY ns = S ns . Y

public export %inline
name : Scoped 1 f n -> BindName
name (S [< x] _) = x

public export %inline
(.name) : Scoped 1 f n -> BindName
s.name = name s