{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Generics.Simplistic.Unify
(
Subst , substEmpty , substInsert , substLkup , substApply
, UnifyErr(..) , unify , unify_ , unifyWith , minimize
) where
import Data.List (sort)
import qualified Data.Map as M
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Writer hiding (All)
import Control.Monad.Cont
import Unsafe.Coerce
import Generics.Simplistic.Deep
import Generics.Simplistic.Util
data UnifyErr kappa fam phi :: * where
OccursCheck :: [Exists phi]
-> UnifyErr kappa fam phi
SymbolClash :: Holes kappa fam phi at
-> Holes kappa fam phi at
-> UnifyErr kappa fam phi
type Subst kappa fam phi
= M.Map (Exists phi) (Exists (Holes kappa fam phi))
substEmpty :: Subst kappa fam phi
substEmpty :: Subst kappa fam phi
substEmpty = Subst kappa fam phi
forall k a. Map k a
M.empty
substLkup :: (Ord (Exists phi))
=> Subst kappa fam phi
-> phi at
-> Maybe (Holes kappa fam phi at)
substLkup :: Subst kappa fam phi -> phi at -> Maybe (Holes kappa fam phi at)
substLkup sigma :: Subst kappa fam phi
sigma var :: phi at
var =
case Exists phi
-> Subst kappa fam phi -> Maybe (Exists (Holes kappa fam phi))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (phi at -> Exists phi
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists phi at
var) Subst kappa fam phi
sigma of
Nothing -> Maybe (Holes kappa fam phi at)
forall a. Maybe a
Nothing
Just (Exists t :: Holes kappa fam phi x
t) -> Holes kappa fam phi at -> Maybe (Holes kappa fam phi at)
forall a. a -> Maybe a
Just (Holes kappa fam phi at -> Maybe (Holes kappa fam phi at))
-> Holes kappa fam phi at -> Maybe (Holes kappa fam phi at)
forall a b. (a -> b) -> a -> b
$ Holes kappa fam phi x -> Holes kappa fam phi at
forall a b. a -> b
unsafeCoerce Holes kappa fam phi x
t
substApply :: (Ord (Exists phi))
=> Subst kappa fam phi
-> Holes kappa fam phi at
-> Holes kappa fam phi at
substApply :: Subst kappa fam phi
-> Holes kappa fam phi at -> Holes kappa fam phi at
substApply sigma :: Subst kappa fam phi
sigma = HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) at
-> Holes kappa fam phi at
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin
(HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) at
-> Holes kappa fam phi at)
-> (Holes kappa fam phi at
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) at)
-> Holes kappa fam phi at
-> Holes kappa fam phi at
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. phi x -> HolesAnn kappa fam U1 phi x)
-> Holes kappa fam phi at
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) at
forall (f :: * -> *) (g :: * -> *) (kappa :: [*]) (fam :: [*])
(ann :: * -> *) a.
(forall x. f x -> g x)
-> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a
holesMap (\v :: phi x
v -> Holes kappa fam phi x
-> (Holes kappa fam phi x -> Holes kappa fam phi x)
-> Maybe (Holes kappa fam phi x)
-> Holes kappa fam phi x
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (phi x -> Holes kappa fam phi x
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole phi x
v) Holes kappa fam phi x -> Holes kappa fam phi x
forall a. a -> a
id (Maybe (Holes kappa fam phi x) -> Holes kappa fam phi x)
-> Maybe (Holes kappa fam phi x) -> Holes kappa fam phi x
forall a b. (a -> b) -> a -> b
$ Subst kappa fam phi -> phi x -> Maybe (Holes kappa fam phi x)
forall (phi :: * -> *) (kappa :: [*]) (fam :: [*]) at.
Ord (Exists phi) =>
Subst kappa fam phi -> phi at -> Maybe (Holes kappa fam phi at)
substLkup Subst kappa fam phi
sigma phi x
v)
substInsert :: (Ord (Exists phi))
=> Subst kappa fam phi
-> phi at
-> Holes kappa fam phi at
-> Subst kappa fam phi
substInsert :: Subst kappa fam phi
-> phi at -> Holes kappa fam phi at -> Subst kappa fam phi
substInsert sigma :: Subst kappa fam phi
sigma v :: phi at
v x :: Holes kappa fam phi at
x = Exists phi
-> Exists (HolesAnn kappa fam U1 phi)
-> Subst kappa fam phi
-> Subst kappa fam phi
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (phi at -> Exists phi
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists phi at
v) (Holes kappa fam phi at -> Exists (HolesAnn kappa fam U1 phi)
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists Holes kappa fam phi at
x) Subst kappa fam phi
sigma
type UnifyM kappa fam phi
= StateT (Subst kappa fam phi) (Except (UnifyErr kappa fam phi))
unify_ :: (All Eq kappa , Ord (Exists phi) , EqHO phi)
=> Holes kappa fam phi at
-> Holes kappa fam phi at
-> Maybe (Subst kappa fam phi)
unify_ :: Holes kappa fam phi at
-> Holes kappa fam phi at -> Maybe (Subst kappa fam phi)
unify_ a :: Holes kappa fam phi at
a = (UnifyErr kappa fam phi -> Maybe (Subst kappa fam phi))
-> (Subst kappa fam phi -> Maybe (Subst kappa fam phi))
-> Either (UnifyErr kappa fam phi) (Subst kappa fam phi)
-> Maybe (Subst kappa fam phi)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Subst kappa fam phi)
-> UnifyErr kappa fam phi -> Maybe (Subst kappa fam phi)
forall a b. a -> b -> a
const Maybe (Subst kappa fam phi)
forall a. Maybe a
Nothing) Subst kappa fam phi -> Maybe (Subst kappa fam phi)
forall a. a -> Maybe a
Just
(Either (UnifyErr kappa fam phi) (Subst kappa fam phi)
-> Maybe (Subst kappa fam phi))
-> (Holes kappa fam phi at
-> Either (UnifyErr kappa fam phi) (Subst kappa fam phi))
-> Holes kappa fam phi at
-> Maybe (Subst kappa fam phi)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
-> Either (UnifyErr kappa fam phi) (Subst kappa fam phi)
forall e a. Except e a -> Either e a
runExcept (Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
-> Either (UnifyErr kappa fam phi) (Subst kappa fam phi))
-> (Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi))
-> Holes kappa fam phi at
-> Either (UnifyErr kappa fam phi) (Subst kappa fam phi)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
forall (kappa :: [*]) (phi :: * -> *) (fam :: [*]) at.
(All Eq kappa, Ord (Exists phi), EqHO phi) =>
Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
unify Holes kappa fam phi at
a
unify :: (All Eq kappa , Ord (Exists phi) , EqHO phi)
=> Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi)
(Subst kappa fam phi)
unify :: Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
unify = Subst kappa fam phi
-> Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
forall (kappa :: [*]) (phi :: * -> *) (fam :: [*]) at.
(All Eq kappa, Ord (Exists phi), EqHO phi) =>
Subst kappa fam phi
-> Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
unifyWith Subst kappa fam phi
forall (kappa :: [*]) (fam :: [*]) (phi :: * -> *).
Subst kappa fam phi
substEmpty
unifyWith :: (All Eq kappa , Ord (Exists phi) , EqHO phi)
=> Subst kappa fam phi
-> Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi)
(Subst kappa fam phi)
unifyWith :: Subst kappa fam phi
-> Holes kappa fam phi at
-> Holes kappa fam phi at
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
unifyWith sigma :: Subst kappa fam phi
sigma x :: Holes kappa fam phi at
x y :: Holes kappa fam phi at
y = StateT (Subst kappa fam phi) (Except (UnifyErr kappa fam phi)) ()
-> Subst kappa fam phi
-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Holes kappa fam phi at
-> Holes kappa fam phi at
-> StateT
(Subst kappa fam phi) (Except (UnifyErr kappa fam phi)) ()
forall (kappa :: [*]) (fam :: [*]) (phi :: * -> *) at.
(All Eq kappa, EqHO phi, Ord (Exists phi)) =>
Holes kappa fam phi at
-> Holes kappa fam phi at -> UnifyM kappa fam phi ()
unifyM Holes kappa fam phi at
x Holes kappa fam phi at
y) Subst kappa fam phi
sigma
unifyM :: forall kappa fam phi at
. (All Eq kappa , EqHO phi , Ord (Exists phi))
=> Holes kappa fam phi at
-> Holes kappa fam phi at
-> UnifyM kappa fam phi ()
unifyM :: Holes kappa fam phi at
-> Holes kappa fam phi at -> UnifyM kappa fam phi ()
unifyM x :: Holes kappa fam phi at
x y :: Holes kappa fam phi at
y = do
()
_ <- Holes kappa fam phi at
-> Holes kappa fam phi at -> UnifyM kappa fam phi ()
forall b.
Holes kappa fam phi b
-> Holes kappa fam phi b -> UnifyM kappa fam phi ()
getEquivs Holes kappa fam phi at
x Holes kappa fam phi at
y
Subst kappa fam phi
s <- StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(Subst kappa fam phi)
forall s (m :: * -> *). MonadState s m => m s
get
case Subst kappa fam phi -> Either [Exists phi] (Subst kappa fam phi)
forall (kappa :: [*]) (fam :: [*]) (phi :: * -> *).
Ord (Exists phi) =>
Subst kappa fam phi -> Either [Exists phi] (Subst kappa fam phi)
minimize Subst kappa fam phi
s of
Left vs :: [Exists phi]
vs -> UnifyErr kappa fam phi -> UnifyM kappa fam phi ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([Exists phi] -> UnifyErr kappa fam phi
forall (phi :: * -> *) (kappa :: [*]) (fam :: [*]).
[Exists phi] -> UnifyErr kappa fam phi
OccursCheck [Exists phi]
vs)
Right s' :: Subst kappa fam phi
s' -> Subst kappa fam phi -> UnifyM kappa fam phi ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Subst kappa fam phi
s'
where
getEquivs :: Holes kappa fam phi b
-> Holes kappa fam phi b
-> UnifyM kappa fam phi ()
getEquivs :: Holes kappa fam phi b
-> Holes kappa fam phi b -> UnifyM kappa fam phi ()
getEquivs p :: Holes kappa fam phi b
p q :: Holes kappa fam phi b
q = StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) b)
-> UnifyM kappa fam phi ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) b)
-> UnifyM kappa fam phi ())
-> StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) b)
-> UnifyM kappa fam phi ()
forall a b. (a -> b) -> a -> b
$ (forall x.
(:*:) (HolesAnn kappa fam U1 phi) (HolesAnn kappa fam U1 phi) x
-> StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(HolesAnn kappa fam U1 phi x))
-> HolesAnn
kappa
fam
U1
(HolesAnn kappa fam U1 phi :*: HolesAnn kappa fam U1 phi)
b
-> StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(HolesAnn kappa fam U1 (HolesAnn kappa fam U1 phi) b)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
(fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM ((Holes kappa fam phi x
-> Holes kappa fam phi x
-> UnifyM kappa fam phi (Holes kappa fam phi x))
-> (:*:) (HolesAnn kappa fam U1 phi) (HolesAnn kappa fam U1 phi) x
-> UnifyM kappa fam phi (Holes kappa fam phi x)
forall k (f :: k -> *) (x :: k) (g :: k -> *) a.
(f x -> g x -> a) -> (:*:) f g x -> a
uncurry' Holes kappa fam phi x
-> Holes kappa fam phi x
-> UnifyM kappa fam phi (Holes kappa fam phi x)
forall b.
Holes kappa fam phi b
-> Holes kappa fam phi b
-> UnifyM kappa fam phi (Holes kappa fam phi b)
getEq) (Holes kappa fam phi b
-> Holes kappa fam phi b
-> HolesAnn
kappa
fam
U1
(HolesAnn kappa fam U1 phi :*: HolesAnn kappa fam U1 phi)
b
forall (kappa :: [*]) (fam :: [*]) (h :: * -> *) (i :: * -> *) a.
All Eq kappa =>
Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg Holes kappa fam phi b
p Holes kappa fam phi b
q)
getEq :: Holes kappa fam phi b
-> Holes kappa fam phi b
-> UnifyM kappa fam phi (Holes kappa fam phi b)
getEq :: Holes kappa fam phi b
-> Holes kappa fam phi b
-> UnifyM kappa fam phi (Holes kappa fam phi b)
getEq p :: Holes kappa fam phi b
p (Hole var :: phi b
var) = phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()
forall b. phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()
record_eq phi b
var Holes kappa fam phi b
p UnifyM kappa fam phi ()
-> UnifyM kappa fam phi (Holes kappa fam phi b)
-> UnifyM kappa fam phi (Holes kappa fam phi b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Holes kappa fam phi b
-> UnifyM kappa fam phi (Holes kappa fam phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return Holes kappa fam phi b
p
getEq p :: Holes kappa fam phi b
p@(Hole var :: phi b
var) q :: Holes kappa fam phi b
q = phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()
forall b. phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()
record_eq phi b
var Holes kappa fam phi b
q UnifyM kappa fam phi ()
-> UnifyM kappa fam phi (Holes kappa fam phi b)
-> UnifyM kappa fam phi (Holes kappa fam phi b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Holes kappa fam phi b
-> UnifyM kappa fam phi (Holes kappa fam phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return Holes kappa fam phi b
p
getEq p :: Holes kappa fam phi b
p q :: Holes kappa fam phi b
q | Holes kappa fam phi b -> Holes kappa fam phi b -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO Holes kappa fam phi b
p Holes kappa fam phi b
q = Holes kappa fam phi b
-> UnifyM kappa fam phi (Holes kappa fam phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return Holes kappa fam phi b
p
| Bool
otherwise = UnifyErr kappa fam phi
-> UnifyM kappa fam phi (Holes kappa fam phi b)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Holes kappa fam phi b
-> Holes kappa fam phi b -> UnifyErr kappa fam phi
forall (kappa :: [*]) (fam :: [*]) (phi :: * -> *) at.
Holes kappa fam phi at
-> Holes kappa fam phi at -> UnifyErr kappa fam phi
SymbolClash Holes kappa fam phi b
p Holes kappa fam phi b
q)
record_eq :: phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()
record_eq :: phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()
record_eq var :: phi b
var q :: Holes kappa fam phi b
q = do
Subst kappa fam phi
sigma <- StateT
(Subst kappa fam phi)
(Except (UnifyErr kappa fam phi))
(Subst kappa fam phi)
forall s (m :: * -> *). MonadState s m => m s
get
case Subst kappa fam phi -> phi b -> Maybe (Holes kappa fam phi b)
forall (phi :: * -> *) (kappa :: [*]) (fam :: [*]) at.
Ord (Exists phi) =>
Subst kappa fam phi -> phi at -> Maybe (Holes kappa fam phi at)
substLkup Subst kappa fam phi
sigma phi b
var of
Nothing -> Bool -> UnifyM kappa fam phi () -> UnifyM kappa fam phi ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Holes kappa fam phi b -> Holes kappa fam phi b -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO Holes kappa fam phi b
q (phi b -> Holes kappa fam phi b
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole phi b
var))
(UnifyM kappa fam phi () -> UnifyM kappa fam phi ())
-> UnifyM kappa fam phi () -> UnifyM kappa fam phi ()
forall a b. (a -> b) -> a -> b
$ (Subst kappa fam phi -> Subst kappa fam phi)
-> UnifyM kappa fam phi ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: Subst kappa fam phi
s -> Subst kappa fam phi
-> phi b -> Holes kappa fam phi b -> Subst kappa fam phi
forall (phi :: * -> *) (kappa :: [*]) (fam :: [*]) at.
Ord (Exists phi) =>
Subst kappa fam phi
-> phi at -> Holes kappa fam phi at -> Subst kappa fam phi
substInsert Subst kappa fam phi
s phi b
var Holes kappa fam phi b
q)
Just q' :: Holes kappa fam phi b
q' -> Bool -> UnifyM kappa fam phi () -> UnifyM kappa fam phi ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Holes kappa fam phi b -> Holes kappa fam phi b -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO Holes kappa fam phi b
q' Holes kappa fam phi b
q)
(UnifyM kappa fam phi () -> UnifyM kappa fam phi ())
-> UnifyM kappa fam phi () -> UnifyM kappa fam phi ()
forall a b. (a -> b) -> a -> b
$ UnifyM kappa fam phi () -> UnifyM kappa fam phi ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (UnifyM kappa fam phi () -> UnifyM kappa fam phi ())
-> UnifyM kappa fam phi () -> UnifyM kappa fam phi ()
forall a b. (a -> b) -> a -> b
$ Holes kappa fam phi b
-> Holes kappa fam phi b -> UnifyM kappa fam phi ()
forall b.
Holes kappa fam phi b
-> Holes kappa fam phi b -> UnifyM kappa fam phi ()
getEquivs Holes kappa fam phi b
q Holes kappa fam phi b
q'
minimize :: forall kappa fam phi . (Ord (Exists phi))
=> Subst kappa fam phi
-> Either [Exists phi] (Subst kappa fam phi)
minimize :: Subst kappa fam phi -> Either [Exists phi] (Subst kappa fam phi)
minimize sigma :: Subst kappa fam phi
sigma =
let sigma' :: Subst kappa fam phi
sigma' = (Exists phi -> Exists (Holes kappa fam phi))
-> (Exists (Holes kappa fam phi) -> Maybe (Exists phi))
-> Subst kappa fam phi
-> Subst kappa fam phi
forall a b.
Ord a =>
(a -> b) -> (b -> Maybe a) -> Map a b -> Map a b
breakCycles Exists phi -> Exists (Holes kappa fam phi)
inj Exists (Holes kappa fam phi) -> Maybe (Exists phi)
proj (Subst kappa fam phi -> Subst kappa fam phi)
-> Subst kappa fam phi -> Subst kappa fam phi
forall a b. (a -> b) -> a -> b
$ (Exists (Holes kappa fam phi) -> Maybe (Exists phi))
-> Subst kappa fam phi -> Subst kappa fam phi
forall a b. Ord a => (b -> Maybe a) -> Map a b -> Map a b
removeIds Exists (Holes kappa fam phi) -> Maybe (Exists phi)
proj Subst kappa fam phi
sigma
in Subst kappa fam phi
-> [Exists phi]
-> (Subst kappa fam phi
-> [Exists phi] -> Writer [Exists phi] (Subst kappa fam phi))
-> Either [Exists phi] (Subst kappa fam phi)
forall a.
Ord (Exists phi) =>
a
-> [Exists phi]
-> (a -> [Exists phi] -> Writer [Exists phi] a)
-> Either [Exists phi] a
whileM Subst kappa fam phi
sigma' [] ((Subst kappa fam phi
-> [Exists phi] -> Writer [Exists phi] (Subst kappa fam phi))
-> Either [Exists phi] (Subst kappa fam phi))
-> (Subst kappa fam phi
-> [Exists phi] -> Writer [Exists phi] (Subst kappa fam phi))
-> Either [Exists phi] (Subst kappa fam phi)
forall a b. (a -> b) -> a -> b
$ \s :: Subst kappa fam phi
s _
-> [(Exists phi, Exists (Holes kappa fam phi))] -> Subst kappa fam phi
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Exists phi, Exists (Holes kappa fam phi))]
-> Subst kappa fam phi)
-> WriterT
[Exists phi] Identity [(Exists phi, Exists (Holes kappa fam phi))]
-> Writer [Exists phi] (Subst kappa fam phi)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Exists phi, Exists (Holes kappa fam phi))
-> WriterT
[Exists phi] Identity (Exists phi, Exists (Holes kappa fam phi)))
-> [(Exists phi, Exists (Holes kappa fam phi))]
-> WriterT
[Exists phi] Identity [(Exists phi, Exists (Holes kappa fam phi))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Exists (Holes kappa fam phi)
-> WriterT [Exists phi] Identity (Exists (Holes kappa fam phi)))
-> (Exists phi, Exists (Holes kappa fam phi))
-> WriterT
[Exists phi] Identity (Exists phi, Exists (Holes kappa fam phi))
forall (m :: * -> *) a b x.
Functor m =>
(a -> m b) -> (x, a) -> m (x, b)
secondF ((forall x.
Holes kappa fam phi x
-> WriterT [Exists phi] Identity (Holes kappa fam phi x))
-> Exists (Holes kappa fam phi)
-> WriterT [Exists phi] Identity (Exists (Holes kappa fam phi))
forall k (m :: * -> *) (f :: k -> *) (g :: k -> *).
Monad m =>
(forall (x :: k). f x -> m (g x)) -> Exists f -> m (Exists g)
exMapM (Subst kappa fam phi
-> Holes kappa fam phi x
-> Writer [Exists phi] (Holes kappa fam phi x)
forall at.
Subst kappa fam phi
-> Holes kappa fam phi at
-> Writer [Exists phi] (Holes kappa fam phi at)
go Subst kappa fam phi
sigma'))) (Subst kappa fam phi -> [(Exists phi, Exists (Holes kappa fam phi))]
forall k a. Map k a -> [(k, a)]
M.toList Subst kappa fam phi
s))
where
inj :: Exists phi -> Exists (Holes kappa fam phi)
inj :: Exists phi -> Exists (Holes kappa fam phi)
inj = (forall x. phi x -> Holes kappa fam phi x)
-> Exists phi -> Exists (Holes kappa fam phi)
forall k (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> Exists f -> Exists g
exMap forall x. phi x -> Holes kappa fam phi x
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole
proj :: Exists (Holes kappa fam phi) -> Maybe (Exists phi)
proj :: Exists (Holes kappa fam phi) -> Maybe (Exists phi)
proj (Exists (Hole phi :: phi x
phi)) = Exists phi -> Maybe (Exists phi)
forall a. a -> Maybe a
Just (Exists phi -> Maybe (Exists phi))
-> Exists phi -> Maybe (Exists phi)
forall a b. (a -> b) -> a -> b
$ phi x -> Exists phi
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists phi x
phi
proj _ = Maybe (Exists phi)
forall a. Maybe a
Nothing
secondF :: (Functor m) => (a -> m b) -> (x , a) -> m (x , b)
secondF :: (a -> m b) -> (x, a) -> m (x, b)
secondF f :: a -> m b
f (x :: x
x , a :: a
a) = (x
x,) (b -> (x, b)) -> m b -> m (x, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
go :: Subst kappa fam phi
-> Holes kappa fam phi at
-> Writer [Exists phi] (Holes kappa fam phi at)
go :: Subst kappa fam phi
-> Holes kappa fam phi at
-> Writer [Exists phi] (Holes kappa fam phi at)
go ss :: Subst kappa fam phi
ss = (forall b.
phi b -> WriterT [Exists phi] Identity (Holes kappa fam phi b))
-> Holes kappa fam phi at
-> Writer [Exists phi] (Holes kappa fam phi at)
forall (m :: * -> *) (f :: * -> *) (kappa :: [*]) (fam :: [*])
(g :: * -> *) a.
Monad m =>
(forall b. f b -> m (Holes kappa fam g b))
-> Holes kappa fam f a -> m (Holes kappa fam g a)
holesRefineHolesM ((forall b.
phi b -> WriterT [Exists phi] Identity (Holes kappa fam phi b))
-> Holes kappa fam phi at
-> Writer [Exists phi] (Holes kappa fam phi at))
-> (forall b.
phi b -> WriterT [Exists phi] Identity (Holes kappa fam phi b))
-> Holes kappa fam phi at
-> Writer [Exists phi] (Holes kappa fam phi at)
forall a b. (a -> b) -> a -> b
$ \var :: phi b
var -> do
case Subst kappa fam phi -> phi b -> Maybe (Holes kappa fam phi b)
forall (phi :: * -> *) (kappa :: [*]) (fam :: [*]) at.
Ord (Exists phi) =>
Subst kappa fam phi -> phi at -> Maybe (Holes kappa fam phi at)
substLkup Subst kappa fam phi
ss phi b
var of
Nothing -> Holes kappa fam phi b
-> WriterT [Exists phi] Identity (Holes kappa fam phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Holes kappa fam phi b
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole phi b
var)
Just r :: Holes kappa fam phi b
r -> [Exists phi] -> WriterT [Exists phi] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [phi b -> Exists phi
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists phi b
var]
WriterT [Exists phi] Identity ()
-> WriterT [Exists phi] Identity (Holes kappa fam phi b)
-> WriterT [Exists phi] Identity (Holes kappa fam phi b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Holes kappa fam phi b
-> WriterT [Exists phi] Identity (Holes kappa fam phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return Holes kappa fam phi b
r
mnub :: (Ord a) => [a] -> [a]
mnub :: [a] -> [a]
mnub [] = []
mnub [x :: a
x] = [a
x]
mnub (x :: a
x:y :: a
y:ys :: [a]
ys)
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a] -> [a]
forall a. Ord a => [a] -> [a]
mnub (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
| Bool
otherwise = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
forall a. Ord a => [a] -> [a]
mnub (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
whileM :: (Ord (Exists phi))
=> a -> [Exists phi] -> (a -> [Exists phi] -> Writer [Exists phi] a)
-> Either [Exists phi] a
whileM :: a
-> [Exists phi]
-> (a -> [Exists phi] -> Writer [Exists phi] a)
-> Either [Exists phi] a
whileM a :: a
a xs :: [Exists phi]
xs f :: a -> [Exists phi] -> Writer [Exists phi] a
f = do
let (x' :: a
x' , xs' :: [Exists phi]
xs') = Writer [Exists phi] a -> (a, [Exists phi])
forall w a. Writer w a -> (a, w)
runWriter (a -> [Exists phi] -> Writer [Exists phi] a
f a
a [Exists phi]
xs)
if [Exists phi] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Exists phi]
xs'
then a -> Either [Exists phi] a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x'
else if ([Exists phi] -> [Exists phi]
forall a. Ord a => [a] -> [a]
mnub ([Exists phi] -> [Exists phi]
forall a. Ord a => [a] -> [a]
sort [Exists phi]
xs') [Exists phi] -> [Exists phi] -> Bool
forall a. Eq a => a -> a -> Bool
== [Exists phi] -> [Exists phi]
forall a. Ord a => [a] -> [a]
mnub ([Exists phi] -> [Exists phi]
forall a. Ord a => [a] -> [a]
sort [Exists phi]
xs))
then [Exists phi] -> Either [Exists phi] a
forall a b. a -> Either a b
Left [Exists phi]
xs'
else a
-> [Exists phi]
-> (a -> [Exists phi] -> Writer [Exists phi] a)
-> Either [Exists phi] a
forall a.
Ord (Exists phi) =>
a
-> [Exists phi]
-> (a -> [Exists phi] -> Writer [Exists phi] a)
-> Either [Exists phi] a
whileM a
x' [Exists phi]
xs' a -> [Exists phi] -> Writer [Exists phi] a
f
removeIds :: forall a b
. (Ord a) => (b -> Maybe a) -> M.Map a b -> M.Map a b
removeIds :: (b -> Maybe a) -> Map a b -> Map a b
removeIds proj :: b -> Maybe a
proj = (a -> b -> Bool) -> Map a b -> Map a b
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\a :: a
a b :: b
b -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
a Maybe a -> Maybe a -> Bool
forall a. Eq a => a -> a -> Bool
== b -> Maybe a
proj b
b)
breakCycles :: forall a b
. (Ord a) => (a -> b) -> (b -> Maybe a) -> M.Map a b -> M.Map a b
breakCycles :: (a -> b) -> (b -> Maybe a) -> Map a b -> Map a b
breakCycles inj :: a -> b
inj proj :: b -> Maybe a
proj m0 :: Map a b
m0
= let (flattenedCycles :: Map a b
flattenedCycles , m' :: Map a b
m') = State (Map a b) (Map a b) -> Map a b -> (Map a b, Map a b)
forall s a. State s a -> s -> (a, s)
runState (Map a b -> State (Map a b) (Map a b)
dropCycles Map a b
m0) Map a b
forall k a. Map k a
M.empty
in Map a b -> Map a b -> Map a b
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map a b
flattenedCycles Map a b
m'
where
dropCycles :: M.Map a b -> State (M.Map a b) (M.Map a b)
dropCycles :: Map a b -> State (Map a b) (Map a b)
dropCycles m :: Map a b
m = case Map a b -> Maybe (a, Map a b)
findCycle Map a b
m of
Nothing -> Map a b -> State (Map a b) (Map a b)
forall (m :: * -> *) a. Monad m => a -> m a
return Map a b
m
Just (a :: a
a , cyc :: Map a b
cyc) -> do
(Map a b -> Map a b) -> StateT (Map a b) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Map a b -> Map a b -> Map a b
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map a b
cyc)
Map a b -> State (Map a b) (Map a b)
dropCycles (a -> Map a b -> Map a b
forall k a. Ord k => k -> Map k a -> Map k a
M.delete a
a (Map a b
m Map a b -> Map a b -> Map a b
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.\\ Map a b
cyc))
cycleFor :: a -> M.Map a b -> Maybe (M.Map a b)
cycleFor :: a -> Map a b -> Maybe (Map a b)
cycleFor a0 :: a
a0 m :: Map a b
m = a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
a0 Map a b
m Maybe b -> (b -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Maybe a
proj Maybe a -> (a -> Maybe (Map a b)) -> Maybe (Map a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map a b -> a -> Maybe (Map a b)
go Map a b
forall k a. Map k a
M.empty
where
go :: M.Map a b -> a -> Maybe (M.Map a b)
go :: Map a b -> a -> Maybe (Map a b)
go aux :: Map a b
aux a' :: a
a'
| a
a' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a0 Bool -> Bool -> Bool
|| a
a' a -> Map a b -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map a b
aux = Map a b -> Maybe (Map a b)
forall (m :: * -> *) a. Monad m => a -> m a
return Map a b
aux
| Bool
otherwise = a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
a' Map a b
m Maybe b -> (b -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> Maybe a
proj Maybe a -> (a -> Maybe (Map a b)) -> Maybe (Map a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map a b -> a -> Maybe (Map a b)
go (a -> b -> Map a b -> Map a b
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
a' (a -> b
inj a
a0) Map a b
aux)
findCycle :: M.Map a b -> Maybe (a , M.Map a b)
findCycle :: Map a b -> Maybe (a, Map a b)
findCycle m :: Map a b
m = (Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
-> (Maybe (a, Map a b) -> Maybe (a, Map a b)) -> Maybe (a, Map a b)
forall r a. Cont r a -> (a -> r) -> r
`runCont` Maybe (a, Map a b) -> Maybe (a, Map a b)
forall a. a -> a
id) (Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
-> Maybe (a, Map a b))
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
-> Maybe (a, Map a b)
forall a b. (a -> b) -> a -> b
$ ((Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ())
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b)))
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
forall (m :: * -> *) a b. MonadCont m => ((a -> m b) -> m a) -> m a
callCC (((Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ())
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b)))
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b)))
-> ((Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ())
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b)))
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
forall a b. (a -> b) -> a -> b
$
\exit :: Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ()
exit -> (ContT (Maybe (a, Map a b)) Identity ()
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (a, Map a b)
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, Map a b)
forall a. Maybe a
Nothing) (ContT (Maybe (a, Map a b)) Identity ()
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b)))
-> ((a -> ContT (Maybe (a, Map a b)) Identity ())
-> ContT (Maybe (a, Map a b)) Identity ())
-> (a -> ContT (Maybe (a, Map a b)) Identity ())
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> ContT (Maybe (a, Map a b)) Identity ())
-> [a] -> ContT (Maybe (a, Map a b)) Identity ())
-> [a]
-> (a -> ContT (Maybe (a, Map a b)) Identity ())
-> ContT (Maybe (a, Map a b)) Identity ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> ContT (Maybe (a, Map a b)) Identity ())
-> [a] -> ContT (Maybe (a, Map a b)) Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Map a b -> [a]
forall k a. Map k a -> [k]
M.keys Map a b
m) ((a -> ContT (Maybe (a, Map a b)) Identity ())
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b)))
-> (a -> ContT (Maybe (a, Map a b)) Identity ())
-> Cont (Maybe (a, Map a b)) (Maybe (a, Map a b))
forall a b. (a -> b) -> a -> b
$
\a :: a
a -> case a -> Map a b -> Maybe (Map a b)
cycleFor a
a Map a b
m of
Nothing -> () -> ContT (Maybe (a, Map a b)) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just r :: Map a b
r -> Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ()
exit (Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ())
-> Maybe (a, Map a b) -> ContT (Maybe (a, Map a b)) Identity ()
forall a b. (a -> b) -> a -> b
$ (a, Map a b) -> Maybe (a, Map a b)
forall a. a -> Maybe a
Just (a
a , Map a b
r)