{-# 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Ident]
labels forall a b. (a -> b) -> a -> b
$ \Ident
l ->
do Prop
t <- TypeSource -> Kind -> InferM Prop
newType (Ident -> TypeSource
TypeOfRecordField Ident
l) Kind
KType
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
l,Prop
t)
forall (m :: * -> *) a. Monad m => a -> m a
return (RecordMap Ident Prop -> Prop
TRec (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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Int
x -> TypeSource -> Kind -> InferM Prop
newType (Int -> TypeSource
TypeOfTupleField Int
x) Kind
KType)
[ Int
0 .. (Int
nforall a. Num a => a -> a -> a
-Int
1) ]
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
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop -> Prop -> Prop
tSeq (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 -> forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
cvt [Ident] -> InferM Prop
recordType Maybe [Ident]
mb
TupleSel Int
_ Maybe Int
mb -> forall {t}. (t -> InferM Prop) -> Maybe t -> InferM Bool
cvt Int -> InferM Prop
tupleType Maybe Int
mb
ListSel Int
_ Maybe Int
mb -> 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 = 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 <- forall t. TVars t => t -> InferM t
applySubst Prop
outerT
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
newT 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
l RecordMap Ident Prop
fs)
TNewtype Newtype
nt [Prop]
ts ->
case forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
l (Newtype -> RecordMap Ident Prop
ntFields Newtype
nt) of
Maybe Prop
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just Prop
t ->
do let su :: Subst
su = [(TParam, Prop)] -> Subst
listParamSubst (forall a b. [a] -> [b] -> [(a, b)]
zip (Newtype -> [TParam]
ntParams Newtype
nt) [Prop]
ts)
ConstraintSource -> [Prop] -> InferM ()
newGoals (Name -> ConstraintSource
CtPartialTypeFun (Newtype -> Name
ntName Newtype
nt))
forall a b. (a -> b) -> a -> b
$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su forall a b. (a -> b) -> a -> b
$ Newtype -> [Prop]
ntConstraints Newtype
nt
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su Prop
t
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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
(TupleSel Int
n Maybe Int
_, Prop
ty) ->
case Prop
ty of
TCon (TC (TCTuple Int
m)) [Prop]
ts ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
0 forall a. Ord a => a -> a -> Bool
<= Int
n Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
< Int
m)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Prop]
ts forall a. [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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
(ListSel Int
n Maybe Int
_, TCon (TC TC
TCSeq) [Prop
l,Prop
t])
| Int
n forall a. Ord a => a -> a -> Bool
< Int
2 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Prop
t)
| Bool
otherwise ->
do ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtSelector [ Prop
l Prop -> Prop -> Prop
>== forall a. Integral a => a -> Prop
tNum (Int
n forall a. Num a => a -> a -> a
- Int
1) ]
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Prop
t)
(Selector, Prop)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do Prop
el' <- Maybe Prop
mb
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)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do Prop
t2' <- Maybe Prop
mb
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 = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
imped, Bool
False)
Just Prop
innerT ->
do ConstraintSource -> [Prop] -> InferM ()
newGoals ConstraintSource
CtExactType 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 <- forall t. TVars t => t -> InferM t
applySubst Prop
outerT
Prop
iT <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Bool
True)
| Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"hasGoalSolved"
[ String
"Unexpected selector proposition:"
, 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
_ -> 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
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
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"mkSelSln" [ String
"Unexpected inner seq type.", 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
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
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"mkSelSln" [ String
"Unexpected inner fun type", forall a. Show a => a -> String
show Prop
innerT ]