{-# 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 #-}

-- | 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.UX.CmdLine (
   -- * Get Command Line Configuration
     getOpts, mkOpts, defConfig, config

   -- * Update Configuration With Pragma
   , withPragmas

   -- * Canonicalize Paths in Config
   , canonicalizePaths

   -- * Exit Function
   , exitWithResult
   , addErrors

   -- * Reporting the output of the checking
   , OutputResult(..)
   , reportResult

   -- * Diff check mode
   , diffcheck

   -- * Show info about this version of LiquidHaskell
   , 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, (<>))



---------------------------------------------------------------------------------
-- Config Magic Numbers----------------------------------------------------------
---------------------------------------------------------------------------------

defaultMaxParams :: Int
defaultMaxParams :: Int
defaultMaxParams = Int
2

---------------------------------------------------------------------------------
-- Parsing Command Line----------------------------------------------------------
---------------------------------------------------------------------------------
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"

  -- PLE-OPT , autoInstantiate
    -- PLE-OPT = def
          -- PLE-OPT &= help "How to instantiate axiomatized functions `smtinstances` for SMT instantiation, `liquidinstances` for terminating instantiation"
          -- PLE-OPT &= name "automatic-instances"

  , 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

-- | Shows the LiquidHaskell banner, that includes things like the copyright, the
-- git commit and the version.
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

-- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
--   to worry about relative paths.
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]
  -- , [" (" ++ _commitCount ++ " commits)" | _commitCount /= ("1"::String) &&
  --                                          _commitCount /= ("UNKNOWN" :: String)]
  , [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
")"
  -- , " (", show (giCommitCount gi), " commits in HEAD)"
  , String
"] "
  ]


-- [NOTE:searchpath]
-- 1. we used to add the directory containing the file to the searchpath,
--    but this is bad because GHC does NOT do this, and it causes spurious
--    "duplicate module" errors in the following scenario
--      > tree
--      .
--      ├── Bar.hs
--      └── Foo
--          ├── Bar.hs
--          └── Goo.hs
--    If we run `liquid Foo/Goo.hs` and that imports Bar, GHC will not know
--    whether we mean to import Bar.hs or Foo/Bar.hs
-- 2. tests fail if you flip order of idirs'

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'
                                   -- See NOTE [searchpath]
                   }

--------------------------------------------------------------------------------
-- | Updating options
--------------------------------------------------------------------------------
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)
  -- , eliminate   = if higherOrderFlag cfg then FC.All else eliminate 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
       -- As the verbosity is set /globally/ via the cmdargs lib, re-set it.
       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) -- restore the original verbosity.
       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

-- | Note that this function doesn't process list arguments properly, like
-- 'cFiles' or 'expectErrorContaining'
-- TODO: This is only used to parse the contents of the env var LIQUIDHASKELL_OPTS
-- so it should be able to parse multiple arguments instead. See issue #1990.
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 -- True
  , 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
  -- PLE-OPT , autoInstantiate   = def
  , 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 = []
  }

-- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and
-- report the result of the checking using a supplied function, or using an
-- implicit JSON function, if @json@ flag is set.
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
         -- For now, always print the \"header\" with colours, irrespective to the logger
         -- passed as input.
         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 {
    OutputResult -> Doc
orHeader :: Doc
    -- ^ The \"header\" like \"LIQUID: SAFE\", or \"LIQUID: UNSAFE\".
  , OutputResult -> [(SrcSpan, Doc)]
orMessages :: [(GHC.SrcSpan, Doc)]
    -- ^ The list of pretty-printable messages (typically errors) together with their
    -- source locations.
  }

-- | Writes the result of this LiquidHaskell run to /stdout/.
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 {- pprint sSpan <> (text ": error: " <+> doc)-})

mkErrorDoc :: PPrint a => a -> Doc -> Doc
mkErrorDoc :: forall a. PPrint a => a -> Doc -> Doc
mkErrorDoc a
sSpan Doc
doc =
  -- Gross on screen, nice for Ghcid
  -- pprint sSpan <> (text ": error: " <+> doc)

  -- Nice on screen, invisible in Ghcid ...
  (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


-- | Given a 'FixResult' parameterised over a 'CError', this function returns the \"header\" to show to
-- the user (i.e. \"SAFE\" or \"UNSAFE\") plus a list of 'Doc's together with the 'SrcSpan' they refer to.
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)
  }

-- | Renders a 'CError' into a 'Doc' and its associated 'SrcSpan'.
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)

{-
   TODO: Never used, do I need to exist?
reportUrl = text "Please submit a bug report at: https://github.com/ucsd-progsys/liquidhaskell" -}

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