module Abt.Class.Abt
( Abt(..)
) where
import Abt.Types.Nat
import Abt.Types.View
import Abt.Class.Monad
import Abt.Class.Show1
import Control.Applicative hiding (Const)
import Data.Vinyl
import Data.Vinyl.Functor
import qualified Data.List as L
class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o where
into
∷ View v o n t
→ t n
out
∷ MonadVar v m
⇒ t n
→ m (View v o n t)
var
∷ v
→ t Z
var = into . V
(\\)
∷ v
→ t n
→ t (S n)
v \\ e = into $ v :\ e
($$)
∷ o ns
→ Rec t ns
→ t Z
o $$ es = into $ o :$ es
infixl 1 $$
subst
∷ MonadVar v m
⇒ t Z
→ v
→ t n
→ m (t n)
subst e v e' = do
oe' ← out e'
case oe' of
V v' → return $ if v == v' then e else e'
v' :\ e'' → (v' \\) <$> subst e v e''
o :$ es → (o $$) <$> subst e v `rtraverse` es
(//)
∷ MonadVar v m
⇒ t (S n)
→ t Z
→ m (t n)
xe // e' = do
v :\ e ← out xe
subst e' v e
freeVars
∷ MonadVar v m
⇒ t n
→ m [v]
freeVars e = do
oe ← out e
case oe of
V v → return [v]
v :\ e' →
L.delete v <$>
freeVars e'
_ :$ es →
fmap concat . sequence . recordToList $
Const . freeVars <<$>> es
toString
∷ MonadVar v m
⇒ t n
→ m String
toString e = do
vu ← out e
case vu of
V v → return $ show v
v :\ e' → do
estr ← toString e'
return $ show v ++ "." ++ estr
o :$ RNil → return $ show1 o
o :$ es → do
es' ← sequence . recordToList $ Const . toString <<$>> es
return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"