module Abt.Concrete.LocallyNameless
( Tm(..)
, Tm0
, _TmOp
, Var(..)
, varName
, varIndex
) where
import Abt.Types.Nat
import Abt.Types.View
import Abt.Class.HEq1
import Abt.Class.Show1
import Abt.Class.Abt
import Abt.Class.Monad
import Control.Applicative
import Data.Profunctor
import Data.Vinyl
data Var
= Var
{ _varName ∷ !(Maybe String)
, _varIndex ∷ !Int
}
instance Show Var where
show (Var (Just v) _) = v
show (Var Nothing i) = "@" ++ show i
instance Eq Var where
(Var _ i) == (Var _ j) = i == j
instance Ord Var where
compare (Var _ i) (Var _ j) = compare i j
varName
∷ Functor f
⇒ (Maybe String → f (Maybe String))
→ Var
→ f Var
varName i (Var n j) =
(\n' → Var n' j)
<$> i n
varIndex
∷ Functor f
⇒ (Int → f Int)
→ Var
→ f Var
varIndex i (Var n j) =
(\j' → Var n j')
<$> i j
data Tm (o ∷ [Nat] → *) (n ∷ Nat) where
Free ∷ Var → Tm0 o
Bound ∷ Int → Tm0 o
Abs ∷ Tm o n → Tm o (S n)
App ∷ o ns → Rec (Tm o) ns → Tm0 o
type Tm0 o = Tm o Z
instance HEq1 o ⇒ HEq1 (Tm o) where
heq1 (Free v1) (Free v2) | v1 == v2 = Just Refl
heq1 (Bound m) (Bound n) | m == n = Just Refl
heq1 (Abs e1) (Abs e2) = cong <$> heq1 e1 e2
heq1 (App o1 es1) (App o2 es2)
| Just Refl ← heq1 o1 o2
, Just Refl ← heq1 es1 es2 = Just Refl
heq1 _ _ = Nothing
shiftVar
∷ Var
→ Int
→ Tm o n
→ Tm o n
shiftVar v n = \case
Free v' → if v == v' then Bound n else Free v'
Bound m → Bound m
Abs e → Abs $ shiftVar v (n + 1) e
App p es → App p $ shiftVar v n <<$>> es
addVar
∷ Var
→ Int
→ Tm o n
→ Tm o n
addVar v n = \case
Free v' → Free v'
Bound m → if m == n then Free v else Bound m
Abs e → Abs $ addVar v (n + 1) e
App p es → App p $ addVar v n <<$>> es
instance Show1 o ⇒ Abt Var o (Tm o) where
into = \case
V v → Free v
v :\ e → Abs $ shiftVar v 0 e
v :$ es → App v es
out = \case
Free v → return $ V v
Bound _ → fail "bound variable occured in out"
Abs e → do
v ← fresh
return $ v :\ addVar v 0 e
App p es → return $ p :$ es
_TmOp
∷ ( Choice p
, Applicative f
, HEq1 o
)
⇒ o ns
→ p (Rec (Tm o) ns) (f (Rec (Tm o) ns))
→ p (Tm0 o) (f (Tm0 o))
_TmOp o = dimap fro (either pure (fmap (App o))) . right'
where
fro = \case
App o' es | Just Refl ← heq1 o o' → Right es
e → Left e