-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

module Cryptol.TypeCheck.Instantiate (instantiateWith) where

import Cryptol.ModuleSystem.Name (nameIdent)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Subst (listSubst,apSubst)
import Cryptol.Parser.Position (Located(..))
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.PP

import Data.Function (on)
import Data.List(sortBy, groupBy, find)
import Data.Maybe(mapMaybe,isJust)
import Data.Either(partitionEithers)
import MonadLib


instantiateWith :: Expr -> Schema -> [Located (Maybe Ident,Type)]
                -> InferM (Expr,Type)
instantiateWith e s ts
  | null named      = instantiateWithPos e s positional
  | null positional = instantiateWithNames e s named
  | otherwise       = do recordError CannotMixPositionalAndNamedTypeParams
                         instantiateWithNames e s named

  where
  (named,positional) = partitionEithers (map classify ts)
  classify t = case thing t of
                 (Just n,ty)  -> Left t { thing = (n,ty) }
                 (Nothing,ty) -> Right ty


instantiateWithPos :: Expr -> Schema -> [Type] -> InferM (Expr,Type)
instantiateWithPos e (Forall as ps t) ts =
  do su <- makeSu (1::Int) [] as ts
     doInst su e ps t
  where
  isNamed q = isJust (tpName q)

  makeSu n su (q : qs) (ty : tys)
    | not (isNamed q) = do r <- unnamed n q
                           makeSu (n+1) (r : su) qs (ty : tys)
    | k1 == k2        = makeSu (n+1) ((tpVar q, ty) : su) qs tys
    | otherwise       = do recordError $ KindMismatch k1 k2
                           r <- unnamed n q
                           makeSu (n+1) (r : su) qs tys
      where k1 = kindOf q
            k2 = kindOf ty

  makeSu _ su [] []       = return (reverse su)
  makeSu n su (q : qs) [] = do r <- unnamed n q
                               makeSu (n+1) (r : su) qs []
  makeSu _ su [] _        = do recordError TooManyPositionalTypeParams
                               return (reverse su)

  unnamed n q = do r <- curRange
                   let src = ordinal n <+> text "type parameter"
                           $$ text "of" <+> ppUse e
                           $$ text "at" <+> pp r
                   ty <- newType src (kindOf q)
                   return (tpVar q, ty)




{- | Instantiate an expression of the given polymorphic type.
The arguments that are provided will be instantiated as requested,
the rest will be instantiated with fresh type variables.

Note that we assume that type parameters are not normalized.
Generally, the resulting expression will look something like this:

ECast (EProofApp (ETApp e t)) t1

  where
  - There will be one `ETApp t` for each insantiated type parameter;
  - there will be one `EProofApp` for each constraint on the schema;
  - there will be `ECast` if we had equality constraints from normalization.
-}
instantiateWithNames :: Expr -> Schema -> [Located (Ident,Type)]
                     -> InferM (Expr,Type)
instantiateWithNames e (Forall as ps t) xs =
  do sequence_ repeatedParams
     sequence_ undefParams
     su' <- mapM paramInst as
     doInst su' e ps t
  where
  -- Choose the type for type parameter `x`
  paramInst x     =
    do let v = tpVar x
           k = kindOf v

           -- We just use nameIdent for comparison here, as all parameter names
           -- should have a NameInfo of Parameter.
           lkp name = find (\th -> fst (thing th) == nameIdent name) xs
           src r = text "type parameter" <+> (case tpName x of
                                               Just n -> quotes (pp n)
                                               Nothing -> empty)
                                        $$ text "of" <+> ppUse e
                                        $$ text "at" <+> pp r
       ty <- case lkp =<< tpName x of
               Just lty
                 | k1 == k   -> return ty
                 | otherwise -> do let r = srcRange lty
                                   inRange r $ recordError (KindMismatch k k1)
                                   newType (src r) k
                  where ty = snd (thing lty)
                        k1 = kindOf ty
               Nothing -> do r <- curRange
                             newType (src r) k
       return (v,ty)

  -- Errors from multiple values for the same parameter.
  repeatedParams  = mapMaybe isRepeated
                  $ groupBy ((==) `on` pName)
                  $ sortBy (compare `on` pName) xs

  isRepeated ys@(a : _ : _)  = Just $ recordError
                                    $ MultipleTypeParamDefs (fst (thing a))
                                                            (map srcRange ys)
  isRepeated _               = Nothing


  paramIdents = [ nameIdent n | Just n <- map tpName as ]

  -- Errors from parameters that are defined, but do not exist in the schema.
  undefParams     = do x <- xs
                       let name = pName x
                       guard (name `notElem` paramIdents)
                       return $ inRange (srcRange x)
                              $ recordError
                              $ UndefinedTypeParam x { thing = name }

  pName = fst . thing





doInst :: [(TVar, Type)] -> Expr -> [Prop] -> Type -> InferM (Expr,Type)
doInst su' e ps t =
  do let su = listSubst su'
     newGoals (CtInst e) (map (apSubst su) ps)
     let t1 = apSubst su t
     return ( addProofParams
            $ addTyParams (map snd su') e
            , t1)
  where
  -- Add type parameters
  addTyParams ts e1 = foldl ETApp e1 ts

  -- Add proof parameters (the proofs are ommited but we mark where they'd go)
  addProofParams e1 = foldl (\e2 _ -> EProofApp e2) e1 ps