-- |
-- Module      :  Cryptol.TypeCheck.Solver.Selector
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# LANGUAGE PatternGuards, Safe #-}
module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where

import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Monad( InferM, unify, newGoals, lookupNewtype
                              , newType, applySubst, solveHasGoal
                              , newParamName
                              )
import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
import Cryptol.Utils.Ident (Ident, packIdent)
import Cryptol.Utils.Panic(panic)

import Control.Monad(forM,guard)


recordType :: [Ident] -> InferM Type
recordType :: [Ident] -> InferM Type
recordType labels :: [Ident]
labels =
  do [(Ident, Type)]
fields <- [Ident]
-> (Ident -> InferM (Ident, Type)) -> InferM [(Ident, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Ident]
labels ((Ident -> InferM (Ident, Type)) -> InferM [(Ident, Type)])
-> (Ident -> InferM (Ident, Type)) -> InferM [(Ident, Type)]
forall a b. (a -> b) -> a -> b
$ \l :: Ident
l ->
        do Type
t <- TVarSource -> Kind -> InferM Type
newType (Ident -> TVarSource
TypeOfRecordField Ident
l) Kind
KType
           (Ident, Type) -> InferM (Ident, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
l,Type
t)
     Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Ident, Type)] -> Type
TRec [(Ident, Type)]
fields)

tupleType :: Int -> InferM Type
tupleType :: Int -> InferM Type
tupleType n :: Int
n =
  do [Type]
fields <- (Int -> InferM Type) -> [Int] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\x :: Int
x -> TVarSource -> Kind -> InferM Type
newType (Int -> TVarSource
TypeOfTupleField Int
x) Kind
KType)
                    [ 0 .. (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) ]
     Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type
tTuple [Type]
fields)

listType :: Int -> InferM Type
listType :: Int -> InferM Type
listType n :: Int
n =
  do Type
elems <- TVarSource -> Kind -> InferM Type
newType TVarSource
TypeOfSeqElement Kind
KType
     Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
tSeq (Int -> Type
forall a. Integral a => a -> Type
tNum Int
n) Type
elems)


improveSelector :: Selector -> Type -> InferM Bool
improveSelector :: Selector -> Type -> InferM Bool
improveSelector sel :: Selector
sel outerT :: Type
outerT =
  case Selector
sel of
    RecordSel _ mb :: Maybe [Ident]
mb -> ([Ident] -> InferM Type) -> Maybe [Ident] -> InferM Bool
forall t. (t -> InferM Type) -> Maybe t -> InferM Bool
cvt [Ident] -> InferM Type
recordType Maybe [Ident]
mb
    TupleSel  _ mb :: Maybe Int
mb -> (Int -> InferM Type) -> Maybe Int -> InferM Bool
forall t. (t -> InferM Type) -> Maybe t -> InferM Bool
cvt Int -> InferM Type
tupleType  Maybe Int
mb
    ListSel   _ mb :: Maybe Int
mb -> (Int -> InferM Type) -> Maybe Int -> InferM Bool
forall t. (t -> InferM Type) -> Maybe t -> InferM Bool
cvt Int -> InferM Type
listType   Maybe Int
mb
  where
  cvt :: (t -> InferM Type) -> Maybe t -> InferM Bool
cvt _ Nothing   = Bool -> InferM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  cvt f :: t -> InferM Type
f (Just a :: t
a)  = do Type
ty <- t -> InferM Type
f t
a
                       ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType ([Type] -> InferM ()) -> InferM [Type] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Type -> InferM [Type]
unify Type
ty Type
outerT
                       Type
newT <- Type -> InferM Type
forall t. TVars t => t -> InferM t
applySubst Type
outerT
                       Bool -> InferM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
newT Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
outerT)


{- | Compute the type of a field based on the selector.
The given type should be "zonked" (i.e., substitution was applied to it),
and (outermost) type synonyms have been expanded.
-}
solveSelector :: Selector -> Type -> InferM (Maybe Type)
solveSelector :: Selector -> Type -> InferM (Maybe Type)
solveSelector sel :: Selector
sel outerT :: Type
outerT =
  case (Selector
sel, Type
outerT) of

    (RecordSel l :: Ident
l _, ty :: Type
ty) ->
      case Type
ty of
        TRec fs :: [(Ident, Type)]
fs  -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> [(Ident, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
l [(Ident, Type)]
fs)
        TCon (TC TCSeq) [len :: Type
len,el :: Type
el] -> Type -> Type -> InferM (Maybe Type)
liftSeq Type
len Type
el
        TCon (TC TCFun) [t1 :: Type
t1,t2 :: Type
t2]  -> Type -> Type -> InferM (Maybe Type)
liftFun Type
t1 Type
t2
        TCon (TC (TCNewtype (UserTC x :: Name
x _))) ts :: [Type]
ts ->
          do Maybe Newtype
mb <- Name -> InferM (Maybe Newtype)
lookupNewtype Name
x
             case Maybe Newtype
mb of
               Nothing -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
               Just nt :: Newtype
nt ->
                 case Ident -> [(Ident, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
l (Newtype -> [(Ident, Type)]
ntFields Newtype
nt) of
                   Nothing -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
                   Just t :: Type
t  ->
                     do let su :: Subst
su = [(TParam, Type)] -> Subst
listParamSubst ([TParam] -> [Type] -> [(TParam, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Newtype -> [TParam]
ntParams Newtype
nt) [Type]
ts)
                        ConstraintSource -> [Type] -> InferM ()
newGoals (Name -> ConstraintSource
CtPartialTypeFun Name
x)
                          ([Type] -> InferM ()) -> [Type] -> InferM ()
forall a b. (a -> b) -> a -> b
$ Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Newtype -> [Type]
ntConstraints Newtype
nt
                        Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> InferM (Maybe Type))
-> Maybe Type -> InferM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t
        _ -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing

    (TupleSel n :: Int
n _, ty :: Type
ty) ->
      case Type
ty of

        TCon (TC (TCTuple m :: Int
m)) ts :: [Type]
ts ->
          Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> InferM (Maybe Type))
-> Maybe Type -> InferM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (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)
                      Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [Type]
ts [Type] -> Int -> Type
forall a. [a] -> Int -> a
!! Int
n

        TCon (TC TCSeq) [len :: Type
len,el :: Type
el] -> Type -> Type -> InferM (Maybe Type)
liftSeq Type
len Type
el
        TCon (TC TCFun) [t1 :: Type
t1,t2 :: Type
t2]  -> Type -> Type -> InferM (Maybe Type)
liftFun Type
t1 Type
t2

        _ -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing


    (ListSel n :: Int
n _, TCon (TC TCSeq) [l :: Type
l,t :: Type
t])
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2 -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t)
      | Bool
otherwise ->
       do ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtSelector [ Type
l Type -> Type -> Type
>== Int -> Type
forall a. Integral a => a -> Type
tNum (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ]
          Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t)

    _ -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing

  where
  liftSeq :: Type -> Type -> InferM (Maybe Type)
liftSeq len :: Type
len el :: Type
el =
    do Maybe Type
mb <- Selector -> Type -> InferM (Maybe Type)
solveSelector Selector
sel (Type -> Type
tNoUser Type
el)
       Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> InferM (Maybe Type))
-> Maybe Type -> InferM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ do Type
el' <- Maybe Type
mb
                   Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCSeq) [Type
len,Type
el'])

  liftFun :: Type -> Type -> InferM (Maybe Type)
liftFun t1 :: Type
t1 t2 :: Type
t2 =
    do Maybe Type
mb <- Selector -> Type -> InferM (Maybe Type)
solveSelector Selector
sel (Type -> Type
tNoUser Type
t2)
       Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> InferM (Maybe Type))
-> Maybe Type -> InferM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ do Type
t2' <- Maybe Type
mb
                   Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (TCon -> [Type] -> Type
TCon (TC -> TCon
TC TC
TCFun) [Type
t1,Type
t2'])


-- | Solve has-constraints.
tryHasGoal :: HasGoal -> InferM (Bool, Bool) -- ^ changes, solved
tryHasGoal :: HasGoal -> InferM (Bool, Bool)
tryHasGoal has :: HasGoal
has
  | TCon (PC (PHas sel :: Selector
sel)) [ th :: Type
th, ft :: Type
ft ] <- Goal -> Type
goal (HasGoal -> Goal
hasGoal HasGoal
has) =
    do Bool
imped     <- Selector -> Type -> InferM Bool
improveSelector Selector
sel Type
th
       Type
outerT    <- Type -> Type
tNoUser (Type -> Type) -> InferM Type -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Type -> InferM Type
forall t. TVars t => t -> InferM t
applySubst Type
th
       Maybe Type
mbInnerT  <- Selector -> Type -> InferM (Maybe Type)
solveSelector Selector
sel Type
outerT
       case Maybe Type
mbInnerT of
         Nothing -> (Bool, Bool) -> InferM (Bool, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
imped, Bool
False)
         Just innerT :: Type
innerT ->
           do ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType ([Type] -> InferM ()) -> InferM [Type] -> InferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Type -> InferM [Type]
unify Type
innerT Type
ft
              Type
oT <- Type -> InferM Type
forall t. TVars t => t -> InferM t
applySubst Type
outerT
              Type
iT <- Type -> InferM Type
forall t. TVars t => t -> InferM t
applySubst Type
innerT
              HasGoalSln
sln <- Selector -> Type -> Type -> InferM HasGoalSln
mkSelSln Selector
sel Type
oT Type
iT
              Int -> HasGoalSln -> InferM ()
solveHasGoal (HasGoal -> Int
hasName HasGoal
has) HasGoalSln
sln
              (Bool, Bool) -> InferM (Bool, Bool)
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 "hasGoalSolved"
                  [ "Unexpected selector proposition:"
                  , Goal -> String
forall a. Show a => a -> String
show (HasGoal -> Goal
hasGoal HasGoal
has)
                  ]



{- | Generator an appropriate selector, once the "Has" constraint
has been discharged.  The resulting selectors should always work
on their corresponding types (i.e., tuple selectros only select from tuples).
This function generates the code for lifting tuple/record selectors to sequences
and functions.

Assumes types are zonked. -}
mkSelSln :: Selector -> Type -> Type -> InferM HasGoalSln
mkSelSln :: Selector -> Type -> Type -> InferM HasGoalSln
mkSelSln s :: Selector
s outerT :: Type
outerT innerT :: Type
innerT =
  case Type -> Type
tNoUser Type
outerT of
    TCon (TC TCSeq) [len :: Type
len,el :: Type
el]
      | TupleSel {} <- Selector
s  -> Type -> Type -> InferM HasGoalSln
liftSeq Type
len Type
el
      | RecordSel {} <- Selector
s -> Type -> Type -> InferM HasGoalSln
liftSeq Type
len Type
el

    TCon (TC TCFun) [t1 :: Type
t1,t2 :: Type
t2]
      | TupleSel {} <- Selector
s -> Type -> Type -> InferM HasGoalSln
liftFun Type
t1 Type
t2
      | RecordSel {} <- Selector
s -> Type -> Type -> InferM HasGoalSln
liftFun Type
t1 Type
t2

    _ -> HasGoalSln -> InferM HasGoalSln
forall (m :: * -> *) a. Monad m => a -> m a
return HasGoalSln :: (Expr -> Expr) -> (Expr -> Expr -> Expr) -> HasGoalSln
HasGoalSln { hasDoSelect :: Expr -> Expr
hasDoSelect = \e :: Expr
e -> Expr -> Selector -> Expr
ESel Expr
e Selector
s
                           , hasDoSet :: Expr -> Expr -> Expr
hasDoSet    = \e :: Expr
e v :: Expr
v -> Expr -> Selector -> Expr -> Expr
ESet Expr
e Selector
s Expr
v }

  where
  -- Has s a t => Has s ([n]a) ([n]t)
  -- xs.s             ~~> [ x.s           | x <- xs ]
  -- { xs | s = ys }  ~~> [ { x | s = y } | x <- xs | y <- ys ]
  liftSeq :: Type -> Type -> InferM HasGoalSln
liftSeq len :: Type
len el :: Type
el =
    do Name
x1 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "x")
       Name
x2 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "x")
       Name
y2 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "y")
       case Type -> Type
tNoUser Type
innerT of
         TCon _ [_,eli :: Type
eli] ->
           do HasGoalSln
d <- Selector -> Type -> Type -> InferM HasGoalSln
mkSelSln Selector
s Type
el Type
eli
              HasGoalSln -> InferM HasGoalSln
forall (f :: * -> *) a. Applicative f => a -> f a
pure HasGoalSln :: (Expr -> Expr) -> (Expr -> Expr -> Expr) -> HasGoalSln
HasGoalSln
                { hasDoSelect :: Expr -> Expr
hasDoSelect = \e :: Expr
e ->
                    Type -> Type -> Expr -> [[Match]] -> Expr
EComp Type
len Type
eli (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d (Name -> Expr
EVar Name
x1))
                                  [[ Name -> Type -> Type -> Expr -> Match
From Name
x1 Type
len Type
el Expr
e ]]
                , hasDoSet :: Expr -> Expr -> Expr
hasDoSet = \e :: Expr
e v :: Expr
v ->
                    Type -> Type -> Expr -> [[Match]] -> Expr
EComp Type
len Type
el  (HasGoalSln -> Expr -> Expr -> Expr
hasDoSet HasGoalSln
d (Name -> Expr
EVar Name
x2) (Name -> Expr
EVar Name
y2))
                                  [ [ Name -> Type -> Type -> Expr -> Match
From Name
x2 Type
len Type
el  Expr
e ]
                                  , [ Name -> Type -> Type -> Expr -> Match
From Name
y2 Type
len Type
eli Expr
v ]
                                  ]
                }


         _ -> String -> [String] -> InferM HasGoalSln
forall a. HasCallStack => String -> [String] -> a
panic "mkSelSln" [ "Unexpected inner seq type.", Type -> String
forall a. Show a => a -> String
show Type
innerT ]

  -- Has s b t => Has s (a -> b)
  -- f.s            ~~> \x -> (f x).s
  -- { f | s = g }  ~~> \x -> { f x | s = g x }
  liftFun :: Type -> Type -> InferM HasGoalSln
liftFun t1 :: Type
t1 t2 :: Type
t2 =
    do Name
x1 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "x")
       Name
x2 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent "x")
       case Type -> Type
tNoUser Type
innerT of
         TCon _ [_,inT :: Type
inT] ->
           do HasGoalSln
d <- Selector -> Type -> Type -> InferM HasGoalSln
mkSelSln Selector
s Type
t2 Type
inT
              HasGoalSln -> InferM HasGoalSln
forall (f :: * -> *) a. Applicative f => a -> f a
pure HasGoalSln :: (Expr -> Expr) -> (Expr -> Expr -> Expr) -> HasGoalSln
HasGoalSln
                { hasDoSelect :: Expr -> Expr
hasDoSelect = \e :: Expr
e ->
                    Name -> Type -> Expr -> Expr
EAbs Name
x1 Type
t1 (HasGoalSln -> Expr -> Expr
hasDoSelect HasGoalSln
d (Expr -> Expr -> Expr
EApp Expr
e (Name -> Expr
EVar Name
x1)))
                , hasDoSet :: Expr -> Expr -> Expr
hasDoSet = \e :: Expr
e v :: Expr
v ->
                    Name -> Type -> Expr -> Expr
EAbs Name
x2 Type
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))) }
         _ -> String -> [String] -> InferM HasGoalSln
forall a. HasCallStack => String -> [String] -> a
panic "mkSelSln" [ "Unexpected inner fun type", Type -> String
forall a. Show a => a -> String
show Type
innerT ]