{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE NamedFieldPuns            #-}
{-# LANGUAGE ViewPatterns              #-}
{-# LANGUAGE LambdaCase                #-}

{-# 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, defConfig

   -- * Update Configuration With Pragma
   , withPragmas

   -- * Collecting errors
   , addErrors

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

   -- * Diff check mode
   , diffcheck

) 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 (Verbosity(..))
import System.Console.CmdArgs.Text
import GitHash

import Data.List                           (nub, intercalate)


import qualified Language.Fixpoint.Types.Config as FC
import qualified Language.Fixpoint.Misc as F
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.Errors hiding (typ)
import Language.Haskell.Liquid.Types.PrettyPrint ()
import Language.Haskell.Liquid.Types.Types
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 = Config -> Mode (CmdArgs Config)
forall a. Data a => a -> Mode (CmdArgs a)
cmdArgsMode Config
defConfig

defConfig :: Config
defConfig :: Config
defConfig = Config {
  loggingVerbosity :: Verbosity
loggingVerbosity
    = [Verbosity] -> Verbosity
forall val. Data val => [val] -> val
enum [ Verbosity
Minimal      Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"minimal" Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Minimal logging verbosity"
           , Verbosity
Quiet        Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"quiet"   Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Silent logging verbosity"
           , Verbosity
Normal       Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"normal"  Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Normal logging verbosity"
           , Verbosity
Loud         Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"verbose" Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Verbose logging"
           ]

 , fullcheck :: Bool
fullcheck
     = Bool
forall a. Default a => a
def
           Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Full Checking: check all binders (DEFAULT)"

 , diffcheck :: Bool
diffcheck
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Incremental Checking: only check changed binders"

 , higherorder :: Bool
higherorder
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow higher order binders into the logic"

 , smtTimeout :: Maybe Int
smtTimeout
    = Maybe Int
forall a. Default a => a
def
          Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Timeout of smt queries in msec"

 , higherorderqs :: Bool
higherorderqs
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow higher order qualifiers to get automatically instantiated"

 , linear :: Bool
linear
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use uninterpreted integer multiplication and division"

 , stringTheory :: Bool
stringTheory
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Interpretation of Strings by z3"

 , saveQuery :: Bool
saveQuery
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Save fixpoint query to file (slow)"

 , checks :: [String]
checks
    = [String]
forall a. Default a => a
def [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Check a specific (top-level) binder"
          [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"check-var"

 , pruneUnsorted :: Bool
pruneUnsorted
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable prunning unsorted Predicates"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"prune-unsorted"

 , notermination :: Bool
notermination
    = Bool
False
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Termination Check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-termination-check"

 , nopositivity :: Bool
nopositivity
    = Bool
False
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Data Type Positivity Check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-positivity-check"

 , rankNTypes :: Bool
rankNTypes
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Adds precise reasoning on presence of rankNTypes"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"rankNTypes"

 , noclasscheck :: Bool
noclasscheck
    = Bool
False
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Class Instance Check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-class-check"

 , nostructuralterm :: Bool
nostructuralterm
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-structural-termination"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable structural termination check"

 , bscope :: Bool
bscope
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"scope of the outer binders on the inner refinements"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"bscope"

 , totalHaskell :: Bool
totalHaskell
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Check for termination and totality; overrides no-termination flags"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"total-Haskell"

 , nowarnings :: Bool
nowarnings
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't display warnings, only show errors"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-warnings"

 , noannotations :: Bool
noannotations
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't create intermediate annotation files"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-annotations"

 , checkDerived :: Bool
checkDerived
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Check GHC generated binders (e.g. Read, Show instances)"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"check-derived"

 , caseExpandDepth :: Int
caseExpandDepth
    = Int
2   Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum depth at which to expand DEFAULT in case-of (default=2)"
          Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"max-case-expand"

 , notruetypes :: Bool
notruetypes
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable Trueing Top Level Types"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-true-types"

 , nototality :: Bool
nototality
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable totality check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-totality"

 , cores :: Maybe Int
cores
    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1 Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use the given number of cores to solve logical constraints (default: 1). Warning: unpredictable performance. See https://github.com/ucsd-progsys/liquidhaskell/issues/2562"

 , minPartSize :: Int
minPartSize
    = Int
FC.defaultMinPartSize
    Int -> Ann -> Int
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
    Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help (String
"If solving on multiple cores, once there are as many partitions " String -> String -> String
forall a. [a] -> [a] -> [a]
++
             String
"as there are cores, don't merge partitions if they will exceed this " String -> String -> String
forall a. [a] -> [a] -> [a]
++
             String
"size. Overrides the minpartsize option.")

 , smtsolver :: Maybe SMTSolver
smtsolver
    = Maybe SMTSolver
forall a. Maybe a
Nothing Maybe SMTSolver -> Ann -> Maybe SMTSolver
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Name of SMT-Solver"

 , noCheckUnknown :: Bool
noCheckUnknown
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-check-unknown"
          Bool -> Ann -> Bool
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 Int -> Ann -> Int
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
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"short-names"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print shortened names, i.e. drop all module qualifiers."

 , shortErrors :: Bool
shortErrors
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"short-errors"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't show long error messages, just line numbers."

 , adtSpec :: Bool
adtSpec
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Generate ADT representations in refinement logic"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"adt"

 , expectErrorContaining :: [String]
expectErrorContaining
    = [] [String] -> Ann -> [String]
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)"
          [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"expect-error-containing"

 , expectAnyError :: Bool
expectAnyError
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Expect an error, no matter which kind or what it contains"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"expect-any-error"

 , scrapeInternals :: Bool
scrapeInternals
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Scrape qualifiers from auto generated specifications"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"scrape-internals"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit

 , elimStats :: Bool
elimStats
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"elimStats"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print eliminate stats"

 , elimBound :: Maybe Int
elimBound
    = Maybe Int
forall a. Maybe a
Nothing
            Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"elimBound"
            Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum chain length for eliminating KVars"

 , noslice :: Bool
noslice
    = Bool
False
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"noSlice"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable non-concrete KVar slicing"

 , noLiftedImport :: Bool
noLiftedImport
    = Bool
False
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-lifted-imports"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Disable loading lifted specifications (for legacy libs)"

 , json :: Bool
json
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"json"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Print results in JSON (for editor integration)"

 , counterExamples :: Bool
counterExamples
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"counter-examples"
            Bool -> Ann -> Bool
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 Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"time-binds"
            Bool -> Ann -> Bool
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 Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"untidy-core"
            Bool -> Ann -> Bool
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
            Eliminate -> Ann -> Eliminate
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"eliminate"
            Eliminate -> Ann -> 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 Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-pattern-inline"
            Bool -> Ann -> Bool
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 Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-simplify-core"
            Bool -> Ann -> Bool
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
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Proof-by-Logical-Evaluation"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ple"

  , pleWithUndecidedGuards :: Bool
pleWithUndecidedGuards
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Unfold invocations with undecided guards in PLE"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ple-with-undecided-guards"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit

  , interpreter :: Bool
interpreter
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use an interpreter to assist PLE in solving constraints"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"interpreter"

  , proofLogicEvalLocal :: Bool
proofLogicEvalLocal
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Proof-by-Logical-Evaluation locally, per function"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ple-local"

  , etabeta :: Bool
etabeta
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Eta expand and beta reduce terms to aid PLE"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"etabeta"

  , dependantCase :: Bool
dependantCase
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow PLE to reason about dependent cases"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"dependantcase"

  , extensionality :: Bool
extensionality
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable extensional interpretation of function equality"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"extensionality"

  , nopolyinfer :: Bool
nopolyinfer
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"No inference of polymorphic type application. Gives imprecision, but speedup."
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"fast"

  , reflection :: Bool
reflection
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable reflection of Haskell functions and theorem proving"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"reflection"

  , compileSpec :: Bool
compileSpec
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"compile-spec"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Only compile specifications (into .bspec file); skip verification"

  , typeclass :: Bool
typeclass
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable Typeclass"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"typeclass"
  , auxInline :: Bool
auxInline
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable inlining of class methods"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"aux-inline"
  ,
    rwTerminationCheck :: Bool
rwTerminationCheck
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"rw-termination-check"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help (   String
"Enable the rewrite divergence checker. "
                 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Can speed up verification if rewriting terminates, but can also cause divergence."
                )
  ,
    skipModule :: Bool
skipModule
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"skip-module"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Completely skip this module, don't even compile any specifications in it."

  , fuel :: Maybe Int
fuel
    = Maybe Int
forall a. Maybe a
Nothing
        Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Maximum fuel (per-function unfoldings) for PLE"

  , environmentReduction :: Bool
environmentReduction
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"environment-reduction"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"perform environment reduction (disabled by default)"
  , noEnvironmentReduction :: Bool
noEnvironmentReduction
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-environment-reduction"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't perform environment reduction"
  , inlineANFBindings :: Bool
inlineANFBindings
    = Bool
False
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"inline-anf-bindings"
        Bool -> Ann -> Bool
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
      Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"pandoc-html"
      Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use pandoc to generate html."
  , excludeAutomaticAssumptionsFor :: [String]
excludeAutomaticAssumptionsFor
    = []
      [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= Ann
explicit
      [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"exclude-automatic-assumptions-for"
      [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Stop loading LHAssumptions modules for imports in these packages."
      [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
typ String
"PACKAGE"
  , dumpOpaqueReflections :: Bool
dumpOpaqueReflections
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Dump all generated opaque reflections"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"dump-opaque-reflections"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
  , dumpPreNormalizedCore :: Bool
dumpPreNormalizedCore
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Dump pre-normalized core (before a-normalization)"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"dump-pre-normalized-core"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
  , dumpNormalizedCore :: Bool
dumpNormalizedCore
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Dump a-normalized core"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"dump-normalized-core"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
  , allowUnsafeConstructors :: Bool
allowUnsafeConstructors
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Allow refining constructors with unsafe refinements"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"allow-unsafe-constructors"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
  , ddumpTimings :: Bool
ddumpTimings
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Dump time measures of the Liquid Haskell plugin"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"ddump-timings"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
  , modern :: Bool
modern
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Enable modern features; enables --reflection, --ple, --etabeta, --dependantcase"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"modern"
  , warnOnTermHoles :: Bool
warnOnTermHoles
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Warn about holes in terms"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"warn-on-term-holes"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit
  } Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
program String
"liquidhaskell"
    Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
help    String
"Refinement Types for Haskell"
    Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
summary String
copyright
    Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= [String] -> Ann
details [ String
"LiquidHaskell is a Refinement Type based verifier for Haskell" ]

getOpts :: [String] -> IO Config
getOpts :: [String] -> IO Config
getOpts [String]
as = do
  cfg0   <- IO Config
envCfg
  cfg1   <- cmdArgsRun'
              config { modeValue = (modeValue config)
                                      { cmdArgsValue   = cfg0 }
                     }
                     as
  let cfg2 = if Config -> Bool
json Config
cfg1 then Config
cfg1 {loggingVerbosity = Quiet} else Config
cfg1
  setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg2)
  withSmtSolver cfg2

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) IO () -> IO a -> IO a
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO a
forall a. IO a
exitFailure
      Right CmdArgs a
a -> CmdArgs a -> IO a
forall a. CmdArgs a -> IO a
cmdArgsApply CmdArgs a
a
    where
      helpMsg :: String -> String
helpMsg String
e = TextFormat -> [Text] -> String
showText TextFormat
defaultWrap ([Text] -> String) -> [Text] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> HelpFormat -> Mode (CmdArgs a) -> [Text]
forall a. [String] -> HelpFormat -> Mode a -> [Text]
helpText [String
e] HelpFormat
HelpFormatDefault Mode (CmdArgs a)
md
      parseResult :: Either String (CmdArgs a)
parseResult = Mode (CmdArgs a) -> [String] -> Either String (CmdArgs a)
forall a. Mode a -> [String] -> Either String a
process Mode (CmdArgs a)
md ([String] -> [String]
wideHelp [String]
as)
      wideHelp :: [String] -> [String]
wideHelp = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
a -> if String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"--help" Bool -> Bool -> Bool
|| String
a String -> String -> Bool
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 found <- SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver SMTSolver
smt
                   case found of
                     Just SMTSolver
_ -> Config -> IO Config
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Config
cfg
                     Maybe SMTSolver
Nothing -> Maybe SrcSpan -> String -> IO Config
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (SMTSolver -> String
forall {a}. Show a => a -> String
missingSmtError SMTSolver
smt)
    Maybe SMTSolver
Nothing  -> do smts <- (SMTSolver -> IO (Maybe SMTSolver))
-> [SMTSolver] -> IO [Maybe SMTSolver]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver [SMTSolver]
smtLookupOrder
                   case catMaybes smts of
                     (SMTSolver
s:[SMTSolver]
_) -> Config -> IO Config
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Config
cfg {smtsolver = Just s})
                     [SMTSolver]
_     -> Maybe SrcSpan -> String -> IO Config
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
noSmtError
  where
    smtLookupOrder :: [SMTSolver]
smtLookupOrder = [SMTSolver
FC.Z3, SMTSolver
FC.Cvc5, SMTSolver
FC.Cvc4, SMTSolver
FC.Mathsat]
    noSmtError :: String
noSmtError = String
"LiquidHaskell requires one of the following SMT solvers to be installed: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (SMTSolver -> String
forall {a}. Show a => a -> String
show (SMTSolver -> String) -> [SMTSolver] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SMTSolver]
smtLookupOrder) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
    missingSmtError :: a -> String
missingSmtError a
smt = String
"Could not find SMT solver '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Show a => a -> String
show a
smt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Is it on your PATH?"

findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver)
findSmtSolver :: SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver = \case
    SMTSolver
FC.Z3mem -> Maybe SMTSolver -> IO (Maybe SMTSolver)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SMTSolver -> IO (Maybe SMTSolver))
-> Maybe SMTSolver -> IO (Maybe SMTSolver)
forall a b. (a -> b) -> a -> b
$ SMTSolver -> Maybe SMTSolver
forall a. a -> Maybe a
Just SMTSolver
FC.Z3mem
    SMTSolver
smt      -> Maybe SMTSolver
-> (String -> Maybe SMTSolver) -> Maybe String -> Maybe SMTSolver
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe SMTSolver
forall a. Maybe a
Nothing (Maybe SMTSolver -> String -> Maybe SMTSolver
forall a b. a -> b -> a
const (Maybe SMTSolver -> String -> Maybe SMTSolver)
-> Maybe SMTSolver -> String -> Maybe SMTSolver
forall a b. (a -> b) -> a -> b
$ SMTSolver -> Maybe SMTSolver
forall a. a -> Maybe a
Just SMTSolver
smt) (Maybe String -> Maybe SMTSolver)
-> IO (Maybe String) -> IO (Maybe SMTSolver)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO (Maybe String)
findExecutable (SMTSolver -> String
forall {a}. Show a => a -> String
show SMTSolver
smt)

envCfg :: IO Config
envCfg :: IO Config
envCfg = do
  so <- String -> IO (Maybe String)
lookupEnv String
"LIQUIDHASKELL_OPTS"
  case so of
    Maybe String
Nothing -> Config -> IO Config
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Config
defConfig
    Just String
s  -> Located String -> IO Config
parsePragma (Located String -> IO Config) -> Located String -> IO Config
forall a b. (a -> b) -> a -> b
$ String -> Located String
forall {a}. a -> Located a
envLoc String
s
  where
    envLoc :: a -> Located a
envLoc  = SourcePos -> SourcePos -> a -> Located a
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 = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
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 = [String] -> String
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
"] "
  ]


--------------------------------------------------------------------------------
-- | Updating options
--------------------------------------------------------------------------------
canonConfig :: Config -> Config
canonConfig :: Config -> Config
canonConfig Config
cfg = Config
cfg
  { diffcheck   = diffcheck cfg && not (fullcheck cfg)
  -- , eliminate   = if higherOrderFlag cfg then FC.All else eliminate cfg
  -- The "modern" flag is a sort of "super flag" which enables a bunch of
  -- features at once.
  , proofLogicEval = modern cfg || proofLogicEval cfg
  , etabeta        = modern cfg || etabeta cfg
  , dependantCase  = modern cfg || dependantCase cfg
  -- Technically those are patched in the `lookup` functions in `Congigs.hs` but
  -- it is better to be explicit here.
  , reflection     = modern cfg || reflection cfg
  }

--------------------------------------------------------------------------------
withPragmas :: MonadIO m => Config -> [Located String] -> (Config -> m a) -> m a
--------------------------------------------------------------------------------
withPragmas :: forall (m :: * -> *) a.
MonadIO m =>
Config -> [Located String] -> (Config -> m a) -> m a
withPragmas Config
cfg [Located String]
ps Config -> m a
action
  = do cfg' <- IO Config -> m Config
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Config -> m Config) -> IO Config -> m Config
forall a b. (a -> b) -> a -> b
$ Config -> [Located String] -> IO Config
processPragmas Config
cfg [Located String]
ps IO Config -> (Config -> Config) -> IO Config
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.
       liftIO $ setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg')
       res <- action cfg'
       liftIO $ setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg) -- restore the original verbosity.
       pure res

processPragmas :: Config -> [Located String] -> IO Config
processPragmas :: Config -> [Located String] -> IO Config
processPragmas Config
c [Located String]
pragmas =
    Mode (CmdArgs Config) -> [String] -> IO (CmdArgs Config)
forall a. Mode a -> [String] -> IO a
processValueIO
      Mode (CmdArgs Config)
config { modeValue = (modeValue config) { cmdArgsValue = c } }
      (Located String -> String
forall a. Located a -> a
val (Located String -> String) -> [Located String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located String]
pragmas)
    IO (CmdArgs Config) -> (CmdArgs Config -> IO Config) -> IO Config
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      CmdArgs Config -> IO Config
forall a. CmdArgs a -> IO a
cmdArgsApply

-- | Note that this function doesn't process list arguments properly, like
-- '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 ([Located String] -> IO Config)
-> (Located String -> [Located String])
-> Located String
-> IO Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located String -> [Located String] -> [Located String]
forall a. a -> [a] -> [a]
:[])

-- | 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
  annm <- {-# SCC "annotate" #-} IO AnnMap -> m AnnMap
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AnnMap -> m AnnMap) -> IO AnnMap -> m AnnMap
forall a b. (a -> b) -> a -> b
$ Config -> [String] -> Output Doc -> IO AnnMap
annotate Config
cfg [String]
targets Output Doc
out
  liftIO $ when (loggingVerbosity cfg >= Normal) $ F.donePhase F.Loud "annotate"
  if json cfg then
    liftIO $ reportResultJson annm
   else do
         let r = Output Doc -> ErrorResult
forall a. Output a -> ErrorResult
o_result Output Doc
out
         liftIO $ writeCheckVars $ o_vars out
         cr <- liftIO $ resultWithContext r
         let outputResult = Tidy -> FixResult (CtxError Doc) -> OutputResult
resDocs Tidy
tidy FixResult (CtxError Doc)
cr
         -- For now, always print the \"header\" with colours, irrespective to the logger
         -- passed as input.
         when (loggingVerbosity cfg >= Minimal) $
             liftIO $ printHeader (colorResult r) (orHeader outputResult)
         logResultFull outputResult
  where
    tidy :: F.Tidy
    tidy :: Tidy
tidy = if Config -> Bool
shortErrors Config
cfg then Tidy
F.Lossy else Tidy
F.Full

    printHeader :: F.Moods -> Doc -> IO ()
    printHeader :: Moods -> Doc -> IO ()
printHeader Moods
mood Doc
d = Moods -> String -> String -> IO ()
F.colorPhaseLn Moods
mood String
"" (Doc -> String
render Doc
d)


reportResultJson :: ACSS.AnnMap -> IO ()
reportResultJson :: AnnMap -> IO ()
reportResultJson AnnMap
annm = do
  String -> IO ()
putStrLn String
"LIQUID"
  ByteString -> IO ()
B.putStrLn (ByteString -> IO ()) -> (AnnMap -> ByteString) -> AnnMap -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnErrors -> ByteString
forall a. ToJSON a => a -> ByteString
encode (AnnErrors -> ByteString)
-> (AnnMap -> AnnErrors) -> AnnMap -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnMap -> AnnErrors
annErrors (AnnMap -> IO ()) -> AnnMap -> IO ()
forall a b. (a -> b) -> a -> b
$ AnnMap
annm

resultWithContext :: F.FixResult UserError -> IO (FixResult CError)
resultWithContext :: ErrorResult -> IO (FixResult (CtxError Doc))
resultWithContext (F.Unsafe Stats
s [TError Doc]
es)  = Stats -> [CtxError Doc] -> FixResult (CtxError Doc)
forall a. Stats -> [a] -> FixResult a
F.Unsafe Stats
s    ([CtxError Doc] -> FixResult (CtxError Doc))
-> IO [CtxError Doc] -> IO (FixResult (CtxError Doc))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TError Doc] -> IO [CtxError Doc]
errorsWithContext [TError Doc]
es
resultWithContext (F.Safe   Stats
stats) = FixResult (CtxError Doc) -> IO (FixResult (CtxError Doc))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Stats -> FixResult (CtxError Doc)
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) = [(TError Doc, Maybe String)] -> ([TError Doc], [Maybe String])
forall a b. [(a, b)] -> ([a], [b])
unzip [(TError Doc, Maybe String)]
es
  errs' <- [TError Doc] -> IO [CtxError Doc]
errorsWithContext [TError Doc]
userErrs
  return (F.Crash (zip errs' msgs) s)




instance Show (CtxError Doc) where
  show :: CtxError Doc -> String
show = CtxError Doc -> String
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    = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
writeCheckVars (Just [])   = Moods -> String -> String -> IO ()
F.colorPhaseLn Moods
F.Loud String
"Checked Binders: None" String
""
writeCheckVars (Just [a]
ns)   = Moods -> String -> String -> IO ()
F.colorPhaseLn Moods
F.Loud String
"Checked Binders:" String
""
                          IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [a] -> (a -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [a]
ns (String -> IO ()
putStrLn (String -> IO ()) -> (a -> String) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
symbolString (Symbol -> String) -> (a -> Symbol) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> (a -> Symbol) -> a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
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
  [(SrcSpan, Doc)] -> ((SrcSpan, Doc) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SrcSpan, Doc)]
messages (((SrcSpan, Doc) -> IO ()) -> IO ())
-> ((SrcSpan, Doc) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(SrcSpan
sSpan, Doc
doc) -> String -> IO ()
putStrLn (Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc
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 ...
  (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
sSpan Doc -> Doc -> Doc
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 (CtxError Doc) -> OutputResult
resDocs Tidy
_ (F.Safe  Stats
stats) =
  OutputResult {
    orHeader :: Doc
orHeader   = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"LIQUID: SAFE (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall {a}. Show a => a -> String
show (Stats -> Int
Solver.numChck Stats
stats) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" constraints checked)"
  , orMessages :: [(SrcSpan, Doc)]
orMessages = [(SrcSpan, Doc)]
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 [(CtxError Doc, 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 = ((CtxError Doc, Maybe String) -> (SrcSpan, Doc))
-> [(CtxError Doc, Maybe String)] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CtxError Doc -> (SrcSpan, Doc)
cErrToSpanned Tidy
k (CtxError Doc -> (SrcSpan, Doc))
-> ((CtxError Doc, Maybe String) -> CtxError Doc)
-> (CtxError Doc, Maybe String)
-> (SrcSpan, Doc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CtxError Doc, Maybe String) -> CtxError Doc
errToFCrash) [(CtxError Doc, Maybe String)]
xs
  }
resDocs Tidy
k (F.Unsafe Stats
stats [CtxError Doc]
xs)   =
  OutputResult {
    orHeader :: Doc
orHeader   = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"LIQUID: UNSAFE (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall {a}. Show a => a -> String
show (Stats -> Int
Solver.numChck Stats
stats) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" constraints checked)"
  , orMessages :: [(SrcSpan, Doc)]
orMessages = (CtxError Doc -> (SrcSpan, Doc))
-> [CtxError Doc] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CtxError Doc -> (SrcSpan, Doc)
cErrToSpanned Tidy
k) ([CtxError Doc] -> [CtxError Doc]
forall a. Eq a => [a] -> [a]
nub [CtxError Doc]
xs)
  }

-- | Renders a 'CError' into a 'Doc' and its associated 'SrcSpan'.
cErrToSpanned :: F.Tidy -> CError -> (GHC.SrcSpan, Doc)
cErrToSpanned :: Tidy -> CtxError Doc -> (SrcSpan, Doc)
cErrToSpanned Tidy
k CtxError{TError Doc
ctErr :: TError Doc
ctErr :: forall t. CtxError t -> TError t
ctErr} = (TError Doc -> SrcSpan
forall t. TError t -> SrcSpan
pos TError Doc
ctErr, Tidy -> TError Doc -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k TError Doc
ctErr)

errToFCrash :: (CError, Maybe String) -> CError
errToFCrash :: (CtxError Doc, Maybe String) -> CtxError Doc
errToFCrash (CtxError Doc
ce, Just String
msg) = CtxError Doc
ce { ctErr = ErrOther (pos (ctErr ce)) (fixMessageDoc msg) }
errToFCrash (CtxError Doc
ce, Maybe String
Nothing)  = CtxError Doc
ce { ctErr = tx $ ctErr ce}
  where
    tx :: TError t -> TError t
tx (ErrSubType SrcSpan
l Doc
m Maybe Integer
_ HashMap Symbol t
g t
t t
t') = SrcSpan -> Doc -> HashMap Symbol t -> t -> t -> TError 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                         = String -> TError t -> TError t
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 (String -> Doc) -> [String] -> [Doc]
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      = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s [a]
errors
addErrors (Unsafe Stats
s [a]
xs) [a]
errors = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
errors)
addErrors FixResult a
r  [a]
_                 = FixResult a
r

instance Fixpoint (F.FixResult CError) where
  toFix :: FixResult (CtxError Doc) -> Doc
toFix = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (FixResult (CtxError Doc) -> [Doc])
-> FixResult (CtxError Doc)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SrcSpan, Doc) -> Doc) -> [(SrcSpan, Doc)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SrcSpan, Doc) -> Doc
forall a b. (a, b) -> b
snd ([(SrcSpan, Doc)] -> [Doc])
-> (FixResult (CtxError Doc) -> [(SrcSpan, Doc)])
-> FixResult (CtxError Doc)
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputResult -> [(SrcSpan, Doc)]
orMessages (OutputResult -> [(SrcSpan, Doc)])
-> (FixResult (CtxError Doc) -> OutputResult)
-> FixResult (CtxError Doc)
-> [(SrcSpan, Doc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> FixResult (CtxError Doc) -> OutputResult
resDocs Tidy
F.Full