-- A data structure for resolving typeclass instances and similar at runtime.
--
-- Takes as input a set of functions ("instances"), and a type, and
-- tries to build a value of that type from the instances given.
--
-- For example, given the instances
--   ordList :: Dict (Arbitrary a) -> Dict (Arbitrary [a])
--   ordChar :: Dict (Arbitrary Char)
-- and the target type Dict (Arbitrary [Char]), it will produce the value
--   ordList ordChar :: Dict (Arbitrary [Char]).
--
-- The instances can in fact be arbitrary Haskell functions - though
-- their types must be such that the instance search will terminate.

{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables, CPP #-}
module QuickSpec.Internal.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where

import Twee.Base
import QuickSpec.Internal.Type
import Data.MemoUgly
import Data.Functor.Identity
import Data.Maybe
import Data.Proxy
import Control.Monad
#if !MIN_VERSION_base(4,9,0)
import Data.Semigroup(Semigroup(..))
#endif

-- A set of instances.
data Instances =
  Instances {
    -- The available instances.
    -- Each instance is a unary function; 'inst' sees to this.
    Instances -> [Poly (Value Identity)]
is_instances :: [Poly (Value Identity)],
    -- The resulting instance search function (memoised).
    Instances -> Type -> [Value Identity]
is_find      :: Type -> [Value Identity] }

-- A smart constructor for Instances.
makeInstances :: [Poly (Value Identity)] -> Instances
makeInstances :: [Poly (Value Identity)] -> Instances
makeInstances [Poly (Value Identity)]
is = Instances
inst
  where
    inst :: Instances
inst = [Poly (Value Identity)] -> (Type -> [Value Identity]) -> Instances
Instances [Poly (Value Identity)]
is (forall a b. Ord a => (a -> b) -> a -> b
memo (Instances -> Type -> [Value Identity]
find_ Instances
inst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typed a => a -> a
canonicaliseType))

instance Semigroup Instances where
  Instances
x <> :: Instances -> Instances -> Instances
<> Instances
y = [Poly (Value Identity)] -> Instances
makeInstances (Instances -> [Poly (Value Identity)]
is_instances Instances
x forall a. [a] -> [a] -> [a]
++ Instances -> [Poly (Value Identity)]
is_instances Instances
y)
instance Monoid Instances where
  mempty :: Instances
mempty = [Poly (Value Identity)] -> Instances
makeInstances []
  mappend :: Instances -> Instances -> Instances
mappend = forall a. Semigroup a => a -> a -> a
(<>)

-- Create a single instance.
inst :: Typeable a => a -> Instances
inst :: forall a. Typeable a => a -> Instances
inst a
x = Value Identity -> Instances
valueInst (forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue (forall a. a -> Identity a
Identity a
x))

valueInst :: Value Identity -> Instances
valueInst :: Value Identity -> Instances
valueInst Value Identity
x = Poly (Value Identity) -> Instances
polyInst (forall a. Typed a => a -> Poly a
poly Value Identity
x)
  where
    polyInst :: Poly (Value Identity) -> Instances
    polyInst :: Poly (Value Identity) -> Instances
polyInst Poly (Value Identity)
x =
      -- Transform x into a single-argument function
      -- (see comment about is_instances).
      case forall a. Typed a => a -> Type
typ Poly (Value Identity)
x of
        -- A function of type a -> (b -> c) gets uncurried.
        App (F Int
_ TyCon
Arrow) (Cons Type
_ (Cons (App (F Int
_ TyCon
Arrow) TermList TyCon
_) TermList TyCon
Empty)) ->
          Poly (Value Identity) -> Instances
polyInst (forall a. Apply a => a -> a -> a
apply Poly (Value Identity)
uncur Poly (Value Identity)
x)
        App (F Int
_ TyCon
Arrow) TermList TyCon
_ ->
          [Poly (Value Identity)] -> Instances
makeInstances [Poly (Value Identity)
x]
        -- A plain old value x (not a function) turns into \() -> x.
        Type
_ ->
          [Poly (Value Identity)] -> Instances
makeInstances [forall a. Apply a => a -> a -> a
apply Poly (Value Identity)
delay Poly (Value Identity)
x]
      where
        uncur :: Poly (Value Identity)
uncur = forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry :: (A -> B -> C) -> (A, B) -> C)
        delay :: Poly (Value Identity)
delay = forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue ((\A
x () -> A
x) :: A -> () -> A)

-- Construct a value of a particular type.
-- If the type is polymorphic, may return an instance of it.
findValue :: Instances -> Type -> Maybe (Value Identity)
findValue :: Instances -> Type -> Maybe (Value Identity)
findValue Instances
insts = forall a. [a] -> Maybe a
listToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instances -> Type -> [Value Identity]
is_find Instances
insts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typed a => a -> a
skolemiseTypeVars

-- Given a type a, construct a value of type f a.
-- If the type is polymorphic, may return an instance of it.
findInstance :: forall f. Typeable f => Instances -> Type -> Maybe (Value f)
findInstance :: forall (f :: * -> *).
Typeable f =>
Instances -> Type -> Maybe (Value f)
findInstance Instances
insts Type
ty =
  forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (h :: k2 -> *).
Typeable g =>
(forall (a :: k2). f (g a) -> h a) -> Value f -> Value h
unwrapFunctor forall a. Identity a -> a
runIdentity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instances -> Type -> Maybe (Value Identity)
findValue Instances
insts Type
ty'
  where
    ty' :: Type
ty' = forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy f) Type -> Type -> Type
`applyType` Type
ty

-- The unmemoised version of the search algorithm.
-- Knows how to apply unary functions, and also knows how to generate:
--   * The unit type ()
--   * Pairs (a, b) - search for a and then for b
-- These two are important because instValue encodes other instances
-- using them.
--
-- Invariant: the type of the returned value is an instance of the argument type.
find_ :: Instances -> Type -> [Value Identity]
find_ :: Instances -> Type -> [Value Identity]
find_ Instances
_ (App (F Int
_ TyCon
unit) TermList TyCon
Empty)
  | TyCon
unit forall a. Eq a => a -> a -> Bool
== forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
tyCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy ()) =
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue (forall a. a -> Identity a
Identity ()))
find_ Instances
insts (App (F Int
_ TyCon
pair) (Cons Type
ty1 (Cons Type
ty2 TermList TyCon
Empty)))
  | TyCon
pair forall a. Eq a => a -> a -> Bool
== forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
tyCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy (,)) = do
    Value Identity
x <- Instances -> Type -> [Value Identity]
is_find Instances
insts Type
ty1
    Subst TyCon
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
match Type
ty1 (forall a. Typed a => a -> Type
typ Value Identity
x))
    -- N.B.: subst sub ty2 because searching for x may have constrained y's type
    Value Identity
y <- Instances -> Type -> [Value Identity]
is_find Instances
insts (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst TyCon
sub Type
ty2)
    Subst TyCon
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
match Type
ty2 (forall a. Typed a => a -> Type
typ Value Identity
y))
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (f :: k -> *) (g :: k -> k -> k).
Typeable g =>
(forall (a :: k) (b :: k). f a -> f b -> f (g a b))
-> Value f -> Value f -> Value f
pairValues (forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,)) (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Value Identity
x) Value Identity
y)
find_ Instances
insts Type
ty = do
  -- Find a function whose result type unifies with ty.
  -- Rename it to avoid clashes with ty.
  Value Identity
fun <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (Typed a, Typed b) => a -> Poly b -> b
polyRename Type
ty) (Instances -> [Poly (Value Identity)]
is_instances Instances
insts)
  App (F Int
_ TyCon
Arrow) (Cons Type
arg (Cons Type
res TermList TyCon
Empty)) <- forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => a -> Type
typ Value Identity
fun)
  Subst TyCon
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
unify Type
ty Type
res)
  Value Identity
fun <- forall (m :: * -> *) a. Monad m => a -> m a
return (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Value Identity
fun)
  Type
arg <- forall (m :: * -> *) a. Monad m => a -> m a
return (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Type
arg)
  -- Find an argument for that function and apply the function.
  Value Identity
val <- Instances -> Type -> [Value Identity]
is_find Instances
insts Type
arg
  Subst TyCon
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
match Type
arg (forall a. Typed a => a -> Type
typ Value Identity
val))
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Apply a => a -> a -> a
apply (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Value Identity
fun) Value Identity
val)