-- |
-- Module      :  Cryptol.TypeCheck.Solver.Selector
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# 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)


{- | 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 -> 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'])


-- | Solve has-constraints.
tryHasGoal :: HasGoal -> InferM (Bool, Bool) -- ^ changes, solved
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)
                  ]



{- | 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 -> 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
  -- 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 :: 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 ]

  -- 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 :: 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 ]