module Language.Haskell.Liquid.Constraint.ToFixpoint (
cgInfoFInfo
) where
import Prelude hiding (error)
import qualified Language.Fixpoint.Types as F
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Types hiding ( binds )
import Language.Fixpoint.Solver ( parseFInfo )
import Data.Monoid
import Language.Haskell.Liquid.Constraint.Qualifier
cgInfoFInfo :: GhcInfo -> CGInfo -> FilePath -> IO (F.FInfo Cinfo)
cgInfoFInfo info cgi fi = do
let tgtFI = targetFInfo info cgi fi
impFI <- parseFInfo $ hqFiles info
return $ tgtFI <> impFI
targetFInfo :: GhcInfo -> CGInfo -> FilePath -> F.FInfo Cinfo
targetFInfo info cgi fn = F.fi cs ws bs ls ks qs bi fn aHO
where
cs = fixCs cgi
ws = fixWfs cgi
bs = binds cgi
ls = fEnv cgi
ks = kuts cgi
qs = targetQuals info cgi
bi = (`Ci` Nothing) <$> bindSpans cgi
aHO = allowHO cgi
targetQuals :: GhcInfo -> CGInfo -> [F.Qualifier]
targetQuals info cgi = spcQs ++ genQs
where
spcQs = qualifiers spc
genQs = specificationQualifiers n info (fEnv cgi)
n = maxParams $ config spc
spc = spec info