-- | This module is internal to QuickSpec.
--
-- Polymorphic types and dynamic values.
{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds, GADTs, TypeOperators #-}
-- To avoid a warning about TyVarNumber's constructor being unused:
{-# OPTIONS_GHC -fno-warn-unused-binds #-}
module QuickSpec.Internal.Type(
  -- * Types
  Typeable,
  Arity(..),
  Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, ClassF, SymA, typeVar, isTypeVar,
  typeOf, typeRep, typeFromTyCon, applyType, fromTypeRep,
  arrowType, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,
  isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,
  -- * Things that have types
  Typed(..), typeSubst, typesDL, tyVars, cast, matchType,
  TypeView(..),
  Apply(..), apply, canApply,
  oneTypeVar, defaultTo, skolemiseTypeVars,
  -- * Polymorphic types
  canonicaliseType,
  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu, polyFunctionMgu,
  -- * Dynamic values
  Value, toValue, fromValue, valueType,
  unwrap, Unwrapped(..), Wrapper(..),
  mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor, bringFunctor) where

import Control.Monad
import Data.DList(DList)
import Data.Maybe
import qualified Data.Typeable as Ty
import Data.Typeable(Typeable)
import GHC.Exts(Any)
import Test.QuickCheck
import Unsafe.Coerce
import Data.Constraint
import Twee.Base
import Data.Proxy
import Data.List hiding (singleton)
import Data.Char
import Data.Functor.Identity

-- | A (possibly polymorphic) type.
type Type = Term TyCon

-- | A type constructor.
data TyCon =
    -- | The function type constructor @(->)@.
    Arrow
    -- | An ordinary Haskell type constructor.
  | TyCon Ty.TyCon
    -- | A string. Can be used to represent miscellaneous types that do not
    -- really exist in Haskell.
  | String String
  deriving (TyCon -> TyCon -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TyCon -> TyCon -> Bool
$c/= :: TyCon -> TyCon -> Bool
== :: TyCon -> TyCon -> Bool
$c== :: TyCon -> TyCon -> Bool
Eq, Eq TyCon
TyCon -> TyCon -> Bool
TyCon -> TyCon -> Ordering
TyCon -> TyCon -> TyCon
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TyCon -> TyCon -> TyCon
$cmin :: TyCon -> TyCon -> TyCon
max :: TyCon -> TyCon -> TyCon
$cmax :: TyCon -> TyCon -> TyCon
>= :: TyCon -> TyCon -> Bool
$c>= :: TyCon -> TyCon -> Bool
> :: TyCon -> TyCon -> Bool
$c> :: TyCon -> TyCon -> Bool
<= :: TyCon -> TyCon -> Bool
$c<= :: TyCon -> TyCon -> Bool
< :: TyCon -> TyCon -> Bool
$c< :: TyCon -> TyCon -> Bool
compare :: TyCon -> TyCon -> Ordering
$ccompare :: TyCon -> TyCon -> Ordering
Ord, Int -> TyCon -> ShowS
[TyCon] -> ShowS
TyCon -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyCon] -> ShowS
$cshowList :: [TyCon] -> ShowS
show :: TyCon -> String
$cshow :: TyCon -> String
showsPrec :: Int -> TyCon -> ShowS
$cshowsPrec :: Int -> TyCon -> ShowS
Show, Typeable)

instance Labelled TyCon

instance Pretty TyCon where
  pPrint :: TyCon -> Doc
pPrint TyCon
Arrow = String -> Doc
text String
"->"
  pPrint (String String
x) = String -> Doc
text String
x
  pPrint (TyCon TyCon
x) = String -> Doc
text (forall a. Show a => a -> String
show TyCon
x)
instance PrettyTerm TyCon where
  termStyle :: TyCon -> TermStyle
termStyle TyCon
Arrow =
    Int -> TermStyle -> TermStyle
fixedArity Int
2 forall a b. (a -> b) -> a -> b
$
    (forall a.
 Pretty a =>
 PrettyLevel -> Rational -> Doc -> [a] -> Doc)
-> TermStyle
TermStyle forall a b. (a -> b) -> a -> b
$ \PrettyLevel
l Rational
p Doc
d [a
x, a
y] ->
      Bool -> Doc -> Doc
maybeParens (Rational
p forall a. Ord a => a -> a -> Bool
> Rational
8) forall a b. (a -> b) -> a -> b
$
        forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
9 a
x Doc -> Doc -> Doc
<+> Doc
d Doc -> Doc -> Doc
<+>
        forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
0 a
y

  termStyle (String String
_) = TermStyle
curried

  termStyle (TyCon TyCon
con)
    | TyCon
con forall a. Eq a => a -> a -> Bool
== TyCon
listTyCon =
      Int -> TermStyle -> TermStyle
fixedArity Int
1 forall a b. (a -> b) -> a -> b
$
      (forall a.
 Pretty a =>
 PrettyLevel -> Rational -> Doc -> [a] -> Doc)
-> TermStyle
TermStyle forall a b. (a -> b) -> a -> b
$ \PrettyLevel
l Rational
_ Doc
_ [a
x] -> Doc -> Doc
brackets (forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
0 a
x)
    | forall a. Show a => a -> String
show TyCon
con forall a. Eq a => a -> a -> Bool
== String
"()" Bool -> Bool -> Bool
|| forall a. Show a => a -> String
show TyCon
con forall a. Eq a => a -> a -> Bool
== String
"(%%)" =
      Int -> TermStyle -> TermStyle
fixedArity Int
0 TermStyle
tupleStyle -- by analogy with case below
    | forall a. Int -> [a] -> [a]
take Int
2 (forall a. Show a => a -> String
show TyCon
con) forall a. Eq a => a -> a -> Bool
== String
"(," Bool -> Bool -> Bool
||
      forall a. Int -> [a] -> [a]
take Int
3 (forall a. Show a => a -> String
show TyCon
con) forall a. Eq a => a -> a -> Bool
== String
"(%," =
      Int -> TermStyle -> TermStyle
fixedArity (Int
1forall a. Num a => a -> a -> a
+forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== Char
',') (forall a. Show a => a -> String
show TyCon
con))) TermStyle
tupleStyle
    | Char -> Bool
isAlphaNum (forall a. [a] -> a
head (forall a. Show a => a -> String
show TyCon
con)) = TermStyle
curried
    | Bool
otherwise = Int -> TermStyle
infixStyle Int
5

-- Type and class variables.
newtype A = A Any deriving Typeable
newtype B = B Any deriving Typeable
newtype C = C Any deriving Typeable
newtype D = D Any deriving Typeable
newtype E = E Any deriving Typeable

class ClassA
deriving instance Typeable ClassA
class ClassB
deriving instance Typeable ClassB
class ClassC
deriving instance Typeable ClassC
class ClassD
deriving instance Typeable ClassD
class ClassE
deriving instance Typeable ClassE
class ClassF
deriving instance Typeable ClassF

-- | A polymorphic type of kind Symbol.
type SymA = "__polymorphic_symbol__"

-- | All type variables that are defined in this module.
typeVars :: [Ty.TypeRep]
typeVars :: [TypeRep]
typeVars =
  [forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy A),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy B),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy C),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy D),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy E),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy ClassA),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy ClassB),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy ClassC),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy ClassD),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy ClassE),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy ClassF),
   forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy SymA)]

-- | A type variable.
typeVar :: Type
typeVar :: Type
typeVar = forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy A)

-- | Check if a type is a type variable.
isTypeVar :: Type -> Bool
isTypeVar :: Type -> Bool
isTypeVar = forall f. Term f -> Bool
isVar

-- | Construct a type from a `Typeable`.
typeOf :: Typeable a => a -> Type
typeOf :: forall a. Typeable a => a -> Type
typeOf a
x = TypeRep -> Type
fromTypeRep (forall a. Typeable a => a -> TypeRep
Ty.typeOf a
x)

-- | Construct a type from a `Typeable`.
typeRep :: Typeable (a :: k) => proxy a -> Type
typeRep :: forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep proxy a
x = TypeRep -> Type
fromTypeRep (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep proxy a
x)

-- | Turn a `TyCon` into a type.
typeFromTyCon :: TyCon -> Type
typeFromTyCon :: TyCon -> Type
typeFromTyCon TyCon
tc = forall a. Build a => a -> Term (BuildFun a)
build (forall f. Fun f -> Builder f
con (forall f. Labelled f => f -> Fun f
fun TyCon
tc))

-- | Function application for type constructors.
--
-- For example, @applyType (typeRep (Proxy :: Proxy [])) (typeRep (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int])@.
applyType :: Type -> Type -> Type
applyType :: Type -> Type -> Type
applyType (App Fun TyCon
f TermList TyCon
tys) Type
ty = forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun TyCon
f (forall f. TermList f -> [Term f]
unpack TermList TyCon
tys forall a. [a] -> [a] -> [a]
++ [Type
ty]))
applyType Type
_ Type
_ = forall a. HasCallStack => String -> a
error String
"tried to apply type variable"

-- | Construct a function type.
arrowType :: [Type] -> Type -> Type
arrowType :: [Type] -> Type -> Type
arrowType [] Type
res = Type
res
arrowType (Type
arg:[Type]
args) Type
res =
  forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app (forall f. Labelled f => f -> Fun f
fun TyCon
Arrow) [Type
arg, [Type] -> Type -> Type
arrowType [Type]
args Type
res])

-- | Is a given type a function type?
isArrowType :: Type -> Bool
isArrowType :: Type -> Bool
isArrowType = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, Type)
unpackArrow

-- | Decompose a function type into (argument, result).
--
-- For multiple-argument functions, unpacks one argument.
unpackArrow :: Type -> Maybe (Type, Type)
unpackArrow :: Type -> Maybe (Type, Type)
unpackArrow (App (F Int
_ TyCon
Arrow) (Cons Type
t (Cons Type
u TermList TyCon
Empty))) =
  forall a. a -> Maybe a
Just (Type
t, Type
u)
unpackArrow Type
_ =
  forall a. Maybe a
Nothing

-- | The arguments of a function type.
typeArgs :: Type -> [Type]
typeArgs :: Type -> [Type]
typeArgs (App (F Int
_ TyCon
Arrow) (Cons Type
arg (Cons Type
res TermList TyCon
Empty))) =
  Type
argforall a. a -> [a] -> [a]
:Type -> [Type]
typeArgs Type
res
typeArgs Type
_ = []

-- | The result of a function type.
typeRes :: Type -> Type
typeRes :: Type -> Type
typeRes (App (F Int
_ TyCon
Arrow) (Cons Type
_ (Cons Type
res TermList TyCon
Empty))) =
  Type -> Type
typeRes Type
res
typeRes Type
ty = Type
ty

-- | Given the type of a function, returns the type of applying that function to
-- @n@ arguments. Crashes if the type does not have enough arguments.
typeDrop :: Int -> Type -> Type
typeDrop :: Int -> Type -> Type
typeDrop Int
0 Type
ty = Type
ty
typeDrop Int
n (App (F Int
_ TyCon
Arrow) (Cons Type
_ (Cons Type
ty TermList TyCon
Empty))) =
  Int -> Type -> Type
typeDrop (Int
nforall a. Num a => a -> a -> a
-Int
1) Type
ty
typeDrop Int
_ Type
_ =
  forall a. HasCallStack => String -> a
error String
"typeDrop on non-function type"

-- | How many arguments does a function take?
typeArity :: Type -> Int
typeArity :: Type -> Int
typeArity = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Type]
typeArgs

-- | Unify all type variables in a type.
oneTypeVar :: Typed a => a -> a
oneTypeVar :: forall a. Typed a => a -> a
oneTypeVar = forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst (forall a b. a -> b -> a
const (forall f. Var -> Builder f
var (Int -> Var
V Int
0)))

-- | Replace all type variables with a particular type.
defaultTo :: Typed a => Type -> a -> a
defaultTo :: forall a. Typed a => Type -> a -> a
defaultTo Type
def = forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst (forall a b. a -> b -> a
const Type
def)

-- | Make a type ground by replacing all type variables
-- with Skolem constants.
skolemiseTypeVars :: Typed a => a -> a
skolemiseTypeVars :: forall a. Typed a => a -> a
skolemiseTypeVars = forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst (forall a b. a -> b -> a
const Type
aTy)
  where
    aTy :: Term (BuildFun (Builder TyCon))
aTy = forall a. Build a => a -> Term (BuildFun a)
build (forall f. Fun f -> Builder f
con (forall f. Labelled f => f -> Fun f
fun (forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
tyCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy A))))

-- | Construct a type from a `Ty.TypeRep`.
fromTypeRep :: Ty.TypeRep -> Type
fromTypeRep :: TypeRep -> Type
fromTypeRep TypeRep
ty
  | Just Int
n <- forall a. Eq a => a -> [a] -> Maybe Int
elemIndex TypeRep
ty [TypeRep]
typeVars =
      forall a. Build a => a -> Term (BuildFun a)
build (forall f. Var -> Builder f
var (Int -> Var
V Int
n))
  | Bool
otherwise =
    let (TyCon
tyCon, [TypeRep]
tys) = TypeRep -> (TyCon, [TypeRep])
Ty.splitTyConApp TypeRep
ty in
    forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app (forall f. Labelled f => f -> Fun f
fun (TyCon -> TyCon
fromTyCon TyCon
tyCon)) (forall a b. (a -> b) -> [a] -> [b]
map TypeRep -> Type
fromTypeRep [TypeRep]
tys))

-- | Construct a `TyCon` type from a "Data.Typeable" `Ty.TyCon`.
fromTyCon :: Ty.TyCon -> TyCon
fromTyCon :: TyCon -> TyCon
fromTyCon TyCon
ty
  | TyCon
ty forall a. Eq a => a -> a -> Bool
== TyCon
arrowTyCon = TyCon
Arrow
  | Bool
otherwise = TyCon -> TyCon
TyCon TyCon
ty

-- | Some built-in type consructors.
arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon
arrowTyCon :: TyCon
arrowTyCon = forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
mkCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy (->))
commaTyCon :: TyCon
commaTyCon = forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
mkCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy (,))
listTyCon :: TyCon
listTyCon  = forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
mkCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy [])
dictTyCon :: TyCon
dictTyCon  = forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
mkCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy Dict)

mkCon :: Typeable a => proxy a -> Ty.TyCon
mkCon :: forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
mkCon = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep -> (TyCon, [TypeRep])
Ty.splitTyConApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
Ty.typeRep

-- | Get the outermost `TyCon` of a `Typeable`.
tyCon :: Typeable a => proxy a -> TyCon
tyCon :: forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
tyCon = TyCon -> TyCon
fromTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
mkCon

-- | Check if a type is of the form @`Dict` c@, and if so, return @c@.
getDictionary :: Type -> Maybe Type
getDictionary :: Type -> Maybe Type
getDictionary (App (F Int
_ (TyCon TyCon
dict)) (Cons Type
ty TermList TyCon
Empty))
  | TyCon
dict forall a. Eq a => a -> a -> Bool
== TyCon
dictTyCon = forall a. a -> Maybe a
Just Type
ty
getDictionary Type
_ = forall a. Maybe a
Nothing

-- | Check if a type is of the form @`Dict` c@.
isDictionary :: Type -> Bool
isDictionary :: Type -> Bool
isDictionary = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Type
getDictionary

-- | Count how many dictionary arguments a type has.
dictArity :: Type -> Int
dictArity :: Type -> Int
dictArity = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
takeWhile Type -> Bool
isDictionary forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Type]
typeArgs

-- | Split a type into constraints and normal type.
splitConstrainedType :: Type -> ([Type], Type)
splitConstrainedType :: Type -> ([Type], Type)
splitConstrainedType Type
ty =
  ([Type]
dicts, [Type] -> Type -> Type
arrowType [Type]
rest (Type -> Type
typeRes Type
ty))
  where
    ([Type]
dicts, [Type]
rest) = forall a. Int -> [a] -> ([a], [a])
splitAt (Type -> Int
dictArity Type
ty) (Type -> [Type]
typeArgs Type
ty)

-- CoArbitrary instances.
instance CoArbitrary Type where
  coarbitrary :: forall b. Type -> Gen b -> Gen b
coarbitrary = forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton
instance CoArbitrary (TermList TyCon) where
  coarbitrary :: forall b. TermList TyCon -> Gen b -> Gen b
coarbitrary TermList TyCon
Empty = forall n a. Integral n => n -> Gen a -> Gen a
variant Integer
0
  coarbitrary ConsSym{hd :: forall f. TermList f -> Term f
hd = Var (V Int
x), rest :: forall f. TermList f -> TermList f
rest = TermList TyCon
ts} =
    forall n a. Integral n => n -> Gen a -> Gen a
variant Integer
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary Int
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary TermList TyCon
ts
  coarbitrary ConsSym{hd :: forall f. TermList f -> Term f
hd = App Fun TyCon
f TermList TyCon
_, rest :: forall f. TermList f -> TermList f
rest = TermList TyCon
ts} =
    forall n a. Integral n => n -> Gen a -> Gen a
variant Integer
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary (forall f. Fun f -> Int
fun_id Fun TyCon
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary TermList TyCon
ts

-- | Pretty-print a type. Differs from the `Pretty` instance by printing type
-- variables in lowercase.
pPrintType :: Type -> Doc
pPrintType :: Type -> Doc
pPrintType = Type -> Doc
ppr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst (\(V Int
x) -> forall a. Build a => a -> Term (BuildFun a)
build (forall f. Fun f -> Builder f
con (forall f. Labelled f => f -> Fun f
fun (String -> TyCon
String ([String]
as forall a. [a] -> Int -> a
!! Int
x))))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> a
canonicalise
  where
    as :: [String]
as = [String] -> [String]
supply [[Char
x] | Char
x <- [Char
'a'..Char
'z']]
    -- Print dictionary arguments specially
    ppr :: Type -> Doc
ppr Type
ty
      | Just (Type
dict, Type
res) <- Type -> Maybe (Type, Type)
unpackArrow Type
ty,
        Just Type
constraint <- Type -> Maybe Type
getDictionary Type
dict =
      forall a. Pretty a => a -> Doc
pPrint Type
constraint Doc -> Doc -> Doc
<+> String -> Doc
text String
"=>" Doc -> Doc -> Doc
<+> Type -> Doc
ppr Type
res
    ppr Type
ty = forall a. Pretty a => a -> Doc
pPrint Type
ty

-- | A class for things that have a type.
class Typed a where
  -- | The type.
  typ :: a -> Type
  -- | Types that appear elsewhere in the `Typed`, for example, types of subterms.
  -- Should return everything which is affected by `typeSubst`.
  otherTypesDL :: a -> DList Type
  otherTypesDL a
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  -- | Substitute for all type variables.
  typeSubst_ :: (Var -> Builder TyCon) -> a -> a

-- | Substitute for all type variables in a `Typed`.
{-# INLINE typeSubst #-}
typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a
typeSubst :: forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst s
s a
x = forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ (forall s. Substitution s => s -> Var -> Builder (SubstFun s)
evalSubst s
s) a
x

-- | A wrapper for using the `Twee.Base.Symbolic` machinery on types.
newtype TypeView a = TypeView { forall a. TypeView a -> a
unTypeView :: a }
instance Typed a => Symbolic (TypeView a) where
  type ConstantOf (TypeView a) = TyCon
  termsDL :: TypeView a -> DList (TermListOf (TypeView a))
termsDL = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall f. Term f -> TermList f
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typed a => a -> DList Type
typesDL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeView a -> a
unTypeView
  subst_ :: (Var -> BuilderOf (TypeView a)) -> TypeView a -> TypeView a
subst_ Var -> BuilderOf (TypeView a)
sub = forall a. a -> TypeView a
TypeView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> BuilderOf (TypeView a)
sub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeView a -> a
unTypeView
instance Typed a => Has (TypeView a) Type where
  the :: TypeView a -> Type
the = forall a. Typed a => a -> Type
typ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TypeView a -> a
unTypeView

-- | All types that occur in a `Typed`.
typesDL :: Typed a => a -> DList Type
typesDL :: forall a. Typed a => a -> DList Type
typesDL a
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => a -> Type
typ a
ty) forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList Type
otherTypesDL a
ty

-- | All type variables that occur in a `Typed`.
tyVars :: Typed a => a -> [Var]
tyVars :: forall a. Typed a => a -> [Var]
tyVars = forall a. Symbolic a => a -> [Var]
vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> TypeView a
TypeView

-- | Cast a `Typed` to a target type.
-- Succeeds if the target type is an instance of the current type.
cast :: Typed a => Type -> a -> Maybe a
cast :: forall a. Typed a => Type -> a -> Maybe a
cast Type
ty a
x = do
  Subst TyCon
s <- forall f. Term f -> Term f -> Maybe (Subst f)
match (forall a. Typed a => a -> Type
typ a
x) Type
ty
  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
s a
x)

-- | Check if the second argument is an instance of the first argument.
matchType :: Type -> Type -> Maybe (Subst TyCon)
matchType :: Type -> Type -> Maybe (Subst TyCon)
matchType = forall f. Term f -> Term f -> Maybe (Subst f)
match

-- | Typed things that support function application.
class Typed a => Apply a where
  -- | Apply a function to its argument.
  --
  -- For most instances of `Typed`, the type of the argument must be exactly
  -- equal to the function's argument type. If you want unification to happen,
  -- use the `Typed` instance of `Poly`.
  tryApply :: a -> a -> Maybe a

-- | Apply a function to its argument, crashing on failure.
--
-- For most instances of `Typed`, the type of the argument must be exactly
-- equal to the function's argument type. If you want unification to happen,
-- use the `Typed` instance of `Poly`.
infixl `apply`
apply :: Apply a => a -> a -> a
apply :: forall a. Apply a => a -> a -> a
apply a
f a
x =
  case forall a. Apply a => a -> a -> Maybe a
tryApply a
f a
x of
    Maybe a
Nothing ->
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"apply: ill-typed term: can't apply " forall a. [a] -> [a] -> [a]
++
        forall a. Pretty a => a -> String
prettyShow (forall a. Typed a => a -> Type
typ a
f) forall a. [a] -> [a] -> [a]
++ String
" to " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall a. Typed a => a -> Type
typ a
x)
    Just a
y -> a
y

-- | Check if a function can be applied to its argument.
canApply :: Apply a => a -> a -> Bool
canApply :: forall a. Apply a => a -> a -> Bool
canApply a
f a
x = forall a. Maybe a -> Bool
isJust (forall a. Apply a => a -> a -> Maybe a
tryApply a
f a
x)

-- Instances.
instance Typed Type where
  typ :: Type -> Type
typ = forall a. a -> a
id
  typeSubst_ :: (Var -> Builder TyCon) -> Type -> Type
typeSubst_ = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst

instance Apply Type where
  tryApply :: Type -> Type -> Maybe Type
tryApply (App (F Int
_ TyCon
Arrow) (Cons Type
arg (Cons Type
res TermList TyCon
Empty))) Type
t
    | Type
t forall a. Eq a => a -> a -> Bool
== Type
arg = forall a. a -> Maybe a
Just Type
res
  tryApply Type
_ Type
_ = forall a. Maybe a
Nothing

instance (Typed a, Typed b) => Typed (a, b) where
  typ :: (a, b) -> Type
typ (a
x, b
y) = forall a. Build a => a -> Term (BuildFun a)
build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app (forall f. Labelled f => f -> Fun f
fun (TyCon -> TyCon
TyCon TyCon
commaTyCon)) [forall a. Typed a => a -> Type
typ a
x, forall a. Typed a => a -> Type
typ b
y])
  otherTypesDL :: (a, b) -> DList Type
otherTypesDL (a
x, b
y) = forall a. Typed a => a -> DList Type
otherTypesDL a
x forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList Type
otherTypesDL b
y
  typeSubst_ :: (Var -> Builder TyCon) -> (a, b) -> (a, b)
typeSubst_ Var -> Builder TyCon
f (a
x, b
y) = (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
f a
x, forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
f b
y)

instance (Typed a, Typed b) => Typed (Either a b) where
  typ :: Either a b -> Type
typ (Left a
x)  = forall a. Typed a => a -> Type
typ a
x
  typ (Right b
x) = forall a. Typed a => a -> Type
typ b
x
  otherTypesDL :: Either a b -> DList Type
otherTypesDL (Left a
x)  = forall a. Typed a => a -> DList Type
otherTypesDL a
x
  otherTypesDL (Right b
x) = forall a. Typed a => a -> DList Type
otherTypesDL b
x
  typeSubst_ :: (Var -> Builder TyCon) -> Either a b -> Either a b
typeSubst_ Var -> Builder TyCon
sub (Left a
x)  = forall a b. a -> Either a b
Left  (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub a
x)
  typeSubst_ Var -> Builder TyCon
sub (Right b
x) = forall a b. b -> Either a b
Right (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub b
x)

instance Typed a => Typed [a] where
  typ :: [a] -> Type
typ [] = forall a. Typeable a => a -> Type
typeOf ()
  typ (a
x:[a]
_) = forall a. Typed a => a -> Type
typ a
x
  otherTypesDL :: [a] -> DList Type
otherTypesDL [] = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  otherTypesDL (a
x:[a]
xs) = forall a. Typed a => a -> DList Type
otherTypesDL a
x forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> DList Type
typesDL [a]
xs)
  typeSubst_ :: (Var -> Builder TyCon) -> [a] -> [a]
typeSubst_ Var -> Builder TyCon
f [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
f) [a]
xs

-- | Represents a forall-quantifier over all the type variables in a type.
-- Wrapping a term in @Poly@ normalises the type by alpha-renaming
-- type variables canonically.
--
-- The `Apply` instance for `Poly` does unification to handle applying a
-- polymorphic function.
newtype Poly a = Poly { forall a. Poly a -> a
unPoly :: a }
  deriving (Poly a -> Poly a -> Bool
forall a. Eq a => Poly a -> Poly a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Poly a -> Poly a -> Bool
$c/= :: forall a. Eq a => Poly a -> Poly a -> Bool
== :: Poly a -> Poly a -> Bool
$c== :: forall a. Eq a => Poly a -> Poly a -> Bool
Eq, Poly a -> Poly a -> Bool
Poly a -> Poly a -> Ordering
Poly a -> Poly a -> Poly a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Poly a)
forall a. Ord a => Poly a -> Poly a -> Bool
forall a. Ord a => Poly a -> Poly a -> Ordering
forall a. Ord a => Poly a -> Poly a -> Poly a
min :: Poly a -> Poly a -> Poly a
$cmin :: forall a. Ord a => Poly a -> Poly a -> Poly a
max :: Poly a -> Poly a -> Poly a
$cmax :: forall a. Ord a => Poly a -> Poly a -> Poly a
>= :: Poly a -> Poly a -> Bool
$c>= :: forall a. Ord a => Poly a -> Poly a -> Bool
> :: Poly a -> Poly a -> Bool
$c> :: forall a. Ord a => Poly a -> Poly a -> Bool
<= :: Poly a -> Poly a -> Bool
$c<= :: forall a. Ord a => Poly a -> Poly a -> Bool
< :: Poly a -> Poly a -> Bool
$c< :: forall a. Ord a => Poly a -> Poly a -> Bool
compare :: Poly a -> Poly a -> Ordering
$ccompare :: forall a. Ord a => Poly a -> Poly a -> Ordering
Ord, Int -> Poly a -> ShowS
forall a. Show a => Int -> Poly a -> ShowS
forall a. Show a => [Poly a] -> ShowS
forall a. Show a => Poly a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Poly a] -> ShowS
$cshowList :: forall a. Show a => [Poly a] -> ShowS
show :: Poly a -> String
$cshow :: forall a. Show a => Poly a -> String
showsPrec :: Int -> Poly a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Poly a -> ShowS
Show, PrettyLevel -> [Poly a] -> Doc
PrettyLevel -> Rational -> Poly a -> Doc
Poly a -> Doc
forall a. Pretty a => PrettyLevel -> [Poly a] -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> Poly a -> Doc
forall a. Pretty a => Poly a -> Doc
forall a.
(PrettyLevel -> Rational -> a -> Doc)
-> (a -> Doc) -> (PrettyLevel -> [a] -> Doc) -> Pretty a
pPrintList :: PrettyLevel -> [Poly a] -> Doc
$cpPrintList :: forall a. Pretty a => PrettyLevel -> [Poly a] -> Doc
pPrint :: Poly a -> Doc
$cpPrint :: forall a. Pretty a => Poly a -> Doc
pPrintPrec :: PrettyLevel -> Rational -> Poly a -> Doc
$cpPrintPrec :: forall a. Pretty a => PrettyLevel -> Rational -> Poly a -> Doc
Pretty, Typeable)

-- | Build a `Poly`.
poly :: Typed a => a -> Poly a
poly :: forall a. Typed a => a -> Poly a
poly a
x = forall a. a -> Poly a
Poly (forall a. Typed a => a -> a
canonicaliseType a
x)

-- | Alpha-rename type variables in a canonical way.
canonicaliseType :: Typed a => a -> a
canonicaliseType :: forall a. Typed a => a -> a
canonicaliseType = forall a. TypeView a -> a
unTypeView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> a
canonicalise forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> TypeView a
TypeView

-- | Get the polymorphic type of a polymorphic value.
polyTyp :: Typed a => Poly a -> Poly Type
polyTyp :: forall a. Typed a => Poly a -> Poly Type
polyTyp (Poly a
x) = forall a. a -> Poly a
Poly (forall a. Typed a => a -> Type
typ a
x)

-- | Rename the type variables of the second argument so that they don't overlap
-- with those of the first argument.
polyRename :: (Typed a, Typed b) => a -> Poly b -> b
polyRename :: forall a b. (Typed a, Typed b) => a -> Poly b -> b
polyRename a
x (Poly b
y) =
  forall a. TypeView a -> a
unTypeView (forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding (forall a. a -> TypeView a
TypeView a
x) (forall a. a -> TypeView a
TypeView b
y))

-- | Rename the type variables of both arguments so that they don't overlap.
polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply :: forall a b c.
(Typed a, Typed b, Typed c) =>
(a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply a -> b -> c
f (Poly a
x) Poly b
y = forall a. Typed a => a -> Poly a
poly (a -> b -> c
f a
x (forall a b. (Typed a, Typed b) => a -> Poly b -> b
polyRename a
x Poly b
y))

-- | Rename the type variables of both arguments so that they don't overlap.
polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
polyPair :: forall a b. (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
polyPair = forall a b c.
(Typed a, Typed b, Typed c) =>
(a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply (,)

-- | Rename the type variables of all arguments so that they don't overlap.
polyList :: Typed a => [Poly a] -> Poly [a]
polyList :: forall a. Typed a => [Poly a] -> Poly [a]
polyList [] = forall a. Typed a => a -> Poly a
poly []
polyList (Poly a
x:[Poly a]
xs) = forall a b c.
(Typed a, Typed b, Typed c) =>
(a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply (:) Poly a
x (forall a. Typed a => [Poly a] -> Poly [a]
polyList [Poly a]
xs)

-- | Find the most general unifier of two types.
polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)
polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)
polyMgu Poly Type
ty1 Poly Type
ty2 = do
  let (Type
ty1', Type
ty2') = forall a. Poly a -> a
unPoly (forall a b. (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
polyPair Poly Type
ty1 Poly Type
ty2)
  Subst TyCon
sub <- forall f. Term f -> Term f -> Maybe (Subst f)
unify Type
ty1' Type
ty2'
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => a -> Poly a
poly (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Type
ty1'))

polyFunctionMgu :: Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))
polyFunctionMgu :: forall a. Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))
polyFunctionMgu Poly a
f Poly a
x = do
  let (a
f', (a
x', Type
resType)) = forall a. Poly a -> a
unPoly (forall a b. (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
polyPair Poly a
f (forall a b. (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
polyPair Poly a
x (forall a. Typed a => a -> Poly a
poly (forall a. Build a => a -> Term (BuildFun a)
build (forall f. Var -> Builder f
var (Int -> Var
V Int
0))))))
  Subst TyCon
s <- forall f. Term f -> Term f -> Maybe (Subst f)
unify (forall a. Typed a => a -> Type
typ a
f') ([Type] -> Type -> Type
arrowType [forall a. Typed a => a -> Type
typ a
x'] Type
resType)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => a -> Poly a
poly (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
s (a
f', a
x')))

instance Typed a => Typed (Poly a) where
  typ :: Poly a -> Type
typ = forall a. Typed a => a -> Type
typ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Poly a -> a
unPoly
  otherTypesDL :: Poly a -> DList Type
otherTypesDL = forall a. Typed a => a -> DList Type
otherTypesDL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Poly a -> a
unPoly
  typeSubst_ :: (Var -> Builder TyCon) -> Poly a -> Poly a
typeSubst_ Var -> Builder TyCon
f (Poly a
x) = forall a. Typed a => a -> Poly a
poly (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
f a
x)

instance Apply a => Apply (Poly a) where
  tryApply :: Poly a -> Poly a -> Maybe (Poly a)
tryApply Poly a
f Poly a
x = do
    (a
f', a
x') <- forall a. Poly a -> a
unPoly forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))
polyFunctionMgu Poly a
f Poly a
x
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Typed a => a -> Poly a
poly (forall a. Apply a => a -> a -> Maybe a
tryApply a
f' a
x')

-- | Convert an ordinary value to a dynamic value.
toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)
toPolyValue :: forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue = forall a. Typed a => a -> Poly a
poly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Dynamic values inside an applicative functor.
--
-- For example, a value of type @Value Maybe@ represents a @Maybe something@.
data Value f =
  Value {
    forall {k} (f :: k -> *). Value f -> Type
valueType :: Type,
    forall {k} (f :: k -> *). Value f -> f Any
value :: f Any }

instance Show (Value f) where
  show :: Value f -> String
show Value f
x = String
"<<" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall a. Typed a => a -> Type
typ Value f
x) forall a. [a] -> [a] -> [a]
++ String
">>"

fromAny :: f Any -> f a
fromAny :: forall {k} (f :: k -> *) (a :: k). f Any -> f a
fromAny = forall a b. a -> b
unsafeCoerce

toAny :: f a -> f Any
toAny :: forall {k} (f :: k -> *) (a :: k). f a -> f Any
toAny = forall a b. a -> b
unsafeCoerce

-- | Construct a `Value`.
toValue :: forall f (a :: *). Typeable a => f a -> Value f
toValue :: forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue f a
x = forall {k} (f :: k -> *). Type -> f Any -> Value f
Value (forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a)) (forall {k} (f :: k -> *) (a :: k). f a -> f Any
toAny f a
x)

-- | Deconstruct a `Value`.
fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a)
fromValue :: forall (f :: * -> *) a. Typeable a => Value f -> Maybe (f a)
fromValue Value f
x = do
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. Typed a => a -> Type
typ Value f
x forall a. Eq a => a -> a -> Bool
== forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a))
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (f :: k -> *) (a :: k). f Any -> f a
fromAny (forall {k} (f :: k -> *). Value f -> f Any
value Value f
x))

instance Typed (Value f) where
  typ :: Value f -> Type
typ = forall {k} (f :: k -> *). Value f -> Type
valueType
  typeSubst_ :: (Var -> Builder TyCon) -> Value f -> Value f
typeSubst_ Var -> Builder TyCon
f (Value Type
ty f Any
x) = forall {k} (f :: k -> *). Type -> f Any -> Value f
Value (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
f Type
ty) f Any
x
instance Applicative f => Apply (Value f) where
  tryApply :: Value f -> Value f -> Maybe (Value f)
tryApply Value f
f Value f
x = do
    Type
ty <- forall a. Apply a => a -> a -> Maybe a
tryApply (forall a. Typed a => a -> Type
typ Value f
f) (forall a. Typed a => a -> Type
typ Value f
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (f :: k -> *). Type -> f Any -> Value f
Value Type
ty (forall {k} (f :: k -> *) (a :: k). f Any -> f a
fromAny (forall {k} (f :: k -> *). Value f -> f Any
value Value f
f) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (f :: k -> *). Value f -> f Any
value Value f
x))

-- | Unwrap a value to get at the thing inside, with an existential type.
unwrap :: Value f -> Unwrapped f
unwrap :: forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value f
x =
  forall {k} (f :: k -> *). Value f -> f Any
value Value f
x forall {k} (f :: k -> *) (a :: k). f a -> Wrapper a -> Unwrapped f
`In`
    forall {k} (a :: k).
(forall (g :: k -> *). g a -> Value g)
-> (forall (g :: k -> *). Value g -> g a) -> Wrapper a
Wrapper
      (\g Any
y -> forall {k} (f :: k -> *). Type -> f Any -> Value f
Value (forall a. Typed a => a -> Type
typ Value f
x) g Any
y)
      (\Value g
y ->
        if forall a. Typed a => a -> Type
typ Value f
x forall a. Eq a => a -> a -> Bool
== forall a. Typed a => a -> Type
typ Value g
y
        then forall {k} (f :: k -> *) (a :: k). f Any -> f a
fromAny (forall {k} (f :: k -> *). Value f -> f Any
value Value g
y)
        else forall a. HasCallStack => String -> a
error String
"non-matching types")

-- | The unwrapped value. Consists of the value itself (with an existential
-- type) and functions to wrap it up again.
data Unwrapped f where
  In :: f a -> Wrapper a -> Unwrapped f

-- | Functions for re-wrapping an `Unwrapped` value.
data Wrapper a =
  Wrapper {
    -- | Wrap up a value which has the same existential type as this one.
    forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). g a -> Value g
wrap :: forall g. g a -> Value g,
    -- | Unwrap a value which has the same existential type as this one.
    forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). Value g -> g a
reunwrap :: forall g. Value g -> g a }

-- | Apply a polymorphic function to a `Value`.
mapValue :: (forall a. f a -> g a) -> Value f -> Value g
mapValue :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Value f -> Value g
mapValue forall (a :: k). f a -> g a
f Value f
v =
  case forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value f
v of
    f a
x `In` Wrapper a
w -> forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). g a -> Value g
wrap Wrapper a
w (forall (a :: k). f a -> g a
f f a
x)

-- | Apply a polymorphic function to a `Value`.
forValue :: Value f -> (forall a. f a -> g a) -> Value g
forValue :: forall {k} (f :: k -> *) (g :: k -> *).
Value f -> (forall (a :: k). f a -> g a) -> Value g
forValue Value f
x forall (a :: k). f a -> g a
f = forall {k} (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Value f -> Value g
mapValue forall (a :: k). f a -> g a
f Value f
x

-- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.
ofValue :: (forall a. f a -> b) -> Value f -> b
ofValue :: forall {k} (f :: k -> *) b.
(forall (a :: k). f a -> b) -> Value f -> b
ofValue forall (a :: k). f a -> b
f Value f
v =
  case forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value f
v of
    f a
x `In` Wrapper a
_ -> forall (a :: k). f a -> b
f f a
x

-- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.
withValue :: Value f -> (forall a. f a -> b) -> b
withValue :: forall {k} (f :: k -> *) b.
Value f -> (forall (a :: k). f a -> b) -> b
withValue Value f
x forall (a :: k). f a -> b
f = forall {k} (f :: k -> *) b.
(forall (a :: k). f a -> b) -> Value f -> b
ofValue forall (a :: k). f a -> b
f Value f
x

-- | Apply a polymorphic function to a pair of `Value`s.
pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f
pairValues :: 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 (a :: k) (b :: k). f a -> f b -> f (g a b)
f Value f
x Value f
y =
  Type
ty seq :: forall a b. a -> b -> b
`seq`
  Value {
    valueType :: Type
valueType = Type
ty,
    value :: f Any
value = forall {k} (f :: k -> *) (a :: k). f a -> f Any
toAny (forall (a :: k) (b :: k). f a -> f b -> f (g a b)
f (forall {k} (f :: k -> *). Value f -> f Any
value Value f
x) (forall {k} (f :: k -> *). Value f -> f Any
value Value f
y)) }
  where
    ty :: Type
ty = forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy g) Type -> Type -> Type
`applyType` forall a. Typed a => a -> Type
typ Value f
x Type -> Type -> Type
`applyType` forall a. Typed a => a -> Type
typ Value f
y

wrapFunctor :: forall f g h. Typeable h => (forall a. f a -> g (h a)) -> Value f -> Value g
wrapFunctor :: forall {k} {k} (f :: k -> *) (g :: k -> *) (h :: k -> k).
Typeable h =>
(forall (a :: k). f a -> g (h a)) -> Value f -> Value g
wrapFunctor forall (a :: k). f a -> g (h a)
f Value f
x =
  Type
ty seq :: forall a b. a -> b -> b
`seq`
  Value {
    valueType :: Type
valueType = Type
ty,
    value :: g Any
value = forall {k} (f :: k -> *) (a :: k). f a -> f Any
toAny (forall (a :: k). f a -> g (h a)
f (forall {k} (f :: k -> *). Value f -> f Any
value Value f
x)) }
  where
    ty :: Type
ty = forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy h) Type -> Type -> Type
`applyType` forall {k} (f :: k -> *). Value f -> Type
valueType Value f
x

unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) -> h a) -> Value f -> Value h
unwrapFunctor :: forall {k} {k} (f :: k -> *) (g :: k -> k) (h :: k -> *).
Typeable g =>
(forall (a :: k). f (g a) -> h a) -> Value f -> Value h
unwrapFunctor forall (a :: k). f (g a) -> h a
f Value f
x =
  case forall a. Typed a => a -> Type
typ Value f
x of
    App Fun TyCon
_ TermList TyCon
tys | tys :: [Type]
tys@(Type
_:[Type]
_) <- forall f. TermList f -> [Term f]
unpack TermList TyCon
tys ->
      case Type
ty Type -> Type -> Type
`applyType` forall a. [a] -> a
last [Type]
tys forall a. Eq a => a -> a -> Bool
== forall a. Typed a => a -> Type
typ Value f
x of
        Bool
True ->
          Value {
            valueType :: Type
valueType = forall a. [a] -> a
last [Type]
tys,
            value :: h Any
value = forall (a :: k). f (g a) -> h a
f (forall {k} (f :: k -> *) (a :: k). f Any -> f a
fromAny (forall {k} (f :: k -> *). Value f -> f Any
value Value f
x)) }
        Bool
False ->
          forall a. HasCallStack => String -> a
error String
"non-matching types"
    Type
_ -> forall a. HasCallStack => String -> a
error String
"value of type f a had wrong type"
  where
    ty :: Type
ty = forall k (a :: k) (proxy :: k -> *). Typeable a => proxy a -> Type
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy g)

bringFunctor :: Functor f => Value f -> f (Value Identity)
bringFunctor :: forall (f :: * -> *). Functor f => Value f -> f (Value Identity)
bringFunctor Value f
val =
  case forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value f
val of
    f a
x `In` Wrapper a
w ->
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). g a -> Value g
wrap Wrapper a
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity) f a
x

class Arity f where
  -- | Measure the arity.
  arity :: f -> Int