{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
-- |Constraint-based unification algorithm for 'Holes'
module Generics.Simplistic.Unify
  ( -- * Substitution
    Subst , substEmpty , substInsert , substLkup , substApply
    -- * Unification
  , 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

-- |Unification can return succesfully or find either
-- a 'OccursCheck' failure or a 'SymbolClash' failure.
data UnifyErr kappa fam phi :: * where
  -- |The occurs-check fails when the variable in question
  -- occurs within the term its supposed to be unified with.
  OccursCheck :: [Exists phi]
              -> UnifyErr kappa fam phi
  -- |A symbol-clash is thrown when the head of the
  -- two terms is different and neither is a variabe.
  SymbolClash :: Holes    kappa fam phi at
              -> Holes    kappa fam phi at
              -> UnifyErr kappa fam phi

-- |A substitution is but a map; the existential quantifiers are
-- necessary to ensure we can reuse from "Data.Map"
--
-- Note that we must be able to compare @Exists phi@. This
-- comparison needs to work heterogeneously and it must
-- return 'EQ' only when the contents are in fact equal.
-- Even though we only need this instance for "Data.Map"
--
-- A typical example for @phi@ is @Const Int at@, representing
-- a variable. The @Ord@ instance would then be:
--
-- > instance Ord (Exists (Const Int)) where
-- >   compare (Exists (Const x)) (Exists (Const y))
-- >     = compare x y
--
type Subst kappa fam phi
  = M.Map (Exists phi) (Exists (Holes kappa fam phi))

-- |Empty substitution
substEmpty :: Subst kappa fam phi
substEmpty :: Subst kappa fam phi
substEmpty = Subst kappa fam phi
forall k a. Map k a
M.empty

-- |Looks a value up in a substitution, see 'substInsert'
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
    -- In case we found something, it must be of the same
    -- type as what we got because we only insert
    -- well-typed things.
    -- TODO: Use our sameTy method to remove the unsafeCoerce
    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

-- |Applies a substitution to a term once; Variables not in the
-- support of the substitution are left untouched.
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)

-- |Inserts a point in a substitution. Note how the index of
-- @phi@ /must/ match the index of the term being inserted.
-- This is important when looking up terms because we must
-- 'unsafeCoerce' the existential type variables to return.
--
-- Please, always use this insertion function; or, if you insert
-- by hand, ensure thetype indices match.
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

-- |Unification is done in a monad.
type UnifyM kappa fam phi
  = StateT (Subst kappa fam phi) (Except (UnifyErr kappa fam phi))

-- |Attempts to unify two 'Holes', but ignores
-- which error happened when they could not be unified.
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

-- |Attempts to unify two 'Holes'
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

-- |Attempts to unify two 'Holes' with an already existing
-- substitution
unifyWith :: (All Eq kappa , Ord (Exists phi) , EqHO phi)
          => Subst kappa fam phi -- ^ Starting subst
          -> 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

-- Actual unification algorithm; In order to improve efficiency,
-- we first register all equivalences we need to satisfy,
-- then on 'mininize' we do the occurs-check.
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)
           
    -- Whenever we see a variable being matched against a term
    -- we record the equivalence. First we make sure we did not
    -- record such equivalence yet, otherwise, we recursively thin
    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
        -- First time we see 'var', we instantiate it and get going.
        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)
        -- It's not the first time we thin 'var'; previously, we had
        -- that 'var' was supposed to be p'. We will check whether it
        -- is the same as q, if not, we will have to thin p' with 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'
          

-- |The minimization step performs the /occurs check/ and removes
--  unecessary steps, returning an idempodent substitution when
--  successful. For example;
--
--  > sigma = fromList
--  >           [ (0 , bin 1 2)
--  >           , (1 , bin 4 4) ]
--
-- Then, @minimize sigma@ will return @fromList [(0 , bin (bin 4 4) 2) , (1 , bin 4 4)]@
-- This returns @Left vs@ if occurs-check fail for variables @vs@.
--
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

    -- The actual engine of the 'minimize' function is thinning the
    -- variables that appear in the image of the substitution under production.
    -- We use the writer monad solely to let us know whether some variables have
    -- been substituted in this current term. After one iteration
    -- of the map where no variable is further refined, we are done.
    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

    -- | Just like nub; but works on a sorted list
    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)

    -- We loop while there is work to be done or no progress
    -- was done.
    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

-- |Removes the keys that project to themselves according to
-- the provided projection.
--
-- > removeIds id $ M.fromList [(0,0), (1,2) , (3,4)]
-- >   = M.fromList [(1,2),(3,4)]
--
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)


-- |Will make sure there are no cycles in the map as per the
-- provided function. For example,
--
-- > breakCycles id Just $ M.fromList [(0,1) , (1,2) , (2,0)]
-- >  = M.fromList [(1,0),(2,0)]
--
-- Usefull when the maps represent some sort of equivalence; the function
-- essentially collapses the equivalence class.
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)