{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE DeriveFunctor             #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE UndecidableInstances      #-}

-- | Module pertaining to Refinement Type descriptions and conversions
--   Likely mergeable with @Language.Rsc.Typecheck.Types@

module Language.Rsc.Liquid.Refinements (

  -- * Manipulating RefType
    rTypeReft
  , rTypeSort
  , rTypeSortedReft
  , rTypeValueVar

  ) where

import qualified Data.HashMap.Strict             as HM
import qualified Language.Fixpoint.Smt.Bitvector as BV
import qualified Language.Fixpoint.Types         as F
import           Language.Rsc.Names
import           Language.Rsc.Typecheck.Types
import           Language.Rsc.Types


--------------------------------------------------------------------------------
rTypeSortedReft   :: F.Reftable r => RTypeQ q r -> F.SortedReft
rTypeReft         :: F.Reftable r => RTypeQ q r -> F.Reft
rTypeValueVar     :: F.Reftable r => RTypeQ q r -> F.Symbol
--------------------------------------------------------------------------------
rTypeSortedReft t = F.RR (rTypeSort t) (rTypeReft t)
rTypeReft         = maybe fTop F.toReft . stripRTypeBase
rTypeValueVar t   = vv where F.Reft (vv,_) = rTypeReft t

--------------------------------------------------------------------------------
stripRTypeBase :: RTypeQ q r -> Maybe r
--------------------------------------------------------------------------------
stripRTypeBase (TPrim _ r)  = Just r
stripRTypeBase (TRef _ r)   = Just r
stripRTypeBase (TVar _ r)   = Just r
stripRTypeBase (TFun _ _ r) = Just r
stripRTypeBase (TObj _ _ r) = Just r
stripRTypeBase (TOr _ r)    = Just r
stripRTypeBase _            = Nothing



-- Avoid incluging mutability of `TRef` - it crashes FP
--------------------------------------------------------------------------------
rTypeSort :: F.Reftable r => RTypeQ q r -> F.Sort
--------------------------------------------------------------------------------
rTypeSort (TVar α _)              = F.FObj $ F.symbol α
rTypeSort (TAll v t)              = rTypeSortForAll $ TAll v t
rTypeSort (TFun xts t _)          = F.mkFFunc 0 $ rTypeSort <$> (b_type <$> xts) ++ [t]
rTypeSort (TPrim c _)             = rTypeSortPrim c
rTypeSort (TOr _ _)               = F.fAppTC (rawStringFTycon unionSym ) []
rTypeSort (TAnd _)                = F.fAppTC (rawStringFTycon intersSym) []
rTypeSort (TRef (Gen n (_:ts)) _) = F.fAppTC (rawSymbolFTycon (F.symbol n)) (rTypeSort <$> ts)
rTypeSort (TRef (Gen n []    ) _) = F.fAppTC (rawSymbolFTycon (F.symbol n)) []
rTypeSort  TObj{}                 = F.fAppTC (rawStringFTycon objectSym) []
rTypeSort  TClass{}               = F.fAppTC (rawStringFTycon classSym ) []
rTypeSort  TMod{}                 = F.fAppTC (rawStringFTycon moduleSym) []
rTypeSort _                       = error "BUG: Unsupported in rTypeSort"


rTypeSortForAll t        = genSort n θ $ rTypeSort tbody
  where
    (αs, tbody)          = bkAll t
    n                    = length αs
    θ                    = HM.fromList $ zip (F.symbol <$> αs) (F.FVar <$> [0..])



rTypeSortPrim TBV32      = BV.mkSort BV.S32
rTypeSortPrim TNumber    = F.intSort
rTypeSortPrim TReal      = F.realSort
rTypeSortPrim TString    = F.strSort
rTypeSortPrim TBoolean   = F.fAppTC (rawStringFTycon boolSym ) []
rTypeSortPrim TVoid      = F.fAppTC (rawStringFTycon voidSym ) []
rTypeSortPrim TTop       = F.fAppTC (rawStringFTycon topSym  ) []
rTypeSortPrim TBot       = F.fAppTC (rawStringFTycon botSym  ) []
rTypeSortPrim TAny       = F.fAppTC (rawStringFTycon anySym  ) []
rTypeSortPrim TNull      = F.fAppTC (rawStringFTycon nullSym ) []
rTypeSortPrim TUndefined = F.fAppTC (rawStringFTycon undefSym) []
rTypeSortPrim TFPBool    = F.boolSort
rTypeSortPrim c          = error $ "impossible: rTypeSortPrim " ++ show c

genSort n θ t = case F.bkFFunc t of
                 Just (_, ts) -> F.mkFFunc n (F.sortSubst θ <$> ts)
                 Nothing      -> F.mkFFunc n [F.sortSubst θ t]

rawStringFTycon = F.symbolFTycon
                . F.locAt "RSC.Types.rawStringFTycon"
                . F.symbol


rawSymbolFTycon :: F.Symbol -> F.FTycon
rawSymbolFTycon = F.symbolFTycon
                . F.locAt "RSC.Types.rawStringFTycon"

