{-# LANGUAGE CPP
, RankNTypes
, FlexibleContexts
, GADTs
, TypeFamilies
#-}
module Unbound.LocallyNameless.Alpha where
import Generics.RepLib hiding (GT)
import Unbound.PermM
import Unbound.LocallyNameless.Types
import Unbound.LocallyNameless.Fresh
import Unbound.Util
import Data.List (intersect)
import Data.Maybe (isJust)
import Data.Semigroup (Semigroup)
import qualified Data.Semigroup as Semigroup
import Data.Monoid
class (Rep1 AlphaD a) => Alpha a where
swaps' :: AlphaCtx -> Perm AnyName -> a -> a
swaps' = swapsR1 rep1
fv' :: Collection f => AlphaCtx -> a -> f AnyName
fv' = fvR1 rep1
lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
lfreshen' = lfreshenR1 rep1
freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
freshen' = freshenR1 rep1
aeq' :: AlphaCtx -> a -> a -> Bool
aeq' = aeqR1 rep1
acompare' :: AlphaCtx -> a -> a -> Ordering
acompare' = acompareR1 rep1
close :: Alpha b => AlphaCtx -> b -> a -> a
close = closeR1 rep1
open :: Alpha b => AlphaCtx -> b -> a -> a
open = openR1 rep1
isPat :: a -> Maybe [AnyName]
isPat = isPatR1 rep1
isTerm :: a -> Bool
isTerm = isTermR1 rep1
isEmbed :: a -> Bool
isEmbed _ = False
nthpatrec :: a -> NthCont
nthpatrec = nthpatR1 rep1
findpatrec :: a -> AnyName -> FindResult
findpatrec = findpatR1 rep1
class IsEmbed e where
type Embedded e :: *
embed :: Embedded e -> e
unembed :: e -> Embedded e
data FindResult = Index Integer
| NamesSeen Integer
deriving (Eq, Ord)
instance Semigroup FindResult where
NamesSeen i <> NamesSeen j = NamesSeen (i + j)
NamesSeen i <> Index j = Index (i + j)
Index j <> _ = Index j
instance Monoid FindResult where
mempty = NamesSeen 0
#if !MIN_VERSION_base(4,11,0)
mappend = (Semigroup.<>)
#endif
findpat :: Alpha a => a -> AnyName -> Maybe Integer
findpat x n = case findpatrec x n of
Index i -> Just i
NamesSeen _ -> Nothing
data NthResult = Found AnyName
| CurIndex Integer
newtype NthCont = NthCont { runNthCont :: Integer -> NthResult }
instance Semigroup NthCont where
(NthCont f) <> (NthCont g)
= NthCont $ \i -> case f i of
Found n -> Found n
CurIndex i' -> g i'
instance Monoid NthCont where
mempty = NthCont $ \i -> CurIndex i
#if !MIN_VERSION_base(4,11,0)
mappend = (Semigroup.<>)
#endif
nthName :: AnyName -> NthCont
nthName nm = NthCont $ \i -> if i == 0
then Found nm
else CurIndex (i-1)
nthpat :: Alpha a => a -> Integer -> AnyName
nthpat x i = case runNthCont (nthpatrec x) i of
CurIndex j -> error
("BUG: pattern index " ++ show i ++
" out of bounds by " ++ show j ++ "in")
Found nm -> nm
data AlphaCtx = AC { mode :: Mode , level :: Integer }
initial :: AlphaCtx
initial = AC Term 0
incr :: AlphaCtx -> AlphaCtx
incr c = c { level = level c + 1 }
decr :: AlphaCtx -> AlphaCtx
decr c =
c { level = level c - 1 }
pat :: AlphaCtx -> AlphaCtx
pat c = c { mode = Pat }
term :: AlphaCtx -> AlphaCtx
term c = c { mode = Term }
data Mode = Term | Pat deriving (Show, Eq, Read)
openT :: (Alpha p, Alpha t) => p -> t -> t
openT = open initial
openP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2
openP = open (pat initial)
closeT :: (Alpha p, Alpha t) => p -> t -> t
closeT = close initial
closeP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2
closeP = close (pat initial)
data AlphaD a = AlphaD {
isPatD :: a -> Maybe [AnyName],
isTermD :: a -> Bool,
isEmbedD :: a -> Bool,
swapsD :: AlphaCtx -> Perm AnyName -> a -> a,
fvD :: forall f. Collection f => AlphaCtx -> a -> f AnyName,
freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName),
lfreshenD :: forall m b. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b,
aeqD :: AlphaCtx -> a -> a -> Bool,
acompareD :: AlphaCtx -> a -> a -> Ordering,
closeD :: forall b. Alpha b => AlphaCtx -> b -> a -> a,
openD :: forall b. Alpha b => AlphaCtx -> b -> a -> a,
findpatD :: a -> AnyName -> FindResult,
nthpatD :: a -> NthCont
}
instance Alpha a => Sat (AlphaD a) where
dict = AlphaD isPat isTerm isEmbed swaps' fv' freshen' lfreshen' aeq'
acompare' close open findpatrec nthpatrec
closeR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
closeR1 (Data1 _ cons) = \i a d ->
case (findCon cons d) of
Val c rec kids ->
to c (map_l (\z -> closeD z i a) rec kids)
closeR1 _ = \_ _ d -> d
openR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a
openR1 (Data1 _ cons) = \i a d ->
case (findCon cons d) of
Val c rec kids ->
to c (map_l (\z -> openD z i a) rec kids)
openR1 _ = \_ _ d -> d
swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a
swapsR1 (Data1 _ cons) = \ p x d ->
case (findCon cons d) of
Val c rec kids -> to c (map_l (\z -> swapsD z p x) rec kids)
swapsR1 _ = \ _ _ d -> d
fvR1 :: Collection f => R1 (AlphaD) a -> AlphaCtx -> a -> f AnyName
fvR1 (Data1 _ cons) = \ p d ->
case (findCon cons d) of
Val _ rec kids -> fv1 rec p kids where
fv1 :: Collection f => MTup (AlphaD) l -> AlphaCtx -> l -> f AnyName
fv1 MNil _ Nil = emptyC
fv1 (r :+: rs) p (p1 :*: t1) =
fvD r p p1 `union` fv1 rs p t1
fvR1 _ = \ _ _ -> emptyC
aeqR1 :: R1 (AlphaD) a -> AlphaCtx -> a -> a -> Bool
aeqR1 (Data1 _ cons) = loop cons where
loop (Con emb reps : rest) p x y =
case (from emb x, from emb y) of
(Just p1, Just p2) -> aeq1 reps p p1 p2
(Nothing, Nothing) -> loop rest p x y
(_,_) -> False
loop [] _ _ _ = error "Impossible"
aeqR1 Int1 = \ _ x y -> x == y
aeqR1 Integer1 = \ _ x y -> x == y
aeqR1 Char1 = \ _ x y -> x == y
aeqR1 (Abstract1 _) = \ _ x y -> error "Must override aeq' for abstract types"
aeqR1 _ = \ _ _ _ -> False
aeq1 :: MTup (AlphaD) l -> AlphaCtx -> l -> l -> Bool
aeq1 MNil _ Nil Nil = True
aeq1 (r :+: rs) c (p1 :*: t1) (p2 :*: t2) = do
aeqD r c p1 p2 && aeq1 rs c t1 t2
freshenR1 :: Fresh m => R1 (AlphaD) a -> AlphaCtx -> a -> m (a,Perm AnyName)
freshenR1 (Data1 _ cons) = \ p d ->
case findCon cons d of
Val c rec kids -> do
(l, p') <- freshenL rec p kids
return (to c l, p')
freshenR1 _ = \ _ n -> return (n, empty)
freshenL :: Fresh m => MTup (AlphaD) l -> AlphaCtx -> l -> m (l, Perm AnyName)
freshenL MNil _ Nil = return (Nil, empty)
freshenL (r :+: rs) p (t :*: ts) = do
(xs, p2) <- freshenL rs p ts
(x, p1) <- freshenD r p (swapsD r p p2 t)
return ( x :*: xs, p1 <> p2)
lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a ->
(a -> Perm AnyName -> m b) -> m b
lfreshenR1 (Data1 _ cons) = \p d f ->
case findCon cons d of
Val c rec kids -> lfreshenL rec p kids (\ l p' -> f (to c l) p')
lfreshenR1 _ = \ _ n f -> f n empty
lfreshenL :: LFresh m => MTup (AlphaD) l -> AlphaCtx -> l ->
(l -> Perm AnyName -> m b) -> m b
lfreshenL MNil _ Nil f = f Nil empty
lfreshenL (r :+: rs) p (t :*: ts) f =
lfreshenL rs p ts ( \ y p2 ->
lfreshenD r p (swapsD r p p2 t) ( \ x p1 ->
f (x :*: y) (p1 <> p2)))
findpatR1 :: R1 AlphaD b -> b -> AnyName -> FindResult
findpatR1 (Data1 _dt cons) = \ d n ->
case findCon cons d of
Val _c rec kids -> findpatL rec kids n
findpatR1 _ = \ _ _ -> mempty
findpatL :: MTup AlphaD l -> l -> AnyName -> FindResult
findpatL MNil Nil _ = mempty
findpatL (r :+: rs) (t :*: ts) n = findpatD r t n <> findpatL rs ts n
nthpatR1 :: R1 AlphaD b -> b -> NthCont
nthpatR1 (Data1 _dt cons) = \ d ->
case findCon cons d of
Val _c rec kids -> nthpatL rec kids
nthpatR1 _ = \ _ -> mempty
nthpatL :: MTup AlphaD l -> l -> NthCont
nthpatL MNil Nil = mempty
nthpatL (r :+: rs) (t :*: ts) = nthpatD r t <> nthpatL rs ts
combine :: Maybe [AnyName] -> Maybe [AnyName] -> Maybe [AnyName]
combine (Just ns1) (Just ns2) | ns1 `intersect` ns2 == [] =
Just (ns1 ++ ns2)
combine _ _ = Nothing
isPatR1 :: R1 AlphaD b -> b -> Maybe [AnyName]
isPatR1 (Data1 _dt cons) = \ d ->
case findCon cons d of
Val _c rec kids ->
foldl_l (\ c b a -> combine (isPatD c a) b) (Just []) rec kids
isPatR1 _ = \ _ -> Just []
isTermR1 :: R1 AlphaD b -> b -> Bool
isTermR1 (Data1 _dt cons) = \ d ->
case findCon cons d of
Val _c rec kids -> foldl_l (\ c b a -> isTermD c a && b) True rec kids
isTermR1 _ = \ _ -> True
acompareR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Ordering
acompareR1 Int1 _ = \x y -> compare x y
acompareR1 Char1 _ = \x y -> compare x y
acompareR1 (Data1 _ cons) c = \x y ->
let loop (Con emb rec : rest) =
case (from emb x, from emb y) of
(Just t1, Just t2) -> compareTupM rec c t1 t2
(Just _ , Nothing) -> LT
(Nothing, Just _ ) -> GT
(Nothing, Nothing) -> loop rest
loop [] = error "acompareR1 found no constructors! Please report this as a bug."
in loop cons
acompareR1 r1 _ = error ("acompare' not supported for " ++ show r1)
compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering
compareTupM MNil _ Nil Nil = EQ
compareTupM (x :+: xs) c (y :*: ys) (z :*: zs) =
mappend (acompareD x c y z) (compareTupM xs c ys zs)
instance Rep a => Alpha (Name a) where
isTerm _ = True
isPat n@(Nm _ _) = Just [AnyName n]
isPat _ = Nothing
fv' c n@(Nm _ _) | mode c == Term = singleton (AnyName n)
fv' _ _ = emptyC
swaps' c p x | mode c == Term =
case apply p (AnyName x) of
AnyName y ->
case gcastR (getR y) (getR x) y of
Just y' -> y'
Nothing -> error "Internal error in swaps': sort mismatch"
swaps' _ _ x = x
aeq' c x y | mode c == Term = x == y
aeq' _ _ _ = True
freshen' c nm | mode c == Pat = do x <- fresh nm
return (x, single (AnyName nm) (AnyName x))
freshen' _ _ = error "freshen' on Name in Term mode"
lfreshen' c nm f = case mode c of
Pat -> do x <- lfresh nm
avoid [AnyName x] $ f x (single (AnyName nm) (AnyName x))
Term -> error "lfreshen' on Name in Term mode"
open c a (Bn r j x) | mode c == Term && level c == j =
case nthpat a x of
AnyName nm -> case gcastR (getR nm) r nm of
Just nm' -> nm'
Nothing -> error "Internal error in open: sort mismatch"
open _ _ n = n
close c a nm@(Nm r _) | mode c == Term && level c >= 0 =
case findpat a (AnyName nm) of
Just x -> Bn r (level c) x
Nothing -> nm
close _ _ n = n
findpatrec nm1 (AnyName nm2) =
case gcastR (getR nm1) (getR nm2) nm1 of
Just nm1' -> if nm1' == nm2 then Index 0 else NamesSeen 1
Nothing -> NamesSeen 1
nthpatrec = nthName . AnyName
acompare' c (Nm r1 n1) (Nm r2 n2)
| mode c == Term = mconcat [compare r1 r2, compare n1 n2]
acompare' c (Bn r1 m1 n1) (Bn r2 m2 n2)
| mode c == Term = mconcat [compare r1 r2, compare m1 m2, compare n1 n2]
acompare' c (Nm _ _) (Bn _ _ _) | mode c == Term = LT
acompare' c (Bn _ _ _) (Nm _ _) | mode c == Term = GT
acompare' _ _ _ = EQ
instance Alpha AnyName where
isTerm _ = True
isPat n@(AnyName (Nm _ _)) = Just [n]
isPat _ = Nothing
fv' c n@(AnyName (Nm _ _)) | mode c == Term = singleton n
fv' _ _ = emptyC
swaps' c p x = case mode c of
Term -> apply p x
Pat -> x
aeq' _ x y | x == y = True
aeq' c _ _ | mode c == Term = False
aeq' _ _ _ = True
acompare' _ x y | x == y = EQ
acompare' c (AnyName n1) (AnyName n2)
| mode c == Term =
case compareR (getR n1) (getR n2) of
EQ -> case gcastR (getR n1) (getR n2) n1 of
Just n1' -> acompare' c n1' n2
Nothing -> error "impossible"
neq -> neq
acompare' _ _ _ = EQ
freshen' c (AnyName nm) = case mode c of
Pat -> do x <- fresh nm
return (AnyName x, single (AnyName nm) (AnyName x))
Term -> error "freshen' on AnyName in Term mode"
lfreshen' c (AnyName nm) f = case mode c of
Pat -> do x <- lfresh nm
avoid [AnyName x] $ f (AnyName x) (single (AnyName nm) (AnyName x))
Term -> error "lfreshen' on AnyName in Term mode"
open c a (AnyName (Bn _ j x)) | level c == j = nthpat a x
open _ _ n = n
close c a nm@(AnyName (Nm r _)) =
case findpat a nm of
Just x -> AnyName (Bn r (level c) x)
Nothing -> nm
close _ _ n = n
findpatrec nm1 nm2 | nm1 == nm2 = Index 0
findpatrec _ _ = NamesSeen 1
nthpatrec = nthName
instance (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) where
isPat _ = Nothing
isTerm (B p t) = isJust (isPat p) && isTerm t
swaps' c pm (B p t) =
(B (swaps' (pat c) pm p)
(swaps' (incr c) pm t))
fv' c (B p t) = fv' (pat c) p `union` fv' (incr c) t
freshen' c (B p t) = do
(p', pm1) <- freshen' (pat c) p
(t', pm2) <- freshen' (incr c) (swaps' (incr c) pm1 t)
return (B p' t', pm1 <> pm2)
lfreshen' c (B p t) f =
lfreshen' (pat c) p (\ p' pm1 ->
lfreshen' (incr c) (swaps' (incr c) pm1 t) (\ t' pm2 ->
f (B p' t') (pm1 <> pm2)))
aeq' c (B p1 t1) (B p2 t2) = do
aeq' (pat c) p1 p2 && aeq' (incr c) t1 t2
open c a (B p t) = B (open (pat c) a p) (open (incr c) a t)
close c a (B p t) = B (close (pat c) a p) (close (incr c) a t)
acompare' c (B p1 t1) (B p2 t2) =
mappend (acompare' (pat c) p1 p2) (acompare' (incr c) t1 t2)
findpatrec _ b = error $ "Binding used as a pattern"
nthpatrec b = error $ "Binding used as a pattern"
instance (Alpha p, Alpha q) => Alpha (Rebind p q) where
isTerm _ = False
isPat (R p q) = combine (isPat p) (isPat q)
swaps' c pm (R p q) = R (swaps' c pm p) (swaps' (incr c) pm q)
fv' c (R p q) = fv' c p `union` fv' (incr c) q
lfreshen' c (R p q) g
| mode c == Term = error "lfreshen' on Rebind in Term mode"
| otherwise =
lfreshen' c p $ \ p' pm1 ->
lfreshen' (incr c) (swaps' (incr c) pm1 q) $ \ q' pm2 ->
g (R p' q') (pm1 <> pm2)
freshen' c (R p q)
| mode c == Term = error "freshen' on Rebind in Term mode"
| otherwise = do
(p', pm1) <- freshen' c p
(q', pm2) <- freshen' (incr c) (swaps' (incr c) pm1 q)
return (R p' q', pm1 <> pm2)
aeq' c (R p1 q1) (R p2 q2 ) = do
aeq' c p1 p2 && aeq' c q1 q2
acompare' c (R a1 a2) (R b1 b2) =
mappend (acompare' c a1 b1) (acompare' (incr c) a2 b2)
open c a (R p q) = R (open c a p) (open (incr c) a q)
close c a (R p q) = R (close c a p) (close (incr c) a q)
findpatrec (R p q) nm = findpatrec p nm <> findpatrec q nm
nthpatrec (R p q) = nthpatrec p <> nthpatrec q
instance Alpha p => Alpha (Rec p) where
isPat (Rec p) = isPat p
isTerm _ = False
open c a (Rec p) = Rec (open (incr c) a p)
close c a (Rec p) = Rec (close (incr c) a p)
instance Alpha t => Alpha (Embed t) where
isPat (Embed t) = if (isTerm t) then Just [] else Nothing
isTerm _ = False
isEmbed (Embed t) = isTerm t
swaps' c pm (Embed t) =
case mode c of
Pat -> Embed (swaps' (term c) pm t)
Term -> Embed t
fv' c (Embed t) =
case mode c of
Pat -> fv' (term c) t
Term -> emptyC
freshen' c p | mode c == Term = error "freshen' called on a term"
| otherwise = return (p, empty)
lfreshen' c p f | mode c == Term = error "lfreshen' called on a term"
| otherwise = f p empty
aeq' c (Embed x) (Embed y) = aeq' (term c) x y
acompare' c (Embed x) (Embed y) = acompare' (term c) x y
close c b (Embed x) = case mode c of
Pat -> Embed (close (term c) b x)
Term -> error "close on Embed"
open c b (Embed x) = case mode c of
Pat -> Embed (open (term c) b x)
Term -> error "open on Embed"
findpatrec _ _ = mempty
nthpatrec _ = mempty
instance IsEmbed (Embed t) where
type Embedded (Embed t) = t
embed = Embed
unembed (Embed t) = t
instance Alpha a => Alpha (Shift a) where
isPat (Shift a) = if (isEmbed a) then Just [] else Nothing
isTerm _ = False
isEmbed (Shift a) = isEmbed a
close c b (Shift x) = Shift (close (decr c) b x)
open c b (Shift x) = Shift (open (decr c) b x)
instance IsEmbed e => IsEmbed (Shift e) where
type Embedded (Shift e) = Embedded e
embed = Shift . embed
unembed (Shift e) = unembed e
instance Alpha Bool
instance Alpha Float
instance Alpha ()
instance Alpha a => Alpha [a]
instance Alpha Int
instance Alpha Integer
instance Alpha Double
instance Alpha Char
instance Alpha a => Alpha (Maybe a)
instance (Alpha a,Alpha b) => Alpha (Either a b)
instance (Alpha a,Alpha b) => Alpha (a,b)
instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)
instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
Alpha (a,b,c,d,e)
instance (Rep a) => Alpha (R a)