{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
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
import Data.Semigroup(Semigroup(..))
data Instances =
Instances {
is_instances :: [Poly (Value Identity)],
is_find :: Type -> [Value Identity] }
makeInstances :: [Poly (Value Identity)] -> Instances
makeInstances is = inst
where
inst = Instances is (memo (find_ inst . canonicaliseType))
instance Semigroup Instances where
x <> y = makeInstances (is_instances x ++ is_instances y)
instance Monoid Instances where
mempty = makeInstances []
mappend = (<>)
inst :: Typeable a => a -> Instances
inst x = valueInst (toValue (Identity x))
valueInst :: Value Identity -> Instances
valueInst x = polyInst (poly x)
where
polyInst :: Poly (Value Identity) -> Instances
polyInst x =
case typ x of
App (F Arrow) (Cons _ (Cons (App (F Arrow) _) Empty)) ->
polyInst (apply uncur x)
App (F Arrow) _ ->
makeInstances [x]
_ ->
makeInstances [apply delay x]
where
uncur = toPolyValue (uncurry :: (A -> B -> C) -> (A, B) -> C)
delay = toPolyValue ((\x () -> x) :: A -> () -> A)
findValue :: Instances -> Type -> Maybe (Value Identity)
findValue insts = listToMaybe . is_find insts . skolemiseTypeVars
findInstance :: forall f. Typeable f => Instances -> Type -> Maybe (Value f)
findInstance insts ty =
unwrapFunctor runIdentity <$> findValue insts ty'
where
ty' = typeRep (Proxy :: Proxy f) `applyType` ty
find_ :: Instances -> Type -> [Value Identity]
find_ _ (App (F unit) Empty)
| unit == tyCon (Proxy :: Proxy ()) =
return (toValue (Identity ()))
find_ insts (App (F pair) (Cons ty1 (Cons ty2 Empty)))
| pair == tyCon (Proxy :: Proxy (,)) = do
x <- is_find insts ty1
sub <- maybeToList (match ty1 (typ x))
y <- is_find insts (subst sub ty2)
sub <- maybeToList (match ty2 (typ y))
return (pairValues (liftM2 (,)) (typeSubst sub x) y)
find_ insts ty = do
fun <- fmap (polyRename ty) (is_instances insts)
App (F Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)
sub <- maybeToList (unify ty res)
fun <- return (typeSubst sub fun)
arg <- return (typeSubst sub arg)
val <- is_find insts arg
sub <- maybeToList (match arg (typ val))
return (apply (typeSubst sub fun) val)