-- |
-- 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
                              , newType, applySubst, solveHasGoal
                              , newParamName
                              )
import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
import Cryptol.Utils.Ident (Ident, packIdent)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap

import Control.Monad(forM,guard)


recordType :: [Ident] -> InferM Type
recordType :: [Ident] -> InferM Type
recordType [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
$ \Ident
l ->
        do Type
t <- TypeSource -> Kind -> InferM Type
newType (Ident -> TypeSource
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 (RecordMap Ident Type -> Type
TRec ([(Ident, Type)] -> RecordMap Ident Type
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [(Ident, Type)]
fields))

tupleType :: Int -> InferM Type
tupleType :: Int -> InferM Type
tupleType 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 (\Int
x -> TypeSource -> Kind -> InferM Type
newType (Int -> TypeSource
TypeOfTupleField Int
x) Kind
KType)
                    [ Int
0 .. (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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 Int
n =
  do Type
elems <- TypeSource -> Kind -> InferM Type
newType TypeSource
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 Selector
sel Type
outerT =
  case Selector
sel of
    RecordSel Ident
_ 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  Int
_ 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   Int
_ 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 t -> InferM Type
_ Maybe t
Nothing   = Bool -> InferM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  cvt t -> InferM Type
f (Just t
a)  = do Type
ty <- t -> InferM Type
f t
a
                       [Type]
ps <- TypeWithSource -> Type -> InferM [Type]
unify (Type -> TypeSource -> TypeWithSource
WithSource Type
outerT (Selector -> TypeSource
selSrc Selector
sel)) Type
ty
                       ConstraintSource -> [Type] -> InferM ()
newGoals ConstraintSource
CtExactType [Type]
ps
                       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 Selector
sel Type
outerT =
  case (Selector
sel, Type
outerT) of

    (RecordSel Ident
l Maybe [Ident]
_, Type
ty) ->
      case Type
ty of
        TRec RecordMap Ident Type
fs -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> RecordMap Ident Type -> Maybe Type
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
l RecordMap Ident Type
fs)
        TNewtype Newtype
nt [Type]
ts ->
          case Ident -> RecordMap Ident Type -> Maybe Type
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
l (Newtype -> RecordMap Ident Type
ntFields Newtype
nt) of
            Maybe Type
Nothing -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
            Just 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 (Newtype -> Name
ntName Newtype
nt))
                   ([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

        TCon (TC TC
TCSeq) [Type
len,Type
el] -> Type -> Type -> InferM (Maybe Type)
liftSeq Type
len Type
el
        TCon (TC TC
TCFun) [Type
t1,Type
t2]  -> Type -> Type -> InferM (Maybe Type)
liftFun Type
t1 Type
t2
        Type
_ -> Maybe Type -> InferM (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing

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

        TCon (TC (TCTuple Int
m)) [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 (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)
                      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 TC
TCSeq) [Type
len,Type
el] -> Type -> Type -> InferM (Maybe Type)
liftSeq Type
len Type
el
        TCon (TC TC
TCFun) [Type
t1,Type
t2]  -> Type -> Type -> InferM (Maybe Type)
liftFun Type
t1 Type
t2

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


    (ListSel Int
n Maybe Int
_, TCon (TC TC
TCSeq) [Type
l,Type
t])
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
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
- Int
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)

    (Selector, Type)
_ -> 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 Type
len 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 Type
t1 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 HasGoal
has
  | TCon (PC (PHas Selector
sel)) [ Type
th, 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
         Maybe Type
Nothing -> (Bool, Bool) -> InferM (Bool, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
imped, Bool
False)
         Just 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
=<< TypeWithSource -> Type -> InferM [Type]
unify (Type -> TypeSource -> TypeWithSource
WithSource Type
innerT (Selector -> TypeSource
selSrc Selector
sel)) 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 String
"hasGoalSolved"
                  [ String
"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 Selector
s Type
outerT Type
innerT =
  case Type -> Type
tNoUser Type
outerT of
    TCon (TC TC
TCSeq) [Type
len,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 TC
TCFun) [Type
t1,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

    Type
_ -> HasGoalSln -> InferM HasGoalSln
forall (m :: * -> *) a. Monad m => a -> m a
return HasGoalSln :: (Expr -> Expr) -> (Expr -> Expr -> Expr) -> HasGoalSln
HasGoalSln { hasDoSelect :: Expr -> Expr
hasDoSelect = \Expr
e -> Expr -> Selector -> Expr
ESel Expr
e Selector
s
                           , hasDoSet :: Expr -> Expr -> Expr
hasDoSet    = \Expr
e Expr
v -> Type -> Expr -> Selector -> Expr -> Expr
ESet Type
outerT 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 Type
len Type
el =
    do Name
x1 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent String
"x")
       Name
x2 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent String
"x")
       Name
y2 <- Ident -> InferM Name
newParamName (String -> Ident
packIdent String
"y")
       case Type -> Type
tNoUser Type
innerT of
         TCon TCon
_ [Type
_,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 = \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 = \Expr
e 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 ]
                                  ]
                }


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

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