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

   -- * Update Configuration With Pragma
   , withPragmas

   -- * Canonicalize Paths in Config
   , canonicalizePaths

   -- * 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)


import System.FilePath                     (isAbsolute, takeDirectory, (</>))

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 -> Mode (CmdArgs Config))
-> Config -> Mode (CmdArgs Config)
forall a b. (a -> b) -> a -> b
$ 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"
           ]

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

 , idirs :: [String]
idirs
    = [String]
forall a. Default a => a
def [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= Ann
typDir
          [String] -> Ann -> [String]
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"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
&= 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
forall a. Default a => a
def 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
forall a. Default a => a
def
          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
forall a. Default a => a
def
          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
forall a. Default a => a
def 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
forall a. Default a => a
def
          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"

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

 , bscope :: Bool
bscope
    = Bool
forall a. Default a => a
def 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"

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

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

 , totalHaskell :: Bool
totalHaskell
    = Bool
forall a. Default a => a
def 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
forall a. Default a => a
def 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
forall a. Default a => a
def 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
forall a. Default a => a
def 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
forall a. Default a => a
def 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
forall a. Default a => a
def 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
    = Maybe Int
forall a. Default a => a
def Maybe Int -> Ann -> Maybe Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Use m cores to solve logical constraints"

 , 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. Default a => a
def 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
forall a. Default a => a
def 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
forall a. Default a => a
def 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."

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

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

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

 , port :: Int
port
     = Int
defaultPort
          Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"port"
          Int -> Ann -> Int
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"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
&= String -> Ann
help String
"Exact Type for Data Constructors"
          Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"exact-data-cons"

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

 , expectErrorContaining :: [String]
expectErrorContaining
    = [String]
forall a. Default a => a
def [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
forall a. Default a => a
def 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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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

  , oldPLE :: Bool
oldPLE
    = Bool
forall a. Default a => a
def
        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
"oldple"

  , interpreter :: Bool
interpreter
    = Bool
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
"dependant-case"

  , extensionality :: Bool
extensionality
    = Bool
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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"

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

  , typeclass :: Bool
typeclass
    = Bool
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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
forall a. Default a => a
def
        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."
  ,
    noLazyPLE :: Bool
noLazyPLE
    = Bool
forall a. Default a => a
def
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
name String
"no-lazy-ple"
        Bool -> Ann -> Bool
forall val. Data val => val -> Ann -> val
&= String -> Ann
help String
"Don't use Lazy PLE"

  , 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
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
"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
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-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
forall a. Default a => a
def 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
forall a. Default a => a
def 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
  , allowUnsafeConstructors :: Bool
allowUnsafeConstructors
    = Bool
forall a. Default a => a
def 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
  } Config -> Ann -> Config
forall val. Data val => val -> Ann -> val
&= String -> Ann
program String
"liquid"
    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"
               , String
""
               , String
"To check a Haskell file foo.hs, type:"
               , String
"  liquid foo.hs "
               ]

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

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

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
FC.Z3, SMTSolver
FC.Cvc4, SMTSolver
FC.Mathsat]
                   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
    noSmtError :: String
noSmtError = String
"LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed."
    missingSmtError :: a -> String
missingSmtError a
smt = String
"Could not find SMT solver '" 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)

fixConfig :: Config -> IO Config
fixConfig :: Config -> IO Config
fixConfig Config
config' = do
  pwd <- IO String
getCurrentDirectory
  cfg <- canonicalizePaths pwd config'
  return $ canonConfig cfg

-- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
--   to worry about relative paths.
canonicalizePaths :: FilePath -> Config -> IO Config
canonicalizePaths :: String -> Config -> IO Config
canonicalizePaths String
pwd Config
cfg = do
  tgt   <- String -> IO String
canonicalizePath String
pwd
  isdir <- doesDirectoryExist tgt
  is    <- mapM (canonicalize tgt isdir) $ idirs cfg
  cs    <- mapM (canonicalize tgt isdir) $ cFiles cfg
  return $ cfg { idirs = is, cFiles = cs }

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

envCfg :: IO Config
envCfg :: IO Config
envCfg = do
  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
"] "
  ]


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

mkOpts :: Config -> IO Config
mkOpts :: Config -> IO Config
mkOpts Config
cfg = do
  let files' :: [String]
files' = [String] -> [String]
forall a. Ord a => [a] -> [a]
F.sortNub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Config -> [String]
files Config
cfg
  Config -> IO Config
forall a. a -> IO a
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       = files'
                                   -- See NOTE [searchpath]
                   }

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

--------------------------------------------------------------------------------
withPragmas :: MonadIO m => Config -> FilePath -> [Located String] -> (Config -> m a) -> m a
--------------------------------------------------------------------------------
withPragmas :: forall (m :: * -> *) a.
MonadIO m =>
Config -> String -> [Located String] -> (Config -> m a) -> m a
withPragmas Config
cfg String
fp [Located String]
ps Config -> m a
action
  = do 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 -> 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
>>= String -> Config -> IO Config
canonicalizePaths String
fp) 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
-- 'cFiles' or 'expectErrorContaining'
-- TODO: This is only used to parse the contents of the env var LIQUIDHASKELL_OPTS
-- so it should be able to parse multiple arguments instead. See issue #1990.
parsePragma :: Located String -> IO Config
parsePragma :: Located String -> IO Config
parsePragma = Config -> [Located String] -> IO Config
processPragmas Config
defConfig ([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]
:[])

defConfig :: Config
defConfig :: Config
defConfig = Config
  { loggingVerbosity :: Verbosity
loggingVerbosity         = Verbosity
Minimal
  , files :: [String]
files                    = [String]
forall a. Default a => a
def
  , idirs :: [String]
idirs                    = [String]
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 :: [String]
checks                   = [String]
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
  , nopositivity :: Bool
nopositivity             = Bool
False
  , rankNTypes :: Bool
rankNTypes               = Bool
False
  , noclasscheck :: Bool
noclasscheck             = Bool
False
  , gradual :: Bool
gradual                  = Bool
False
  , bscope :: Bool
bscope                   = Bool
False
  , gdepth :: Int
gdepth                   = Int
1
  , ginteractive :: Bool
ginteractive             = Bool
False
  , totalHaskell :: Bool
totalHaskell             = 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
  , expectErrorContaining :: [String]
expectErrorContaining    = [String]
forall a. Default a => a
def
  , expectAnyError :: Bool
expectAnyError           = Bool
False
  , 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 :: [String]
ghcOptions               = [String]
forall a. Default a => a
def
  , cFiles :: [String]
cFiles                   = [String]
forall a. Default a => a
def
  , port :: Int
port                     = Int
defaultPort
  , scrapeInternals :: Bool
scrapeInternals          = 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
  , pleWithUndecidedGuards :: Bool
pleWithUndecidedGuards   = Bool
False
  , oldPLE :: Bool
oldPLE                   = Bool
False
  , interpreter :: Bool
interpreter              = Bool
False
  , proofLogicEvalLocal :: Bool
proofLogicEvalLocal      = Bool
False
  , etabeta :: Bool
etabeta                  = Bool
False
  , dependantCase :: Bool
dependantCase            = Bool
False
  , reflection :: Bool
reflection               = Bool
False
  , extensionality :: Bool
extensionality           = Bool
False
  , nopolyinfer :: Bool
nopolyinfer              = Bool
False
  , compileSpec :: Bool
compileSpec              = Bool
False
  , noCheckImports :: Bool
noCheckImports           = Bool
False
  , typeclass :: Bool
typeclass                = Bool
False
  , auxInline :: Bool
auxInline                = Bool
False
  , rwTerminationCheck :: Bool
rwTerminationCheck       = Bool
False
  , skipModule :: Bool
skipModule               = Bool
False
  , noLazyPLE :: Bool
noLazyPLE                = Bool
False
  , fuel :: Maybe Int
fuel                     = Maybe Int
forall a. Maybe a
Nothing
  , environmentReduction :: Bool
environmentReduction     = Bool
False
  , noEnvironmentReduction :: Bool
noEnvironmentReduction   = Bool
False
  , inlineANFBindings :: Bool
inlineANFBindings        = Bool
False
  , pandocHtml :: Bool
pandocHtml               = Bool
False
  , excludeAutomaticAssumptionsFor :: [String]
excludeAutomaticAssumptionsFor = []
  , dumpOpaqueReflections :: Bool
dumpOpaqueReflections    = Bool
False
  , dumpPreNormalizedCore :: Bool
dumpPreNormalizedCore    = Bool
False
  , allowUnsafeConstructors :: Bool
allowUnsafeConstructors  = Bool
False
  }

-- | 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 CError -> OutputResult
resDocs Tidy
tidy FixResult CError
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 CError)
resultWithContext (F.Unsafe Stats
s [TError Doc]
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
<$> [TError Doc] -> IO [CError]
errorsWithContext [TError Doc]
es
resultWithContext (F.Safe   Stats
stats) = FixResult CError -> IO (FixResult CError)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Stats -> FixResult CError
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 [CError]
errorsWithContext [TError Doc]
userErrs
  return (F.Crash (zip errs' msgs) s)




instance Show (CtxError Doc) where
  show :: CError -> String
show = CError -> 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 CError -> 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 [(CError, Maybe String)]
xs String
s)  =
  OutputResult {
    orHeader :: Doc
orHeader = String -> Doc
text String
"LIQUID: ERROR:" Doc -> Doc -> Doc
<+> String -> Doc
text String
s
  , orMessages :: [(SrcSpan, Doc)]
orMessages = ((CError, Maybe String) -> (SrcSpan, Doc))
-> [(CError, Maybe String)] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map (Tidy -> CError -> (SrcSpan, Doc)
cErrToSpanned Tidy
k (CError -> (SrcSpan, Doc))
-> ((CError, Maybe String) -> CError)
-> (CError, Maybe String)
-> (SrcSpan, Doc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CError, Maybe String) -> CError
errToFCrash) [(CError, Maybe String)]
xs
  }
resDocs Tidy
k (F.Unsafe Stats
_ [CError]
xs)   =
  OutputResult {
    orHeader :: Doc
orHeader   = String -> Doc
text String
"LIQUID: UNSAFE"
  , orMessages :: [(SrcSpan, Doc)]
orMessages = (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{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 :: (CError, Maybe String) -> CError
errToFCrash (CError
ce, Just String
msg) = CError
ce { ctErr = ErrOther (pos (ctErr ce)) (fixMessageDoc msg) }
errToFCrash (CError
ce, Maybe String
Nothing)  = CError
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 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