{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Multi.Variables
(
HasVars(..),
GSubst,
CxtSubst,
Subst,
varsToHoles,
containsVar,
variables,
variableList,
variables',
appSubst,
compSubst,
getBoundVars,
(&),
(|->),
empty
) where
import Data.Comp.Multi.Algebra
import Data.Comp.Multi.Derive
import Data.Comp.Multi.HFoldable
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Mapping
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
type GSubst v a = Map v (A a)
type CxtSubst h a f v = GSubst v (Cxt h f a)
type Subst f v = CxtSubst NoHole (K ()) f v
type SubstFun v a = NatM Maybe (K v) a
substFun :: Ord v => GSubst v a -> SubstFun v a
substFun :: GSubst v a -> SubstFun v a
substFun GSubst v a
s (K v
v) = (A a -> a i) -> Maybe (A a) -> Maybe (a i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap A a -> a i
forall (f :: * -> *). A f -> forall i. f i
unA (Maybe (A a) -> Maybe (a i)) -> Maybe (A a) -> Maybe (a i)
forall a b. (a -> b) -> a -> b
$ v -> GSubst v a -> Maybe (A a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v GSubst v a
s
class HasVars (f :: (* -> *) -> * -> *) v where
isVar :: f a :=> Maybe v
isVar f a i
_ = Maybe v
forall a. Maybe a
Nothing
bindsVars :: Mapping m a => f a :=> m (Set v)
bindsVars f a i
_ = m (Set v)
forall (m :: * -> *) (k :: * -> *) v. Mapping m k => m v
empty
$(derive [liftSum] [''HasVars])
isVar' :: (HasVars f v, Ord v) => Set v -> f a :=> Maybe v
isVar' :: Set v -> f a :=> Maybe v
isVar' Set v
b f a i
t = do v
v <- f a i -> Maybe v
forall (f :: (* -> *) -> * -> *) v (a :: * -> *).
HasVars f v =>
f a :=> Maybe v
isVar f a i
t
if v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
b
then Maybe v
forall a. Maybe a
Nothing
else v -> Maybe v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
getBoundVars :: forall f a v i . (HasVars f v, HTraversable f) => f a i -> f (a :*: K (Set v)) i
getBoundVars :: f a i -> f (a :*: K (Set v)) i
getBoundVars f a i
t = let n :: f (Numbered a) i
n :: f (Numbered a) i
n = f a i -> f (Numbered a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HTraversable f =>
f a :-> f (Numbered a)
number f a i
t
m :: NumMap a (Set v)
m = f (Numbered a) i -> NumMap a (Set v)
forall (f :: (* -> *) -> * -> *) v (m :: * -> *) (a :: * -> *).
(HasVars f v, Mapping m a) =>
f a :=> m (Set v)
bindsVars f (Numbered a) i
n
trans :: Numbered a :-> (a :*: K (Set v))
trans :: Numbered a i -> (:*:) a (K (Set v)) i
trans (Numbered Int
i a i
x) = a i
x a i -> K (Set v) i -> (:*:) a (K (Set v)) i
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: Set v -> K (Set v) i
forall a i. a -> K a i
K (Set v -> Int -> NumMap a (Set v) -> Set v
forall a (t :: * -> *). a -> Int -> NumMap t a -> a
lookupNumMap Set v
forall a. Set a
Set.empty Int
i NumMap a (Set v)
m)
in (Numbered a :-> (a :*: K (Set v)))
-> f (Numbered a) i -> f (a :*: K (Set v)) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Numbered a :-> (a :*: K (Set v))
trans f (Numbered a) i
n
hfmapBoundVars :: forall f a b v i . (HasVars f v, HTraversable f)
=> (Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars :: (Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars Set v -> a :-> b
f f a i
t = let n :: f (Numbered a) i
n :: f (Numbered a) i
n = f a i -> f (Numbered a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HTraversable f =>
f a :-> f (Numbered a)
number f a i
t
m :: NumMap a (Set v)
m = f (Numbered a) i -> NumMap a (Set v)
forall (f :: (* -> *) -> * -> *) v (m :: * -> *) (a :: * -> *).
(HasVars f v, Mapping m a) =>
f a :=> m (Set v)
bindsVars f (Numbered a) i
n
trans :: Numbered a :-> b
trans :: Numbered a i -> b i
trans (Numbered Int
i a i
x) = Set v -> a i -> b i
Set v -> a :-> b
f (Set v -> Int -> NumMap a (Set v) -> Set v
forall a (t :: * -> *). a -> Int -> NumMap t a -> a
lookupNumMap Set v
forall a. Set a
Set.empty Int
i NumMap a (Set v)
m) a i
x
in (Numbered a :-> b) -> f (Numbered a) i -> f b i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Numbered a :-> b
trans f (Numbered a) i
n
hfoldlBoundVars :: forall f a b v i . (HasVars f v, HTraversable f)
=> (b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars :: (b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars b -> Set v -> a :=> b
f b
e f a i
t = let n :: f (Numbered a) i
n :: f (Numbered a) i
n = f a i -> f (Numbered a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HTraversable f =>
f a :-> f (Numbered a)
number f a i
t
m :: NumMap a (Set v)
m = f (Numbered a) i -> NumMap a (Set v)
forall (f :: (* -> *) -> * -> *) v (m :: * -> *) (a :: * -> *).
(HasVars f v, Mapping m a) =>
f a :=> m (Set v)
bindsVars f (Numbered a) i
n
trans :: b -> Numbered a :=> b
trans :: b -> Numbered a :=> b
trans b
x (Numbered Int
i a i
y) = b -> Set v -> a i -> b
b -> Set v -> a :=> b
f b
x (Set v -> Int -> NumMap a (Set v) -> Set v
forall a (t :: * -> *). a -> Int -> NumMap t a -> a
lookupNumMap Set v
forall a. Set a
Set.empty Int
i NumMap a (Set v)
m) a i
y
in (b -> Numbered a :=> b) -> b -> f (Numbered a) i -> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> Numbered a :=> b
trans b
e f (Numbered a) i
n
newtype C a b i = C{ C a b i -> a -> b i
unC :: a -> b i }
varsToHoles :: forall f v. (HTraversable f, HasVars f v, Ord v) =>
Term f :-> Context f (K v)
varsToHoles :: Term f :-> Context f (K v)
varsToHoles Term f i
t = C (Set v) (Context f (K v)) i -> Set v -> Cxt Hole f (K v) i
forall a (b :: * -> *) i. C a b i -> a -> b i
unC (Alg f (C (Set v) (Context f (K v)))
-> Term f i -> C (Set v) (Context f (K v)) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
Alg f a -> Term f :-> a
cata (HTraversable f, HasVars f v, Ord v) =>
Alg f (C (Set v) (Context f (K v)))
Alg f (C (Set v) (Context f (K v)))
alg Term f i
t) Set v
forall a. Set a
Set.empty
where alg :: (HTraversable f, HasVars f v, Ord v) => Alg f (C (Set v) (Context f (K v)))
alg :: Alg f (C (Set v) (Context f (K v)))
alg f (C (Set v) (Context f (K v))) i
t = (Set v -> Cxt Hole f (K v) i) -> C (Set v) (Context f (K v)) i
forall a (b :: * -> *) i. (a -> b i) -> C a b i
C ((Set v -> Cxt Hole f (K v) i) -> C (Set v) (Context f (K v)) i)
-> (Set v -> Cxt Hole f (K v) i) -> C (Set v) (Context f (K v)) i
forall a b. (a -> b) -> a -> b
$ \Set v
vars -> case f (C (Set v) (Context f (K v))) i -> Maybe v
forall (f :: (* -> *) -> * -> *) v (a :: * -> *).
HasVars f v =>
f a :=> Maybe v
isVar f (C (Set v) (Context f (K v))) i
t of
Just v
v | Bool -> Bool
not (v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vars) -> K v i -> Cxt Hole f (K v) i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole (K v i -> Cxt Hole f (K v) i) -> K v i -> Cxt Hole f (K v) i
forall a b. (a -> b) -> a -> b
$ v -> K v i
forall a i. a -> K a i
K v
v
Maybe v
_ -> f (Context f (K v)) i -> Cxt Hole f (K v) i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (Context f (K v)) i -> Cxt Hole f (K v) i)
-> f (Context f (K v)) i -> Cxt Hole f (K v) i
forall a b. (a -> b) -> a -> b
$ (Set v -> C (Set v) (Context f (K v)) :-> Context f (K v))
-> f (C (Set v) (Context f (K v))) i -> f (Context f (K v)) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) (b :: * -> *) v i.
(HasVars f v, HTraversable f) =>
(Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars Set v -> C (Set v) (Context f (K v)) :-> Context f (K v)
run f (C (Set v) (Context f (K v))) i
t
where
run :: Set v -> C (Set v) (Context f (K v)) :-> Context f (K v)
run :: Set v -> C (Set v) (Context f (K v)) :-> Context f (K v)
run Set v
newVars C (Set v) (Context f (K v)) i
f = C (Set v) (Context f (K v)) i
f C (Set v) (Context f (K v)) i -> Set v -> Context f (K v) i
forall a (b :: * -> *) i. C a b i -> a -> b i
`unC` (Set v
newVars Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
vars)
containsVarAlg :: forall v f . (Ord v, HasVars f v, HTraversable f) => v -> Alg f (K Bool)
containsVarAlg :: v -> Alg f (K Bool)
containsVarAlg v
v f (K Bool) i
t = Bool -> K Bool i
forall a i. a -> K a i
K (Bool -> K Bool i) -> Bool -> K Bool i
forall a b. (a -> b) -> a -> b
$ (Bool -> Set v -> K Bool :=> Bool) -> Bool -> f (K Bool) i -> Bool
forall (f :: (* -> *) -> * -> *) (a :: * -> *) b v i.
(HasVars f v, HTraversable f) =>
(b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars Bool -> Set v -> K Bool :=> Bool
forall i. Bool -> Set v -> K Bool i -> Bool
run Bool
local f (K Bool) i
t
where local :: Bool
local = case f (K Bool) i -> Maybe v
forall (f :: (* -> *) -> * -> *) v (a :: * -> *).
HasVars f v =>
f a :=> Maybe v
isVar f (K Bool) i
t of
Just v
v' -> v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v'
Maybe v
Nothing -> Bool
False
run :: Bool -> Set v -> K Bool i -> Bool
run :: Bool -> Set v -> K Bool i -> Bool
run Bool
acc Set v
vars (K Bool
b) = Bool
acc Bool -> Bool -> Bool
|| (Bool -> Bool
not (v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vars) Bool -> Bool -> Bool
&& Bool
b)
containsVar :: (Ord v, HasVars f v, HTraversable f, HFunctor f)
=> v -> Cxt h f a :=> Bool
containsVar :: v -> Cxt h f a :=> Bool
containsVar v
v = K Bool i -> Bool
forall a i. K a i -> a
unK (K Bool i -> Bool)
-> (Cxt h f a i -> K Bool i) -> Cxt h f a i -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (K Bool) -> (a :-> K Bool) -> Cxt h f a :-> K Bool
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) (b :: * -> *).
HFunctor f =>
Alg f b -> (a :-> b) -> Cxt h f a :-> b
free (v -> Alg f (K Bool)
forall v (f :: (* -> *) -> * -> *).
(Ord v, HasVars f v, HTraversable f) =>
v -> Alg f (K Bool)
containsVarAlg v
v) (K Bool i -> a i -> K Bool i
forall a b. a -> b -> a
const (K Bool i -> a i -> K Bool i) -> K Bool i -> a i -> K Bool i
forall a b. (a -> b) -> a -> b
$ Bool -> K Bool i
forall a i. a -> K a i
K Bool
False)
variableList :: (HasVars f v, HTraversable f, HFunctor f, Ord v)
=> Cxt h f a :=> [v]
variableList :: Cxt h f a :=> [v]
variableList = Set v -> [v]
forall a. Set a -> [a]
Set.toList (Set v -> [v]) -> (Cxt h f a i -> Set v) -> Cxt h f a i -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a i -> Set v
forall v (f :: (* -> *) -> * -> *) h (a :: * -> *).
(Ord v, HasVars f v, HTraversable f, HFunctor f) =>
Cxt h f a :=> Set v
variables
variablesAlg :: (Ord v, HasVars f v, HTraversable f) => Alg f (K (Set v))
variablesAlg :: Alg f (K (Set v))
variablesAlg f (K (Set v)) i
t = Set v -> K (Set v) i
forall a i. a -> K a i
K (Set v -> K (Set v) i) -> Set v -> K (Set v) i
forall a b. (a -> b) -> a -> b
$ (Set v -> Set v -> K (Set v) :=> Set v)
-> Set v -> f (K (Set v)) i -> Set v
forall (f :: (* -> *) -> * -> *) (a :: * -> *) b v i.
(HasVars f v, HTraversable f) =>
(b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars Set v -> Set v -> K (Set v) :=> Set v
forall a i. Ord a => Set a -> Set a -> K (Set a) i -> Set a
run Set v
local f (K (Set v)) i
t
where local :: Set v
local = case f (K (Set v)) i -> Maybe v
forall (f :: (* -> *) -> * -> *) v (a :: * -> *).
HasVars f v =>
f a :=> Maybe v
isVar f (K (Set v)) i
t of
Just v
v -> v -> Set v
forall a. a -> Set a
Set.singleton v
v
Maybe v
Nothing -> Set v
forall a. Set a
Set.empty
run :: Set a -> Set a -> K (Set a) i -> Set a
run Set a
acc Set a
bvars (K Set a
vars) = Set a
acc Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Set a
vars Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
bvars)
variables :: (Ord v, HasVars f v, HTraversable f, HFunctor f)
=> Cxt h f a :=> Set v
variables :: Cxt h f a :=> Set v
variables = K (Set v) i -> Set v
forall a i. K a i -> a
unK (K (Set v) i -> Set v)
-> (Cxt h f a i -> K (Set v) i) -> Cxt h f a i -> Set v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (K (Set v)) -> (a :-> K (Set v)) -> Cxt h f a :-> K (Set v)
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) (b :: * -> *).
HFunctor f =>
Alg f b -> (a :-> b) -> Cxt h f a :-> b
free Alg f (K (Set v))
forall v (f :: (* -> *) -> * -> *).
(Ord v, HasVars f v, HTraversable f) =>
Alg f (K (Set v))
variablesAlg (K (Set v) i -> a i -> K (Set v) i
forall a b. a -> b -> a
const (K (Set v) i -> a i -> K (Set v) i)
-> K (Set v) i -> a i -> K (Set v) i
forall a b. (a -> b) -> a -> b
$ Set v -> K (Set v) i
forall a i. a -> K a i
K Set v
forall a. Set a
Set.empty)
variables' :: (Ord v, HasVars f v, HFoldable f, HFunctor f)
=> Const f :=> Set v
variables' :: Const f :=> Set v
variables' Const f i
c = case Const f i -> Maybe v
forall (f :: (* -> *) -> * -> *) v (a :: * -> *).
HasVars f v =>
f a :=> Maybe v
isVar Const f i
c of
Maybe v
Nothing -> Set v
forall a. Set a
Set.empty
Just v
v -> v -> Set v
forall a. a -> Set a
Set.singleton v
v
class SubstVars v t a where
substVars :: SubstFun v t -> a :-> a
appSubst :: (Ord v, SubstVars v t a) => GSubst v t -> a :-> a
appSubst :: GSubst v t -> a :-> a
appSubst GSubst v t
subst = SubstFun v t -> a :-> a
forall v (t :: * -> *) (a :: * -> *).
SubstVars v t a =>
SubstFun v t -> a :-> a
substVars (GSubst v t -> SubstFun v t
forall v (a :: * -> *). Ord v => GSubst v a -> SubstFun v a
substFun GSubst v t
subst)
instance {-# OVERLAPPABLE #-} (Ord v, HasVars f v, HTraversable f)
=> SubstVars v (Cxt h f a) (Cxt h f a) where
substVars :: SubstFun v (Cxt h f a) -> Cxt h f a :-> Cxt h f a
substVars SubstFun v (Cxt h f a)
subst = Set v -> Cxt h f a :-> Cxt h f a
doSubst Set v
forall a. Set a
Set.empty
where doSubst :: Set v -> Cxt h f a :-> Cxt h f a
doSubst :: Set v -> Cxt h f a :-> Cxt h f a
doSubst Set v
_ (Hole a i
a) = a i -> Cxt Hole f a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
a
doSubst Set v
b (Term f (Cxt h f a) i
t) = case Set v -> f (Cxt h f a) i -> Maybe v
forall (f :: (* -> *) -> * -> *) v (a :: * -> *).
(HasVars f v, Ord v) =>
Set v -> f a :=> Maybe v
isVar' Set v
b f (Cxt h f a) i
t Maybe v -> (v -> Maybe (Cxt h f a i)) -> Maybe (Cxt h f a i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= K v i -> Maybe (Cxt h f a i)
SubstFun v (Cxt h f a)
subst (K v i -> Maybe (Cxt h f a i))
-> (v -> K v i) -> v -> Maybe (Cxt h f a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> K v i
forall a i. a -> K a i
K of
Just Cxt h f a i
new -> Cxt h f a i
new
Maybe (Cxt h f a i)
Nothing -> f (Cxt h f a) i -> Cxt h f a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (Cxt h f a) i -> Cxt h f a i) -> f (Cxt h f a) i -> Cxt h f a i
forall a b. (a -> b) -> a -> b
$ (Set v -> Cxt h f a :-> Cxt h f a)
-> f (Cxt h f a) i -> f (Cxt h f a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) (b :: * -> *) v i.
(HasVars f v, HTraversable f) =>
(Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars Set v -> Cxt h f a :-> Cxt h f a
run f (Cxt h f a) i
t
where run :: Set v -> Cxt h f a :-> Cxt h f a
run :: Set v -> Cxt h f a :-> Cxt h f a
run Set v
vars = Set v -> Cxt h f a :-> Cxt h f a
doSubst (Set v
b Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
vars)
instance {-# OVERLAPPABLE #-} (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where
substVars :: SubstFun v t -> f a :-> f a
substVars SubstFun v t
subst = (a :-> a) -> f a :-> f a
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (SubstFun v t -> a :-> a
forall v (t :: * -> *) (a :: * -> *).
SubstVars v t a =>
SubstFun v t -> a :-> a
substVars SubstFun v t
subst)
compSubst :: (Ord v, HasVars f v, HTraversable f)
=> CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst :: CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst CxtSubst h a f v
s1 = (A (Cxt h f a) -> A (Cxt h f a))
-> CxtSubst h a f v -> CxtSubst h a f v
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (A forall i. Cxt h f a i
t) -> (forall i. Cxt h f a i) -> A (Cxt h f a)
forall (f :: * -> *). (forall i. f i) -> A f
A (CxtSubst h a f v -> Cxt h f a i -> Cxt h f a i
forall v (t :: * -> *) (a :: * -> *).
(Ord v, SubstVars v t a) =>
GSubst v t -> a :-> a
appSubst CxtSubst h a f v
s1 Cxt h f a i
forall i. Cxt h f a i
t))