{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Instantiate
( instantiateWith
, TypeArg(..)
, uncheckedTypeArg
, MaybeCheckedType(..)
) where
import Cryptol.ModuleSystem.Name (nameIdent)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
import Cryptol.TypeCheck.Kind(checkType)
import Cryptol.TypeCheck.Error
import Cryptol.Parser.Position (Located(..))
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Panic(panic)
import qualified Cryptol.Parser.AST as P
import Control.Monad(zipWithM)
import Data.Function (on)
import Data.List(sortBy, groupBy, find)
import Data.Maybe(mapMaybe,isJust)
import Data.Either(partitionEithers)
import qualified Data.Set as Set
data TypeArg = TypeArg
{ TypeArg -> Maybe (Located Ident)
tyArgName :: Maybe (Located Ident)
, TypeArg -> MaybeCheckedType
tyArgType :: MaybeCheckedType
}
uncheckedTypeArg :: P.TypeInst Name -> TypeArg
uncheckedTypeArg :: TypeInst Name -> TypeArg
uncheckedTypeArg TypeInst Name
a =
case TypeInst Name
a of
P.NamedInst Named (Type Name)
x ->
TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = forall a. a -> Maybe a
Just (forall a. Named a -> Located Ident
P.name Named (Type Name)
x), tyArgType :: MaybeCheckedType
tyArgType = Type Name -> MaybeCheckedType
Unchecked (forall a. Named a -> a
P.value Named (Type Name)
x) }
P.PosInst Type Name
t ->
TypeArg { tyArgName :: Maybe (Located Ident)
tyArgName = forall a. Maybe a
Nothing, tyArgType :: MaybeCheckedType
tyArgType = Type Name -> MaybeCheckedType
Unchecked Type Name
t }
data MaybeCheckedType = Checked Type | Unchecked (P.Type Name)
checkTyParam :: TypeSource -> Kind -> MaybeCheckedType -> InferM Type
checkTyParam :: TypeSource -> Kind -> MaybeCheckedType -> InferM Prop
checkTyParam TypeSource
src Kind
k MaybeCheckedType
mb =
case MaybeCheckedType
mb of
Checked Prop
t
| Kind
k forall a. Eq a => a -> a -> Bool
== Kind
k' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
t
| Bool
otherwise -> do Error -> InferM ()
recordError (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch (forall a. a -> Maybe a
Just TypeSource
src) Kind
k Kind
k')
TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
k
where k' :: Kind
k' = forall t. HasKind t => t -> Kind
kindOf Prop
t
Unchecked Type Name
t -> Type Name -> Maybe Kind -> InferM Prop
checkType Type Name
t (forall a. a -> Maybe a
Just Kind
k)
instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr,Type)
instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
nm Expr
e Schema
s [TypeArg]
ts
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Located (Ident, MaybeCheckedType)]
named = Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr, Prop)
instantiateWithPos Name
nm Expr
e Schema
s [MaybeCheckedType]
positional
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [MaybeCheckedType]
positional = Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Prop)
instantiateWithNames Name
nm Expr
e Schema
s [Located (Ident, MaybeCheckedType)]
named
| Bool
otherwise = do Error -> InferM ()
recordError Error
CannotMixPositionalAndNamedTypeParams
Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Prop)
instantiateWithNames Name
nm Expr
e Schema
s [Located (Ident, MaybeCheckedType)]
named
where
([Located (Ident, MaybeCheckedType)]
named,[MaybeCheckedType]
positional) = forall a b. [Either a b] -> ([a], [b])
partitionEithers (forall a b. (a -> b) -> [a] -> [b]
map TypeArg
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType
classify [TypeArg]
ts)
classify :: TypeArg
-> Either (Located (Ident, MaybeCheckedType)) MaybeCheckedType
classify TypeArg
t = case TypeArg -> Maybe (Located Ident)
tyArgName TypeArg
t of
Just Located Ident
n -> forall a b. a -> Either a b
Left Located Ident
n { thing :: (Ident, MaybeCheckedType)
thing = (forall a. Located a -> a
thing Located Ident
n, TypeArg -> MaybeCheckedType
tyArgType TypeArg
t) }
Maybe (Located Ident)
Nothing -> forall a b. b -> Either a b
Right (TypeArg -> MaybeCheckedType
tyArgType TypeArg
t)
instantiateWithPos ::
Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr,Type)
instantiateWithPos :: Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr, Prop)
instantiateWithPos Name
nm Expr
e (Forall [TParam]
as [Prop]
ps Prop
t) [MaybeCheckedType]
ts =
do [(TParam, Prop)]
su <- Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
1::Int) [] [TParam]
as [MaybeCheckedType]
ts
[(TParam, Prop)] -> Expr -> [Prop] -> Prop -> InferM (Expr, Prop)
doInst [(TParam, Prop)]
su Expr
e [Prop]
ps Prop
t
where
isNamed :: TParam -> Bool
isNamed TParam
q = forall a. Maybe a -> Bool
isJust (TParam -> Maybe Name
tpName TParam
q)
makeSu :: Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu Int
n [(TParam, Prop)]
su (TParam
q : [TParam]
qs) (MaybeCheckedType
mbty : [MaybeCheckedType]
tys)
| Bool -> Bool
not (TParam -> Bool
isNamed TParam
q) = do (TParam, Prop)
r <- forall {a}. HasKind a => Int -> a -> InferM (a, Prop)
unnamed Int
n TParam
q
Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
nforall a. Num a => a -> a -> a
+Int
1) ((TParam, Prop)
r forall a. a -> [a] -> [a]
: [(TParam, Prop)]
su) [TParam]
qs (MaybeCheckedType
mbty forall a. a -> [a] -> [a]
: [MaybeCheckedType]
tys)
| Bool
otherwise = do Prop
ty <- TypeSource -> Kind -> MaybeCheckedType -> InferM Prop
checkTyParam (Name -> Int -> TypeSource
TypeParamInstPos Name
nm Int
n) (forall t. HasKind t => t -> Kind
kindOf TParam
q) MaybeCheckedType
mbty
Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
nforall a. Num a => a -> a -> a
+Int
1) ((TParam
q,Prop
ty) forall a. a -> [a] -> [a]
: [(TParam, Prop)]
su) [TParam]
qs [MaybeCheckedType]
tys
makeSu Int
_ [(TParam, Prop)]
su [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [(TParam, Prop)]
su)
makeSu Int
n [(TParam, Prop)]
su (TParam
q : [TParam]
qs) [] = do (TParam, Prop)
r <- forall {a}. HasKind a => Int -> a -> InferM (a, Prop)
unnamed Int
n TParam
q
Int
-> [(TParam, Prop)]
-> [TParam]
-> [MaybeCheckedType]
-> InferM [(TParam, Prop)]
makeSu (Int
nforall a. Num a => a -> a -> a
+Int
1) ((TParam, Prop)
r forall a. a -> [a] -> [a]
: [(TParam, Prop)]
su) [TParam]
qs []
makeSu Int
_ [(TParam, Prop)]
su [] [MaybeCheckedType]
_ = do Error -> InferM ()
recordError Error
TooManyPositionalTypeParams
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [(TParam, Prop)]
su)
unnamed :: Int -> a -> InferM (a, Prop)
unnamed Int
n a
q = do Prop
ty <- TypeSource -> Kind -> InferM Prop
newType TypeSource
src (forall t. HasKind t => t -> Kind
kindOf a
q)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
q, Prop
ty)
where
src :: TypeSource
src = case forall a. Int -> [a] -> [a]
drop (Int
nforall a. Num a => a -> a -> a
-Int
1) [TParam]
as of
TParam
p:[TParam]
_ ->
case TParam -> Maybe Name
tpName TParam
p of
Just Name
a -> Name -> Ident -> TypeSource
TypeParamInstNamed Name
nm (Name -> Ident
nameIdent Name
a)
Maybe Name
_ -> Name -> Int -> TypeSource
TypeParamInstPos Name
nm Int
n
[TParam]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"instantiateWithPos"
[ String
"Invalid parameter index", forall a. Show a => a -> String
show Int
n, forall a. Show a => a -> String
show [TParam]
as ]
instantiateWithNames ::
Name -> Expr -> Schema -> [Located (Ident,MaybeCheckedType)]
-> InferM (Expr,Type)
instantiateWithNames :: Name
-> Expr
-> Schema
-> [Located (Ident, MaybeCheckedType)]
-> InferM (Expr, Prop)
instantiateWithNames Name
nm Expr
e (Forall [TParam]
as [Prop]
ps Prop
t) [Located (Ident, MaybeCheckedType)]
xs =
do forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [InferM ()]
repeatedParams
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Error -> InferM ()
recordError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located Ident -> Error
UndefinedTypeParameter forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) [Located (Ident, MaybeCheckedType)]
undefParams
[(TParam, Prop)]
su' <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> TParam -> InferM (TParam, Prop)
paramInst [ Int
1.. ] [TParam]
as
[(TParam, Prop)] -> Expr -> [Prop] -> Prop -> InferM (Expr, Prop)
doInst [(TParam, Prop)]
su' Expr
e [Prop]
ps Prop
t
where
paramInst :: Int -> TParam -> InferM (TParam, Prop)
paramInst Int
n TParam
x =
do let k :: Kind
k = TParam -> Kind
tpKind TParam
x
lkp :: Name -> Maybe (Located (Ident, MaybeCheckedType))
lkp Name
name = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Located (Ident, MaybeCheckedType)
th -> forall a b. (a, b) -> a
fst (forall a. Located a -> a
thing Located (Ident, MaybeCheckedType)
th) forall a. Eq a => a -> a -> Bool
== Name -> Ident
nameIdent Name
name) [Located (Ident, MaybeCheckedType)]
xs
src :: TypeSource
src = case TParam -> Maybe Name
tpName TParam
x of
Just Name
na -> Name -> Ident -> TypeSource
TypeParamInstNamed Name
nm (Name -> Ident
nameIdent Name
na)
Maybe Name
Nothing -> Name -> Int -> TypeSource
TypeParamInstPos Name
nm Int
n
Prop
ty <- case Name -> Maybe (Located (Ident, MaybeCheckedType))
lkp forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TParam -> Maybe Name
tpName TParam
x of
Just Located (Ident, MaybeCheckedType)
lty -> TypeSource -> Kind -> MaybeCheckedType -> InferM Prop
checkTyParam TypeSource
src Kind
k (forall a b. (a, b) -> b
snd (forall a. Located a -> a
thing Located (Ident, MaybeCheckedType)
lty))
Maybe (Located (Ident, MaybeCheckedType))
Nothing -> TypeSource -> Kind -> InferM Prop
newType TypeSource
src Kind
k
forall (m :: * -> *) a. Monad m => a -> m a
return (TParam
x, Prop
ty)
repeatedParams :: [InferM ()]
repeatedParams = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {b}. [Located (Ident, b)] -> Maybe (InferM ())
isRepeated
forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall {c} {b}. Located (c, b) -> c
pName)
forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall {c} {b}. Located (c, b) -> c
pName) [Located (Ident, MaybeCheckedType)]
xs
isRepeated :: [Located (Ident, b)] -> Maybe (InferM ())
isRepeated ys :: [Located (Ident, b)]
ys@(Located (Ident, b)
a : Located (Ident, b)
_ : [Located (Ident, b)]
_) =
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Error -> InferM ()
recordError (Ident -> [Range] -> Error
RepeatedTypeParameter (forall a b. (a, b) -> a
fst (forall a. Located a -> a
thing Located (Ident, b)
a)) (forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> Range
srcRange [Located (Ident, b)]
ys))
isRepeated [Located (Ident, b)]
_ = forall a. Maybe a
Nothing
paramIdents :: [Ident]
paramIdents = [ Name -> Ident
nameIdent Name
n | Just Name
n <- forall a b. (a -> b) -> [a] -> [b]
map TParam -> Maybe Name
tpName [TParam]
as ]
undefParams :: [Located (Ident, MaybeCheckedType)]
undefParams = [ Located (Ident, MaybeCheckedType)
x | Located (Ident, MaybeCheckedType)
x <- [Located (Ident, MaybeCheckedType)]
xs, forall {c} {b}. Located (c, b) -> c
pName Located (Ident, MaybeCheckedType)
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Ident]
paramIdents ]
pName :: Located (c, b) -> c
pName = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
thing
doInst :: [(TParam, Type)] -> Expr -> [Prop] -> Type -> InferM (Expr,Type)
doInst :: [(TParam, Prop)] -> Expr -> [Prop] -> Prop -> InferM (Expr, Prop)
doInst [(TParam, Prop)]
su' Expr
e [Prop]
ps Prop
t =
do let su :: Subst
su = [(TParam, Prop)] -> Subst
listParamSubst [(TParam, Prop)]
su'
ConstraintSource -> [Prop] -> InferM ()
newGoals (Expr -> ConstraintSource
CtInst Expr
e) (forall a b. (a -> b) -> [a] -> [b]
map (forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Prop]
ps)
let t1 :: Prop
t1 = forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
t
[Prop]
ps' <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TParam, Prop) -> InferM [Prop]
checkInst [(TParam, Prop)]
su'
ConstraintSource -> [Prop] -> InferM ()
newGoals (Expr -> ConstraintSource
CtInst Expr
e) [Prop]
ps'
forall (m :: * -> *) a. Monad m => a -> m a
return ( Expr -> Expr
addProofParams (forall {t :: * -> *}. Foldable t => t Prop -> Expr -> Expr
addTyParams (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(TParam, Prop)]
su') Expr
e), Prop
t1 )
where
addTyParams :: t Prop -> Expr -> Expr
addTyParams t Prop
ts Expr
e1 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp Expr
e1 t Prop
ts
addProofParams :: Expr -> Expr
addProofParams Expr
e1 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
e2 Prop
_ -> Expr -> Expr
EProofApp Expr
e2) Expr
e1 [Prop]
ps
frees :: Set TVar
frees = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map forall t. FVS t => t -> Set TVar
fvs (Prop
t forall a. a -> [a] -> [a]
: [Prop]
ps))
bounds :: Set TParam
bounds = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map TVar -> Set TParam
scope (forall a. Set a -> [a]
Set.toList Set TVar
frees))
where
scope :: TVar -> Set TParam
scope (TVFree Int
_ Kind
_ Set TParam
vs TVarInfo
_) = Set TParam
vs
scope (TVBound TParam
_) = forall a. Set a
Set.empty
checkInst :: (TParam, Type) -> InferM [Prop]
checkInst :: (TParam, Prop) -> InferM [Prop]
checkInst (TParam
tp, Prop
ty)
| forall a. Ord a => a -> Set a -> Bool
Set.notMember TParam
tp Set TParam
bounds = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = let a :: TVar
a = TParam -> TVar
tpVar TParam
tp
src :: TypeSource
src = TVarInfo -> TypeSource
tvarDesc (TVar -> TVarInfo
tvInfo TVar
a)
rng :: Maybe Range
rng = forall a. a -> Maybe a
Just (TVarInfo -> Range
tvarSource (TVar -> TVarInfo
tvInfo TVar
a))
in TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource (TVar -> Prop
TVar TVar
a) TypeSource
src Maybe Range
rng) Prop
ty