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