module Language.Fixpoint.Types.Sorts (
Sort (..)
, Sub (..)
, FTycon, TCEmb
, sortFTycon
, intFTyCon, boolFTyCon, realFTyCon, numFTyCon
, intSort, realSort, boolSort, strSort, funcSort
, setSort, bitVecSort, mapSort
, listFTyCon
, isListTC
, fTyconSymbol, symbolFTycon, fTyconSort
, fApp, fApp', fAppTC
, fObj
, sortSubst
, functionSort
, mkFFunc
, bkFFunc
) where
import qualified Data.Binary as B
import Data.Generics (Data)
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Data.Hashable
import Data.List (foldl')
import Control.DeepSeq
import Data.Maybe (fromMaybe)
import Language.Fixpoint.Types.Names
import Language.Fixpoint.Types.PrettyPrint
import Language.Fixpoint.Types.Spans
import Language.Fixpoint.Misc
import Text.PrettyPrint.HughesPJ
import qualified Data.HashMap.Strict as M
newtype FTycon = TC LocSymbol deriving (Eq, Ord, Show, Data, Typeable, Generic)
type TCEmb a = M.HashMap a FTycon
intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon, strFTyCon, listFTyCon :: FTycon
intFTyCon = TC $ dummyLoc "int"
boolFTyCon = TC $ dummyLoc "bool"
realFTyCon = TC $ dummyLoc "real"
numFTyCon = TC $ dummyLoc "num"
funcFTyCon = TC $ dummyLoc "function"
strFTyCon = TC $ dummyLoc strConName
listFTyCon = TC $ dummyLoc listConName
isListConName :: LocSymbol -> Bool
isListConName x = c == listConName || c == listLConName --"List"
where
c = val x
isListTC :: FTycon -> Bool
isListTC (TC z) = isListConName z
fTyconSymbol :: FTycon -> Located Symbol
fTyconSymbol (TC s) = s
symbolFTycon :: LocSymbol -> FTycon
symbolFTycon c
| isListConName c
= TC $ fmap (const listConName) c
| otherwise
= TC c
fApp :: Sort -> [Sort] -> Sort
fApp = foldl' FApp
fAppTC :: FTycon -> [Sort] -> Sort
fAppTC = fApp . fTyconSort
fApp' :: Sort -> ListNE Sort
fApp' = go []
where
go acc (FApp t1 t2) = go (t2 : acc) t1
go acc t = t : acc
fObj :: LocSymbol -> Sort
fObj = fTyconSort . TC
sortFTycon :: Sort -> Maybe FTycon
sortFTycon FInt = Just intFTyCon
sortFTycon FReal = Just realFTyCon
sortFTycon FNum = Just numFTyCon
sortFTycon (FTC c) = Just c
sortFTycon _ = Nothing
functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
functionSort s
| null is && null ss
= Nothing
| otherwise
= Just (is, ss, r)
where
(is, ss, r) = go [] [] s
go vs ss (FAbs i t) = go (i:vs) ss t
go vs ss (FFunc s1 s2) = go vs (s1:ss) s2
go vs ss t = (reverse vs, reverse ss, t)
data Sort = FInt
| FReal
| FNum
| FFrac
| FObj Symbol
| FVar !Int
| FFunc !Sort !Sort
| FAbs !Int !Sort
| FTC FTycon
| FApp Sort Sort
deriving (Eq, Ord, Show, Data, Typeable, Generic)
mkFFunc :: Int -> [Sort] -> Sort
mkFFunc i ss = go [0..i1] ss
where
go [] [s] = s
go [] (s:ss) = FFunc s $ go [] ss
go (i:is) ss = FAbs i $ go is ss
go _ _ = error "cannot happen"
bkFFunc :: Sort -> Maybe (Int, [Sort])
bkFFunc t = (maximum (0 : as),) <$> bkFun t'
where
(as, t') = bkAbs t
bkAbs :: Sort -> ([Int], Sort)
bkAbs (FAbs i t) = (i:is, t') where (is, t') = bkAbs t
bkAbs t = ([], t)
bkFun :: Sort -> Maybe [Sort]
bkFun z@(FFunc _ _) = Just (go z)
where
go (FFunc t1 t2) = t1 : go t2
go t = [t]
bkFun _ = Nothing
instance Hashable FTycon where
hashWithSalt i (TC s) = hashWithSalt i s
instance Hashable Sort
newtype Sub = Sub [(Int, Sort)] deriving (Generic)
instance Fixpoint Sort where
toFix = toFixSort
toFixSort :: Sort -> Doc
toFixSort (FVar i) = text "@" <> parens (toFix i)
toFixSort FInt = text "int"
toFixSort FReal = text "real"
toFixSort FFrac = text "frac"
toFixSort (FObj x) = toFix x
toFixSort FNum = text "num"
toFixSort t@(FAbs _ _) = toFixAbsApp t
toFixSort t@(FFunc _ _)= toFixAbsApp t
toFixSort (FTC c) = toFix c
toFixSort t@(FApp _ _) = toFixFApp (fApp' t)
toFixAbsApp t = text "func" <> parens (toFix n <> text ", " <> toFix ts)
where
Just (vs, ss, s) = functionSort t
n = length vs
ts = ss ++ [s]
toFixFApp :: ListNE Sort -> Doc
toFixFApp [t] = toFixSort t
toFixFApp [FTC c, t]
| isListTC c = brackets $ toFixSort t
toFixFApp ts = parens $ intersperse space (toFixSort <$> ts)
instance Fixpoint FTycon where
toFix (TC s) = toFix s
boolSort, intSort, realSort, strSort, funcSort :: Sort
boolSort = fTyconSort boolFTyCon
strSort = fTyconSort strFTyCon
intSort = fTyconSort intFTyCon
realSort = fTyconSort realFTyCon
funcSort = fTyconSort funcFTyCon
bitVecSort :: Sort
mapSort :: Sort -> Sort -> Sort
setSort :: Sort -> Sort
setSort = FApp (FTC $ symbolFTycon' "Set_Set")
bitVecSort = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' size32Name)
mapSort k v = FApp (FApp (FTC $ symbolFTycon' "Map_t") k) v
symbolFTycon' = symbolFTycon . dummyLoc
fTyconSort :: FTycon -> Sort
fTyconSort c
| c == intFTyCon = FInt
| c == realFTyCon = FReal
| c == numFTyCon = FNum
| otherwise = FTC c
sortSubst :: M.HashMap Symbol Sort -> Sort -> Sort
sortSubst θ t@(FObj x) = fromMaybe t (M.lookup x θ)
sortSubst θ (FFunc t1 t2) = FFunc (sortSubst θ t1) (sortSubst θ t2)
sortSubst θ (FApp t1 t2) = FApp (sortSubst θ t1) (sortSubst θ t2)
sortSubst θ (FAbs i t) = FAbs i (sortSubst θ t)
sortSubst _ t = t
instance B.Binary FTycon
instance B.Binary Sort
instance B.Binary Sub
instance NFData FTycon
instance NFData Sort
instance NFData Sub
instance Monoid Sort where
mempty = FObj "any"
mappend t1 t2
| t1 == mempty = t2
| t2 == mempty = t1
| t1 == t2 = t1
| otherwise = errorstar $ "mappend-sort: conflicting sorts t1 =" ++ show t1 ++ " t2 = " ++ show t2