{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wwarn=deprecations #-}
{-# OPTIONS_GHC -fno-cse #-}
{-# LANGUAGE FlexibleContexts #-}
module Language.Haskell.Liquid.UX.CmdLine (
getOpts, mkOpts, defConfig, config
, withPragmas
, canonicalizePaths
, exitWithResult
, addErrors
, OutputResult(..)
, reportResult
, diffcheck
, printLiquidHaskellBanner
) where
import Prelude hiding (error)
import Control.Monad
import Control.Monad.IO.Class
import Data.Maybe
import Data.Functor ((<&>))
import Data.Aeson (encode)
import qualified Data.ByteString.Lazy.Char8 as B
import Development.GitRev (gitCommitCount)
import qualified Paths_liquidhaskell_boot as Meta
import System.Directory
import System.Exit
import System.Environment
import System.Console.CmdArgs.Explicit
import System.Console.CmdArgs.Implicit hiding (Loud)
import qualified System.Console.CmdArgs.Verbosity as CmdArgs
import System.Console.CmdArgs.Text
import GitHash
import Data.List (nub)
import System.FilePath (isAbsolute, takeDirectory, (</>))
import qualified Language.Fixpoint.Types.Config as FC
import Language.Fixpoint.Misc
import Language.Fixpoint.Types.Names
import Language.Fixpoint.Types hiding (panic, Error, Result, saveQuery)
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Solver.Stats as Solver
import Language.Haskell.Liquid.UX.Annotate
import Language.Haskell.Liquid.UX.Config
import Language.Haskell.Liquid.UX.SimpleVersion (simpleVersion)
import Language.Haskell.Liquid.GHC.Misc
import Language.Haskell.Liquid.Types.PrettyPrint ()
import Language.Haskell.Liquid.Types hiding (typ)
import qualified Language.Haskell.Liquid.UX.ACSS as ACSS
import qualified Liquid.GHC.API as GHC
import Language.Haskell.TH.Syntax.Compat (fromCode, toCode)
import Text.PrettyPrint.HughesPJ hiding (Mode, (<>))
defaultMaxParams :: Int
defaultMaxParams :: Int
defaultMaxParams = Int
2
config :: Mode (CmdArgs Config)
config :: Mode (CmdArgs Config)
config = forall a. Data a => a -> Mode (CmdArgs a)
cmdArgsMode forall a b. (a -> b) -> a -> b
$ Config {
loggingVerbosity :: Verbosity
loggingVerbosity
= forall val. Data val => [val] -> val
enum [ Verbosity
Quiet forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"quiet" forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Minimal logging verbosity"
, Verbosity
Normal forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"normal" forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Normal logging verbosity"
, Verbosity
CmdArgs.Loud forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"verbose" forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Verbose logging"
]
, files :: [String]
files
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
typ String
"TARGET"
forall val. Data val => val -> Ann -> val
&= Ann
args
forall val. Data val => val -> Ann -> val
&= Ann
typFile
, idirs :: [String]
idirs
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= Ann
typDir
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Paths to Spec Include Directory "
, fullcheck :: Bool
fullcheck
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Full Checking: check all binders (DEFAULT)"
, diffcheck :: Bool
diffcheck
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Incremental Checking: only check changed binders"
, higherorder :: Bool
higherorder
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow higher order binders into the logic"
, smtTimeout :: Maybe Int
smtTimeout
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Timeout of smt queries in msec"
, higherorderqs :: Bool
higherorderqs
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow higher order qualifiers to get automatically instantiated"
, linear :: Bool
linear
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use uninterpreted integer multiplication and division"
, stringTheory :: Bool
stringTheory
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Interpretation of Strings by z3"
, saveQuery :: Bool
saveQuery
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Save fixpoint query to file (slow)"
, checks :: [String]
checks
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Check a specific (top-level) binder"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"check-var"
, pruneUnsorted :: Bool
pruneUnsorted
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable prunning unsorted Predicates"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"prune-unsorted"
, notermination :: Bool
notermination
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Termination Check"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-termination-check"
, nopositivity :: Bool
nopositivity
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Data Type Positivity Check"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-positivity-check"
, rankNTypes :: Bool
rankNTypes
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Adds precise reasoning on presence of rankNTypes"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"rankNTypes"
, noclasscheck :: Bool
noclasscheck
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Class Instance Check"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-class-check"
, nostructuralterm :: Bool
nostructuralterm
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-structural-termination"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable structural termination check"
, gradual :: Bool
gradual
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable gradual refinement type checking"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"gradual"
, bscope :: Bool
bscope
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"scope of the outer binders on the inner refinements"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"bscope"
, gdepth :: Int
gdepth
= Int
1
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Size of gradual conretizations, 1 by default"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"gradual-depth"
, ginteractive :: Bool
ginteractive
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Interactive Gradual Solving"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ginteractive"
, totalHaskell :: Bool
totalHaskell
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Check for termination and totality; overrides no-termination flags"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"total-Haskell"
, nowarnings :: Bool
nowarnings
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't display warnings, only show errors"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-warnings"
, noannotations :: Bool
noannotations
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't create intermediate annotation files"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-annotations"
, checkDerived :: Bool
checkDerived
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Check GHC generated binders (e.g. Read, Show instances)"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"check-derived"
, caseExpandDepth :: Int
caseExpandDepth
= Int
2 forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum depth at which to expand DEFAULT in case-of (default=2)"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"max-case-expand"
, notruetypes :: Bool
notruetypes
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Trueing Top Level Types"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-true-types"
, nototality :: Bool
nototality
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable totality check"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-totality"
, cores :: Maybe Int
cores
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use m cores to solve logical constraints"
, minPartSize :: Int
minPartSize
= Int
FC.defaultMinPartSize
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"If solving on multiple cores, ensure that partitions are of at least m size"
, maxPartSize :: Int
maxPartSize
= Int
FC.defaultMaxPartSize
forall val. Data val => val -> Ann -> val
&= String -> Ann
help (String
"If solving on multiple cores, once there are as many partitions " forall a. [a] -> [a] -> [a]
++
String
"as there are cores, don't merge partitions if they will exceed this " forall a. [a] -> [a] -> [a]
++
String
"size. Overrides the minpartsize option.")
, smtsolver :: Maybe SMTSolver
smtsolver
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Name of SMT-Solver"
, noCheckUnknown :: Bool
noCheckUnknown
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= Ann
explicit
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-check-unknown"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't complain about specifications for unexported and unused values "
, maxParams :: Int
maxParams
= Int
defaultMaxParams forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Restrict qualifier mining to those taking at most `m' parameters (2 by default)"
, shortNames :: Bool
shortNames
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"short-names"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print shortened names, i.e. drop all module qualifiers."
, shortErrors :: Bool
shortErrors
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"short-errors"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't show long error messages, just line numbers."
, cabalDir :: Bool
cabalDir
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"cabal-dir"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Find and use .cabal to add paths to sources for imported files"
, ghcOptions :: [String]
ghcOptions
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ghc-option"
forall val. Data val => val -> Ann -> val
&= String -> Ann
typ String
"OPTION"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Pass this option to GHC"
, cFiles :: [String]
cFiles
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"c-files"
forall val. Data val => val -> Ann -> val
&= String -> Ann
typ String
"OPTION"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Tell GHC to compile and link against these files"
, port :: Int
port
= Int
defaultPort
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"port"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Port at which lhi should listen"
, exactDC :: Bool
exactDC
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Exact Type for Data Constructors"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"exact-data-cons"
, noADT :: Bool
noADT
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Do not generate ADT representations in refinement logic"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-adt"
, expectErrorContaining :: [String]
expectErrorContaining
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Expect an error which containing the provided string from verification (can be provided more than once)"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"expect-error-containing"
, expectAnyError :: Bool
expectAnyError
= forall a. Default a => a
def forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Expect an error, no matter which kind or what it contains"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"expect-any-error"
, scrapeImports :: Bool
scrapeImports
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Scrape qualifiers from imported specifications"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"scrape-imports"
forall val. Data val => val -> Ann -> val
&= Ann
explicit
, scrapeInternals :: Bool
scrapeInternals
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Scrape qualifiers from auto generated specifications"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"scrape-internals"
forall val. Data val => val -> Ann -> val
&= Ann
explicit
, scrapeUsedImports :: Bool
scrapeUsedImports
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Scrape qualifiers from used, imported specifications"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"scrape-used-imports"
forall val. Data val => val -> Ann -> val
&= Ann
explicit
, elimStats :: Bool
elimStats
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"elimStats"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print eliminate stats"
, elimBound :: Maybe Int
elimBound
= forall a. Maybe a
Nothing
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"elimBound"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum chain length for eliminating KVars"
, noslice :: Bool
noslice
= Bool
False
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"noSlice"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable non-concrete KVar slicing"
, noLiftedImport :: Bool
noLiftedImport
= Bool
False
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-lifted-imports"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable loading lifted specifications (for legacy libs)"
, json :: Bool
json
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"json"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print results in JSON (for editor integration)"
, counterExamples :: Bool
counterExamples
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"counter-examples"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Attempt to generate counter-examples to type errors (experimental!)"
, timeBinds :: Bool
timeBinds
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"time-binds"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Solve each (top-level) asserted type signature separately & time solving."
, untidyCore :: Bool
untidyCore
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"untidy-core"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print fully qualified identifier names in verbose mode"
, eliminate :: Eliminate
eliminate
= Eliminate
FC.Some
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"eliminate"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use elimination for 'all' (use TRUE for cut-kvars), 'some' (use quals for cut-kvars) or 'none' (use quals for all kvars)."
, noPatternInline :: Bool
noPatternInline
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-pattern-inline"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't inline special patterns (e.g. `>>=` and `return`) during constraint generation."
, noSimplifyCore :: Bool
noSimplifyCore
= Bool
False forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-simplify-core"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't simplify GHC core before constraint generation"
, proofLogicEval :: Bool
proofLogicEval
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Proof-by-Logical-Evaluation"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ple"
, pleWithUndecidedGuards :: Bool
pleWithUndecidedGuards
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Unfold invocations with undecided guards in PLE"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ple-with-undecided-guards"
forall val. Data val => val -> Ann -> val
&= Ann
explicit
, oldPLE :: Bool
oldPLE
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Proof-by-Logical-Evaluation"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"oldple"
, interpreter :: Bool
interpreter
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use an interpreter to assist PLE in solving constraints"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"interpreter"
, proofLogicEvalLocal :: Bool
proofLogicEvalLocal
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Proof-by-Logical-Evaluation locally, per function"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ple-local"
, extensionality :: Bool
extensionality
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable extensional interpretation of function equality"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"extensionality"
, nopolyinfer :: Bool
nopolyinfer
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"No inference of polymorphic type application. Gives imprecision, but speedup."
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"fast"
, reflection :: Bool
reflection
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable reflection of Haskell functions and theorem proving"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"reflection"
, compileSpec :: Bool
compileSpec
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"compile-spec"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Only compile specifications (into .bspec file); skip verification"
, noCheckImports :: Bool
noCheckImports
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-check-imports"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Do not check the transitive imports; only check the target files."
, typeclass :: Bool
typeclass
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Typeclass"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"typeclass"
, auxInline :: Bool
auxInline
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable inlining of class methods"
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"aux-inline"
,
rwTerminationCheck :: Bool
rwTerminationCheck
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"rw-termination-check"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help ( String
"Enable the rewrite divergence checker. "
forall a. [a] -> [a] -> [a]
++ String
"Can speed up verification if rewriting terminates, but can also cause divergence."
)
,
skipModule :: Bool
skipModule
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"skip-module"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Completely skip this module, don't even compile any specifications in it."
,
noLazyPLE :: Bool
noLazyPLE
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-lazy-ple"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't use Lazy PLE"
, fuel :: Maybe Int
fuel
= forall a. Maybe a
Nothing
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum fuel (per-function unfoldings) for PLE"
, environmentReduction :: Bool
environmentReduction
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= Ann
explicit
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"environment-reduction"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"perform environment reduction (disabled by default)"
, noEnvironmentReduction :: Bool
noEnvironmentReduction
= forall a. Default a => a
def
forall val. Data val => val -> Ann -> val
&= Ann
explicit
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-environment-reduction"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't perform environment reduction"
, inlineANFBindings :: Bool
inlineANFBindings
= Bool
False
forall val. Data val => val -> Ann -> val
&= Ann
explicit
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"inline-anf-bindings"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help ([String] -> String
unwords
[ String
"Inline ANF bindings."
, String
"Sometimes improves performance and sometimes worsens it."
, String
"Disabled by --no-environment-reduction"
])
, pandocHtml :: Bool
pandocHtml
= Bool
False
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"pandoc-html"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use pandoc to generate html."
, excludeAutomaticAssumptionsFor :: [String]
excludeAutomaticAssumptionsFor
= []
forall val. Data val => val -> Ann -> val
&= Ann
explicit
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"exclude-automatic-assumptions-for"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Stop loading LHAssumptions modules for imports in these packages."
forall val. Data val => val -> Ann -> val
&= String -> Ann
typ String
"PACKAGE"
} forall val. Data val => val -> Ann -> val
&= String -> Ann
program String
"liquid"
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Refinement Types for Haskell"
forall val. Data val => val -> Ann -> val
&= String -> Ann
summary String
copyright
forall val. Data val => val -> Ann -> val
&= [String] -> Ann
details [ String
"LiquidHaskell is a Refinement Type based verifier for Haskell"
, String
""
, String
"To check a Haskell file foo.hs, type:"
, String
" liquid foo.hs "
]
defaultPort :: Int
defaultPort :: Int
defaultPort = Int
3000
getOpts :: [String] -> IO Config
getOpts :: [String] -> IO Config
getOpts [String]
as = do
Config
cfg0 <- IO Config
envCfg
Config
cfg1 <- Config -> IO Config
mkOpts forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Mode (CmdArgs a) -> [String] -> IO a
cmdArgsRun'
Mode (CmdArgs Config)
config { modeValue :: CmdArgs Config
modeValue = (forall a. Mode a -> a
modeValue Mode (CmdArgs Config)
config)
{ cmdArgsValue :: Config
cmdArgsValue = Config
cfg0
}
}
[String]
as
Config
cfg <- Config -> IO Config
fixConfig Config
cfg1
Verbosity -> IO ()
setVerbosity (Config -> Verbosity
loggingVerbosity Config
cfg)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
json Config
cfg) forall a b. (a -> b) -> a -> b
$ Verbosity -> IO ()
setVerbosity Verbosity
Quiet
Config -> IO Config
withSmtSolver Config
cfg
printLiquidHaskellBanner :: IO ()
printLiquidHaskellBanner :: IO ()
printLiquidHaskellBanner = IO () -> IO ()
whenNormal forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
copyright
cmdArgsRun' :: Mode (CmdArgs a) -> [String] -> IO a
cmdArgsRun' :: forall a. Mode (CmdArgs a) -> [String] -> IO a
cmdArgsRun' Mode (CmdArgs a)
md [String]
as
= case Either String (CmdArgs a)
parseResult of
Left String
e -> String -> IO ()
putStrLn (String -> String
helpMsg String
e) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. IO a
exitFailure
Right CmdArgs a
a -> forall a. CmdArgs a -> IO a
cmdArgsApply CmdArgs a
a
where
helpMsg :: String -> String
helpMsg String
e = TextFormat -> [Text] -> String
showText TextFormat
defaultWrap forall a b. (a -> b) -> a -> b
$ forall a. [String] -> HelpFormat -> Mode a -> [Text]
helpText [String
e] HelpFormat
HelpFormatDefault Mode (CmdArgs a)
md
parseResult :: Either String (CmdArgs a)
parseResult = forall a. Mode a -> [String] -> Either String a
process Mode (CmdArgs a)
md ([String] -> [String]
wideHelp [String]
as)
wideHelp :: [String] -> [String]
wideHelp = forall a b. (a -> b) -> [a] -> [b]
map (\String
a -> if String
a forall a. Eq a => a -> a -> Bool
== String
"--help" Bool -> Bool -> Bool
|| String
a forall a. Eq a => a -> a -> Bool
== String
"-help" then String
"--help=120" else String
a)
withSmtSolver :: Config -> IO Config
withSmtSolver :: Config -> IO Config
withSmtSolver Config
cfg =
case Config -> Maybe SMTSolver
smtsolver Config
cfg of
Just SMTSolver
smt -> do Maybe SMTSolver
found <- SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver SMTSolver
smt
case Maybe SMTSolver
found of
Just SMTSolver
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Config
cfg
Maybe SMTSolver
Nothing -> forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing (forall {a}. Show a => a -> String
missingSmtError SMTSolver
smt)
Maybe SMTSolver
Nothing -> do [Maybe SMTSolver]
smts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver [SMTSolver
FC.Z3, SMTSolver
FC.Cvc4, SMTSolver
FC.Mathsat]
case forall a. [Maybe a] -> [a]
catMaybes [Maybe SMTSolver]
smts of
(SMTSolver
s:[SMTSolver]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Config
cfg {smtsolver :: Maybe SMTSolver
smtsolver = forall a. a -> Maybe a
Just SMTSolver
s})
[SMTSolver]
_ -> forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
noSmtError
where
noSmtError :: String
noSmtError = String
"LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed."
missingSmtError :: a -> String
missingSmtError a
smt = String
"Could not find SMT solver '" forall a. [a] -> [a] -> [a]
++ forall {a}. Show a => a -> String
show a
smt forall a. [a] -> [a] -> [a]
++ String
"'. Is it on your PATH?"
findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver)
findSmtSolver :: SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver SMTSolver
smt = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Maybe a
Nothing (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SMTSolver
smt) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO (Maybe String)
findExecutable (forall {a}. Show a => a -> String
show SMTSolver
smt)
fixConfig :: Config -> IO Config
fixConfig :: Config -> IO Config
fixConfig Config
config' = do
String
pwd <- IO String
getCurrentDirectory
Config
cfg <- String -> Config -> IO Config
canonicalizePaths String
pwd Config
config'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Config -> Config
canonConfig Config
cfg
canonicalizePaths :: FilePath -> Config -> IO Config
canonicalizePaths :: String -> Config -> IO Config
canonicalizePaths String
pwd Config
cfg = do
String
tgt <- String -> IO String
canonicalizePath String
pwd
Bool
isdir <- String -> IO Bool
doesDirectoryExist String
tgt
[String]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Bool -> String -> IO String
canonicalize String
tgt Bool
isdir) forall a b. (a -> b) -> a -> b
$ Config -> [String]
idirs Config
cfg
[String]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Bool -> String -> IO String
canonicalize String
tgt Bool
isdir) forall a b. (a -> b) -> a -> b
$ Config -> [String]
cFiles Config
cfg
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Config
cfg { idirs :: [String]
idirs = [String]
is, cFiles :: [String]
cFiles = [String]
cs }
canonicalize :: FilePath -> Bool -> FilePath -> IO FilePath
canonicalize :: String -> Bool -> String -> IO String
canonicalize String
tgt Bool
isdir String
f
| String -> Bool
isAbsolute String
f = forall (m :: * -> *) a. Monad m => a -> m a
return String
f
| Bool
isdir = String -> IO String
canonicalizePath (String
tgt String -> String -> String
</> String
f)
| Bool
otherwise = String -> IO String
canonicalizePath (String -> String
takeDirectory String
tgt String -> String -> String
</> String
f)
envCfg :: IO Config
envCfg :: IO Config
envCfg = do
Maybe String
so <- String -> IO (Maybe String)
lookupEnv String
"LIQUIDHASKELL_OPTS"
case Maybe String
so of
Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Config
defConfig
Just String
s -> Located String -> IO Config
parsePragma forall a b. (a -> b) -> a -> b
$ forall {a}. a -> Located a
envLoc String
s
where
envLoc :: a -> Located a
envLoc = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l
l :: SourcePos
l = String -> Int -> Int -> SourcePos
safeSourcePos String
"ENVIRONMENT" Int
1 Int
1
copyright :: String
copyright :: String
copyright = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [String
"LiquidHaskell "]
, [$(simpleVersion Meta.version)]
, [String
gitInfo]
, [String
"\nCopyright 2013-19 Regents of the University of California. All Rights Reserved.\n"]
]
where
_commitCount :: String
_commitCount = $String
gitCommitCount
gitInfo :: String
gitInfo :: String
gitInfo = String
msg
where
giTry :: Either String GitInfo
giTry :: Either String GitInfo
giTry = $$(fromCode (toCode tGitInfoCwdTry))
msg :: String
msg = case Either String GitInfo
giTry of
Left String
_ -> String
" no git information"
Right GitInfo
gi -> GitInfo -> String
gitMsg GitInfo
gi
gitMsg :: GitInfo -> String
gitMsg :: GitInfo -> String
gitMsg GitInfo
gi = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
" [", GitInfo -> String
giBranch GitInfo
gi, String
"@", GitInfo -> String
giHash GitInfo
gi
, String
" (", GitInfo -> String
giCommitDate GitInfo
gi, String
")"
, String
"] "
]
mkOpts :: Config -> IO Config
mkOpts :: Config -> IO Config
mkOpts Config
cfg = do
let files' :: [String]
files' = forall a. Ord a => [a] -> [a]
sortNub forall a b. (a -> b) -> a -> b
$ Config -> [String]
files Config
cfg
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Config
cfg { files :: [String]
files = [String]
files'
}
canonConfig :: Config -> Config
canonConfig :: Config -> Config
canonConfig Config
cfg = Config
cfg
{ diffcheck :: Bool
diffcheck = Config -> Bool
diffcheck Config
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
fullcheck Config
cfg)
}
withPragmas :: MonadIO m => Config -> FilePath -> [Located String] -> (Config -> m a) -> m a
withPragmas :: forall (m :: * -> *) a.
MonadIO m =>
Config -> String -> [Located String] -> (Config -> m a) -> m a
withPragmas Config
cfg String
fp [Located String]
ps Config -> m a
action
= do Config
cfg' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (Config -> [Located String] -> IO Config
processPragmas Config
cfg [Located String]
ps forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Config -> IO Config
canonicalizePaths String
fp) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Config -> Config
canonConfig
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Verbosity -> IO ()
setVerbosity (Config -> Verbosity
loggingVerbosity Config
cfg')
a
res <- Config -> m a
action Config
cfg'
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Verbosity -> IO ()
setVerbosity (Config -> Verbosity
loggingVerbosity Config
cfg)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
res
processPragmas :: Config -> [Located String] -> IO Config
processPragmas :: Config -> [Located String] -> IO Config
processPragmas Config
c [Located String]
pragmas =
forall a. Mode a -> [String] -> IO a
processValueIO
Mode (CmdArgs Config)
config { modeValue :: CmdArgs Config
modeValue = (forall a. Mode a -> a
modeValue Mode (CmdArgs Config)
config) { cmdArgsValue :: Config
cmdArgsValue = Config
c } }
(forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located String]
pragmas)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
forall a. CmdArgs a -> IO a
cmdArgsApply
parsePragma :: Located String -> IO Config
parsePragma :: Located String -> IO Config
parsePragma = Config -> [Located String] -> IO Config
processPragmas Config
defConfig forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[])
defConfig :: Config
defConfig :: Config
defConfig = Config
{ loggingVerbosity :: Verbosity
loggingVerbosity = Verbosity
Quiet
, files :: [String]
files = forall a. Default a => a
def
, idirs :: [String]
idirs = forall a. Default a => a
def
, fullcheck :: Bool
fullcheck = forall a. Default a => a
def
, linear :: Bool
linear = forall a. Default a => a
def
, stringTheory :: Bool
stringTheory = forall a. Default a => a
def
, higherorder :: Bool
higherorder = forall a. Default a => a
def
, smtTimeout :: Maybe Int
smtTimeout = forall a. Default a => a
def
, higherorderqs :: Bool
higherorderqs = forall a. Default a => a
def
, diffcheck :: Bool
diffcheck = forall a. Default a => a
def
, saveQuery :: Bool
saveQuery = forall a. Default a => a
def
, checks :: [String]
checks = forall a. Default a => a
def
, nostructuralterm :: Bool
nostructuralterm = forall a. Default a => a
def
, noCheckUnknown :: Bool
noCheckUnknown = forall a. Default a => a
def
, notermination :: Bool
notermination = Bool
False
, nopositivity :: Bool
nopositivity = Bool
False
, rankNTypes :: Bool
rankNTypes = Bool
False
, noclasscheck :: Bool
noclasscheck = Bool
False
, gradual :: Bool
gradual = Bool
False
, bscope :: Bool
bscope = Bool
False
, gdepth :: Int
gdepth = Int
1
, ginteractive :: Bool
ginteractive = Bool
False
, totalHaskell :: Bool
totalHaskell = forall a. Default a => a
def
, nowarnings :: Bool
nowarnings = forall a. Default a => a
def
, noannotations :: Bool
noannotations = forall a. Default a => a
def
, checkDerived :: Bool
checkDerived = Bool
False
, caseExpandDepth :: Int
caseExpandDepth = Int
2
, notruetypes :: Bool
notruetypes = forall a. Default a => a
def
, nototality :: Bool
nototality = Bool
False
, pruneUnsorted :: Bool
pruneUnsorted = forall a. Default a => a
def
, exactDC :: Bool
exactDC = forall a. Default a => a
def
, noADT :: Bool
noADT = forall a. Default a => a
def
, expectErrorContaining :: [String]
expectErrorContaining = forall a. Default a => a
def
, expectAnyError :: Bool
expectAnyError = Bool
False
, cores :: Maybe Int
cores = forall a. Default a => a
def
, minPartSize :: Int
minPartSize = Int
FC.defaultMinPartSize
, maxPartSize :: Int
maxPartSize = Int
FC.defaultMaxPartSize
, maxParams :: Int
maxParams = Int
defaultMaxParams
, smtsolver :: Maybe SMTSolver
smtsolver = forall a. Default a => a
def
, shortNames :: Bool
shortNames = forall a. Default a => a
def
, shortErrors :: Bool
shortErrors = forall a. Default a => a
def
, cabalDir :: Bool
cabalDir = forall a. Default a => a
def
, ghcOptions :: [String]
ghcOptions = forall a. Default a => a
def
, cFiles :: [String]
cFiles = forall a. Default a => a
def
, port :: Int
port = Int
defaultPort
, scrapeInternals :: Bool
scrapeInternals = Bool
False
, scrapeImports :: Bool
scrapeImports = Bool
False
, scrapeUsedImports :: Bool
scrapeUsedImports = Bool
False
, elimStats :: Bool
elimStats = Bool
False
, elimBound :: Maybe Int
elimBound = forall a. Maybe a
Nothing
, json :: Bool
json = Bool
False
, counterExamples :: Bool
counterExamples = Bool
False
, timeBinds :: Bool
timeBinds = Bool
False
, untidyCore :: Bool
untidyCore = Bool
False
, eliminate :: Eliminate
eliminate = Eliminate
FC.Some
, noPatternInline :: Bool
noPatternInline = Bool
False
, noSimplifyCore :: Bool
noSimplifyCore = Bool
False
, noslice :: Bool
noslice = Bool
False
, noLiftedImport :: Bool
noLiftedImport = Bool
False
, proofLogicEval :: Bool
proofLogicEval = Bool
False
, pleWithUndecidedGuards :: Bool
pleWithUndecidedGuards = Bool
False
, oldPLE :: Bool
oldPLE = Bool
False
, interpreter :: Bool
interpreter = Bool
False
, proofLogicEvalLocal :: Bool
proofLogicEvalLocal = Bool
False
, reflection :: Bool
reflection = Bool
False
, extensionality :: Bool
extensionality = Bool
False
, nopolyinfer :: Bool
nopolyinfer = Bool
False
, compileSpec :: Bool
compileSpec = Bool
False
, noCheckImports :: Bool
noCheckImports = Bool
False
, typeclass :: Bool
typeclass = Bool
False
, auxInline :: Bool
auxInline = Bool
False
, rwTerminationCheck :: Bool
rwTerminationCheck = Bool
False
, skipModule :: Bool
skipModule = Bool
False
, noLazyPLE :: Bool
noLazyPLE = Bool
False
, fuel :: Maybe Int
fuel = forall a. Maybe a
Nothing
, environmentReduction :: Bool
environmentReduction = Bool
False
, noEnvironmentReduction :: Bool
noEnvironmentReduction = Bool
False
, inlineANFBindings :: Bool
inlineANFBindings = Bool
False
, pandocHtml :: Bool
pandocHtml = Bool
False
, excludeAutomaticAssumptionsFor :: [String]
excludeAutomaticAssumptionsFor = []
}
reportResult :: MonadIO m
=> (OutputResult -> m ())
-> Config
-> [FilePath]
-> Output Doc
-> m ()
reportResult :: forall (m :: * -> *).
MonadIO m =>
(OutputResult -> m ()) -> Config -> [String] -> Output Doc -> m ()
reportResult OutputResult -> m ()
logResultFull Config
cfg [String]
targets Output Doc
out = do
AnnMap
annm <- {-# SCC "annotate" #-} forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Config -> [String] -> Output Doc -> IO AnnMap
annotate Config
cfg [String]
targets Output Doc
out
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenNormal forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
donePhase Moods
Loud String
"annotate"
if Config -> Bool
json Config
cfg then
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ AnnMap -> IO ()
reportResultJson AnnMap
annm
else do
let r :: ErrorResult
r = forall a. Output a -> ErrorResult
o_result Output Doc
out
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => Maybe [a] -> IO ()
writeCheckVars forall a b. (a -> b) -> a -> b
$ forall a. Output a -> Maybe [String]
o_vars Output Doc
out
FixResult CError
cr <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ ErrorResult -> IO (FixResult CError)
resultWithContext ErrorResult
r
let outputResult :: OutputResult
outputResult = Tidy -> FixResult CError -> OutputResult
resDocs Tidy
tidy FixResult CError
cr
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Moods -> Doc -> IO ()
printHeader (forall a. FixResult a -> Moods
colorResult ErrorResult
r) (OutputResult -> Doc
orHeader OutputResult
outputResult)
OutputResult -> m ()
logResultFull OutputResult
outputResult
where
tidy :: F.Tidy
tidy :: Tidy
tidy = if Config -> Bool
shortErrors Config
cfg then Tidy
F.Lossy else Tidy
F.Full
printHeader :: Moods -> Doc -> IO ()
printHeader :: Moods -> Doc -> IO ()
printHeader Moods
mood Doc
d = Moods -> String -> String -> IO ()
colorPhaseLn Moods
mood String
"" (Doc -> String
render Doc
d)
exitWithResult :: Config -> [FilePath] -> Output Doc -> IO ()
exitWithResult :: Config -> [String] -> Output Doc -> IO ()
exitWithResult Config
cfg [String]
targets Output Doc
out = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadIO m =>
(OutputResult -> m ()) -> Config -> [String] -> Output Doc -> m ()
reportResult OutputResult -> IO ()
writeResultStdout Config
cfg [String]
targets Output Doc
out
reportResultJson :: ACSS.AnnMap -> IO ()
reportResultJson :: AnnMap -> IO ()
reportResultJson AnnMap
annm = do
String -> IO ()
putStrLn String
"LIQUID"
ByteString -> IO ()
B.putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToJSON a => a -> ByteString
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnMap -> AnnErrors
annErrors forall a b. (a -> b) -> a -> b
$ AnnMap
annm
resultWithContext :: F.FixResult UserError -> IO (FixResult CError)
resultWithContext :: ErrorResult -> IO (FixResult CError)
resultWithContext (F.Unsafe Stats
s [TError Doc]
es) = forall a. Stats -> [a] -> FixResult a
F.Unsafe Stats
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TError Doc] -> IO [CError]
errorsWithContext [TError Doc]
es
resultWithContext (F.Safe Stats
stats) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Stats -> FixResult a
F.Safe Stats
stats)
resultWithContext (F.Crash [(TError Doc, Maybe String)]
es String
s) = do
let ([TError Doc]
userErrs, [Maybe String]
msgs) = forall a b. [(a, b)] -> ([a], [b])
unzip [(TError Doc, Maybe String)]
es
[CError]
errs' <- [TError Doc] -> IO [CError]
errorsWithContext [TError Doc]
userErrs
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [(a, Maybe String)] -> String -> FixResult a
F.Crash (forall a b. [a] -> [b] -> [(a, b)]
zip [CError]
errs' [Maybe String]
msgs) String
s)
instance Show (CtxError Doc) where
show :: CError -> String
show = forall a. PPrint a => a -> String
showpp
writeCheckVars :: Symbolic a => Maybe [a] -> IO ()
writeCheckVars :: forall a. Symbolic a => Maybe [a] -> IO ()
writeCheckVars Maybe [a]
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return ()
writeCheckVars (Just []) = Moods -> String -> String -> IO ()
colorPhaseLn Moods
Loud String
"Checked Binders: None" String
""
writeCheckVars (Just [a]
ns) = Moods -> String -> String -> IO ()
colorPhaseLn Moods
Loud String
"Checked Binders:" String
""
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [a]
ns (String -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
symbolString forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol)
type CError = CtxError Doc
data OutputResult = OutputResult {
:: Doc
, OutputResult -> [(SrcSpan, Doc)]
orMessages :: [(GHC.SrcSpan, Doc)]
}
writeResultStdout :: OutputResult -> IO ()
writeResultStdout :: OutputResult -> IO ()
writeResultStdout (OutputResult -> [(SrcSpan, Doc)]
orMessages -> [(SrcSpan, Doc)]
messages) = do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SrcSpan, Doc)]
messages forall a b. (a -> b) -> a -> b
$ \(SrcSpan
sSpan, Doc
doc) -> String -> IO ()
putStrLn (Doc -> String
render forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc -> Doc
mkErrorDoc SrcSpan
sSpan Doc
doc )
mkErrorDoc :: PPrint a => a -> Doc -> Doc
mkErrorDoc :: forall a. PPrint a => a -> Doc -> Doc
mkErrorDoc a
sSpan Doc
doc =
(forall a. PPrint a => a -> Doc
pprint a
sSpan forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
": error: ") Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
doc
resDocs :: F.Tidy -> F.FixResult CError -> OutputResult
resDocs :: Tidy -> FixResult CError -> OutputResult
resDocs Tidy
_ (F.Safe Stats
stats) =
OutputResult {
orHeader :: Doc
orHeader = String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"LIQUID: SAFE (" forall a. Semigroup a => a -> a -> a
<> forall {a}. Show a => a -> String
show (Stats -> Int
Solver.numChck Stats
stats) forall a. Semigroup a => a -> a -> a
<> String
" constraints checked)"
, orMessages :: [(SrcSpan, Doc)]
orMessages = forall a. Monoid a => a
mempty
}
resDocs Tidy
_k (F.Crash [] String
s) =
OutputResult {
orHeader :: Doc
orHeader = String -> Doc
text String
"LIQUID: ERROR"
, orMessages :: [(SrcSpan, Doc)]
orMessages = [(SrcSpan
GHC.noSrcSpan, String -> Doc
text String
s)]
}
resDocs Tidy
k (F.Crash [(CError, Maybe String)]
xs String
s) =
OutputResult {
orHeader :: Doc
orHeader = String -> Doc
text String
"LIQUID: ERROR:" Doc -> Doc -> Doc
<+> String -> Doc
text String
s
, orMessages :: [(SrcSpan, Doc)]
orMessages = forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CError -> (SrcSpan, Doc)
cErrToSpanned Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CError, Maybe String) -> CError
errToFCrash) [(CError, Maybe String)]
xs
}
resDocs Tidy
k (F.Unsafe Stats
_ [CError]
xs) =
OutputResult {
orHeader :: Doc
orHeader = String -> Doc
text String
"LIQUID: UNSAFE"
, orMessages :: [(SrcSpan, Doc)]
orMessages = forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CError -> (SrcSpan, Doc)
cErrToSpanned Tidy
k) (forall a. Eq a => [a] -> [a]
nub [CError]
xs)
}
cErrToSpanned :: F.Tidy -> CError -> (GHC.SrcSpan, Doc)
cErrToSpanned :: Tidy -> CError -> (SrcSpan, Doc)
cErrToSpanned Tidy
k CtxError{TError Doc
ctErr :: forall t. CtxError t -> TError t
ctErr :: TError Doc
ctErr} = (forall t. TError t -> SrcSpan
pos TError Doc
ctErr, forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k TError Doc
ctErr)
errToFCrash :: (CError, Maybe String) -> CError
errToFCrash :: (CError, Maybe String) -> CError
errToFCrash (CError
ce, Just String
msg) = CError
ce { ctErr :: TError Doc
ctErr = forall t. SrcSpan -> Doc -> TError t
ErrOther (forall t. TError t -> SrcSpan
pos (forall t. CtxError t -> TError t
ctErr CError
ce)) (String -> Doc
fixMessageDoc String
msg) }
errToFCrash (CError
ce, Maybe String
Nothing) = CError
ce { ctErr :: TError Doc
ctErr = forall {t}. PPrint (TError t) => TError t -> TError t
tx forall a b. (a -> b) -> a -> b
$ forall t. CtxError t -> TError t
ctErr CError
ce}
where
tx :: TError t -> TError t
tx (ErrSubType SrcSpan
l Doc
m Maybe SubcId
_ HashMap Symbol t
g t
t t
t') = forall t. SrcSpan -> Doc -> HashMap Symbol t -> t -> t -> TError t
ErrFCrash SrcSpan
l Doc
m HashMap Symbol t
g t
t t
t'
tx TError t
e = forall a. PPrint a => String -> a -> a
F.notracepp String
"errToFCrash?" TError t
e
fixMessageDoc :: String -> Doc
fixMessageDoc :: String -> Doc
fixMessageDoc String
msg = [Doc] -> Doc
vcat (String -> Doc
text forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> [String]
lines String
msg)
addErrors :: FixResult a -> [a] -> FixResult a
addErrors :: forall a. FixResult a -> [a] -> FixResult a
addErrors FixResult a
r [] = FixResult a
r
addErrors (Safe Stats
s) [a]
errors = forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s [a]
errors
addErrors (Unsafe Stats
s [a]
xs) [a]
errors = forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s ([a]
xs forall a. [a] -> [a] -> [a]
++ [a]
errors)
addErrors FixResult a
r [a]
_ = FixResult a
r
instance Fixpoint (F.FixResult CError) where
toFix :: FixResult CError -> Doc
toFix = [Doc] -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputResult -> [(SrcSpan, Doc)]
orMessages forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> FixResult CError -> OutputResult
resDocs Tidy
F.Full