{-# 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 {forall a. Substitution a -> Map (Name a) a
getSubst :: Map (Name a) a}
deriving (Substitution a -> Substitution a -> Bool
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, 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
Ord, Int -> Substitution a -> ShowS
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 :: forall a b. (a -> b) -> Substitution a -> Substitution b
fmap a -> b
f (Substitution Map (Name a) a
m) = forall a. Map (Name a) a -> Substitution a
Substitution (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
M.map a -> b
f forall a b. (a -> b) -> a -> b
$ Map (Name a) a
m)
instance Pretty a => Pretty (Substitution a) where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Substitution a -> Sem r (Doc ann)
pretty (Substitution Map (Name a) a
s) = do
let es :: [Sem r (Doc ann)]
es = forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a (r :: EffectRow) ann.
(Pretty a, Members '[Reader PA, LFresh] r) =>
Name a -> a -> Sem r (Doc ann)
prettyMapping) (forall k a. Map k a -> [(k, a)]
M.assocs Map (Name a) a
s)
[Sem r (Doc ann)]
ds <- forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f [f (Doc ann)]
punctuate Sem r (Doc ann)
"," [Sem r (Doc ann)]
es
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
braces (forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Sem r (Doc ann)]
ds)
prettyMapping :: (Pretty a, Members '[Reader PA, LFresh] r) => Name a -> a -> Sem r (Doc ann)
prettyMapping :: forall a (r :: EffectRow) ann.
(Pretty a, Members '[Reader PA, LFresh] r) =>
Name a -> a -> Sem r (Doc ann)
prettyMapping Name a
x a
a = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name a
x forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"->" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty a
a
dom :: Substitution a -> Set (Name a)
dom :: forall a. Substitution a -> Set (Name a)
dom = forall k a. Map k a -> Set k
M.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitution a -> Map (Name a) a
getSubst
idS :: Substitution a
idS :: forall a. Substitution a
idS = forall a. Map (Name a) a -> Substitution a
Substitution forall k a. Map k a
M.empty
(|->) :: Name a -> a -> Substitution a
Name a
x |-> :: forall a. Name a -> a -> Substitution a
|-> a
t = forall a. Map (Name a) a -> Substitution a
Substitution (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) @@ :: forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
@@ (Substitution Map (Name a) a
s2) = forall a. Map (Name a) a -> Substitution a
Substitution ((forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall b a. Subst b a => Substitution b -> a -> a
applySubst (forall a. Map (Name a) a -> Substitution a
Substitution Map (Name a) a
s1))) Map (Name a) a
s2 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 :: forall a (t :: * -> *).
(Subst a a, Foldable t) =>
t (Substitution a) -> Substitution a
compose = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a.
Subst a a =>
Substitution a -> Substitution a -> Substitution a
(@@) forall a. Substitution a
idS
applySubst :: Subst b a => Substitution b -> a -> a
applySubst :: forall b a. Subst b a => Substitution b -> a -> a
applySubst (Substitution Map (Name b) b
s) = forall b a. Subst b a => [(Name b, b)] -> a -> a
substs (forall k a. Map k a -> [(k, a)]
M.assocs Map (Name b) b
s)
fromList :: [(Name a, a)] -> Substitution a
fromList :: forall a. [(Name a, a)] -> Substitution a
fromList = forall a. Map (Name a) a -> Substitution a
Substitution forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
toList :: Substitution a -> [(Name a, a)]
toList :: forall a. Substitution a -> [(Name a, a)]
toList (Substitution Map (Name a) a
m) = forall k a. Map k a -> [(k, a)]
M.assocs Map (Name a) a
m
lookup :: Name a -> Substitution a -> Maybe a
lookup :: forall a. Name a -> Substitution a -> Maybe a
lookup Name a
x (Substitution Map (Name a) a
m) = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name a
x Map (Name a) a
m