{-# LANGUAGE PatternGuards #-}
module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where
import Cryptol.Parser.Position(Range)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Monad( InferM, unify, newGoals
, newType, applySubst, solveHasGoal
, newLocalName
)
import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
import Cryptol.Utils.Ident (Ident, packIdent,Namespace(..))
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
import Control.Monad(forM,guard)
recordType :: [Ident] -> InferM Type
recordType :: [Ident] -> InferM Prop
recordType [Ident]
labels =
do [(Ident, Prop)]
fields <- [Ident]
-> (Ident -> InferM (Ident, Prop)) -> InferM [(Ident, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Ident]
labels ((Ident -> InferM (Ident, Prop)) -> InferM [(Ident, Prop)])
-> (Ident -> InferM (Ident, Prop)) -> InferM [(Ident, Prop)]
forall a b. (a -> b) -> a -> b
$ \Ident
l ->
do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Ident -> TypeSource
TypeOfRecordField Ident
l) Kind
KType
(Ident, Prop) -> InferM (Ident, Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
l,Prop
t)
Prop -> InferM Prop
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordMap Ident Prop -> Prop
TRec ([(Ident, Prop)] -> RecordMap Ident Prop
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [(Ident, Prop)]
fields))
tupleType :: Int -> InferM Type
tupleType :: Int -> InferM Prop
tupleType Int
n =
do [Prop]
fields <- (Int -> InferM Prop) -> [Int] -> InferM [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
x -> TypeSource -> Kind -> InferM Prop
newType (Int -> TypeSource
TypeOfTupleField Int
x) Kind
KType)
[ Int
0 .. (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ]
Prop -> InferM Prop
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Prop] -> Prop
tTuple [Prop]
fields)
listType :: Int -> InferM Type
listType :: Int -> InferM Prop
listType Int
n =
do Prop
elems <- TypeSource -> Kind -> InferM Prop
newType TypeSource
TypeOfSeqElement Kind
KType
Prop -> InferM Prop
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Prop -> Prop
tSeq (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
n) Prop
elems)
improveSelector :: Maybe Range -> Selector -> Type -> InferM Bool
improveSelector :: Maybe Range -> Selector -> Prop -> InferM Bool
improveSelector Maybe Range
rng Selector
sel Prop
outerT =
case Selector
sel of
RecordSel Ident
_ Maybe [Ident]
mb -> ([Ident] -> InferM Prop) -> Maybe [Ident] -> InferM Bool
forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
cvt [Ident] -> InferM Prop
recordType Maybe [Ident]
mb
TupleSel Int
_ Maybe Int
mb -> (Int -> InferM Prop) -> Maybe Int -> InferM Bool
forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
cvt Int -> InferM Prop
tupleType Maybe Int
mb
ListSel Int
_ Maybe Int
mb -> (Int -> InferM Prop) -> Maybe Int -> InferM Bool
forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
cvt Int -> InferM Prop
listType Maybe Int
mb
where
cvt :: (t -> InferM Prop) -> Maybe t -> InferM Bool
cvt t -> InferM Prop
_ Maybe t
Nothing = Bool -> InferM Bool
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
cvt t -> InferM Prop
f (Just t
a) = do Prop
ty <- t -> InferM Prop
f t
a
[Prop]
ps <- TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
outerT (Selector -> TypeSource
selSrc Selector
sel) Maybe Range
rng) Prop
ty
ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType [Prop]
ps
Prop
newT <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
outerT
Bool -> InferM Bool
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
newT Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
/= Prop
outerT)
solveSelector :: Selector -> Type -> InferM (Maybe Type)
solveSelector :: Selector -> Prop -> InferM (Maybe Prop)
solveSelector Selector
sel Prop
outerT =
case (Selector
sel, Prop
outerT) of
(RecordSel Ident
l Maybe [Ident]
_, Prop
ty) ->
case Prop
ty of
TRec RecordMap Ident Prop
fs -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> RecordMap Ident Prop -> Maybe Prop
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
l RecordMap Ident Prop
fs)
TNominal NominalType
nt [Prop]
ts ->
case NominalType -> NominalTypeDef
ntDef NominalType
nt of
Struct StructCon
c ->
case Ident -> RecordMap Ident Prop -> Maybe Prop
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
l (StructCon -> RecordMap Ident Prop
ntFields StructCon
c) of
Maybe Prop
Nothing -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Prop
forall a. Maybe a
Nothing
Just Prop
t ->
do let su :: Subst
su = [(TParam, Prop)] -> Subst
listParamSubst ([TParam] -> [Prop] -> [(TParam, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip (NominalType -> [TParam]
ntParams NominalType
nt) [Prop]
ts)
ConstraintSource -> [Prop] -> InferM ()
newGoals (Name -> ConstraintSource
CtPartialTypeFun (NominalType -> Name
ntName NominalType
nt))
([Prop] -> InferM ()) -> [Prop] -> InferM ()
forall a b. (a -> b) -> a -> b
$ Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ NominalType -> [Prop]
ntConstraints NominalType
nt
Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Prop -> InferM (Maybe Prop))
-> Maybe Prop -> InferM (Maybe Prop)
forall a b. (a -> b) -> a -> b
$ Prop -> Maybe Prop
forall a. a -> Maybe a
Just (Prop -> Maybe Prop) -> Prop -> Maybe Prop
forall a b. (a -> b) -> a -> b
$ Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
t
Enum {} -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Prop
forall a. Maybe a
Nothing
NominalTypeDef
Abstract -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Prop
forall a. Maybe a
Nothing
TCon (TC TC
TCSeq) [Prop
len,Prop
el] -> Prop -> Prop -> InferM (Maybe Prop)
liftSeq Prop
len Prop
el
TCon (TC TC
TCFun) [Prop
t1,Prop
t2] -> Prop -> Prop -> InferM (Maybe Prop)
liftFun Prop
t1 Prop
t2
Prop
_ -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Prop
forall a. Maybe a
Nothing
(TupleSel Int
n Maybe Int
_, Prop
ty) ->
case Prop
ty of
TCon (TC (TCTuple Int
m)) [Prop]
ts ->
Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Prop -> InferM (Maybe Prop))
-> Maybe Prop -> InferM (Maybe Prop)
forall a b. (a -> b) -> a -> b
$ do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m)
Prop -> Maybe Prop
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Maybe Prop) -> Prop -> Maybe Prop
forall a b. (a -> b) -> a -> b
$ [Prop]
ts [Prop] -> Int -> Prop
forall a. HasCallStack => [a] -> Int -> a
!! Int
n
TCon (TC TC
TCSeq) [Prop
len,Prop
el] -> Prop -> Prop -> InferM (Maybe Prop)
liftSeq Prop
len Prop
el
TCon (TC TC
TCFun) [Prop
t1,Prop
t2] -> Prop -> Prop -> InferM (Maybe Prop)
liftFun Prop
t1 Prop
t2
Prop
_ -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Prop
forall a. Maybe a
Nothing
(ListSel Int
n Maybe Int
_, TCon (TC TC
TCSeq) [Prop
l,Prop
t])
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t)
| Bool
otherwise ->
do ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtSelector [ Prop
l Prop -> Prop -> Prop
>== Int -> Prop
forall a. Integral a => a -> Prop
tNum (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ]
Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Maybe Prop
forall a. a -> Maybe a
Just Prop
t)
(Selector, Prop)
_ -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Prop
forall a. Maybe a
Nothing
where
liftSeq :: Prop -> Prop -> InferM (Maybe Prop)
liftSeq Prop
len Prop
el =
do Maybe Prop
mb <- Selector -> Prop -> InferM (Maybe Prop)
solveSelector Selector
sel (Prop -> Prop
tNoUser Prop
el)
Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Prop -> InferM (Maybe Prop))
-> Maybe Prop -> InferM (Maybe Prop)
forall a b. (a -> b) -> a -> b
$ do Prop
el' <- Maybe Prop
mb
Prop -> Maybe Prop
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCSeq) [Prop
len,Prop
el'])
liftFun :: Prop -> Prop -> InferM (Maybe Prop)
liftFun Prop
t1 Prop
t2 =
do Maybe Prop
mb <- Selector -> Prop -> InferM (Maybe Prop)
solveSelector Selector
sel (Prop -> Prop
tNoUser Prop
t2)
Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Prop -> InferM (Maybe Prop))
-> Maybe Prop -> InferM (Maybe Prop)
forall a b. (a -> b) -> a -> b
$ do Prop
t2' <- Maybe Prop
mb
Prop -> Maybe Prop
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC TC
TCFun) [Prop
t1,Prop
t2'])
tryHasGoal :: HasGoal -> InferM (Bool, Bool)
tryHasGoal :: HasGoal -> InferM (Bool, Bool)
tryHasGoal HasGoal
has
| TCon (PC (PHas Selector
sel)) [ Prop
th, Prop
ft ] <- Goal -> Prop
goal (HasGoal -> Goal
hasGoal HasGoal
has) =
do let rng :: Maybe Range
rng = Range -> Maybe Range
forall a. a -> Maybe a
Just (Goal -> Range
goalRange (HasGoal -> Goal
hasGoal HasGoal
has))
Bool
imped <- Maybe Range -> Selector -> Prop -> InferM Bool
improveSelector Maybe Range
rng Selector
sel Prop
th
Prop
outerT <- Prop -> Prop
tNoUser (Prop -> Prop) -> InferM Prop -> InferM Prop
forall a b. (a -> b) -> InferM a -> InferM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
th
Maybe Prop
mbInnerT <- Selector -> Prop -> InferM (Maybe Prop)
solveSelector Selector
sel Prop
outerT
case Maybe Prop
mbInnerT of
Maybe Prop
Nothing -> (Bool, Bool) -> InferM (Bool, Bool)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
imped, Bool
False)
Just Prop
innerT ->
do ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType ([Prop] -> InferM ()) -> InferM [Prop] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
TypeWithSource -> Prop -> InferM [Prop]
unify (Prop -> TypeSource -> Maybe Range -> TypeWithSource
WithSource Prop
innerT (Selector -> TypeSource
selSrc Selector
sel) Maybe Range
rng) Prop
ft
Prop
oT <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
outerT
Prop
iT <- Prop -> InferM Prop
forall t. TVars t => t -> InferM t
applySubst Prop
innerT
HasGoalSln
sln <- Selector -> Prop -> Prop -> InferM HasGoalSln
mkSelSln Selector
sel Prop
oT Prop
iT
Int -> HasGoalSln -> InferM ()
solveHasGoal (HasGoal -> Int
hasName HasGoal
has) HasGoalSln
sln
(Bool, Bool) -> InferM (Bool, Bool)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Bool
True)
| Bool
otherwise = String -> [String] -> InferM (Bool, Bool)
forall a. HasCallStack => String -> [String] -> a
panic String
"hasGoalSolved"
[ String
"Unexpected selector proposition:"
, Goal -> String
forall a. Show a => a -> String
show (HasGoal -> Goal
hasGoal HasGoal
has)
]
mkSelSln :: Selector -> Type -> Type -> InferM HasGoalSln
mkSelSln :: Selector -> Prop -> Prop -> InferM HasGoalSln
mkSelSln Selector
s Prop
outerT Prop
innerT =
case Prop -> Prop
tNoUser Prop
outerT of
TCon (TC TC
TCSeq) [Prop
len,Prop
el]
| TupleSel {} <- Selector
s -> Prop -> Prop -> InferM HasGoalSln
liftSeq Prop
len Prop
el
| RecordSel {} <- Selector
s -> Prop -> Prop -> InferM HasGoalSln
liftSeq Prop
len Prop
el
TCon (TC TC
TCFun) [Prop
t1,Prop
t2]
| TupleSel {} <- Selector
s -> Prop -> Prop -> InferM HasGoalSln
liftFun Prop
t1 Prop
t2
| RecordSel {} <- Selector
s -> Prop -> Prop -> InferM HasGoalSln
liftFun Prop
t1 Prop
t2
Prop
_ -> HasGoalSln -> InferM HasGoalSln
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return HasGoalSln { hasDoSelect :: Expr -> Expr
hasDoSelect = \Expr
e -> Expr -> Selector -> Expr
ESel Expr
e Selector
s
, hasDoSet :: Expr -> Expr -> Expr
hasDoSet = \Expr
e Expr
v -> Prop -> Expr -> Selector -> Expr -> Expr
ESet Prop
outerT Expr
e Selector
s Expr
v }
where
liftSeq :: Prop -> Prop -> InferM HasGoalSln
liftSeq Prop
len Prop
el =
do Name
x1 <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"x")
Name
x2 <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"x")
Name
y2 <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"y")
case Prop -> Prop
tNoUser Prop
innerT of
TCon TCon
_ [Prop
_,Prop
eli] ->
do HasGoalSln
d <- Selector -> Prop -> Prop -> InferM HasGoalSln
mkSelSln Selector
s Prop
el Prop
eli
HasGoalSln -> InferM HasGoalSln
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HasGoalSln
{ hasDoSelect :: Expr -> Expr
hasDoSelect = \Expr
e ->
Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp Prop
len Prop
eli (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d (Name -> Expr
EVar Name
x1))
[[ Name -> Prop -> Prop -> Expr -> Match
From Name
x1 Prop
len Prop
el Expr
e ]]
, hasDoSet :: Expr -> Expr -> Expr
hasDoSet = \Expr
e Expr
v ->
Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp Prop
len Prop
el (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d (Name -> Expr
EVar Name
x2) (Name -> Expr
EVar Name
y2))
[ [ Name -> Prop -> Prop -> Expr -> Match
From Name
x2 Prop
len Prop
el Expr
e ]
, [ Name -> Prop -> Prop -> Expr -> Match
From Name
y2 Prop
len Prop
eli Expr
v ]
]
}
Prop
_ -> String -> [String] -> InferM HasGoalSln
forall a. HasCallStack => String -> [String] -> a
panic String
"mkSelSln" [ String
"Unexpected inner seq type.", Prop -> String
forall a. Show a => a -> String
show Prop
innerT ]
liftFun :: Prop -> Prop -> InferM HasGoalSln
liftFun Prop
t1 Prop
t2 =
do Name
x1 <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"x")
Name
x2 <- Namespace -> Ident -> InferM Name
newLocalName Namespace
NSValue (String -> Ident
packIdent String
"x")
case Prop -> Prop
tNoUser Prop
innerT of
TCon TCon
_ [Prop
_,Prop
inT] ->
do HasGoalSln
d <- Selector -> Prop -> Prop -> InferM HasGoalSln
mkSelSln Selector
s Prop
t2 Prop
inT
HasGoalSln -> InferM HasGoalSln
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HasGoalSln
{ hasDoSelect :: Expr -> Expr
hasDoSelect = \Expr
e ->
Name -> Prop -> Expr -> Expr
EAbs Name
x1 Prop
t1 (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d (Expr -> Expr -> Expr
EApp Expr
e (Name -> Expr
EVar Name
x1)))
, hasDoSet :: Expr -> Expr -> Expr
hasDoSet = \Expr
e Expr
v ->
Name -> Prop -> Expr -> Expr
EAbs Name
x2 Prop
t1 (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d (Expr -> Expr -> Expr
EApp Expr
e (Name -> Expr
EVar Name
x2))
(Expr -> Expr -> Expr
EApp Expr
v (Name -> Expr
EVar Name
x2))) }
Prop
_ -> String -> [String] -> InferM HasGoalSln
forall a. HasCallStack => String -> [String] -> a
panic String
"mkSelSln" [ String
"Unexpected inner fun type", Prop -> String
forall a. Show a => a -> String
show Prop
innerT ]