content: {-# LANGUAGE BlockArguments  #-}
  {-# LANGUAGE RecordWildCards #-}
  {-# LANGUAGE ViewPatterns    #-}
  {-# LANGUAGE Safe    #-}
  
  -- | Checking and conversion of 'Type's to 'FFIType's.
  module Cryptol.TypeCheck.FFI
    ( toFFIFunType
    ) where
  
  import  Data.Bifunctor
  import  Data.Containers.ListUtils
  import  Data.Either
  
  import Cryptol.Utils.Panic(panic)
  import Cryptol.Parser.AST(ForeignMode(..))
  import Cryptol.TypeCheck.FFI.Error
  import Cryptol.TypeCheck.FFI.FFIType
  import Cryptol.TypeCheck.SimpType
  import Cryptol.TypeCheck.Type
  import Cryptol.TypeCheck.AST(FFI(..))
  import Cryptol.TypeCheck.Subst
  import Cryptol.Utils.RecordMap
  import Cryptol.Utils.Types
  
  
  -- | Convert a 'Schema' to a 'FFIFunType', along with any 'Prop's that must be
  -- satisfied for the 'FFIFunType' to be valid.
  toFFIFunType :: ForeignMode -> Schema -> Either FFITypeError ([Prop], FFI)
  toFFIFunType how (Forall params _ t) =
  
    case how of
      ForeignAbstract -> checkForeignAbstract params t
      ForeignC ->
         -- Remove all type synonyms and simplify the type before processing it
         case go $ tRebuild' False t of
           Just (Right (props, fft)) -> Right
             -- Remove duplicate constraints
             (nubOrd $ map (fin . TVar . TVBound) params ++ props, CallC fft)
           Just (Left errs) -> Left $ FFITypeError t $ FFIBadComponentTypes errs
           Nothing -> Left $ FFITypeError t FFINotFunction
    where go (TCon (TC TCFun) [argType, retType]) = Just
            case toFFIType argType of
              Right (ps, ffiArgType) ->
                case go retType of
                  Just (Right (ps', ffiFunType)) -> Right
                    ( ps ++ ps'
                    , ffiFunType
                        { ffiArgTypes = ffiArgType : ffiArgTypes ffiFunType } )
                  Just (Left errs) -> Left errs
                  Nothing ->
                    case toFFIType retType of
                      Right (ps', ffiRetType) -> Right
                        ( ps ++ ps'
                        , FFIFunType
                            { ffiTParams = params
                            , ffiArgTypes = [ffiArgType], .. } )
                      Left err -> Left [err]
              Left err -> Left
                case go retType of
                  Just (Right _) -> [err]
                  Just (Left errs) -> err : errs
                  Nothing ->
                    case toFFIType retType of
                      Right _   -> [err]
                      Left err' -> [err, err']
          go _ = Nothing
  
  -- | Convert a 'Type' to a 'FFIType', along with any 'Prop's that must be
  -- satisfied for the 'FFIType' to be valid.
  toFFIType :: Type -> Either FFITypeError ([Prop], FFIType)
  toFFIType t =
    case t of
      TCon (TC TCBit) [] -> Right ([], FFIBool)
      (toFFIBasicType -> Just r) -> (\fbt -> ([], FFIBasic fbt)) <$> r
      TCon (TC TCSeq) _ ->
        (\(szs, fbt) -> (map fin szs, FFIArray szs fbt)) <$> go t
        where go (toFFIBasicType -> Just r) =
                case r of
                  Right fbt -> Right ([], fbt)
                  Left err  -> Left $ FFITypeError t $ FFIBadComponentTypes [err]
              go (TCon (TC TCSeq) [sz, ty]) = first (sz:) <$> go ty
              go _ = Left $ FFITypeError t FFIBadArrayType
      TCon (TC (TCTuple _)) ts ->
        case partitionEithers $ map toFFIType ts of
          ([], unzip -> (pss, fts)) -> Right (concat pss, FFITuple fts)
          (errs, _) -> Left $ FFITypeError t $ FFIBadComponentTypes errs
      TRec tMap ->
        case sequence resMap of
          Right resMap' -> Right $ FFIRecord <$>
            recordMapAccum (\ps (ps', ft) -> (ps' ++ ps, ft)) [] resMap'
          Left _ -> Left $ FFITypeError t $
            FFIBadComponentTypes $ lefts $ displayElements resMap
        where resMap = fmap toFFIType tMap
      _ -> Left $ FFITypeError t FFIBadType
  
  -- | Convert a 'Type' to a 'FFIBasicType', returning 'Nothing' if it isn't a
  -- basic type and 'Left' if it is but there was some other issue with it.
  toFFIBasicType :: Type -> Maybe (Either FFITypeError FFIBasicType)
  toFFIBasicType t =
    case t of
      TCon (TC TCSeq) [TCon (TC (TCNum n)) [], TCon (TC TCBit) []]
        | n <= 8 -> word FFIWord8
        | n <= 16 -> word FFIWord16
        | n <= 32 -> word FFIWord32
        | n <= 64 -> word FFIWord64
        | otherwise -> Just $ Left $ FFITypeError t FFIBadWordSize
        where word = Just . Right . FFIBasicVal . FFIWord n
      TCon (TC TCFloat) [TCon (TC (TCNum e)) [], TCon (TC (TCNum p)) []]
        | (e, p) == float32ExpPrec -> float FFIFloat32
        | (e, p) == float64ExpPrec -> float FFIFloat64
        | otherwise -> Just $ Left $ FFITypeError t FFIBadFloatSize
        where float = Just . Right . FFIBasicVal . FFIFloat e p
      TCon (TC TCInteger) [] -> integer Nothing
      TCon (TC TCIntMod) [n] -> integer $ Just n
      TCon (TC TCRational) [] -> Just $ Right $ FFIBasicRef FFIRational
      _ -> Nothing
    where integer = Just . Right . FFIBasicRef . FFIInteger
  
  fin :: Type -> Prop
  fin t = TCon (PC PFin) [t]
  
  
  -- XXX: eliminate stuff we know will not work at runtime
  checkForeignAbstract :: [TParam] -> Type -> Either FFITypeError ([Prop], FFI)
  checkForeignAbstract params t =
    do fromArgs <- validForeignAbstractTypes args
       fromRes <- validForeignAbstractType res
       pure ( fromRes ++ fromArgs
            , CallAbstract
                FFIFunType { ffiTParams = params
                           , ffiArgTypes = args
                           , ffiRetType = res }
            )
    where
    (args,res) = go t
    go ty =
      case tIsFun ty of
        Just (a,r) ->
          let (bs,r1) = go r
          in (a:bs,r1)
        Nothing -> ([],ty)
  
  
  
  validForeignAbstractTypes ::
   Traversable t => t Type -> Either FFITypeError [Prop]
  validForeignAbstractTypes ts = concat <$> traverse validForeignAbstractType ts
  
  validForeignAbstractType :: Type -> Either FFITypeError [Prop]
  validForeignAbstractType t =
    let nope = Left . FFITypeError t
    in
    case t of
      TCon c ts ->
        case c of
          PC {} -> bad "PC"
          TF {} -> bad "TF"
          TError {} -> bad "TError"
          TC tc ->
           case tc of
             TCNum {} -> bad "TCNum"
             TCInf {} -> bad "TCInf"
             TCBit    -> pure []   
             TCInteger -> pure [] 
             TCFloat ->
               case ts of
                 [e',p'] ->
                   case (tIsNum e', tIsNum p') of
                     (Just e, Just p)
                       | (e, p) == float32ExpPrec -> pure []
                       | (e, p) == float64ExpPrec -> pure []
                     _ -> nope FFIBadFloatSize
                 _ -> bad "TCFloat"
             TCIntMod -> pure []
             TCRational -> pure []    
             TCArray -> nope FFIBadType
             TCSeq ->
               case ts of
                 [len,el] ->
                    do ps <- validForeignAbstractType el
                       let prop = pFin len
                       case tIsError prop of
                         Just err -> pure (err : ps)
                         Nothing -> pure (prop : ps)
                 _ -> bad "TCSeq"
             TCFun -> nope FFIBadType
             TCTuple {} -> validForeignAbstractTypes ts
             
      TVar {} -> nope FFIBadType
      TUser _ _ t1 -> validForeignAbstractType t1
      TRec rs -> validForeignAbstractTypes rs
      TNominal nm ts ->
        let su = listParamSubst (ntParams nm `zip` ts) in
        validForeignAbstractNominalType t su (ntDef nm)
    where
    bad msg = panic "validOfreignAbstactType" [msg]
  
  validForeignAbstractNominalType ::
    Type -> Subst -> NominalTypeDef -> Either FFITypeError[Prop]
  validForeignAbstractNominalType ty su def =
    case def of
      Struct sc -> concat <$> traverse validT (recordElements (ntFields sc))
      Enum cs -> concat <$> traverse validCon cs
      Abstract -> Left (FFITypeError ty FFIBadType)
    where
    validT t = validForeignAbstractType (apSubst su t)
    validCon c = concat <$> traverse validT (ecFields c)