{-# 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
data Instances =
Instances {
Instances -> [Poly (Value Identity)]
is_instances :: [Poly (Value Identity)],
Instances -> Type -> [Value Identity]
is_find :: Type -> [Value Identity] }
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
(<>)
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 =
case forall a. Typed a => a -> Type
typ Poly (Value Identity)
x of
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]
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)
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
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
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))
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
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)
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)