liquidhaskell-0.1: Language/Haskell/Liquid/CmdLine.hs
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE BangPatterns #-}
-- | This module contains all the code needed to output the result which
-- is either: `SAFE` or `WARNING` with some reasonable error message when
-- something goes wrong. All forms of errors/exceptions should go through
-- here. The idea should be to report the error, the source position that
-- causes it, generate a suitable .json file and then exit.
module Language.Haskell.Liquid.CmdLine (
-- * Get Command Line Configuration
getOpts
-- * Update Configuration With Pragma
, withPragmas
-- * Exit Function
, exitWithResult
-- * Extra Outputs
, Output (..)
) where
import Control.DeepSeq
import Control.Monad
import Control.Applicative ((<$>))
import Data.List (foldl')
import Data.Maybe
import Data.Monoid
import qualified Data.HashMap.Strict as M
import System.FilePath (dropFileName)
import System.Environment (withArgs)
import System.Console.CmdArgs hiding (Loud)
import System.Console.CmdArgs.Verbosity (whenLoud)
import Language.Fixpoint.Misc
import Language.Fixpoint.Files
import Language.Fixpoint.Names (dropModuleNames)
import Language.Fixpoint.Types hiding (config)
import Language.Fixpoint.Config hiding (config, Config)
import Language.Haskell.Liquid.Annotate
import Language.Haskell.Liquid.Misc
import Language.Haskell.Liquid.PrettyPrint
import Language.Haskell.Liquid.Types hiding (config, typ)
import Name
import SrcLoc (SrcSpan)
import Text.PrettyPrint.HughesPJ
---------------------------------------------------------------------------------
-- Parsing Command Line----------------------------------------------------------
---------------------------------------------------------------------------------
config = Config {
files
= def &= typ "TARGET"
&= args
&= typFile
, idirs
= def &= typDir
&= help "Paths to Spec Include Directory "
, diffcheck
= def
&= help "Incremental Checking: only check changed binders"
, binders
= def &= help "Check a specific set of binders"
, nofalse
= def &= help "Remove false predicates from the refinements"
, noPrune
= def &= help "Disable prunning unsorted Predicates"
&= name "no-prune-unsorted"
, notermination
= def &= help "Disable Termination Check"
&= name "no-termination-check"
, totality
= def &= help "Check totality"
, smtsolver
= def &= help "Name of SMT-Solver"
, noCheckUnknown
= def &= explicit
&= name "no-check-unknown"
&= help "Don't complain about specifications for unexported and unused values "
, maxParams
= 2 &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)"
-- , verbose
-- = def &= help "Generate Verbose Output"
-- &= name "verbose-output"
} &= verbosity
&= program "liquid"
&= help "Refinement Types for Haskell"
&= summary copyright
&= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell"
, ""
, "To check a Haskell file foo.hs, type:"
, " liquid foo.hs "
]
getOpts :: IO Config
getOpts = do md <- cmdArgs config
putStrLn $ copyright
whenLoud $ putStrLn $ "liquid " ++ show args ++ "\n"
mkOpts md
copyright = "LiquidHaskell © Copyright 2009-13 Regents of the University of California. All Rights Reserved.\n"
mkOpts :: Config -> IO Config
mkOpts md
= do files' <- sortNub . concat <$> mapM getHsTargets (files md)
idirs' <- if null (idirs md) then single <$> getIncludeDir else return (idirs md)
return $ md { files = files' } { idirs = map dropFileName files' ++ idirs' }
-- tests fail if you flip order of idirs'
---------------------------------------------------------------------------------------
-- | Updating options
---------------------------------------------------------------------------------------
---------------------------------------------------------------------------------------
withPragmas :: Config -> [Located String] -> IO Config
---------------------------------------------------------------------------------------
withPragmas = foldM withPragma
withPragma :: Config -> Located String -> IO Config
withPragma c s = (c `mappend`) <$> parsePragma s
parsePragma :: Located String -> IO Config
parsePragma s = withArgs [val s] $ cmdArgs config
---------------------------------------------------------------------------------------
-- | Monoid instances for updating options
---------------------------------------------------------------------------------------
instance Monoid Config where
mempty = Config def def def def def def def def def 2 def
mappend c1 c2 = Config (sortNub $ files c1 ++ files c2)
(sortNub $ idirs c1 ++ idirs c2)
(diffcheck c1 || diffcheck c2)
(sortNub $ binders c1 ++ binders c2)
(noCheckUnknown c1 || noCheckUnknown c2)
(nofalse c1 || nofalse c2)
(notermination c1 || notermination c2)
(totality c1 || totality c2)
(noPrune c1 || noPrune c2)
(maxParams c1 `max` maxParams c2)
(smtsolver c1 `mappend` smtsolver c2)
instance Monoid SMTSolver where
mempty = def
mappend s1 s2
| s1 == s2 = s1
| s2 == def = s1
| otherwise = s2
------------------------------------------------------------------------
-- | Exit Function -----------------------------------------------------
------------------------------------------------------------------------
exitWithResult :: FilePath -> Maybe Output -> ErrorResult -> IO ErrorResult
exitWithResult target o r = writeExit target r $ fromMaybe emptyOutput o
writeExit target r out = do {-# SCC "annotate" #-} annotate target r (o_soln out) (o_annot out)
donePhase Loud "annotate"
let rs = showFix r
writeResult (colorResult r) r
writeFile (extFileName Result target) rs
writeWarns $ o_warns out
writeCheckVars $ o_vars out
return r
writeWarns [] = return ()
writeWarns ws = colorPhaseLn Angry "Warnings:" "" >> putStrLn (unlines ws)
writeCheckVars Nothing = return ()
writeCheckVars (Just ns) = colorPhaseLn Loud "Checked Binders:" "" >> forM_ ns (putStrLn . dropModuleNames . showpp)
writeResult c = mapM_ (writeDoc c) . resDocs
where
writeDoc c = writeBlock c . lines . render
writeBlock c (s:ss) = do {colorPhaseLn c s ""; forM_ ss putStrLn }
writeBlock c _ = return ()
resDocs Safe = [text "SAFE"]
resDocs (Crash xs s) = text ("CRASH: " ++ s) : pprManyOrdered "CRASH: " xs
resDocs (Unsafe xs) = pprManyOrdered "UNSAFE: " xs
resDocs (UnknownError d) = [text "PANIC: Unexpected Error: " <+> d, reportUrl]
reportUrl = text "Please submit a bug report at:"
$+$ text " https://github.com/ucsd-progsys/liquidhaskell"
instance Fixpoint (FixResult Error) where
toFix = vcat . resDocs
-- vcat [[String]]
-- toFix Safe = text "SAFE"
-- toFix (UnknownError d) = text "Unknown Error!"
-- toFix (Crash xs msg) = vcat $ text "Crash!" : pprManyOrdered "CRASH: " xs ++ [parens (text msg)]
-- toFix (Unsafe xs) = vcat $ text "Unsafe:" : pprManyOrdered "WARNING: " xs
------------------------------------------------------------------------
-- | Stuff To Output ---------------------------------------------------
------------------------------------------------------------------------
data Output = O { o_vars :: Maybe [Name]
, o_warns :: [String]
, o_soln :: FixSolution
, o_annot :: !(AnnInfo Annot)
}
emptyOutput = O Nothing [] M.empty mempty