{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Variables
(
HasVars(..),
Subst,
CxtSubst,
varsToHoles,
containsVar,
variables,
variableList,
variables',
substVars,
appSubst,
compSubst,
getBoundVars,
(&),
(|->),
empty
) where
import Data.Comp.Algebra
import Data.Comp.Derive
import Data.Comp.Mapping
import Data.Comp.Term
import Data.Comp.Ops
import Data.Foldable hiding (elem, notElem)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding (foldl, or)
type CxtSubst h a f v = Map v (Cxt h f a)
type Subst f v = CxtSubst NoHole () f v
class HasVars f v where
isVar :: f a -> Maybe v
isVar f a
_ = forall a. Maybe a
Nothing
bindsVars :: Mapping m a => f a -> m (Set v)
bindsVars f a
_ = forall (m :: * -> *) k v. Mapping m k => m v
empty
$(derive [liftSum] [''HasVars])
instance HasVars f v => HasVars (f :&: a) v where
isVar :: forall a. (:&:) f a a -> Maybe v
isVar (f a
f :&: a
_) = forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar f a
f
bindsVars :: forall (m :: * -> *) a. Mapping m a => (:&:) f a a -> m (Set v)
bindsVars (f a
f :&: a
_) = forall (f :: * -> *) v (m :: * -> *) a.
(HasVars f v, Mapping m a) =>
f a -> m (Set v)
bindsVars f a
f
isVar' :: (HasVars f v, Ord v) => Set v -> f a -> Maybe v
isVar' :: forall (f :: * -> *) v a.
(HasVars f v, Ord v) =>
Set v -> f a -> Maybe v
isVar' Set v
b f a
t = do v
v <- forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar f a
t
if v
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
b
then forall a. Maybe a
Nothing
else forall (m :: * -> *) a. Monad m => a -> m a
return v
v
getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a)
getBoundVars :: forall (f :: * -> *) v a.
(HasVars f v, Traversable f) =>
f a -> f (Set v, a)
getBoundVars f a
t = let n :: f (Numbered a)
n = forall (f :: * -> *) a. Traversable f => f a -> f (Numbered a)
number f a
t
m :: NumMap a (Set v)
m = forall (f :: * -> *) v (m :: * -> *) a.
(HasVars f v, Mapping m a) =>
f a -> m (Set v)
bindsVars f (Numbered a)
n
trans :: Numbered a -> (Set v, a)
trans (Numbered Int
i a
x) = (forall a t. a -> Int -> NumMap t a -> a
lookupNumMap forall a. Set a
Set.empty Int
i NumMap a (Set v)
m, a
x)
in forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Numbered a -> (Set v, a)
trans f (Numbered a)
n
fmapBoundVars :: (HasVars f v, Traversable f) => (Set v -> a -> b) -> f a -> f b
fmapBoundVars :: forall (f :: * -> *) v a b.
(HasVars f v, Traversable f) =>
(Set v -> a -> b) -> f a -> f b
fmapBoundVars Set v -> a -> b
f f a
t = let n :: f (Numbered a)
n = forall (f :: * -> *) a. Traversable f => f a -> f (Numbered a)
number f a
t
m :: NumMap a (Set v)
m = forall (f :: * -> *) v (m :: * -> *) a.
(HasVars f v, Mapping m a) =>
f a -> m (Set v)
bindsVars f (Numbered a)
n
trans :: Numbered a -> b
trans (Numbered Int
i a
x) = Set v -> a -> b
f (forall a t. a -> Int -> NumMap t a -> a
lookupNumMap forall a. Set a
Set.empty Int
i NumMap a (Set v)
m) a
x
in forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Numbered a -> b
trans f (Numbered a)
n
foldlBoundVars :: (HasVars f v, Traversable f) => (b -> Set v -> a -> b) -> b -> f a -> b
foldlBoundVars :: forall (f :: * -> *) v b a.
(HasVars f v, Traversable f) =>
(b -> Set v -> a -> b) -> b -> f a -> b
foldlBoundVars b -> Set v -> a -> b
f b
e f a
t = let n :: f (Numbered a)
n = forall (f :: * -> *) a. Traversable f => f a -> f (Numbered a)
number f a
t
m :: NumMap a (Set v)
m = forall (f :: * -> *) v (m :: * -> *) a.
(HasVars f v, Mapping m a) =>
f a -> m (Set v)
bindsVars f (Numbered a)
n
trans :: b -> Numbered a -> b
trans b
x (Numbered Int
i a
y) = b -> Set v -> a -> b
f b
x (forall a t. a -> Int -> NumMap t a -> a
lookupNumMap forall a. Set a
Set.empty Int
i NumMap a (Set v)
m) a
y
in forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> Numbered a -> b
trans b
e f (Numbered a)
n
varsToHoles :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v
varsToHoles :: forall (f :: * -> *) v.
(Traversable f, HasVars f v, Ord v) =>
Term f -> Context f v
varsToHoles Term f
t = forall (f :: * -> *) a. Functor f => Alg f a -> Term f -> a
cata forall (f :: * -> *) v.
(Traversable f, HasVars f v, Ord v) =>
Alg f (Set v -> Context f v)
alg Term f
t forall a. Set a
Set.empty
where alg :: (Traversable f, HasVars f v, Ord v) => Alg f (Set v -> Context f v)
alg :: forall (f :: * -> *) v.
(Traversable f, HasVars f v, Ord v) =>
Alg f (Set v -> Context f v)
alg f (Set v -> Context f v)
t Set v
vars = case forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar f (Set v -> Context f v)
t of
Just v
v | Bool -> Bool
not (v
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vars) -> forall c (b :: * -> *). c -> Cxt Hole b c
Hole v
v
Maybe v
_ -> forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) v a b.
(HasVars f v, Traversable f) =>
(Set v -> a -> b) -> f a -> f b
fmapBoundVars Set v -> (Set v -> Context f v) -> Context f v
run f (Set v -> Context f v)
t
where
run :: Set v -> (Set v -> Context f v) -> Context f v
run Set v
newVars Set v -> Context f v
f = Set v -> Context f v
f forall a b. (a -> b) -> a -> b
$ Set v
newVars forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
vars
containsVarAlg :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Alg f Bool
containsVarAlg :: forall v (f :: * -> *).
(Eq v, HasVars f v, Traversable f, Ord v) =>
v -> Alg f Bool
containsVarAlg v
v f Bool
t = forall (f :: * -> *) v b a.
(HasVars f v, Traversable f) =>
(b -> Set v -> a -> b) -> b -> f a -> b
foldlBoundVars Bool -> Set v -> Bool -> Bool
run Bool
local f Bool
t
where local :: Bool
local = case forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar f Bool
t of
Just v
v' -> v
v forall a. Eq a => a -> a -> Bool
== v
v'
Maybe v
Nothing -> Bool
False
run :: Bool -> Set v -> Bool -> Bool
run Bool
acc Set v
vars Bool
b = Bool
acc Bool -> Bool -> Bool
|| (Bool -> Bool
not (v
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vars) Bool -> Bool -> Bool
&& Bool
b)
containsVar :: (Eq v, HasVars f v, Traversable f, Ord v)
=> v -> Cxt h f a -> Bool
containsVar :: forall v (f :: * -> *) h a.
(Eq v, HasVars f v, Traversable f, Ord v) =>
v -> Cxt h f a -> Bool
containsVar v
v = forall (f :: * -> *) h a b.
Functor f =>
Alg f b -> (a -> b) -> Cxt h f a -> b
free (forall v (f :: * -> *).
(Eq v, HasVars f v, Traversable f, Ord v) =>
v -> Alg f Bool
containsVarAlg v
v) (forall a b. a -> b -> a
const Bool
False)
variablesAlg :: (Ord v, HasVars f v, Traversable f) => Alg f (Set v)
variablesAlg :: forall v (f :: * -> *).
(Ord v, HasVars f v, Traversable f) =>
Alg f (Set v)
variablesAlg f (Set v)
t = forall (f :: * -> *) v b a.
(HasVars f v, Traversable f) =>
(b -> Set v -> a -> b) -> b -> f a -> b
foldlBoundVars forall {a}. Ord a => Set a -> Set a -> Set a -> Set a
run Set v
local f (Set v)
t
where local :: Set v
local = case forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar f (Set v)
t of
Just v
v -> forall a. a -> Set a
Set.singleton v
v
Maybe v
Nothing -> forall a. Set a
Set.empty
run :: Set a -> Set a -> Set a -> Set a
run Set a
acc Set a
bvars Set a
vars = Set a
acc forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Set a
vars forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
bvars)
variableList :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> [v]
variableList :: forall v (f :: * -> *) h a.
(Ord v, HasVars f v, Traversable f) =>
Cxt h f a -> [v]
variableList = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v (f :: * -> *) h a.
(Ord v, HasVars f v, Traversable f) =>
Cxt h f a -> Set v
variables
variables :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> Set v
variables :: forall v (f :: * -> *) h a.
(Ord v, HasVars f v, Traversable f) =>
Cxt h f a -> Set v
variables = forall (f :: * -> *) h a b.
Functor f =>
Alg f b -> (a -> b) -> Cxt h f a -> b
free forall v (f :: * -> *).
(Ord v, HasVars f v, Traversable f) =>
Alg f (Set v)
variablesAlg (forall a b. a -> b -> a
const forall a. Set a
Set.empty)
variables' :: (Ord v, HasVars f v, Foldable f, Functor f) => Const f -> Set v
variables' :: forall v (f :: * -> *).
(Ord v, HasVars f v, Foldable f, Functor f) =>
Const f -> Set v
variables' Const f
c = case forall (f :: * -> *) v a. HasVars f v => f a -> Maybe v
isVar Const f
c of
Maybe v
Nothing -> forall a. Set a
Set.empty
Just v
v -> forall a. a -> Set a
Set.singleton v
v
class SubstVars v t a where
substVars :: (v -> Maybe t) -> a -> a
appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a
appSubst :: forall v t a. (Ord v, SubstVars v t a) => Map v t -> a -> a
appSubst Map v t
subst = forall v t a. SubstVars v t a => (v -> Maybe t) -> a -> a
substVars v -> Maybe t
f
where f :: v -> Maybe t
f v
v = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v t
subst
instance {-# OVERLAPPABLE #-} (Ord v, HasVars f v, Traversable f)
=> SubstVars v (Cxt h f a) (Cxt h f a) where
substVars :: (v -> Maybe (Cxt h f a)) -> Cxt h f a -> Cxt h f a
substVars v -> Maybe (Cxt h f a)
subst = Set v -> Cxt h f a -> Cxt h f a
doSubst forall a. Set a
Set.empty
where doSubst :: Set v -> Cxt h f a -> Cxt h f a
doSubst Set v
_ (Hole a
a) = forall c (b :: * -> *). c -> Cxt Hole b c
Hole a
a
doSubst Set v
b (Term f (Cxt h f a)
t) = case forall (f :: * -> *) v a.
(HasVars f v, Ord v) =>
Set v -> f a -> Maybe v
isVar' Set v
b f (Cxt h f a)
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> Maybe (Cxt h f a)
subst of
Just Cxt h f a
new -> Cxt h f a
new
Maybe (Cxt h f a)
Nothing -> forall (b :: * -> *) a c. b (Cxt a b c) -> Cxt a b c
Term forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) v a b.
(HasVars f v, Traversable f) =>
(Set v -> a -> b) -> f a -> f b
fmapBoundVars Set v -> Cxt h f a -> Cxt h f a
run f (Cxt h f a)
t
where 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 forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
vars)
instance {-# OVERLAPPABLE #-} (SubstVars v t a, Functor f) => SubstVars v t (f a) where
substVars :: (v -> Maybe t) -> f a -> f a
substVars v -> Maybe t
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall v t a. SubstVars v t a => (v -> Maybe t) -> a -> a
substVars v -> Maybe t
f)
compSubst :: (Ord v, HasVars f v, Traversable f)
=> CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst :: forall v (f :: * -> *) h a.
(Ord v, HasVars f v, Traversable f) =>
CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst CxtSubst h a f v
s1 CxtSubst h a f v
s2 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall v t a. (Ord v, SubstVars v t a) => Map v t -> a -> a
appSubst CxtSubst h a f v
s1) CxtSubst h a f v
s2 forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` CxtSubst h a f v
s1