z:a -> Bool\>. y:a -> a\
\@-}@ +-- +-- * At the __binder__ (inside 'RAllP'): +-- @PV{pname="p", ptype=a, parg="LIQUID$dummy", pargs=[(a, "x", EVar "x")]}@ +-- * At the __use site__ @a\
@ (inside 'ur_pred'):
+-- @PV{pname="p", ptype=a, parg="LIQUID$dummy", pargs=[(a, "x", EVar "y")]}@
+--
+-- * @pname@ is the name of the predicate variable, e.g. @p@
+-- * @ptype@ is the type of the last (value) argument, i.e. the type being
+-- constrained, e.g. @a@
+-- * @parg@ is an internal dummy binder — always @"LIQUID$dummy"@. It is used
+-- by 'pToRef' as the value-position variable in the uninterpreted function
+-- call @papp_n(p, parg, e1, ..., en)@ when converting a standalone
+-- 'PredicateBV' to a 'F.Reft' via 'toReft'. In the main constraint
+-- generation path ('replacePredsWithRefs' / 'pVartoRConc'), the @ur_reft@
+-- binder is used instead.
+-- * @pargs@ is the list of non-value arguments (excluding the last one).
+-- Each triple is @(type, formal-binder, actual-expr)@.
+-- The __formal-binder__ always comes from the predicate declaration site
+-- (preserved by 'txPvar'); the __actual-expr__ is updated at each call site.
+--
+-- The expressions in @pargs@ are the __actual arguments__ at each use site.
+-- In 'meetListWithPSub' (abstract refinement subtyping), if all expressions
+-- equal their formal binders (@\(_, x, EVar y) -> x == y@) no substitution
+-- is needed; otherwise the substitution @[(formal, actual), ...]@ built from
+-- @pargs@ is applied to the concrete predicate body.
+--
data PVarBV b v t = PV
{ pname :: !b
, ptype :: !t
@@ -369,7 +404,7 @@
type Predicate = PredicateV Symbol
type PredicateV v = PredicateBV Symbol v
newtype PredicateBV b v = Pr [UsedPVarBV b v]
- deriving (Generic, Data)
+ deriving (Generic, Data, Show)
deriving (B.Binary, Hashable) via Generically (PredicateBV b v)
mapPredicateV :: (v -> v') -> PredicateV v -> PredicateV v'
@@ -438,7 +473,7 @@
deriving (Show, Generic, Data)
deriving (B.Binary, Hashable) via Generically BTyVar
-newtype RTyVar = RTV TyVar deriving (Generic, Data)
+newtype RTyVar = RTV TyVar deriving (Generic, Data, Show)
instance Eq BTyVar where
(BTV x) == (BTV y) = x == y
@@ -473,7 +508,7 @@
, btc_class :: !Bool -- ^ Is this a class type constructor?
, btc_prom :: !Bool -- ^ Is Promoted Data Con?
}
- deriving (Generic, Data)
+ deriving (Generic, Data, Show)
deriving (B.Binary, Hashable) via Generically BTyCon
data RTyCon = RTyCon
@@ -481,7 +516,7 @@
, rtc_pvars :: ![RPVar] -- ^ Predicate Parameters
, rtc_info :: !TyConInfo -- ^ TyConInfo
}
- deriving (Generic, Data)
+ deriving (Generic, Data, Show)
instance F.Symbolic RTyCon where
symbol = F.symbol . rtc_tc
@@ -672,12 +707,6 @@
instance F.PPrint v => F.PPrint (RTVar v s) where
pprintTidy k (RTVar x _) = F.pprintTidy k x
-instance Show RTyCon where
- show = F.showpp
-
-instance Show BTyCon where
- show = F.showpp
-
instance F.Loc BTyCon where
srcSpan = F.srcSpan . btc_tc
@@ -705,13 +734,10 @@
{ varianceTyArgs :: !VarianceInfo -- ^ variance info for type variables
, variancePsArgs :: !VarianceInfo -- ^ variance info for predicate variables
, sizeFunction :: !(Maybe SizeFun) -- ^ logical UNARY function that computes the size of the structure
- } deriving (Generic, Data)
+ } deriving (Generic, Data, Show)
instance NFData TyConInfo
-instance Show TyConInfo where
- show (TyConInfo x y _) = show x ++ "\n" ++ show y
-
--------------------------------------------------------------------------------
-- | Unified Representation of Refinement Types --------------------------------
--------------------------------------------------------------------------------
@@ -723,17 +749,61 @@
type PVUV v c tv = PVarV v (RTypeV v c tv NoReft)
type PVUBV b v c tv = PVarBV b v (RTypeBV b v c tv (NoReftB b))
-instance Show tv => Show (RTVU c tv) where
- show (RTVar t _) = show t
-
type RType c tv r = RTypeV Symbol c tv r
type RTypeV v c tv = RTypeBV Symbol v c tv
+-- | A refinement type
+--
+-- * @b@ is the type of bindings
+-- * @v@ is the type of variables appearing in expressions
+-- * @c@ is the type of type constructors
+-- * @tv@ is the type of type variables
+-- * @r@ is the type of refinements
+--
+-- A refinement might be missing (e.g. @r@ is @()@), if the RTypeBV is used to
+-- represent the type of an entity that can't use refinements, e.g. the type of
+-- an abstract predicate.
data RTypeBV b v c tv r
- = RVar {
+ =
+ -- | A type variable, e.g. @a@ in @a -> a@
+ --
+ -- When the refinement is @(v, e)@, the constructor represents @{v:a | e}@.
+ --
+ -- The scope of @v@ is the expression @e@ and the type @a@.
+ --
+ -- * @rt_var@ is the type variable, e.g. @a@
+ -- * @rt_reft@ is the refinement, e.g. @(v, v > 0)@ in @{v:a | v > 0}@
+ --
+ RVar {
rt_var :: !tv
, rt_reft :: !r
}
+ -- | A function type, e.g. @x:a -> y:{y1:a | x = y1} -> {v:a | y == v}@
+ --
+ -- * @rt_bind@ is the binder of the first argument, e.g. @x@ in the above
+ -- example. The scope of @rt_bind@ is @rt_in@ and @rt_out@. Note, however,
+ -- that @rt_bind@ is not used in @rt_in@ after a SpecType is constructed.
+ -- This is because all the occurrences of the binder are switched to the
+ -- name of the binder in the refinement type of @rt_in@ (e.g.
+ -- @{y:{y1:a | x = y} -> ...}@ is changed to @{y:{y1:a | x = y1} -> ...}@).
+ -- This transformation is performed by @rebind@ in @ofBRType@.
+ --
+ -- * @rt_rinfo@ controls whether typeclass method elaboration is permitted
+ -- on this arrow. @RFInfo (Just True)@ means typeclass arguments are
+ -- allowed; @RFInfo Nothing@ is the default for user-written types.
+ --
+ -- * @rt_in@ is the type of the first argument, e.g. @a@
+ --
+ -- * @rt_out@ is the type of the result, e.g.
+ -- @y:{y1:a | x = y1} -> {v:a | y == v}@
+ --
+ -- * @rt_reft@ is the refinement of the function type. If the refinement is
+ -- @(v0, e)@, then the represented type is
+ -- @{v0: (x:a -> y:{y1:a | x = y1} -> {v:a | y == v}) | e}@.
+ --
+ -- The scope of @v0@ is the entire function type and @e@, i.e.
+ -- @x:a -> y:{y1:a | x = y1} -> {v:a | y == v}@.
+ --
| RFun {
rt_bind :: !b
, rt_rinfo :: !RFInfo
@@ -742,22 +812,61 @@
, rt_reft :: !r
}
+ -- | A universally quantified type, e.g. @forall (a :: k). a -> a@
+ --
+ -- * @rt_tvbind@ is the type variable and its kind, e.g. @a :: k@ in the
+ -- above example. If @rtv_is_val@ is True in the variable's info, the
+ -- type variable also introduces an expression-level binder (a "value
+ -- type variable") with name @rtv_name@ and kind @rtv_kind@.
+ --
+ -- * @rt_ty@ is the body of the quantified type, e.g. @a -> a@
+ --
+ -- * @rt_ref@ is the refinement of the quantified type.
+ -- If the refinement is @(v, e)@, then the represented type is
+ -- @{v: (forall (a :: k). a -> a) | e}@.
+ --
+ -- The scope of @v@ is the entire quantified type and @e@.
+ --
| RAllT {
- rt_tvbind :: !(RTVUBV b v c tv) -- RTVar tv (RType c tv ()))
+ rt_tvbind :: !(RTVUBV b v c tv)
, rt_ty :: !(RTypeBV b v c tv r)
, rt_ref :: !r
}
- -- | "forall x y Bool\>. {v:Int | p v} -> Int@
+ --
+ -- * @rt_pvbind@ is the predicate variable and its type, e.g.
+ -- @p :: Int -> Bool@ in the above example. See 'PVarBV' for details on
+ -- how predicate variable arguments are stored.
+ --
+ -- * @rt_ty@ is the body of the quantified type, e.g.
+ -- @{v:Int | p v} -> Int@. The predicate variable @rt_pvbind@ is in scope
+ -- in @rt_ty@ and can be applied to type constructors via @rt_pargs@ in
+ -- 'RApp'.
+ --
| RAllP {
rt_pvbind :: !(PVUBV b v c tv)
, rt_ty :: !(RTypeBV b v c tv r)
}
- -- | For example, in [a]<{\h -> v > h}>, we apply (via `RApp`)
- -- * the `RProp` denoted by `{\h -> v > h}` to
- -- * the `RTyCon` denoted by `[]`.
+ -- | Application of a type constructor, e.g. @{v:[a]\<{\\h v -> v > h}\> | len v > 0}@
+ --
+ -- * @rt_tycon@ is the type constructor, e.g. @[]@
+ --
+ -- * @rt_args@ is the list of type arguments, e.g. the singleton list
+ -- containing the type @a@
+ --
+ -- * @rt_pargs@ is the list of predicate arguments, e.g. the singleton list
+ -- containing the predicate value @RProp [("h",_)] (RHole {v > h})@.
+ -- These are the abstract refinements supplied inside @\<...\>@.
+ --
+ -- * @rt_reft@ is the refinement of the type application.
+ -- If the refinement is @(v, e)@, then the represented type is
+ -- @{v: [a]\<{\\h v -> v > h}\> | e}@, e.g. @(v, len v > 0)@.
+ --
+ -- The scope of @v@ is the entire type application and @e@.
+ --
| RApp {
rt_tycon :: !c
, rt_args :: ![RTypeBV b v c tv r]
@@ -765,26 +874,100 @@
, rt_reft :: !r
}
- | RAllE {
- rt_bind :: !b
- , rt_allarg :: !(RTypeBV b v c tv r)
- , rt_ty :: !(RTypeBV b v c tv r)
- }
-
+ -- | Existential quantification over an expression variable.
+ -- Printed as @exists [x:T]. TYPE@.
+ --
+ -- @REx@ is introduced by A-normalisation ('addExist' in @Bare/Expand.hs@)
+ -- when an abstract refinement is applied to a complex (non-variable)
+ -- expression. A fresh ghost variable is created to name the expression so
+ -- that the fixpoint solver can reason about it without duplicating it.
+ -- See @tests/pos/TestREx.hs@ for an actual test.
+ --
+ -- Example: the return type @a\ @ of
+ --
+ -- > assume next :: forall a a -> Bool>. i:Int -> a -> a
+ --
+ -- is A-normalised to:
+ --
+ -- @REx "ex#0" {v:Int | v == i+1} (RApp a [] [RProp [("ex#0",_)] (a )] _)@
+ --
+ -- * @rt_bind@ is the ghost binder, e.g. @ex#0@ above.
+ -- Its scope is @rt_ty@.
+ -- * @rt_exarg@ is the type of the ghost variable, e.g.
+ -- @{v:Int | v == i+1}@ — a singleton type pinning the ghost to the
+ -- original expression.
+ -- * @rt_ty@ is the body type, e.g. @a\ @, which now mentions the
+ -- ghost instead of the original complex expression.
+ --
+ -- Semantics: when checking @REx x tx t \<: t2@, a fresh name @y@ is
+ -- generated, @y:tx@ is added to the environment, and @t[x:=y] \<: t2@ is
+ -- checked. On the RHS, @t1 \<: REx x tx t2@ is handled symmetrically.
+ --
| REx {
rt_bind :: !b
, rt_exarg :: !(RTypeBV b v c tv r)
, rt_ty :: !(RTypeBV b v c tv r)
}
- | RExprArg (F.Located (ExprBV b v)) -- ^ For expression arguments to type aliases
- -- see tests/pos/vector2.hs
+ -- | An expression argument to a type alias (not a proper type).
+ --
+ -- Example: given @{-\@ type VectorN a N = {v:[a] | len v == N} \@-}@,
+ -- the usage @VectorN Int 3@ is represented as:
+ -- @RApp VectorN [RApp Int ..., RExprArg (ECon (I 3))] [] _@
+ --
+ -- The @RExprArg@ appears in the @rt_args@ list of 'RApp' in position
+ -- corresponding to the expression parameter @N@.
+ --
+ -- Parsed from: bare numeric literals (e.g. @3@), or expressions in braces
+ -- @{expr}@ or parentheses @(expr)@ at type-argument positions.
+ --
+ | RExprArg (F.Located (ExprBV b v))
+
+ -- | Type-level application that is /not/ a saturated type constructor
+ -- application, e.g. @f a@ where @f@ is a type variable of higher kind.
+ --
+ -- Example: in @forall (f :: * -> *) a. f a -> f a@,
+ -- the @f a@ part is:
+ -- @RAppTy (RVar f (v, True)) (RVar a (v, True)) (v, True)@
+ --
+ -- * @rt_arg@ is the type being applied, e.g. @RVar f _@
+ -- * @rt_res@ is the type argument, e.g. @RVar a _@
+ -- * @rt_reft@ is the refinement of the application result.
+ -- If the refinement is @(v, e)@, then the represented type is
+ -- @{v: f a | e}@.
+ --
+ -- The scope of @v@ is the entire type application and @e@.
+ --
| RAppTy{
rt_arg :: !(RTypeBV b v c tv r)
, rt_res :: !(RTypeBV b v c tv r)
, rt_reft :: !r
}
+ -- | A type annotated with a verification obligation (constraint, invariant,
+ -- or termination metric). It wraps an actual type @rt_ty@ with auxiliary
+ -- information for constraint generation.
+ --
+ -- Example (OCons): the type @{x:Int |- {v:Int | v > 0} \<: {v:Int | v > x}} => Int -> Int@
+ -- is represented as:
+ -- @RRTy [("x", Int), (dummySymbol, {v:Int | v > 0}), (dummySymbol, {v:Int | v > x})]@
+ -- @trueReft OCons (Int -> Int)@
+ --
+ -- * @rt_env@ is the typing environment and subtyping pair. For @OCons@,
+ -- the last two entries are the LHS and RHS of the subtyping obligation;
+ -- preceding entries form the local typing environment.
+ -- * @rt_ref@ is the refinement predicate (for @OInv@ and @OTerm@ this
+ -- carries the invariant or termination metric).
+ -- * @rt_obl@ is the kind of obligation:
+ -- - @OCons@: subtyping constraint, parsed from
+ -- @{env |- t1 \<: t2} => TYPE@
+ -- - @OInv@: data-type invariant, generated by 'addInvCond'
+ -- - @OTerm@: termination metric, generated by 'addObligation'
+ -- * @rt_ty@ is the underlying actual type, e.g. @Int -> Int@
+ --
+ -- In all cases, the obligation is discharged as a side-effect during
+ -- constraint generation, and @rt_ty@ is the type used for further checking.
+ --
| RRTy {
rt_env :: ![(b, RTypeBV b v c tv r)]
, rt_ref :: !r
@@ -792,9 +975,19 @@
, rt_ty :: !(RTypeBV b v c tv r)
}
- | RHole r -- ^ let LH match against the Haskell type and add k-vars, e.g. `x:_`
- -- see tests/pos/Holes.hs
- deriving (Eq, Generic, Data, Functor, Foldable, Traversable)
+ -- | A hole: a placeholder that instructs LH to infer the type by matching
+ -- against the Haskell type and inserting k-variables for inference.
+ --
+ -- Example: @{-\@ f :: x:_ -> {v:_ | v > x} \@-}@ contains two holes.
+ -- Each @_@ becomes @RHole r@ where @r@ is either a @true@ refinement or a
+ -- user-supplied refinement (e.g. @v > x@ in the second hole).
+ --
+ -- During elaboration, holes are replaced with actual types from GHC's type
+ -- checker, with fresh k-variables for the refinements.
+ -- See: tests/pos/Holes.hs
+ --
+ | RHole r
+ deriving (Eq, Generic, Data, Functor, Foldable, Show, Traversable)
deriving (B.Binary, Hashable) via Generically (RTypeBV b v c tv r)
instance (NFData c, NFData tv, NFData r) => NFData (RType c tv r)
@@ -809,10 +1002,13 @@
instance (Eq tv) => Eq (RTVar tv s) where
t1 == t2 = ty_var_value t1 == ty_var_value t2
+-- | @RTVar@ is the type of type variables in the refinement type system. It
+-- contains a type variable, optionally a kind, and information about how to
+-- instantiate it (polymorphic vs. monomorphic refinements).
data RTVar tv s = RTVar
{ ty_var_value :: tv
, ty_var_info :: RTVInfo s
- } deriving (Generic, Data, Functor, Foldable, Traversable)
+ } deriving (Generic, Data, Functor, Foldable, Show, Traversable)
deriving (B.Binary, Hashable) via Generically (RTVar tv s)
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
@@ -829,7 +1025,7 @@
, rtv_is_pol :: Bool -- true iff the type variable gets instantiated with
-- any refinement (ie is polymorphic on refinements),
-- false iff instantiation is with true refinement
- } deriving (Generic, Data, Functor, Eq, Foldable, Traversable)
+ } deriving (Generic, Data, Functor, Eq, Foldable, Show, Traversable)
deriving (B.Binary, Hashable) via Generically (RTVInfo s)
@@ -859,7 +1055,7 @@
data RefB b τ t = RProp
{ rf_args :: [(b, τ)] -- ^ arguments. e.g. @h@ in the above example
, rf_body :: t -- ^ Abstract refinement associated with `RTyCon`. e.g. @v > h@ in the above example
- } deriving (Eq, Generic, Data, Functor, Foldable, Traversable)
+ } deriving (Eq, Generic, Data, Functor, Foldable, Show, Traversable)
deriving (B.Binary, Hashable) via Generically (RefB b τ t)
instance (NFData τ, NFData t) => NFData (Ref τ t)
@@ -875,11 +1071,55 @@
type UReft r = UReftV F.Symbol r
type UReftV v r = UReftBV F.Symbol v r
+
+-- | A combined refinement carrying both a first-order predicate and a
+-- conjunction of abstract-refinement (predicate-variable) applications.
+-- This is the @r@ parameter of 'RTypeBV' in fully-elaborated types:
+-- @SpecType = 'RRType' RReft@ where @RReft = UReft F.Reft =
+-- UReftBV Symbol Symbol F.Reft@.
+--
+-- Example: the type @Int\ @ where @p :: x:Int -> z:Int -> Bool@ is an
+-- abstract refinement quantified by an enclosing 'RAllP', applied with
+-- extra argument @m@, is represented as:
+--
+-- @
+-- MkUReft
+-- { ur_reft = F.Reft ("VV", PTrue) -- no first-order constraint
+-- , ur_pred = Pr [ PV { pname = "p"
+-- , ptype = intSort
+-- , parg = "LIQUID$dummy"
+-- , pargs = [(intSort, "x", EVar "m")] } ]
+-- }
+-- @
+--
+-- If the type also carries a first-order constraint, e.g. a type alias that
+-- expands to @{VV:Int | VV > 0}@ combined with an abstract refinement, then
+-- @ur_reft@ would be @F.Reft ("VV", VV > 0)@ alongside the non-empty @ur_pred@.
+--
+-- * @ur_reft@ is the first-order part of the refinement, stored as a fixpoint
+-- 'F.Reft' @(binder, predicate)@. The standard value-variable is @"VV"@
+-- (fixpoint's canonical binder, normalised from the user's @v@ choice).
+-- * @ur_pred@ is the abstract-refinement part: a 'PredicateBV' (= @Pr [UsedPVarBV]@),
+-- i.e. a conjunction of predicate-variable applications.
+-- Each 'UsedPVarBV' records which predicate variable is used (via @pname@),
+-- the internal dummy binder (@parg = "LIQUID$dummy"@), and the actual
+-- argument expressions (@pargs@) at this use site (see 'PVarBV').
+--
+-- During constraint generation, @ur_pred@ is eliminated by
+-- 'replacePredsWithRefs': each predicate-variable application is converted
+-- to an uninterpreted function call @papp_n(p, VV, e1, ..., en)@ via
+-- 'pVartoRConc' (using the @ur_reft@ binder @VV@, __not__ @parg@) and
+-- conjoined into @ur_reft@, producing a pure 'F.Reft' understood by the SMT
+-- solver. After this step, @ur_pred@ becomes @Pr []@.
+--
+-- 'toReft' on a 'UReftBV' discards @ur_pred@ entirely and returns only
+-- @ur_reft@; it must therefore be called only after predicate-replacement.
+--
data UReftBV b v r = MkUReft
{ ur_reft :: !r
, ur_pred :: !(PredicateBV b v)
}
- deriving (Eq, Generic, Data, Functor, Foldable, Traversable)
+ deriving (Eq, Generic, Data, Functor, Foldable, Show, Traversable)
deriving (B.Binary, Hashable) via Generically (UReftBV b v r)
mapUReftV :: (v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
@@ -892,7 +1132,7 @@
type NoReft = NoReftB Symbol
data NoReftB b = NoReft
- deriving (Eq, Generic, Data, Functor, Foldable, Traversable)
+ deriving (Eq, Generic, Data, Functor, Foldable, Show, Traversable)
deriving (B.Binary, Hashable) via Generically (NoReftB b)
instance NFData (NoReftB b)
@@ -947,18 +1187,6 @@
--------------------------------------------------------------------------------
-- | Printing Refinement Types -------------------------------------------------
--------------------------------------------------------------------------------
-
-instance Show RTyVar where
- show = F.showpp
-
-instance F.PPrint (UReft r) => Show (UReft r) where
- show = F.showpp
-
-instance F.PPrint (RType c tv r) => Show (RType c tv r) where
- show = F.showpp
-
-instance F.PPrint (RTProp c tv r) => Show (RTProp c tv r) where
- show = F.showpp
instance F.PPrint BTyVar where
pprintTidy _ (BTV α) = text (F.symbolString $ F.val α)
diff --git a/src/Language/Haskell/Liquid/Types/RTypeOp.hs b/src/Language/Haskell/Liquid/Types/RTypeOp.hs
--- a/src/Language/Haskell/Liquid/Types/RTypeOp.hs
+++ b/src/Language/Haskell/Liquid/Types/RTypeOp.hs
@@ -315,7 +315,6 @@
emapReft f γ (RAllP π t) = RAllP π (emapReft f γ t)
emapReft f γ (RFun x i t t' r) = RFun x i (emapReft f γ t) (emapReft f (x:γ) t') (f (x:γ) r)
emapReft f γ (RApp c ts rs r) = RApp c (emapReft f γ <$> ts) (emapRef f γ <$> rs) (f γ r)
-emapReft f γ (RAllE z t t') = RAllE z (emapReft f γ t) (emapReft f γ t')
emapReft f γ (REx z t t') = REx z (emapReft f γ t) (emapReft f γ t')
emapReft _ _ (RExprArg e) = RExprArg e
emapReft f γ (RAppTy t t' r) = RAppTy (emapReft f γ t) (emapReft f γ t') (f γ r)
@@ -334,7 +333,6 @@
mapRTypeV f (RApp c ts rs r) = RApp c (mapRTypeV f <$> ts) (mapRefV <$> rs) r
where
mapRefV (RProp ss t) = RProp (map (fmap (mapRTypeV f)) ss) (mapRTypeV f t)
-mapRTypeV f (RAllE z t t') = RAllE z (mapRTypeV f t) (mapRTypeV f t')
mapRTypeV f (REx z t t') = REx z (mapRTypeV f t) (mapRTypeV f t')
mapRTypeV f (RExprArg e) = RExprArg (fmap (fmap f) e)
mapRTypeV f (RAppTy t t' r) = RAppTy (mapRTypeV f t) (mapRTypeV f t') r
@@ -349,7 +347,6 @@
mapRTypeVM f (RApp c ts rs r) = RApp c <$> mapM (mapRTypeVM f) ts <*> mapM mapRefVM rs <*> pure r
where
mapRefVM (RProp ss t) = RProp <$> mapM (traverse (mapRTypeVM f)) ss <*> mapRTypeVM f t
-mapRTypeVM f (RAllE z t t') = RAllE z <$> mapRTypeVM f t <*> mapRTypeVM f t'
mapRTypeVM f (REx z t t') = REx z <$> mapRTypeVM f t <*> mapRTypeVM f t'
mapRTypeVM f (RExprArg e) = RExprArg <$> traverse (traverse f) e
mapRTypeVM f (RAppTy t t' r) = RAppTy <$> mapRTypeVM f t <*> mapRTypeVM f t' <*> pure r
@@ -377,7 +374,6 @@
go γ (RApp c ts rs r) =
let γ' = if bscp then F.reftBind (toReft r) : γ else γ
in RApp c <$> mapM (go γ') ts <*> mapM (emapRefM bscp vf f γ) rs <*> f γ r
- go γ (RAllE z t t') = RAllE z <$> go γ t <*> go γ t'
go γ (REx z t t') = REx z <$> go γ t <*> go γ t'
go γ (RExprArg e) = RExprArg <$> traverse (emapExprVM (vf . (++γ))) e
go γ (RAppTy t t' r) = RAppTy <$> go γ t <*> go γ t' <*> f γ r
@@ -459,7 +455,6 @@
go γ (RAllP π t) = RAllP π (go γ t)
go γ (RFun x i t t' r) = RFun x i (go γ t) (go (x:γ) t') r
go γ (RApp c ts rs r) = RApp c (go γ <$> ts) (mo γ <$> rs) r
- go γ (RAllE z t t') = RAllE z (go γ t) (go γ t')
go γ (REx z t t') = REx z (go γ t) (go γ t')
go γ (RExprArg e) = RExprArg (f γ <$> e) -- <---- actual substitution
go γ (RAppTy t t' r) = RAppTy (go γ t) (go γ t') r
@@ -483,7 +478,6 @@
go a (RAllT _ t _) = step a t
go a (RAllP _ t) = step a t
go a (RFun _ _ t t' _) = foldl' step a [t, t']
- go a (RAllE _ t t') = foldl' step a [t, t']
go a (REx _ t t') = foldl' step a [t, t']
go a (RAppTy t t' _) = foldl' step a [t, t']
go a (RApp _ ts rs _) = foldl' prep (foldl' step a ts) rs
@@ -506,7 +500,6 @@
isBase RFun{} = False
isBase (RAppTy t1 t2 _) = isBase t1 && isBase t2
isBase (RRTy _ _ _ t) = isBase t
-isBase (RAllE _ _ t) = isBase t
isBase (REx _ _ t) = isBase t
isBase _ = False
@@ -516,7 +509,6 @@
hasHoleTy (RAllP _ t) = hasHoleTy t
hasHoleTy (RFun _ _ t t' _) = hasHoleTy t || hasHoleTy t'
hasHoleTy (RApp _ ts _ _) = any hasHoleTy ts
-hasHoleTy (RAllE _ t t') = hasHoleTy t || hasHoleTy t'
hasHoleTy (REx _ t t') = hasHoleTy t || hasHoleTy t'
hasHoleTy (RExprArg _) = False
hasHoleTy (RAppTy t t' _) = hasHoleTy t || hasHoleTy t'
@@ -524,7 +516,6 @@
hasHoleTy (RRTy xts _ _ t) = hasHoleTy t || any hasHoleTy (snd <$> xts)
isFunTy :: RType t t1 t2 -> Bool
-isFunTy (RAllE _ _ t) = isFunTy t
isFunTy (RAllT _ t _) = isFunTy t
isFunTy (RAllP _ t) = isFunTy t
isFunTy RFun{} = True
@@ -536,7 +527,6 @@
mapReftM f (RAllP π t) = fmap (RAllP π) (mapReftM f t)
mapReftM f (RFun x i t t' r) = liftM3 (RFun x i) (mapReftM f t) (mapReftM f t') (f r)
mapReftM f (RApp c ts rs r) = liftM3 (RApp c) (mapM (mapReftM f) ts) (mapM (mapRefM f) rs) (f r)
-mapReftM f (RAllE z t t') = liftM2 (RAllE z) (mapReftM f t) (mapReftM f t')
mapReftM f (REx z t t') = liftM2 (REx z) (mapReftM f t) (mapReftM f t')
mapReftM _ (RExprArg e) = return $ RExprArg e
mapReftM f (RAppTy t t' r) = liftM3 RAppTy (mapReftM f t) (mapReftM f t') (f r)
@@ -552,7 +542,6 @@
mapPropM f (RAllP π t) = fmap (RAllP π) (mapPropM f t)
mapPropM f (RFun x i t t' r) = liftM3 (RFun x i) (mapPropM f t) (mapPropM f t') (return r)
mapPropM f (RApp c ts rs r) = liftM3 (RApp c) (mapM (mapPropM f) ts) (mapM f rs) (return r)
-mapPropM f (RAllE z t t') = liftM2 (RAllE z) (mapPropM f t) (mapPropM f t')
mapPropM f (REx z t t') = liftM2 (REx z) (mapPropM f t) (mapPropM f t')
mapPropM _ (RExprArg e) = return $ RExprArg e
mapPropM f (RAppTy t t' r) = liftM3 RAppTy (mapPropM f t) (mapPropM f t') (return r)
@@ -616,7 +605,6 @@
go γ z me@(RApp _ ts rs r) = f γ (Just me) r (ho' γ (go' γ' z ts) rs)
where γ' = if bsc then insertSEnv (rTypeValueVar me) (g me) γ else γ
- go γ z (RAllE x t t') = go (insertSEnv x (g t) γ) (go γ z t) t'
go γ z (REx x t t') = go (insertSEnv x (g t) γ) (go γ z t) t'
go γ z me@(RRTy [] r _ t) = f γ (Just me) r (go γ z t)
go γ z me@(RRTy xts r _ t) = f γ (Just me) r (go γ (go γ z (envtoType xts)) t)
@@ -643,7 +631,6 @@
mapRFInfo f (RAppTy t t' r) = RAppTy (mapRFInfo f t) (mapRFInfo f t') r
mapRFInfo f (RApp c ts rs r) = RApp c (mapRFInfo f <$> ts) (mapRFInfoRef f <$> rs) r
mapRFInfo f (REx b t1 t2) = REx b (mapRFInfo f t1) (mapRFInfo f t2)
-mapRFInfo f (RAllE b t1 t2) = RAllE b (mapRFInfo f t1) (mapRFInfo f t2)
mapRFInfo f (RRTy e r o t) = RRTy (fmap (mapRFInfo f) <$> e) r o (mapRFInfo f t)
mapRFInfo _ t' = t'
@@ -659,7 +646,6 @@
mapBot f (RAppTy t t' r) = RAppTy (mapBot f t) (mapBot f t') r
mapBot f (RApp c ts rs r) = f $ RApp c (mapBot f <$> ts) (mapBotRef f <$> rs) r
mapBot f (REx b t1 t2) = REx b (mapBot f t1) (mapBot f t2)
-mapBot f (RAllE b t1 t2) = RAllE b (mapBot f t1) (mapBot f t2)
mapBot f (RRTy e r o t) = RRTy (fmap (mapBot f) <$> e) r o (mapBot f t)
mapBot f t' = f t'
@@ -675,7 +661,6 @@
go (RAllP π t) = RAllP (mapP π) (go t)
go (RFun b i t1 t2 r) = RFun (f b) i (go t1) (go t2) r
go (RApp c ts rs r) = RApp c (go <$> ts) (mapR <$> rs) r
- go (RAllE b t1 t2) = RAllE (f b) (go t1) (go t2)
go (REx b t1 t2) = REx (f b) (go t1) (go t2)
go (RVar α r) = RVar α r
go (RHole r) = RHole r
@@ -700,7 +685,6 @@
stripAnnotations :: RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations (RAllT α t r) = RAllT α (stripAnnotations t) r
stripAnnotations (RAllP _ t) = stripAnnotations t
-stripAnnotations (RAllE _ _ t) = stripAnnotations t
stripAnnotations (REx _ _ t) = stripAnnotations t
stripAnnotations (RFun x i t t' r) = RFun x i (stripAnnotations t) (stripAnnotations t') r
stripAnnotations (RAppTy t t' r) = RAppTy (stripAnnotations t) (stripAnnotations t') r
diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs
--- a/src/Language/Haskell/Liquid/Types/RefType.hs
+++ b/src/Language/Haskell/Liquid/Types/RefType.hs
@@ -532,10 +532,8 @@
nlzP ps t@(RRTy _ _ _ t')
= (t, ps ++ ps')
where ps' = snd $ nlzP [] t'
-nlzP ps t@RAllE{}
- = (t, ps)
nlzP _ t
- = panic Nothing $ "RefType.nlzP: cannot handle " ++ show t
+ = panic Nothing $ "RefType.nlzP: cannot handle " ++ F.showpp t
strengthenRefTypeGen, strengthenRefType ::
( OkRTBV v v c tv r
@@ -622,15 +620,6 @@
strengthenRefType_ f t1 (RAllP p t2)
= RAllP p $ strengthenRefType_ f t1 t2
-strengthenRefType_ f (RAllE x tx t1) (RAllE y ty t2) | x == y
- = RAllE x (strengthenRefType_ f tx ty) $ strengthenRefType_ f t1 t2
-
-strengthenRefType_ f (RAllE x tx t1) t2
- = RAllE x tx $ strengthenRefType_ f t1 t2
-
-strengthenRefType_ f t1 (RAllE x tx t2)
- = RAllE x tx $ strengthenRefType_ f t1 t2
-
strengthenRefType_ f (RAppTy t1 t1' r1) (RAppTy t2 t2' r2)
= RAppTy t t' (r1 `meet` r2)
where t = strengthenRefType_ f t1 t2
@@ -887,7 +876,6 @@
freeTyVars (RFun _ _ t t' _) = freeTyVars t `L.union` freeTyVars t'
freeTyVars (RApp _ ts _ _) = L.nub $ concatMap freeTyVars ts
freeTyVars (RVar α _) = [makeRTVar α]
-freeTyVars (RAllE _ tx t) = freeTyVars tx `L.union` freeTyVars t
freeTyVars (REx _ tx t) = freeTyVars tx `L.union` freeTyVars t
freeTyVars (RExprArg _) = []
freeTyVars (RAppTy t t' _) = freeTyVars t `L.union` freeTyVars t'
@@ -898,7 +886,6 @@
tyClasses :: (OkRT RTyCon tv r) => RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses (RAllP _ t) = tyClasses t
tyClasses (RAllT _ t _) = tyClasses t
-tyClasses (RAllE _ _ t) = tyClasses t
tyClasses (REx _ _ t) = tyClasses t
tyClasses (RFun _ _ t t' _) = tyClasses t ++ tyClasses t'
tyClasses (RAppTy t t' _) = tyClasses t ++ tyClasses t'
@@ -910,7 +897,7 @@
tyClasses (RVar _ _) = []
tyClasses (RRTy _ _ _ t) = tyClasses t
tyClasses (RHole _) = []
-tyClasses t = panic Nothing ("RefType.tyClasses cannot handle" ++ show t)
+tyClasses t = panic Nothing ("RefType.tyClasses cannot handle" ++ F.showpp t)
--------------------------------------------------------------------------------
@@ -1014,8 +1001,6 @@
= if meet' then t' `strengthen` subt (α, τ) r else t'
| otherwise
= RVar (subt (α', τ) α) r
-subsFree m s z (RAllE x t t')
- = RAllE x (subsFree m s z t) (subsFree m s z t')
subsFree m s z (REx x t t')
= REx x (subsFree m s z t) (subsFree m s z t')
subsFree m s z@(α, τ, _) (RAppTy t t' r)
@@ -1196,7 +1181,6 @@
subt su (RFun x i t1 t2 r) = RFun x i (subt su t1) (subt su t2) r
subt su (RAllP p t) = RAllP p (subt su t)
subt su (RApp c ts ps r) = RApp c (subt su <$> ts) (subt su <$> ps) r
- subt su (RAllE x t1 t2) = RAllE x (subt su t1) (subt su t2)
subt su (REx x t1 t2) = REx x (subt su t1) (subt su t2)
subt _ (RExprArg e) = RExprArg e
subt su (RAppTy t1 t2 r) = RAppTy (subt su t1) (subt su t2) r
@@ -1434,8 +1418,6 @@
= TyVarTy α
toType useRFInfo (RApp RTyCon{rtc_tc = c} ts _ _)
= TyConApp c (toType useRFInfo <$> filter notExprArg ts)
-toType useRFInfo (RAllE _ _ t)
- = toType useRFInfo t
toType useRFInfo (REx _ _ t)
= toType useRFInfo t
toType useRFInfo (RAppTy t (RExprArg _) _)
@@ -1820,7 +1802,6 @@
go p (RAllT _ t _) = go p t
go p (RAllP _ t) = go p t
go p (RApp c ts _ _) = mconcat (zipWith go (getPosition p <$> varianceTyArgs (rtc_info c)) ts)
- go p (RAllE _ t1 t2) = go p t1 <> go p t2
go p (REx _ t1 t2) = go p t1 <> go p t2
go _ (RExprArg _) = mempty
go p (RAppTy t1 t2 _) = go p t1 <> go p t2
diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs
--- a/src/Language/Haskell/Liquid/UX/CmdLine.hs
+++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs
@@ -38,38 +38,36 @@
) where
import Prelude hiding (error)
-
+import Prelude (error)
import Control.Monad
import Control.Monad.IO.Class
+import Data.Char (toLower)
import Data.Maybe
-import Data.Functor ((<&>))
-import Data.Aeson (encode)
+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.Console.GetOpt
+import qualified Language.Fixpoint.Verbosity as FxV
import System.Directory
import System.Exit
import System.Environment
-import System.Console.CmdArgs.Explicit
-import System.Console.CmdArgs.Implicit hiding (Verbosity(..))
-import System.Console.CmdArgs.Text
import GitHash
-import Data.List (nub, intercalate)
-
+import Data.List (nub, intercalate)
import qualified Language.Fixpoint.Types.Config as FC
import qualified Language.Fixpoint.Misc as F
import Language.Fixpoint.Types.Names
-import Language.Fixpoint.Types hiding (panic, Error, Result, saveQuery)
+import 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.Errors hiding (typ)
import Language.Haskell.Liquid.Types.PrettyPrint ()
import Language.Haskell.Liquid.Types.Types
import qualified Language.Haskell.Liquid.UX.ACSS as ACSS
@@ -77,8 +75,7 @@
import qualified Liquid.GHC.API as GHC
import Language.Haskell.TH.Syntax.Compat (fromCode, toCode)
-import Text.PrettyPrint.HughesPJ hiding (Mode, (<>))
-
+import Text.PrettyPrint.HughesPJ hiding ((<>))
---------------------------------------------------------------------------------
@@ -91,372 +88,418 @@
---------------------------------------------------------------------------------
-- Parsing Command Line----------------------------------------------------------
---------------------------------------------------------------------------------
-config :: Mode (CmdArgs Config)
-config = cmdArgsMode defConfig
+-- | Default configuration: plain Haskell record, no cmdargs annotations.
defConfig :: Config
-defConfig = Config {
- loggingVerbosity
- = enum [ Minimal &= name "minimal" &= help "Minimal logging verbosity"
- , Quiet &= name "quiet" &= help "Silent logging verbosity"
- , Normal &= name "normal" &= help "Normal logging verbosity"
- , Loud &= name "verbose" &= help "Verbose logging"
- ]
-
- , fullcheck
- = def
- &= help "Full Checking: check all binders (DEFAULT)"
-
- , diffcheck
- = def
- &= help "Incremental Checking: only check changed binders"
-
- , higherorder
- = def
- &= help "Allow higher order binders into the logic"
-
- , smtTimeout
- = def
- &= help "Timeout of smt queries in msec"
-
- , higherorderqs
- = def
- &= help "Allow higher order qualifiers to get automatically instantiated"
-
- , linear
- = def
- &= help "Use uninterpreted integer multiplication and division"
-
- , stringTheory
- = def
- &= help "Interpretation of Strings by z3"
-
- , saveQuery
- = def &= help "Save fixpoint query to file (slow)"
-
- , checks
- = def &= help "Check a specific (top-level) binder"
- &= name "check-var"
-
- , pruneUnsorted
- = False &= help "Disable prunning unsorted Predicates"
- &= name "prune-unsorted"
-
- , notermination
- = False
- &= help "Disable Termination Check"
- &= name "no-termination-check"
-
- , nopositivity
- = False
- &= help "Disable Data Type Positivity Check"
- &= name "no-positivity-check"
-
- , rankNTypes
- = False &= help "Adds precise reasoning on presence of rankNTypes"
- &= name "rankNTypes"
-
- , noclasscheck
- = False
- &= help "Disable Class Instance Check"
- &= name "no-class-check"
-
- , nostructuralterm
- = def &= name "no-structural-termination"
- &= help "Disable structural termination check"
-
- , bscope
- = False &= help "scope of the outer binders on the inner refinements"
- &= name "bscope"
-
- , totalHaskell
- = False &= help "Check for termination and totality; overrides no-termination flags"
- &= name "total-Haskell"
-
- , nowarnings
- = False &= help "Don't display warnings, only show errors"
- &= name "no-warnings"
-
- , noannotations
- = False &= help "Don't create intermediate annotation files"
- &= name "no-annotations"
-
- , checkDerived
- = False &= help "Check GHC generated binders (e.g. Read, Show instances)"
- &= name "check-derived"
-
- , caseExpandDepth
- = 2 &= help "Maximum depth at which to expand DEFAULT in case-of (default=2)"
- &= name "max-case-expand"
-
- , notruetypes
- = False &= help "Disable Trueing Top Level Types"
- &= name "no-true-types"
-
- , nototality
- = False &= help "Disable totality check"
- &= name "no-totality"
-
- , cores
- = Just 1 &= help "Use the given number of cores to solve logical constraints (default: 1). Warning: unpredictable performance. See https://github.com/ucsd-progsys/liquidhaskell/issues/2562"
-
- , minPartSize
- = FC.defaultMinPartSize
- &= help "If solving on multiple cores, ensure that partitions are of at least m size"
-
- , maxPartSize
- = FC.defaultMaxPartSize
- &= help ("If solving on multiple cores, once there are as many partitions " ++
- "as there are cores, don't merge partitions if they will exceed this " ++
- "size. Overrides the minpartsize option.")
-
- , smtsolver
- = Nothing &= help "Name of SMT-Solver"
-
- , noCheckUnknown
- = def &= explicit
- &= name "no-check-unknown"
- &= help "Don't complain about specifications for unexported and unused values "
-
- , maxParams
- = defaultMaxParams &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)"
-
- , shortNames
- = False &= name "short-names"
- &= help "Print shortened names, i.e. drop all module qualifiers."
-
- , shortErrors
- = False &= name "short-errors"
- &= help "Don't show long error messages, just line numbers."
-
- , adtSpec
- = False &= help "Generate ADT representations in refinement logic"
- &= name "adt"
-
- , expectErrorContaining
- = [] &= help "Expect an error which containing the provided string from verification (can be provided more than once)"
- &= name "expect-error-containing"
+defConfig = Config
+ { loggingVerbosity = Minimal
+ , fullcheck = False
+ , diffcheck = False
+ , higherorder = False
+ , smtTimeout = Nothing
+ , higherorderqs = False
+ , linear = False
+ , stringTheory = False
+ , saveQuery = False
+ , saveBfqOnError = False
+ , checks = []
+ , pruneUnsorted = False
+ , notermination = False
+ , nopositivity = False
+ , rankNTypes = False
+ , noclasscheck = False
+ , nostructuralterm = False
+ , bscope = False
+ , totalHaskell = False
+ , nowarnings = False
+ , noannotations = False
+ , checkDerived = False
+ , caseExpandDepth = 2
+ , notruetypes = False
+ , nototality = False
+ , cores = Just 1
+ , minPartSize = FC.defaultMinPartSize
+ , maxPartSize = FC.defaultMaxPartSize
+ , smtsolver = Nothing
+ , noCheckUnknown = False
+ , maxParams = defaultMaxParams
+ , shortNames = False
+ , shortErrors = False
+ , adtSpec = False
+ , expectErrorContaining = []
+ , expectAnyError = False
+ , scrapeInternals = False
+ , elimStats = False
+ , elimBound = Nothing
+ , json = False
+ , counterExamples = False
+ , timeBinds = False
+ , untidyCore = False
+ , eliminate = FC.Some
+ , noPatternInline = False
+ , noSimplifyCore = False
+ , noslice = False
+ , noLiftedImport = False
+ , proofLogicEval = False
+ , pleWithUndecidedGuards = False
+ , interpreter = False
+ , proofLogicEvalLocal = False
+ , etabeta = False
+ , dependantCase = False
+ , extensionality = False
+ , nopolyinfer = False
+ , reflection = False
+ , compileSpec = False
+ , typeclass = False
+ , auxInline = False
+ , rwTerminationCheck = False
+ , skipModule = False
+ , fuel = Nothing
+ , environmentReduction = False
+ , noEnvironmentReduction = False
+ , inlineANFBindings = False
+ , pandocHtml = False
+ , excludeAutomaticAssumptionsFor = []
+ , dumpOpaqueReflections = False
+ , dumpPreNormalizedCore = False
+ , dumpNormalizedCore = False
+ , allowUnsafeConstructors = False
+ , ddumpTimings = False
+ , modern = False
+ , warnOnTermHoles = False
+ }
- , expectAnyError
- = False &= help "Expect an error, no matter which kind or what it contains"
- &= name "expect-any-error"
+-- | A flag is either a config transformer or a request for --help/--version.
+data Flag
+ = FlagMod (Config -> Config)
+ | FlagHelp
+ | FlagVersion
- , scrapeInternals
- = False &= help "Scrape qualifiers from auto generated specifications"
- &= name "scrape-internals"
- &= explicit
+-- | The GetOpt option table. Each entry lists all accepted long-option
+-- names (aliases included) so that legacy pragmas keep working.
+lhOptions :: [OptDescr Flag]
+lhOptions =
+ -- Verbosity
+ [ opt [] ["minimal"] (NoArg $ fm $ \c -> c { loggingVerbosity = Minimal })
+ "Minimal logging verbosity (default)"
+ , opt [] ["quiet"] (NoArg $ fm $ \c -> c { loggingVerbosity = Quiet })
+ "Silent logging verbosity"
+ , opt [] ["normal"] (NoArg $ fm $ \c -> c { loggingVerbosity = Normal })
+ "Normal logging verbosity"
+ , opt [] ["verbose"] (NoArg $ fm $ \c -> c { loggingVerbosity = Loud })
+ "Verbose logging"
- , elimStats
- = False &= name "elimStats"
- &= help "Print eliminate stats"
+ -- Checking mode
+ , opt [] ["fullcheck"] (NoArg $ fm $ \c -> c { fullcheck = True })
+ "Full Checking: check all binders (DEFAULT)"
+ , opt [] ["diffcheck", "diff"] (NoArg $ fm $ \c -> c { diffcheck = True })
+ "Incremental Checking: only check changed binders"
+ , opt [] ["higherorder"] (NoArg $ fm $ \c -> c { higherorder = True })
+ "Allow higher order binders into the logic"
+ , opt [] ["higherorderqs"] (NoArg $ fm $ \c -> c { higherorderqs = True })
+ "Allow higher order qualifiers to get automatically instantiated"
+ , opt [] ["linear"] (NoArg $ fm $ \c -> c { linear = True })
+ "Use uninterpreted integer multiplication and division"
+ , opt [] ["string-theory", "stringtheory"] (NoArg $ fm $ \c -> c { stringTheory = True })
+ "Interpretation of Strings by z3"
+ , opt [] ["save-query", "save"] (NoArg $ fm $ \c -> c { saveQuery = True })
+ "Save fixpoint query to file (slow)"
+ , opt [] ["save-bfq-on-error"] (NoArg $ fm $ \c -> c { saveBfqOnError = True })
+ "Save fixpoint query as .bfq only when verification fails"
- , elimBound
- = Nothing
- &= name "elimBound"
- &= help "Maximum chain length for eliminating KVars"
+ -- SMT
+ , opt [] ["smt-timeout"] (ReqArg (fm . setSmtTimeout) "MSEC")
+ "Timeout of smt queries in msec"
+ , opt [] ["smtsolver"] (ReqArg (fm . setSmtSolverOpt) "SOLVER")
+ "SMT solver to use: z3, z3mem, cvc4, cvc5, mathsat"
+ , opt [] ["cores"] (ReqArg (fm . setCores) "N")
+ (unlines
+ [ "Number of cores to use (default 1)"
+ , "Use the given number of cores to solve logical constraints (default: 1)."
+ , "Warning: unpredictable performance."
+ , "See https://github.com/ucsd-progsys/liquidhaskell/issues/2562"
+ ]
+ )
+ , opt [] ["min-part-size"] (ReqArg (fm . setMinPartSize) "N")
+ "Minimum partition size for multi-core solving"
+ , opt [] ["max-part-size"] (ReqArg (fm . setMaxPartSize) "N")
+ "Maximum partition size for multi-core solving"
- , noslice
- = False
- &= name "noSlice"
- &= help "Disable non-concrete KVar slicing"
+ -- Checking options
+ , opt [] ["check-var", "checks"] (ReqArg (fm . addCheckVar) "VAR")
+ "Check a specific (top-level) binder (can be repeated)"
+ , opt [] ["prune-unsorted", "pruneunsorted"] (NoArg $ fm $ \c -> c { pruneUnsorted = True })
+ "Prune unsorted predicates"
+ , opt [] ["no-termination-check", "no-termination", "notermination"]
+ (NoArg $ fm $ \c -> c { notermination = True })
+ "Disable Termination Check"
+ , opt [] ["no-positivity-check"] (NoArg $ fm $ \c -> c { nopositivity = True })
+ "Disable Data Type Positivity Check"
+ , opt [] ["rankNTypes"] (NoArg $ fm $ \c -> c { rankNTypes = True })
+ "Adds precise reasoning on presence of rankNTypes"
+ , opt [] ["no-class-check", "noclasscheck"] (NoArg $ fm $ \c -> c { noclasscheck = True })
+ "Disable Class Instance Check"
+ , opt [] ["no-structural-termination", "nostruct"]
+ (NoArg $ fm $ \c -> c { nostructuralterm = True })
+ "Disable structural termination check"
+ , opt [] ["bscope"] (NoArg $ fm $ \c -> c { bscope = True })
+ "Scope of the outer binders on the inner refinements"
+ , opt [] ["total-Haskell"] (NoArg $ fm $ \c -> c { totalHaskell = True })
+ "Check for termination and totality; overrides no-termination flags"
+ , opt [] ["no-warnings"] (NoArg $ fm $ \c -> c { nowarnings = True })
+ "Don't display warnings, only show errors"
+ , opt [] ["no-annotations"] (NoArg $ fm $ \c -> c { noannotations = True })
+ "Don't create intermediate annotation files"
+ , opt [] ["check-derived"] (NoArg $ fm $ \c -> c { checkDerived = True })
+ "Check GHC generated binders (e.g. Read, Show instances)"
+ , opt [] ["max-case-expand"] (ReqArg (fm . setCaseExpandDepth) "N")
+ "Maximum depth at which to expand DEFAULT in case-of (default=2)"
+ , opt [] ["no-true-types"] (NoArg $ fm $ \c -> c { notruetypes = True })
+ "Disable Trueing Top Level Types"
+ , opt [] ["no-totality"] (NoArg $ fm $ \c -> c { nototality = True })
+ "Disable totality check"
+ , opt [] ["totality"] (NoArg $ fm $ \c -> c { nototality = False })
+ "Enable totality check (default)"
+ , opt [] ["no-check-unknown"] (NoArg $ fm $ \c -> c { noCheckUnknown = True })
+ "Don't complain about specifications for unexported and unused values"
+ , opt [] ["max-params", "maxparams"] (ReqArg (fm . setMaxParams) "N")
+ "Restrict qualifier mining to at most N parameters (default 2)"
+ , opt [] ["short-names"] (NoArg $ fm $ \c -> c { shortNames = True })
+ "Print shortened names, i.e. drop all module qualifiers"
+ , opt [] ["short-errors"] (NoArg $ fm $ \c -> c { shortErrors = True })
+ "Don't show long error messages, just line numbers"
+ , opt [] ["adt"] (NoArg $ fm $ \c -> c { adtSpec = True })
+ "Generate ADT representations in refinement logic"
+ , opt [] ["expect-error-containing"] (ReqArg (fm . addExpectError) "MSG")
+ "Expect an error containing MSG (can be repeated)"
+ , opt [] ["expect-any-error"] (NoArg $ fm $ \c -> c { expectAnyError = True })
+ "Expect an error, no matter which kind"
+ , opt [] ["scrape-internals"] (NoArg $ fm $ \c -> c { scrapeInternals = True })
+ "Scrape qualifiers from auto generated specifications"
+ , opt [] ["elimStats"] (NoArg $ fm $ \c -> c { elimStats = True })
+ "Print eliminate stats"
+ , opt [] ["elimBound"] (ReqArg (fm . setElimBound) "N")
+ "Maximum chain length for eliminating KVars"
+ , opt [] ["noSlice"] (NoArg $ fm $ \c -> c { noslice = True })
+ "Disable non-concrete KVar slicing"
+ , opt [] ["no-lifted-imports"] (NoArg $ fm $ \c -> c { noLiftedImport = True })
+ "Disable loading lifted specifications (for legacy libs)"
+ , opt [] ["json"] (NoArg $ fm $ \c -> c { json = True })
+ "Print results in JSON (for editor integration)"
+ , opt [] ["counter-examples"] (NoArg $ fm $ \c -> c { counterExamples = True })
+ "Attempt to generate counter-examples to type errors (experimental!)"
+ , opt [] ["time-binds"] (NoArg $ fm $ \c -> c { timeBinds = True })
+ "Solve each (top-level) asserted type signature separately & time solving"
+ , opt [] ["untidy-core"] (NoArg $ fm $ \c -> c { untidyCore = True })
+ "Print fully qualified identifier names in verbose mode"
+ , opt [] ["eliminate"] (ReqArg (fm . setEliminate) "ELIM")
+ (unlines
+ [ "Use elimination for 'all', 'some' (default), 'none', 'horn', or 'existentials'"
+ , " all: use TRUE for cut-kvars"
+ , " some: use quals for cut-kvars"
+ , " none: use quals for all kvars"
+ , " horn: ??"
+ , " existentials: ??"
+ ]
+ )
+ , opt [] ["no-pattern-inline"] (NoArg $ fm $ \c -> c { noPatternInline = True })
+ "Don't inline special patterns (e.g. >>= and return) during constraint generation"
+ , opt [] ["no-simplify-core"] (NoArg $ fm $ \c -> c { noSimplifyCore = True })
+ "Don't simplify GHC core before constraint generation"
- , noLiftedImport
- = False
- &= name "no-lifted-imports"
- &= help "Disable loading lifted specifications (for legacy libs)"
+ -- PLE options
+ , opt [] ["ple"] (NoArg $ fm $ \c -> c { proofLogicEval = True })
+ "Enable Proof-by-Logical-Evaluation"
+ , opt [] ["ple-with-undecided-guards"] (NoArg $ fm $ \c -> c { pleWithUndecidedGuards = True })
+ "Unfold invocations with undecided guards in PLE"
+ , opt [] ["interpreter"] (NoArg $ fm $ \c -> c { interpreter = True })
+ "Use an interpreter to assist PLE in solving constraints"
+ , opt [] ["ple-local"] (NoArg $ fm $ \c -> c { proofLogicEvalLocal = True })
+ "Enable Proof-by-Logical-Evaluation locally, per function"
+ , opt [] ["etabeta"] (NoArg $ fm $ \c -> c { etabeta = True })
+ "Eta expand and beta reduce terms to aid PLE"
+ , opt [] ["dependantcase"] (NoArg $ fm $ \c -> c { dependantCase = True })
+ "Allow PLE to reason about dependent cases"
+ , opt [] ["extensionality"] (NoArg $ fm $ \c -> c { extensionality = True })
+ "Enable extensional interpretation of function equality"
+ , opt [] ["fast"] (NoArg $ fm $ \c -> c { nopolyinfer = True })
+ "No inference of polymorphic type application (imprecise but faster)"
+ , opt [] ["reflection"] (NoArg $ fm $ \c -> c { reflection = True })
+ "Enable reflection of Haskell functions and theorem proving"
+ , opt [] ["compile-spec"] (NoArg $ fm $ \c -> c { compileSpec = True })
+ "Only compile specifications (into .bspec file); skip verification"
+ , opt [] ["typeclass"] (NoArg $ fm $ \c -> c { typeclass = True })
+ "Enable Typeclass support"
+ , opt [] ["aux-inline"] (NoArg $ fm $ \c -> c { auxInline = True })
+ "Enable inlining of class methods"
+ , opt [] ["rw-termination-check"] (NoArg $ fm $ \c -> c { rwTerminationCheck = True })
+ ("Enable the rewrite divergence checker. Can speed up verification if rewriting\n" ++
+ "terminates, but can also cause divergence."
+ )
+ , opt [] ["skip-module"] (NoArg $ fm $ \c -> c { skipModule = True })
+ "Completely skip this module"
+ , opt [] ["fuel"] (ReqArg (fm . setFuel) "N")
+ "Maximum fuel (per-function unfoldings) for PLE"
+ , opt [] ["environment-reduction"] (NoArg $ fm $ \c -> c { environmentReduction = True })
+ "Perform environment reduction (disabled by default)"
+ , opt [] ["no-environment-reduction"] (NoArg $ fm $ \c -> c { noEnvironmentReduction = True })
+ "Don't perform environment reduction"
+ , opt [] ["inline-anf-bindings"] (NoArg $ fm $ \c -> c { inlineANFBindings = True })
+ ("Inline ANF bindings (sometimes improves performance and sometimes worsens it)\n" ++
+ "Disabled by --no-environment-reduction"
+ )
+ , opt [] ["pandoc-html"] (NoArg $ fm $ \c -> c { pandocHtml = True })
+ "Use pandoc to generate html"
+ , opt [] ["exclude-automatic-assumptions-for"] (ReqArg (fm . addExcludeAssumptions) "PACKAGE")
+ "Stop loading LHAssumptions modules for imports in these packages (repeat for multiple packages)"
+ , opt [] ["dump-opaque-reflections"] (NoArg $ fm $ \c -> c { dumpOpaqueReflections = True })
+ "Dump all generated opaque reflections"
+ , opt [] ["dump-pre-normalized-core"] (NoArg $ fm $ \c -> c { dumpPreNormalizedCore = True })
+ "Dump pre-normalized core (before a-normalization)"
+ , opt [] ["dump-normalized-core"] (NoArg $ fm $ \c -> c { dumpNormalizedCore = True })
+ "Dump a-normalized core"
+ , opt [] ["allow-unsafe-constructors"] (NoArg $ fm $ \c -> c { allowUnsafeConstructors = True })
+ "Allow refining constructors with unsafe refinements"
+ , opt [] ["ddump-timings"] (NoArg $ fm $ \c -> c { ddumpTimings = True })
+ "Dump time measures of the Liquid Haskell plugin"
+ , opt [] ["modern"] (NoArg $ fm $ \c -> c { modern = True })
+ "Enable modern features (--reflection, --ple, --etabeta, --dependantcase)"
+ , opt [] ["warn-on-term-holes"] (NoArg $ fm $ \c -> c { warnOnTermHoles = True })
+ "Warn about holes in terms"
- , json
- = False &= name "json"
- &= help "Print results in JSON (for editor integration)"
+ -- Meta
+ , opt "h" ["help"] (NoArg FlagHelp) "Show this help message"
+ , opt "V" ["version"] (NoArg FlagVersion) "Show version information"
+ ]
+ where
+ opt s l a h = Option s l a h
+ fm = FlagMod
- , counterExamples
- = False &= name "counter-examples"
- &= help "Attempt to generate counter-examples to type errors (experimental!)"
+-- | Helpers for option argument parsing.
+setSmtTimeout :: String -> Config -> Config
+setSmtTimeout s c = c { smtTimeout = Just (readInt "smt-timeout" s) }
- , timeBinds
- = False &= name "time-binds"
- &= help "Solve each (top-level) asserted type signature separately & time solving."
+setSmtSolverOpt :: String -> Config -> Config
+setSmtSolverOpt s c = c { smtsolver = Just (parseSMTSolver s) }
- , untidyCore
- = False &= name "untidy-core"
- &= help "Print fully qualified identifier names in verbose mode"
+setCores :: String -> Config -> Config
+setCores s c = c { cores = Just (readInt "cores" s) }
- , eliminate
- = FC.Some
- &= name "eliminate"
- &= help "Use elimination for 'all' (use TRUE for cut-kvars), 'some' (use quals for cut-kvars) or 'none' (use quals for all kvars)."
+setMinPartSize :: String -> Config -> Config
+setMinPartSize s c = c { minPartSize = readInt "min-part-size" s }
- , noPatternInline
- = False &= name "no-pattern-inline"
- &= help "Don't inline special patterns (e.g. `>>=` and `return`) during constraint generation."
+setMaxPartSize :: String -> Config -> Config
+setMaxPartSize s c = c { maxPartSize = readInt "max-part-size" s }
- , noSimplifyCore
- = False &= name "no-simplify-core"
- &= help "Don't simplify GHC core before constraint generation"
+addCheckVar :: String -> Config -> Config
+addCheckVar s c = c { checks = checks c ++ [s] }
- -- 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"
+setCaseExpandDepth :: String -> Config -> Config
+setCaseExpandDepth s c = c { caseExpandDepth = readInt "max-case-expand" s }
- , proofLogicEval
- = False
- &= help "Enable Proof-by-Logical-Evaluation"
- &= name "ple"
+setMaxParams :: String -> Config -> Config
+setMaxParams s c = c { maxParams = readInt "max-params" s }
- , pleWithUndecidedGuards
- = False
- &= help "Unfold invocations with undecided guards in PLE"
- &= name "ple-with-undecided-guards"
- &= explicit
+addExpectError :: String -> Config -> Config
+addExpectError s c = c { expectErrorContaining = expectErrorContaining c ++ [s] }
- , interpreter
- = False
- &= help "Use an interpreter to assist PLE in solving constraints"
- &= name "interpreter"
+setElimBound :: String -> Config -> Config
+setElimBound s c = c { elimBound = Just (readInt "elimBound" s) }
- , proofLogicEvalLocal
- = False
- &= help "Enable Proof-by-Logical-Evaluation locally, per function"
- &= name "ple-local"
+setEliminate :: String -> Config -> Config
+setEliminate s c = c { eliminate = parseEliminate s }
- , etabeta
- = False
- &= help "Eta expand and beta reduce terms to aid PLE"
- &= name "etabeta"
+setFuel :: String -> Config -> Config
+setFuel s c = c { fuel = Just (readInt "fuel" s) }
- , dependantCase
- = False
- &= help "Allow PLE to reason about dependent cases"
- &= name "dependantcase"
+addExcludeAssumptions :: String -> Config -> Config
+addExcludeAssumptions s c =
+ c { excludeAutomaticAssumptionsFor = excludeAutomaticAssumptionsFor c ++ [s] }
- , extensionality
- = False
- &= help "Enable extensional interpretation of function equality"
- &= name "extensionality"
+readInt :: String -> String -> Int
+readInt opt s = case reads s of
+ [(n, "")] -> n
+ _ -> error $ "Expected integer for --" ++ opt ++ ", got: " ++ show s
- , nopolyinfer
- = False
- &= help "No inference of polymorphic type application. Gives imprecision, but speedup."
- &= name "fast"
+parseSMTSolver :: String -> FC.SMTSolver
+parseSMTSolver s = case map toLower s of
+ "z3" -> FC.Z3
+ "z3mem" -> FC.Z3mem
+ "z3 api" -> FC.Z3mem
+ "cvc4" -> FC.Cvc4
+ "cvc5" -> FC.Cvc5
+ "mathsat" -> FC.Mathsat
+ _ -> error $ "Unknown SMT solver: " ++ show s
+ ++ ". Use one of: z3, z3mem, cvc4, cvc5, mathsat"
- , reflection
- = False
- &= help "Enable reflection of Haskell functions and theorem proving"
- &= name "reflection"
+parseEliminate :: String -> FC.Eliminate
+parseEliminate s = case map toLower s of
+ "none" -> FC.None
+ "some" -> FC.Some
+ "all" -> FC.All
+ "horn" -> FC.Horn
+ "existentials" -> FC.Existentials
+ _ -> error $ "Unknown eliminate value: " ++ show s
+ ++ ". Use one of: none, some, all, horn, existentials"
- , compileSpec
- = False
- &= name "compile-spec"
- &= help "Only compile specifications (into .bspec file); skip verification"
+-- | Map LH's 'Verbosity' to liquid-fixpoint's 'Language.Fixpoint.Verbosity.Verbosity'
+-- and set the global IORef so that whenLoud/whenNormal work throughout the solver.
+setFxVerbosity :: Verbosity -> IO ()
+setFxVerbosity Quiet = FxV.setVerbosity FxV.Quiet
+setFxVerbosity Minimal = FxV.setVerbosity FxV.Quiet
+setFxVerbosity Normal = FxV.setVerbosity FxV.Normal
+setFxVerbosity Loud = FxV.setVerbosity FxV.Loud
- , typeclass
- = False
- &= help "Enable Typeclass"
- &= name "typeclass"
- , auxInline
- = False
- &= help "Enable inlining of class methods"
- &= name "aux-inline"
- ,
- rwTerminationCheck
- = False
- &= name "rw-termination-check"
- &= help ( "Enable the rewrite divergence checker. "
- ++ "Can speed up verification if rewriting terminates, but can also cause divergence."
- )
- ,
- skipModule
- = False
- &= name "skip-module"
- &= help "Completely skip this module, don't even compile any specifications in it."
+getOpts :: [String] -> IO Config
+getOpts as = do
+ cfg0 <- envCfg
+ case getOpt Permute lhOptions as of
+ (flags, _rest, []) -> do
+ when (any isHelp flags) $ putStr (formatHelp usageHeader lhOptions) >> error "LiquidHaskell:--help"
+ when (any isVersion flags) $ putStrLn copyright >> error "LiquidHaskell:--version"
+ let mods = [f | FlagMod f <- flags]
+ let cfg1 = foldl (flip ($)) cfg0 mods
+ let cfg2 = if json cfg1 then cfg1 { loggingVerbosity = Quiet } else cfg1
+ setFxVerbosity (loggingVerbosity cfg2)
+ withSmtSolver cfg2
+ (_, _, optErrs) ->
+ putStr (concat optErrs ++ formatHelp usageHeader lhOptions) >> exitFailure
- , fuel
- = Nothing
- &= help "Maximum fuel (per-function unfoldings) for PLE"
+usageHeader :: String
+usageHeader = "Liquid Haskell Options:"
- , environmentReduction
- = False
- &= explicit
- &= name "environment-reduction"
- &= help "perform environment reduction (disabled by default)"
- , noEnvironmentReduction
- = False
- &= explicit
- &= name "no-environment-reduction"
- &= help "Don't perform environment reduction"
- , inlineANFBindings
- = False
- &= explicit
- &= name "inline-anf-bindings"
- &= help (unwords
- [ "Inline ANF bindings."
- , "Sometimes improves performance and sometimes worsens it."
- , "Disabled by --no-environment-reduction"
- ])
- , pandocHtml
- = False
- &= name "pandoc-html"
- &= help "Use pandoc to generate html."
- , excludeAutomaticAssumptionsFor
- = []
- &= explicit
- &= name "exclude-automatic-assumptions-for"
- &= help "Stop loading LHAssumptions modules for imports in these packages."
- &= typ "PACKAGE"
- , dumpOpaqueReflections
- = False &= help "Dump all generated opaque reflections"
- &= name "dump-opaque-reflections"
- &= explicit
- , dumpPreNormalizedCore
- = False &= help "Dump pre-normalized core (before a-normalization)"
- &= name "dump-pre-normalized-core"
- &= explicit
- , dumpNormalizedCore
- = False &= help "Dump a-normalized core"
- &= name "dump-normalized-core"
- &= explicit
- , allowUnsafeConstructors
- = False &= help "Allow refining constructors with unsafe refinements"
- &= name "allow-unsafe-constructors"
- &= explicit
- , ddumpTimings
- = False &= help "Dump time measures of the Liquid Haskell plugin"
- &= name "ddump-timings"
- &= explicit
- , modern
- = False &= help "Enable modern features; enables --reflection, --ple, --etabeta, --dependantcase"
- &= name "modern"
- , warnOnTermHoles
- = False &= help "Warn about holes in terms"
- &= name "warn-on-term-holes"
- &= explicit
- } &= program "liquidhaskell"
- &= help "Refinement Types for Haskell"
- &= summary copyright
- &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell" ]
+-- | Format the help text in a man-page style: each option's synopsis on its
+-- own line, followed by the description indented on the next line.
+--
+-- Example output:
+--
+-- @
+-- --ple
+--
+-- Enable Proof-by-Logical-Evaluation
+--
+-- --reflection
+--
+-- Enable reflection of Haskell functions and theorem proving
+-- @
+formatHelp :: String -> [OptDescr a] -> String
+formatHelp hdr opts = unlines $ intercalate [""] $ [hdr] : map formatOne opts
+ where
+ formatOne (Option shorts longs argD helpTxt) =
+ let indentedDesc = map (" " ++) $ lines helpTxt
+ in [ " " ++ synopsis shorts longs argD
+ , ""
+ ] ++
+ indentedDesc
-getOpts :: [String] -> IO Config
-getOpts as = do
- cfg0 <- envCfg
- cfg1 <- cmdArgsRun'
- config { modeValue = (modeValue config)
- { cmdArgsValue = cfg0 }
- }
- as
- let cfg2 = if json cfg1 then cfg1 {loggingVerbosity = Quiet} else cfg1
- setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg2)
- withSmtSolver cfg2
+ synopsis shorts longs argD =
+ intercalate ", " $
+ [ "-" ++ [s] | s <- shorts ]
+ ++ [ "--" ++ l ++ argSuffix argD | l <- longs ]
-cmdArgsRun' :: Mode (CmdArgs a) -> [String] -> IO a
-cmdArgsRun' md as
- = case parseResult of
- Left e -> putStrLn (helpMsg e) >> exitFailure
- Right a -> cmdArgsApply a
- where
- helpMsg e = showText defaultWrap $ helpText [e] HelpFormatDefault md
- parseResult = process md (wideHelp as)
- wideHelp = map (\a -> if a == "--help" || a == "-help" then "--help=120" else a)
+ argSuffix (NoArg _) = ""
+ argSuffix (ReqArg _ mv) = "=" ++ mv
+ argSuffix (OptArg _ mv) = "[=" ++ mv ++ "]"
--------------------------------------------------------------------------------
@@ -482,27 +525,30 @@
FC.Z3mem -> return $ Just FC.Z3mem
smt -> maybe Nothing (const $ Just smt) <$> findExecutable (show smt)
+-- | Parse the @LIQUIDHASKELL_OPTS@ environment variable (if set) to produce a
+-- baseline 'Config'. Unlike the old cmdargs-based @parsePragma@, this
+-- implementation properly handles multiple space-separated options.
envCfg :: IO Config
envCfg = do
so <- lookupEnv "LIQUIDHASKELL_OPTS"
case so of
Nothing -> return defConfig
- Just s -> parsePragma $ envLoc s
+ Just s -> applyGetOpt defConfig (words s)
where
- envLoc = Loc l l
- l = safeSourcePos "ENVIRONMENT" 1 1
+ applyGetOpt cfg toks =
+ case getOpt Permute lhOptions toks of
+ (flags, _, []) ->
+ return $ foldl (flip ($)) cfg [f | FlagMod f <- flags]
+ (_, _, optErrs) ->
+ putStrLn (unlines optErrs) >> exitFailure
copyright :: String
copyright = concat $ concat
[ ["LiquidHaskell "]
, [$(simpleVersion Meta.version)]
, [gitInfo]
- -- , [" (" ++ _commitCount ++ " commits)" | _commitCount /= ("1"::String) &&
- -- _commitCount /= ("UNKNOWN" :: String)]
- , ["\nCopyright 2013-19 Regents of the University of California. All Rights Reserved.\n"]
+ , ["\n\nCopyright 2013-19 Regents of the University of California. All Rights Reserved.\n"]
]
- where
- _commitCount = $gitCommitCount
gitInfo :: String
gitInfo = msg
@@ -517,7 +563,6 @@
gitMsg gi = concat
[ " [", giBranch gi, "@", giHash gi
, " (", giCommitDate gi, ")"
- -- , " (", show (giCommitCount gi), " commits in HEAD)"
, "] "
]
@@ -544,24 +589,41 @@
--------------------------------------------------------------------------------
withPragmas cfg ps action
= do cfg' <- liftIO $ processPragmas cfg ps <&> canonConfig
- -- As the verbosity is set /globally/ via the cmdargs lib, re-set it.
- liftIO $ setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg')
+ -- The global verbosity IORef (read by liquid-fixpoint) must be kept in
+ -- sync whenever the verbosity may have changed.
+ liftIO $ setFxVerbosity (loggingVerbosity cfg')
res <- action cfg'
- liftIO $ setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg) -- restore the original verbosity.
+ liftIO $ setFxVerbosity (loggingVerbosity cfg) -- restore
pure res
+-- | Apply a list of pragma strings (each is one option, e.g. @"--ple"@ or
+-- @"--expect-error-containing=Mismatch"@) on top of an existing 'Config'.
+-- Each pragma string is tokenised with 'words' so that a two-token form like
+-- @"--check-var foo"@ also works.
processPragmas :: Config -> [Located String] -> IO Config
-processPragmas c pragmas =
- processValueIO
- config { modeValue = (modeValue config) { cmdArgsValue = c } }
- (val <$> pragmas)
- >>=
- cmdArgsApply
+processPragmas cfg pragmas = foldM applyOne cfg pragmas
+ where
+ applyOne c loc =
+ case getOpt Permute lhOptions (words (val loc)) of
+ (flags, _, []) -> do
+ when (any isHelp flags) $
+ putStr (formatHelp usageHeader lhOptions) >> error "LiquidHaskell:--help"
+ when (any isVersion flags) $
+ putStrLn copyright >> error "LiquidHaskell:--version"
+ return $ foldl (flip ($)) c [f | FlagMod f <- flags]
+ (_, _, optErrs) ->
+ putStrLn (unlines optErrs) >> exitFailure
--- | Note that this function doesn't process list arguments properly, like
--- 'expectErrorContaining'
--- TODO: This is only used to parse the contents of the env var LIQUIDHASKELL_OPTS
--- so it should be able to parse multiple arguments instead. See issue #1990.
+isHelp :: Flag -> Bool
+isHelp FlagHelp = True
+isHelp _ = False
+
+isVersion :: Flag -> Bool
+isVersion FlagVersion = True
+isVersion _ = False
+
+-- | Parse a single pragma string against 'defConfig'.
+-- Also used to parse the @LIQUIDHASKELL_OPTS@ environment variable.
parsePragma :: Located String -> IO Config
parsePragma = processPragmas defConfig . (:[])
diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs
--- a/src/Language/Haskell/Liquid/UX/Config.hs
+++ b/src/Language/Haskell/Liquid/UX/Config.hs
@@ -1,6 +1,5 @@
-- | Command Line Configuration Options ----------------------------------------
-{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
module Language.Haskell.Liquid.UX.Config (
@@ -8,7 +7,6 @@
, HasConfig (..)
, Verbosity (..)
, allowPLE, allowLocalPLE, allowGlobalPLE
- , cmdargsVerbosity
, patternFlag
, higherOrderFlag
, pruneFlag
@@ -23,18 +21,9 @@
import Prelude hiding (error)
import Language.Fixpoint.Types.Config hiding (Config)
import GHC.Generics
-import System.Console.CmdArgs hiding (Verbosity(..))
-import qualified System.Console.CmdArgs as CmdArgs
data Verbosity = Quiet | Minimal | Normal | Loud
- deriving (Data, Generic, Show, Eq, Ord)
-
--- | liquid-fixpoint uses CmdArg.Verbosity at least to show the progress bar.
-cmdargsVerbosity :: Verbosity -> CmdArgs.Verbosity
-cmdargsVerbosity Quiet = CmdArgs.Quiet
-cmdargsVerbosity Minimal = CmdArgs.Quiet
-cmdargsVerbosity Normal = CmdArgs.Normal
-cmdargsVerbosity Loud = CmdArgs.Loud
+ deriving (Generic, Show, Eq, Ord)
-- NOTE: adding strictness annotations breaks the help message
@@ -48,6 +37,7 @@
, smtTimeout :: Maybe Int -- ^ smt timeout
, fullcheck :: Bool -- ^ check all binders (overrides diffcheck)
, saveQuery :: Bool -- ^ save fixpoint query
+ , saveBfqOnError :: Bool -- ^ save fixpoint query as .bfq only on verification failure
, checks :: [String] -- ^ set of binders to check
, noCheckUnknown :: Bool -- ^ whether to complain about specifications for unexported and unused values
, notermination :: Bool -- ^ disable termination check
@@ -117,7 +107,7 @@
-- Only needed to work around https://github.com/haskell/cabal/issues/11116
, modern :: Bool -- ^ Enable modern features; enables reflection, ple, etabeta, dependantcase, adt
, warnOnTermHoles :: Bool -- ^ Warn about holes in the terms
- } deriving (Generic, Data, Show, Eq)
+ } deriving (Generic, Show, Eq)
allowPLE :: Config -> Bool
allowPLE cfg
diff --git a/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs b/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs
--- a/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs
+++ b/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs
@@ -171,8 +171,6 @@
simplifyBareType'' s(RAllP _ t) =
simplifyBareType'' s t
-simplifyBareType'' s (RAllE _ _ t) =
- simplifyBareType'' s t
simplifyBareType'' s (REx _ _ t) =
simplifyBareType'' s t
simplifyBareType'' s (RRTy _ _ _ t) =
diff --git a/src/Language/Haskell/Liquid/UX/Tidy.hs b/src/Language/Haskell/Liquid/UX/Tidy.hs
--- a/src/Language/Haskell/Liquid/UX/Tidy.hs
+++ b/src/Language/Haskell/Liquid/UX/Tidy.hs
@@ -172,7 +172,6 @@
tyVars (RAppTy t t' _) = tyVars t ++ tyVars t'
tyVars (RApp _ ts _ _) = concatMap tyVars ts
tyVars (RVar α _) = [α]
-tyVars (RAllE _ _ t) = tyVars t
tyVars (REx _ _ t) = tyVars t
tyVars (RExprArg _) = []
tyVars (RRTy _ _ _ t) = tyVars t
@@ -199,7 +198,6 @@
funBinds (RAllP _ t) = funBinds t
funBinds (RFun b _ t1 t2 _) = b : funBinds t1 ++ funBinds t2
funBinds (RApp _ ts _ _) = concatMap funBinds ts
-funBinds (RAllE b t1 t2) = b : funBinds t1 ++ funBinds t2
funBinds (REx b t1 t2) = b : funBinds t1 ++ funBinds t2
funBinds (RVar _ _) = []
funBinds (RRTy _ _ _ t) = funBinds t
diff --git a/tests/Parser.hs b/tests/Parser.hs
--- a/tests/Parser.hs
+++ b/tests/Parser.hs
@@ -260,6 +260,10 @@
parseSingleSpec "x :: k:Int -> Int" @?==
"x :: k:Int -> Int"
+ , testCase "k:Int -> B (k + 1)" $
+ parseSingleSpec "x :: k:Int -> B (k + 1)" @?==
+ "x :: k:Int -> (B {k + 1})"
+
, testCase "type spec 1 " $
parseSingleSpec "type IncrListD a D = [a]<{\\x y -> (x+D) <= y}>" @?==
"type IncrListD a D = [a]<\\x##2 _ -> {y##3 : LIQUID$dummy | x##2 + D <= y##3}>"
@@ -485,6 +489,18 @@
, "unexpected ':'"
, "expecting \"->\", \"=>\", '/', bareTyArgP, end of input, mmonoPredicateP, or monoPredicateP"
]
+
+ , testCase "type t = Nat (type aliases should start with upper case)" $
+ parseSingleSpec "type t = Nat" @?==
+ unlines
+ [ "