-- |
-- 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 <- [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)


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


-- | 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 = 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)
                  ]



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

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