module Abt.Class.Abt
( Abt(..)
) where
import Abt.Types.Nat
import Abt.Types.HList
import Abt.Types.View
import Abt.Class.Monad
import Abt.Class.Show1
import Control.Applicative
import qualified Data.List as L
class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o, o → t 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
→ HList 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'' → do
e''' ← subst e v e''
return $ v' \\ e'''
o :$ es → do
es' ← htraverse (subst e v) es
return $ o $$ 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' → do
L.delete v <$>
freeVars e'
o :$ es → do
concat <$>
homogenizeA 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
e' ← toString e
return $ show v ++ "." ++ e'
o :$ es → do
es' ← homogenizeA toString es
return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"