60 lines
1.3 KiB
Idris
60 lines
1.3 KiB
Idris
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
|