{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE NamedFieldPuns            #-}
{-# LANGUAGE MultiWayIf                #-}
{-# LANGUAGE ViewPatterns              #-}
{-# OPTIONS_GHC -fno-cse #-}

-- | 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.Aeson (encode)
import qualified Data.ByteString.Lazy.Char8 as B
import Development.GitRev (gitCommitCount)
import Options.Applicative.Simple (simpleVersion)
import qualified Paths_liquidhaskell 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.GHC.Misc
import Language.Haskell.Liquid.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 Language.Haskell.Liquid.GHC.API as GHC


import Text.Parsec.Pos                     (newPos)
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 -> Mode (CmdArgs Config))
-> Config -> Mode (CmdArgs Config)
forall a b. (a -> b) -> a -> b
$ Config :: Verbosity
-> [FilePath]
-> [FilePath]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Bool
-> Bool
-> [FilePath]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Int
-> Int
-> Int
-> Maybe SMTSolver
-> Bool
-> Bool
-> Bool
-> [FilePath]
-> [FilePath]
-> Eliminate
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Int
-> Maybe Int
-> Bool
-> Config
Config {
  loggingVerbosity :: Verbosity
loggingVerbosity
    = [Verbosity] -> Verbosity
forall val. Data val => [val] -> val
enum [ Verbosity
Quiet        Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"quiet"   Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Minimal logging verbosity"
           , Verbosity
Normal       Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"normal"  Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Normal logging verbosity"
           , Verbosity
CmdArgs.Loud Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"verbose" Verbosity -> Ann -> Verbosity
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Verbose logging"
           ]

 , files :: [FilePath]
files
    = [FilePath]
forall a. Default a => a
def [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
typ FilePath
"TARGET"
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= Ann
args
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= Ann
typFile

 , idirs :: [FilePath]
idirs
    = [FilePath]
forall a. Default a => a
def [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= Ann
typDir
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Paths to Spec Include Directory "

 , fullcheck :: Bool
fullcheck
     = Bool
forall a. Default a => a
def
           Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"Save fixpoint query to file (slow)"

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

 , pruneUnsorted :: Bool
pruneUnsorted
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Disable prunning unsorted Predicates"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"prune-unsorted"

 , notermination :: Bool
notermination
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Disable Termination Check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"no-termination-check"

 , rankNTypes :: Bool
rankNTypes
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Adds precise reasoning on presence of rankNTypes"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"rankNTypes"

 , noclasscheck :: Bool
noclasscheck
    = Bool
forall a. Default a => a
def
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Disable Class Instance Check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"no-class-check"

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

 , gradual :: Bool
gradual
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Enable gradual refinement type checking"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"gradual"

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

 , gdepth :: Int
gdepth
    = Int
1
    Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help (FilePath
"Size of gradual conretizations, 1 by default")
    Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"gradual-depth"

 , ginteractive :: Bool
ginteractive
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Interactive Gradual Solving"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"ginteractive"

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

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

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

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

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

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

 , nototality :: Bool
nototality
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Disable totality check"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"no-totality"

 , cores :: Maybe Int
cores
    = Maybe Int
forall a. Default a => a
def Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Use m cores to solve logical constraints"

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

 , smtsolver :: Maybe SMTSolver
smtsolver
    = Maybe SMTSolver
forall a. Default a => a
def Maybe SMTSolver -> Ann -> Maybe SMTSolver
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
name FilePath
"no-check-unknown"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
help FilePath
"Restrict qualifier mining to those taking at most `m' parameters (2 by default)"

 , shortNames :: Bool
shortNames
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"short-names"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Print shortened names, i.e. drop all module qualifiers."

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

 , cabalDir :: Bool
cabalDir
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"cabal-dir"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Find and use .cabal to add paths to sources for imported files"

 , ghcOptions :: [FilePath]
ghcOptions
    = [FilePath]
forall a. Default a => a
def [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"ghc-option"
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
typ FilePath
"OPTION"
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Pass this option to GHC"

 , cFiles :: [FilePath]
cFiles
    = [FilePath]
forall a. Default a => a
def [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"c-files"
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
typ FilePath
"OPTION"
          [FilePath] -> Ann -> [FilePath]
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Tell GHC to compile and link against these files"

 , port :: Int
port
     = Int
defaultPort
          Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"port"
          Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Port at which lhi should listen"

 , exactDC :: Bool
exactDC
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Exact Type for Data Constructors"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"exact-data-cons"

 , noADT :: Bool
noADT
    = Bool
forall a. Default a => a
def Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Do not generate ADT representations in refinement logic"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"no-adt"

 , scrapeImports :: Bool
scrapeImports
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Scrape qualifiers from imported specifications"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"scrape-imports"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= Ann
explicit

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

 , scrapeUsedImports :: Bool
scrapeUsedImports
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Scrape qualifiers from used, imported specifications"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"scrape-used-imports"
            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
&= FilePath -> Ann
name FilePath
"elimStats"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
name FilePath
"elimBound"
            Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Maximum chain length for eliminating KVars"

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

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

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

 , counterExamples :: Bool
counterExamples
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"counter-examples"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Attempt to generate counter-examples to type errors (experimental!)"

 , timeBinds :: Bool
timeBinds
    = Bool
False Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"time-binds"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
name FilePath
"untidy-core"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Print fully qualified identifier names in verbose mode"

  , eliminate :: Eliminate
eliminate
    = Eliminate
FC.Some
            Eliminate -> Ann -> Eliminate
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"eliminate"
            Eliminate -> Ann -> Eliminate
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
name FilePath
"no-pattern-inline"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
&= FilePath -> Ann
name FilePath
"no-simplify-core"
            Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"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
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Enable Proof-by-Logical-Evaluation"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"ple"

  , oldPLE :: Bool
oldPLE
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Enable Proof-by-Logical-Evaluation"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"oldple"

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

  , extensionality :: Bool
extensionality
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Enable extensional interpretation of function equality"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"extensionality"

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

  , reflection :: Bool
reflection
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Enable reflection of Haskell functions and theorem proving"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"reflection"

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

  , noCheckImports :: Bool
noCheckImports
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"no-check-imports"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Do not check the transitive imports; only check the target files."

  , typedHoles :: Bool
typedHoles
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"typed-holes"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Use (refinement) typed-holes [currently warns on '_x' variables]"
  , maxMatchDepth :: Int
maxMatchDepth
    = Int
forall a. Default a => a
def
        Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"max-match-depth"
        Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help FilePath
"Define the number of expressions to pattern match on (typed-holes must be on to use this flag)."
  , maxAppDepth :: Int
maxAppDepth
    = Int
forall a. Default a => a
def
        Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"max-app-depth"
  , maxArgsDepth :: Int
maxArgsDepth
    = Int
forall a. Default a => a
def
        Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"max-args-depth"
  ,
    maxRWOrderingConstraints :: Maybe Int
maxRWOrderingConstraints
    = Maybe Int
forall a. Default a => a
def
        Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"max-rw-ordering-constraints"
        Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help (   FilePath
"Maximium number of symbols to compare for rewrite termination. " 
                 FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Lower values can speedup verification, but rewriting may terminate prematurely. "
                 FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Leave empty to consider all symbols." )
  ,
    rwTerminationCheck :: Bool
rwTerminationCheck
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
name FilePath
"rw-termination-check"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help (   FilePath
"Enable the rewrite divergence checker. " 
                 FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Can speed up verification if rewriting terminates, but can also cause divergence."
                )
  } Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
program FilePath
"liquid"
    Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
help    FilePath
"Refinement Types for Haskell"
    Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= FilePath -> Ann
summary FilePath
copyright
    Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= [FilePath] -> Ann
details [ FilePath
"LiquidHaskell is a Refinement Type based verifier for Haskell"
               , FilePath
""
               , FilePath
"To check a Haskell file foo.hs, type:"
               , FilePath
"  liquid foo.hs "
               ]

defaultPort :: Int
defaultPort :: Int
defaultPort = Int
3000

getOpts :: [String] -> IO Config
getOpts :: [FilePath] -> IO Config
getOpts [FilePath]
as = do
  Config
cfg0   <- IO Config
envCfg
  Config
cfg1   <- Config -> IO Config
mkOpts (Config -> IO Config) -> IO Config -> IO Config
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Mode (CmdArgs Config) -> [FilePath] -> IO Config
forall a. Mode (CmdArgs a) -> [FilePath] -> IO a
cmdArgsRun'
                         Mode (CmdArgs Config)
config { modeValue :: CmdArgs Config
modeValue = (Mode (CmdArgs Config) -> CmdArgs Config
forall a. Mode a -> a
modeValue Mode (CmdArgs Config)
config)
                                                { cmdArgsValue :: Config
cmdArgsValue   = Config
cfg0
                                                }
                                }
                         [FilePath]
as
  Config
cfg    <- Config -> IO Config
fixConfig Config
cfg1
  Verbosity -> IO ()
setVerbosity (Config -> Verbosity
loggingVerbosity Config
cfg)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
json Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
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 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn FilePath
copyright

cmdArgsRun' :: Mode (CmdArgs a) -> [String] -> IO a
cmdArgsRun' :: Mode (CmdArgs a) -> [FilePath] -> IO a
cmdArgsRun' Mode (CmdArgs a)
md [FilePath]
as
  = case Either FilePath (CmdArgs a)
parseResult of
      Left FilePath
e  -> FilePath -> IO ()
putStrLn (FilePath -> FilePath
helpMsg FilePath
e) IO () -> IO a -> IO a
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 :: FilePath -> FilePath
helpMsg FilePath
e = TextFormat -> [Text] -> FilePath
showText TextFormat
defaultWrap ([Text] -> FilePath) -> [Text] -> FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> HelpFormat -> Mode (CmdArgs a) -> [Text]
forall a. [FilePath] -> HelpFormat -> Mode a -> [Text]
helpText [FilePath
e] HelpFormat
HelpFormatDefault Mode (CmdArgs a)
md
      parseResult :: Either FilePath (CmdArgs a)
parseResult = Mode (CmdArgs a) -> [FilePath] -> Either FilePath (CmdArgs a)
forall a. Mode a -> [FilePath] -> Either FilePath a
process Mode (CmdArgs a)
md ([FilePath] -> [FilePath]
wideHelp [FilePath]
as)
      wideHelp :: [FilePath] -> [FilePath]
wideHelp = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (\FilePath
a -> if FilePath
a FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"--help" Bool -> Bool -> Bool
|| FilePath
a FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"-help" then FilePath
"--help=120" else FilePath
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
_ -> Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return Config
cfg
                     Maybe SMTSolver
Nothing -> Maybe SrcSpan -> FilePath -> IO Config
forall a. Maybe SrcSpan -> FilePath -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (SMTSolver -> FilePath
forall a. Show a => a -> FilePath
missingSmtError SMTSolver
smt)
    Maybe SMTSolver
Nothing  -> do [Maybe SMTSolver]
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)
mapM SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver [SMTSolver
FC.Z3, SMTSolver
FC.Cvc4, SMTSolver
FC.Mathsat]
                   case [Maybe SMTSolver] -> [SMTSolver]
forall a. [Maybe a] -> [a]
catMaybes [Maybe SMTSolver]
smts of
                     (SMTSolver
s:[SMTSolver]
_) -> Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return (Config
cfg {smtsolver :: Maybe SMTSolver
smtsolver = SMTSolver -> Maybe SMTSolver
forall a. a -> Maybe a
Just SMTSolver
s})
                     [SMTSolver]
_     -> Maybe SrcSpan -> FilePath -> IO Config
forall a. Maybe SrcSpan -> FilePath -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing FilePath
noSmtError
  where
    noSmtError :: FilePath
noSmtError = FilePath
"LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed."
    missingSmtError :: a -> FilePath
missingSmtError a
smt = FilePath
"Could not find SMT solver '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
smt FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"'. Is it on your PATH?"

findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver)
findSmtSolver :: SMTSolver -> IO (Maybe SMTSolver)
findSmtSolver SMTSolver
smt = Maybe SMTSolver
-> (FilePath -> Maybe SMTSolver)
-> Maybe FilePath
-> Maybe SMTSolver
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe SMTSolver
forall a. Maybe a
Nothing (Maybe SMTSolver -> FilePath -> Maybe SMTSolver
forall a b. a -> b -> a
const (Maybe SMTSolver -> FilePath -> Maybe SMTSolver)
-> Maybe SMTSolver -> FilePath -> Maybe SMTSolver
forall a b. (a -> b) -> a -> b
$ SMTSolver -> Maybe SMTSolver
forall a. a -> Maybe a
Just SMTSolver
smt) (Maybe FilePath -> Maybe SMTSolver)
-> IO (Maybe FilePath) -> IO (Maybe SMTSolver)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO (Maybe FilePath)
findExecutable (SMTSolver -> FilePath
forall a. Show a => a -> FilePath
show SMTSolver
smt)

fixConfig :: Config -> IO Config
fixConfig :: Config -> IO Config
fixConfig Config
cfg = do
  FilePath
pwd <- IO FilePath
getCurrentDirectory
  Config
cfg <- FilePath -> Config -> IO Config
canonicalizePaths FilePath
pwd Config
cfg
  Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> IO Config) -> Config -> IO Config
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 :: FilePath -> Config -> IO Config
canonicalizePaths FilePath
pwd Config
cfg = do
  FilePath
tgt   <- FilePath -> IO FilePath
canonicalizePath FilePath
pwd
  Bool
isdir <- FilePath -> IO Bool
doesDirectoryExist FilePath
tgt
  [FilePath]
is    <- (FilePath -> IO FilePath) -> [FilePath] -> IO [FilePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FilePath -> Bool -> FilePath -> IO FilePath
canonicalize FilePath
tgt Bool
isdir) ([FilePath] -> IO [FilePath]) -> [FilePath] -> IO [FilePath]
forall a b. (a -> b) -> a -> b
$ Config -> [FilePath]
idirs Config
cfg
  [FilePath]
cs    <- (FilePath -> IO FilePath) -> [FilePath] -> IO [FilePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FilePath -> Bool -> FilePath -> IO FilePath
canonicalize FilePath
tgt Bool
isdir) ([FilePath] -> IO [FilePath]) -> [FilePath] -> IO [FilePath]
forall a b. (a -> b) -> a -> b
$ Config -> [FilePath]
cFiles Config
cfg
  Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> IO Config) -> Config -> IO Config
forall a b. (a -> b) -> a -> b
$ Config
cfg { idirs :: [FilePath]
idirs = [FilePath]
is, cFiles :: [FilePath]
cFiles = [FilePath]
cs }

canonicalize :: FilePath -> Bool -> FilePath -> IO FilePath
canonicalize :: FilePath -> Bool -> FilePath -> IO FilePath
canonicalize FilePath
tgt Bool
isdir FilePath
f
  | FilePath -> Bool
isAbsolute FilePath
f = FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
f
  | Bool
isdir        = FilePath -> IO FilePath
canonicalizePath (FilePath
tgt FilePath -> FilePath -> FilePath
</> FilePath
f)
  | Bool
otherwise    = FilePath -> IO FilePath
canonicalizePath (FilePath -> FilePath
takeDirectory FilePath
tgt FilePath -> FilePath -> FilePath
</> FilePath
f)

envCfg :: IO Config
envCfg :: IO Config
envCfg = do
  Maybe FilePath
so <- FilePath -> IO (Maybe FilePath)
lookupEnv FilePath
"LIQUIDHASKELL_OPTS"
  case Maybe FilePath
so of
    Maybe FilePath
Nothing -> Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return Config
defConfig
    Just FilePath
s  -> Located FilePath -> IO Config
parsePragma (Located FilePath -> IO Config) -> Located FilePath -> IO Config
forall a b. (a -> b) -> a -> b
$ FilePath -> Located FilePath
forall a. a -> Located a
envLoc FilePath
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       = FilePath -> Int -> Int -> SourcePos
newPos FilePath
"ENVIRONMENT" Int
0 Int
0

copyright :: String
copyright :: FilePath
copyright = [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ [[FilePath]] -> [FilePath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [FilePath
"LiquidHaskell "]
  , [$(simpleVersion Meta.version)]
  , [FilePath
gitInfo]
  -- , [" (" ++ _commitCount ++ " commits)" | _commitCount /= ("1"::String) &&
  --                                          _commitCount /= ("UNKNOWN" :: String)]
  , [FilePath
"\nCopyright 2013-19 Regents of the University of California. All Rights Reserved.\n"]
  ]
  where
    _commitCount :: FilePath
_commitCount = FilePath
$gitCommitCount

gitInfo :: String
gitInfo :: FilePath
gitInfo  = FilePath
msg
  where
    giTry :: Either FilePath GitInfo
giTry  = FilePath
FilePath -> Either FilePath GitInfo
forall a b. a -> Either a b
$$tGitInfoCwdTry
    msg :: FilePath
msg    = case Either FilePath GitInfo
giTry of
               Left FilePath
_   -> FilePath
" no git information"
               Right GitInfo
gi -> GitInfo -> FilePath
gitMsg GitInfo
gi

gitMsg :: GitInfo -> String
gitMsg :: GitInfo -> FilePath
gitMsg GitInfo
gi = [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ FilePath
" [", GitInfo -> FilePath
giBranch GitInfo
gi, FilePath
"@", GitInfo -> FilePath
giHash GitInfo
gi
  , FilePath
" (", GitInfo -> FilePath
giCommitDate GitInfo
gi, FilePath
")"
  -- , " (", show (giCommitCount gi), " commits in HEAD)"
  , FilePath
"] "
  ]


-- [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' :: [FilePath]
files' = [FilePath] -> [FilePath]
forall a. Ord a => [a] -> [a]
sortNub ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ Config -> [FilePath]
files Config
cfg
  FilePath
id0       <- IO FilePath
getIncludeDir
  Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return     (Config -> IO Config) -> Config -> IO Config
forall a b. (a -> b) -> a -> b
$ Config
cfg { files :: [FilePath]
files       = [FilePath]
files'
                                   -- See NOTE [searchpath]
                   , idirs :: [FilePath]
idirs       = [FilePath
id0 FilePath -> FilePath -> FilePath
</> FilePath
gHC_VERSION, FilePath
id0]
                                [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ Config -> [FilePath]
idirs Config
cfg
                   }

--------------------------------------------------------------------------------
-- | 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 :: Config -> FilePath -> [Located String] -> IO Config
--------------------------------------------------------------------------------
withPragmas :: Config -> FilePath -> [Located FilePath] -> IO Config
withPragmas Config
cfg FilePath
fp [Located FilePath]
ps
  = (Config -> Located FilePath -> IO Config)
-> Config -> [Located FilePath] -> IO Config
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Config -> Located FilePath -> IO Config
withPragma Config
cfg [Located FilePath]
ps IO Config -> (Config -> IO Config) -> IO Config
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> Config -> IO Config
canonicalizePaths FilePath
fp IO Config -> (Config -> IO Config) -> IO Config
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Config -> IO Config
forall (m :: * -> *) a. Monad m => a -> m a
return (Config -> IO Config) -> (Config -> Config) -> Config -> IO Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Config
canonConfig)

withPragma :: Config -> Located String -> IO Config
withPragma :: Config -> Located FilePath -> IO Config
withPragma Config
c Located FilePath
s = [FilePath] -> IO Config -> IO Config
forall a. [FilePath] -> IO a -> IO a
withArgs [Located FilePath -> FilePath
forall a. Located a -> a
val Located FilePath
s] (IO Config -> IO Config) -> IO Config -> IO Config
forall a b. (a -> b) -> a -> b
$ Mode (CmdArgs Config) -> IO Config
forall a. Mode (CmdArgs a) -> IO a
cmdArgsRun
          Mode (CmdArgs Config)
config { modeValue :: CmdArgs Config
modeValue = (Mode (CmdArgs Config) -> CmdArgs Config
forall a. Mode a -> a
modeValue Mode (CmdArgs Config)
config) { cmdArgsValue :: Config
cmdArgsValue = Config
c } }

parsePragma   :: Located String -> IO Config
parsePragma :: Located FilePath -> IO Config
parsePragma = Config -> Located FilePath -> IO Config
withPragma Config
defConfig

defConfig :: Config
defConfig :: Config
defConfig = Config :: Verbosity
-> [FilePath]
-> [FilePath]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Bool
-> Bool
-> [FilePath]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Int
-> Int
-> Int
-> Maybe SMTSolver
-> Bool
-> Bool
-> Bool
-> [FilePath]
-> [FilePath]
-> Eliminate
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Int
-> Maybe Int
-> Bool
-> Config
Config
  { loggingVerbosity :: Verbosity
loggingVerbosity         = Verbosity
Quiet
  , files :: [FilePath]
files                    = [FilePath]
forall a. Default a => a
def
  , idirs :: [FilePath]
idirs                    = [FilePath]
forall a. Default a => a
def
  , fullcheck :: Bool
fullcheck                = Bool
forall a. Default a => a
def
  , linear :: Bool
linear                   = Bool
forall a. Default a => a
def
  , stringTheory :: Bool
stringTheory             = Bool
forall a. Default a => a
def
  , higherorder :: Bool
higherorder              = Bool
forall a. Default a => a
def
  , smtTimeout :: Maybe Int
smtTimeout               = Maybe Int
forall a. Default a => a
def
  , higherorderqs :: Bool
higherorderqs            = Bool
forall a. Default a => a
def
  , diffcheck :: Bool
diffcheck                = Bool
forall a. Default a => a
def
  , saveQuery :: Bool
saveQuery                = Bool
forall a. Default a => a
def
  , checks :: [FilePath]
checks                   = [FilePath]
forall a. Default a => a
def
  , nostructuralterm :: Bool
nostructuralterm         = Bool
forall a. Default a => a
def
  , noCheckUnknown :: Bool
noCheckUnknown           = Bool
forall a. Default a => a
def
  , notermination :: Bool
notermination            = 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             = Bool
forall a. Default a => a
def -- True
  , nowarnings :: Bool
nowarnings               = Bool
forall a. Default a => a
def
  , noannotations :: Bool
noannotations            = Bool
forall a. Default a => a
def
  , checkDerived :: Bool
checkDerived             = Bool
False
  , caseExpandDepth :: Int
caseExpandDepth          = Int
2
  , notruetypes :: Bool
notruetypes              = Bool
forall a. Default a => a
def
  , nototality :: Bool
nototality               = Bool
False
  , pruneUnsorted :: Bool
pruneUnsorted            = Bool
forall a. Default a => a
def
  , exactDC :: Bool
exactDC                  = Bool
forall a. Default a => a
def
  , noADT :: Bool
noADT                    = Bool
forall a. Default a => a
def
  , cores :: Maybe Int
cores                    = Maybe Int
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                = Maybe SMTSolver
forall a. Default a => a
def
  , shortNames :: Bool
shortNames               = Bool
forall a. Default a => a
def
  , shortErrors :: Bool
shortErrors              = Bool
forall a. Default a => a
def
  , cabalDir :: Bool
cabalDir                 = Bool
forall a. Default a => a
def
  , ghcOptions :: [FilePath]
ghcOptions               = [FilePath]
forall a. Default a => a
def
  , cFiles :: [FilePath]
cFiles                   = [FilePath]
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                = Maybe Int
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
  , oldPLE :: Bool
oldPLE                   = 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
  , typedHoles :: Bool
typedHoles               = Bool
False
  , maxMatchDepth :: Int
maxMatchDepth            = Int
4
  , maxAppDepth :: Int
maxAppDepth              = Int
2
  , maxArgsDepth :: Int
maxArgsDepth             = Int
1
  , maxRWOrderingConstraints :: Maybe Int
maxRWOrderingConstraints = Maybe Int
forall a. Maybe a
Nothing
  , rwTerminationCheck :: Bool
rwTerminationCheck       = Bool
False
  }


-- | Writes the annotations (i.e. the files in the \".liquid\" hidden folder) and report the result
-- of the checking using a supplied function.
reportResult :: MonadIO m
             => (OutputResult -> m ())
             -> Config
             -> [FilePath]
             -> Output Doc
             -> m ()
reportResult :: (OutputResult -> m ())
-> Config -> [FilePath] -> Output Doc -> m ()
reportResult OutputResult -> m ()
logResultFull Config
cfg [FilePath]
targets Output Doc
out = do
  AnnMap
annm <- {-# SCC "annotate" #-} IO AnnMap -> m AnnMap
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 -> [FilePath] -> Output Doc -> IO AnnMap
annotate Config
cfg [FilePath]
targets Output Doc
out
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenNormal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> FilePath -> IO ()
donePhase Moods
Loud FilePath
"annotate"
  if | Config -> Bool
json Config
cfg  -> IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ AnnMap -> IO ()
reportResultJson AnnMap
annm
     | Bool
otherwise -> do
         let r :: ErrorResult
r = Output Doc -> ErrorResult
forall a. Output a -> ErrorResult
o_result Output Doc
out
         IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Maybe [FilePath] -> IO ()
forall a. Symbolic a => Maybe [a] -> IO ()
writeCheckVars (Maybe [FilePath] -> IO ()) -> Maybe [FilePath] -> IO ()
forall a b. (a -> b) -> a -> b
$ Output Doc -> Maybe [FilePath]
forall a. Output a -> Maybe [FilePath]
o_vars Output Doc
out
         FixResult CError
cr <- IO (FixResult CError) -> m (FixResult CError)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (FixResult CError) -> m (FixResult CError))
-> IO (FixResult CError) -> m (FixResult CError)
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.
         IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Moods -> Doc -> IO ()
printHeader (ErrorResult -> Moods
forall a. FixResult a -> Moods
colorResult ErrorResult
r) (OutputResult -> Doc
orHeader OutputResult
outputResult)
         OutputResult -> m ()
logResultFull OutputResult
outputResult
  () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  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 -> FilePath -> FilePath -> IO ()
colorPhaseLn Moods
mood FilePath
"" (Doc -> FilePath
render Doc
d)


------------------------------------------------------------------------
exitWithResult :: Config -> [FilePath] -> Output Doc -> IO ()
------------------------------------------------------------------------
exitWithResult :: Config -> [FilePath] -> Output Doc -> IO ()
exitWithResult Config
cfg = (OutputResult -> IO ())
-> Config -> [FilePath] -> Output Doc -> IO ()
forall (m :: * -> *).
MonadIO m =>
(OutputResult -> m ())
-> Config -> [FilePath] -> Output Doc -> m ()
reportResult OutputResult -> IO ()
writeResultStdout Config
cfg

reportResultJson :: ACSS.AnnMap -> IO ()
reportResultJson :: AnnMap -> IO ()
reportResultJson AnnMap
annm = do
  FilePath -> IO ()
putStrLn FilePath
"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 CError)
resultWithContext (F.Unsafe Stats
s [UserError]
es)  = Stats -> [CError] -> FixResult CError
forall a. Stats -> [a] -> FixResult a
F.Unsafe Stats
s    ([CError] -> FixResult CError)
-> IO [CError] -> IO (FixResult CError)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UserError] -> IO [CError]
errorsWithContext [UserError]
es
resultWithContext (F.Crash  [UserError]
es FilePath
s)  = ([CError] -> FilePath -> FixResult CError
forall a. [a] -> FilePath -> FixResult a
`F.Crash` FilePath
s) ([CError] -> FixResult CError)
-> IO [CError] -> IO (FixResult CError)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UserError] -> IO [CError]
errorsWithContext [UserError]
es
resultWithContext (F.Safe   Stats
stats) = FixResult CError -> IO (FixResult CError)
forall (m :: * -> *) a. Monad m => a -> m a
return (Stats -> FixResult CError
forall a. Stats -> FixResult a
F.Safe Stats
stats)

instance Show (CtxError Doc) where
  show :: CError -> FilePath
show = CError -> FilePath
forall a. PPrint a => a -> FilePath
showpp

writeCheckVars :: Symbolic a => Maybe [a] -> IO ()
writeCheckVars :: Maybe [a] -> IO ()
writeCheckVars Maybe [a]
Nothing     = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
writeCheckVars (Just [])   = Moods -> FilePath -> FilePath -> IO ()
colorPhaseLn Moods
Loud FilePath
"Checked Binders: None" FilePath
""
writeCheckVars (Just [a]
ns)   = Moods -> FilePath -> FilePath -> IO ()
colorPhaseLn Moods
Loud FilePath
"Checked Binders:" FilePath
""
                          IO () -> IO () -> IO ()
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 (FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> (a -> FilePath) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> FilePath
symbolString (Symbol -> FilePath) -> (a -> Symbol) -> a -> FilePath
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) -> FilePath -> IO ()
putStrLn (Doc -> FilePath
render (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc
forall a. PPrint a => a -> Doc
pprint SrcSpan
sSpan Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (FilePath -> Doc
text FilePath
": error: " Doc -> Doc -> Doc
<+> 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 :: Doc -> [(SrcSpan, Doc)] -> OutputResult
OutputResult {
    orHeader :: Doc
orHeader   = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"LIQUID: SAFE (" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> Int -> FilePath
forall a. Show a => a -> FilePath
show (Stats -> Int
Solver.numChck Stats
stats) FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" constraints checked)"
  , orMessages :: [(SrcSpan, Doc)]
orMessages = [(SrcSpan, Doc)]
forall a. Monoid a => a
mempty
  }
resDocs Tidy
k (F.Crash [CError]
xs FilePath
s)  =
  OutputResult :: Doc -> [(SrcSpan, Doc)] -> OutputResult
OutputResult {
    orHeader :: Doc
orHeader = FilePath -> Doc
text FilePath
"LIQUID: ERROR" Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
s
  , orMessages :: [(SrcSpan, Doc)]
orMessages = (CError -> (SrcSpan, Doc)) -> [CError] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CError -> (SrcSpan, Doc)
cErrToSpanned Tidy
k (CError -> (SrcSpan, Doc))
-> (CError -> CError) -> CError -> (SrcSpan, Doc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CError -> CError
forall a. CtxError a -> CtxError a
errToFCrash) [CError]
xs
  }
resDocs Tidy
k (F.Unsafe Stats
_ [CError]
xs)   =
  OutputResult :: Doc -> [(SrcSpan, Doc)] -> OutputResult
OutputResult {
    orHeader :: Doc
orHeader   = FilePath -> Doc
text FilePath
"LIQUID: UNSAFE"
  , orMessages :: [(SrcSpan, Doc)]
orMessages = (CError -> (SrcSpan, Doc)) -> [CError] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CError -> (SrcSpan, Doc)
cErrToSpanned Tidy
k) ([CError] -> [CError]
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{UserError
ctErr :: forall t. CtxError t -> TError t
ctErr :: UserError
ctErr} = (UserError -> SrcSpan
forall t. TError t -> SrcSpan
pos UserError
ctErr, Tidy -> UserError -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k UserError
ctErr)

errToFCrash :: CtxError a -> CtxError a
errToFCrash :: CtxError a -> CtxError a
errToFCrash CtxError a
ce = CtxError a
ce { ctErr :: TError a
ctErr    = TError a -> TError a
forall t. TError t -> TError t
tx (TError a -> TError a) -> TError a -> TError a
forall a b. (a -> b) -> a -> b
$ CtxError a -> TError a
forall t. CtxError t -> TError t
ctErr CtxError a
ce}
  where
    tx :: TError t -> TError t
tx (ErrSubType SrcSpan
l Doc
m 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                       = TError t
e

{-
   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 :: FixResult a -> [a] -> FixResult a
addErrors FixResult a
r []               = FixResult a
r
addErrors (Safe Stats
s) [a]
errs      = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s [a]
errs
addErrors (Unsafe Stats
s [a]
xs) [a]
errs = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
errs)
addErrors FixResult a
r  [a]
_               = FixResult a
r

instance Fixpoint (F.FixResult CError) where
  toFix :: FixResult CError -> Doc
toFix = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (FixResult CError -> [Doc]) -> FixResult CError -> 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 CError -> [(SrcSpan, Doc)])
-> FixResult CError
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputResult -> [(SrcSpan, Doc)]
orMessages (OutputResult -> [(SrcSpan, Doc)])
-> (FixResult CError -> OutputResult)
-> FixResult CError
-> [(SrcSpan, Doc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> FixResult CError -> OutputResult
resDocs Tidy
F.Full