{-# LANGUAGE OverloadedStrings #-}
module Disco.Subst
(
Substitution(..), dom
, idS, (|->), fromList, toList
, (@@), compose, applySubst, lookup
)
where
import Prelude hiding (lookup)
import Unbound.Generics.LocallyNameless (Name, Subst, substs)
import Data.Coerce
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import Disco.Effects.LFresh
import Disco.Pretty
import Polysemy
import Polysemy.Reader
newtype Substitution a = Substitution { Substitution a -> Map (Name a) a
getSubst :: Map (Name a) a }
deriving (Substitution a -> Substitution a -> Bool
(Substitution a -> Substitution a -> Bool)
-> (Substitution a -> Substitution a -> Bool)
-> Eq (Substitution a)
forall a. Eq a => Substitution a -> Substitution a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Substitution a -> Substitution a -> Bool
$c/= :: forall a. Eq a => Substitution a -> Substitution a -> Bool
== :: Substitution a -> Substitution a -> Bool
$c== :: forall a. Eq a => Substitution a -> Substitution a -> Bool
Eq, Eq (Substitution a)
Eq (Substitution a)
-> (Substitution a -> Substitution a -> Ordering)
-> (Substitution a -> Substitution a -> Bool)
-> (Substitution a -> Substitution a -> Bool)
-> (Substitution a -> Substitution a -> Bool)
-> (Substitution a -> Substitution a -> Bool)
-> (Substitution a -> Substitution a -> Substitution a)
-> (Substitution a -> Substitution a -> Substitution a)
-> Ord (Substitution a)
Substitution a -> Substitution a -> Bool
Substitution a -> Substitution a -> Ordering
Substitution a -> Substitution a -> Substitution a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Substitution a)
forall a. Ord a => Substitution a -> Substitution a -> Bool
forall a. Ord a => Substitution a -> Substitution a -> Ordering
forall a.
Ord a =>
Substitution a -> Substitution a -> Substitution a
min :: Substitution a -> Substitution a -> Substitution a
$cmin :: forall a.
Ord a =>
Substitution a -> Substitution a -> Substitution a
max :: Substitution a -> Substitution a -> Substitution a
$cmax :: forall a.
Ord a =>
Substitution a -> Substitution a -> Substitution a
>= :: Substitution a -> Substitution a -> Bool
$c>= :: forall a. Ord a => Substitution a -> Substitution a -> Bool
> :: Substitution a -> Substitution a -> Bool
$c> :: forall a. Ord a => Substitution a -> Substitution a -> Bool
<= :: Substitution a -> Substitution a -> Bool
$c<= :: forall a. Ord a => Substitution a -> Substitution a -> Bool
< :: Substitution a -> Substitution a -> Bool
$c< :: forall a. Ord a => Substitution a -> Substitution a -> Bool
compare :: Substitution a -> Substitution a -> Ordering
$ccompare :: forall a. Ord a => Substitution a -> Substitution a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Substitution a)
Ord, Int -> Substitution a -> ShowS
[Substitution a] -> ShowS
Substitution a -> String
(Int -> Substitution a -> ShowS)
-> (Substitution a -> String)
-> ([Substitution a] -> ShowS)
-> Show (Substitution a)
forall a. Show a => Int -> Substitution a -> ShowS
forall a. Show a => [Substitution a] -> ShowS
forall a. Show a => Substitution a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Substitution a] -> ShowS
$cshowList :: forall a. Show a => [Substitution a] -> ShowS
show :: Substitution a -> String
$cshow :: forall a. Show a => Substitution a -> String
showsPrec :: Int -> Substitution a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Substitution a -> ShowS
Show)
instance Functor Substitution where
fmap :: (a -> b) -> Substitution a -> Substitution b
fmap a -> b
f (Substitution Map (Name a) a
m) = Map (Name b) b -> Substitution b
forall a. Map (Name a) a -> Substitution a
Substitution ((Name a -> Name b) -> Map (Name a) b -> Map (Name b) b
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys Name a -> Name b
coerce (Map (Name a) b -> Map (Name b) b)
-> (Map (Name a) a -> Map (Name a) b)
-> Map (Name a) a
-> Map (Name b) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Map (Name a) a -> Map (Name a) b
forall a b k. (a -> b) -> Map k a -> Map k b
M.map a -> b
f (Map (Name a) a -> Map (Name b) b)
-> Map (Name a) a -> Map (Name b) b
forall a b. (a -> b) -> a -> b
$ Map (Name a) a
m)
instance Pretty a => Pretty (Substitution a) where
pretty :: Substitution a -> Sem r Doc
pretty (Substitution Map (Name a) a
s) = do
let es :: [Sem r Doc]
es = ((Name a, a) -> Sem r Doc) -> [(Name a, a)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Name a -> a -> Sem r Doc) -> (Name a, a) -> Sem r Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name a -> a -> Sem r Doc
forall a (r :: EffectRow).
(Pretty a, Members '[Reader PA, LFresh] r) =>
Name a -> a -> Sem r Doc
prettyMapping) (Map (Name a) a -> [(Name a, a)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (Name a) a
s)
[Sem r Doc]
ds <- Sem r Doc -> [Sem r Doc] -> Sem r [Sem r Doc]
forall (f :: * -> *).
Applicative f =>
f Doc -> [f Doc] -> f [f Doc]
punctuate Sem r Doc
"," [Sem r Doc]
es
Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
braces ([Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Sem r Doc]
ds)
prettyMapping :: (Pretty a, Members '[Reader PA, LFresh] r) => Name a -> a -> Sem r Doc
prettyMapping :: Name a -> a -> Sem r Doc
prettyMapping Name a
x a
a = Name a -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name a
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"->" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> a -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty a
a
dom :: Substitution a -> Set (Name a)
dom :: Substitution a -> Set (Name a)
dom = Map (Name a) a -> Set (Name a)
forall k a. Map k a -> Set k
M.keysSet (Map (Name a) a -> Set (Name a))
-> (Substitution a -> Map (Name a) a)
-> Substitution a
-> Set (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution a -> Map (Name a) a
forall a. Substitution a -> Map (Name a) a
getSubst
idS :: Substitution a
idS :: Substitution a
idS = Map (Name a) a -> Substitution a
forall a. Map (Name a) a -> Substitution a
Substitution Map (Name a) a
forall k a. Map k a
M.empty
(|->) :: Name a -> a -> Substitution a
Name a
x |-> :: Name a -> a -> Substitution a
|-> a
t = Map (Name a) a -> Substitution a
forall a. Map (Name a) a -> Substitution a
Substitution (Name a -> a -> Map (Name a) a
forall k a. k -> a -> Map k a
M.singleton Name a
x a
t)
(@@) :: Subst a a => Substitution a -> Substitution a -> Substitution a
(Substitution Map (Name a) a
s1) @@ :: Substitution a -> Substitution a -> Substitution a
@@ (Substitution Map (Name a) a
s2) = Map (Name a) a -> Substitution a
forall a. Map (Name a) a -> Substitution a
Substitution (((a -> a) -> Map (Name a) a -> Map (Name a) a
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Substitution a -> a -> a
forall b a. Subst b a => Substitution b -> a -> a
applySubst (Map (Name a) a -> Substitution a
forall a. Map (Name a) a -> Substitution a
Substitution Map (Name a) a
s1))) Map (Name a) a
s2 Map (Name a) a -> Map (Name a) a -> Map (Name a) a
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map (Name a) a
s1)
compose :: (Subst a a, Foldable t) => t (Substitution a) -> Substitution a
compose :: t (Substitution a) -> Substitution a
compose = (Substitution a -> Substitution a -> Substitution a)
-> Substitution a -> t (Substitution a) -> Substitution a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Substitution a -> Substitution a -> Substitution a
forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
(@@) Substitution a
forall a. Substitution a
idS
applySubst :: Subst b a => Substitution b -> a -> a
applySubst :: Substitution b -> a -> a
applySubst (Substitution Map (Name b) b
s) = [(Name b, b)] -> a -> a
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs (Map (Name b) b -> [(Name b, b)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (Name b) b
s)
fromList :: [(Name a, a)] -> Substitution a
fromList :: [(Name a, a)] -> Substitution a
fromList = Map (Name a) a -> Substitution a
forall a. Map (Name a) a -> Substitution a
Substitution (Map (Name a) a -> Substitution a)
-> ([(Name a, a)] -> Map (Name a) a)
-> [(Name a, a)]
-> Substitution a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name a, a)] -> Map (Name a) a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
toList :: Substitution a -> [(Name a, a)]
toList :: Substitution a -> [(Name a, a)]
toList (Substitution Map (Name a) a
m) = Map (Name a) a -> [(Name a, a)]
forall k a. Map k a -> [(k, a)]
M.assocs Map (Name a) a
m
lookup :: Name a -> Substitution a -> Maybe a
lookup :: Name a -> Substitution a -> Maybe a
lookup Name a
x (Substitution Map (Name a) a
m) = Name a -> Map (Name a) a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name a
x Map (Name a) a
m