liquidhaskell-boot 0.9.14.1 → 0.9.14.1.1
raw patch · 37 files changed
+817/−739 lines, 37 filesdep −cmdargsdep −optparse-applicativedep ~liquid-fixpoint
Dependencies removed: cmdargs, optparse-applicative
Dependency ranges changed: liquid-fixpoint
Files
- liquidhaskell-boot.cabal +2/−5
- src/Language/Haskell/Liquid/Bare/Check.hs +0/−4
- src/Language/Haskell/Liquid/Bare/DataType.hs +2/−2
- src/Language/Haskell/Liquid/Bare/Elaborate.hs +0/−18
- src/Language/Haskell/Liquid/Bare/Expand.hs +1/−4
- src/Language/Haskell/Liquid/Bare/Misc.hs +0/−2
- src/Language/Haskell/Liquid/Bare/Plugged.hs +0/−1
- src/Language/Haskell/Liquid/Bare/Resolve.hs +1/−1
- src/Language/Haskell/Liquid/Bare/ToBare.hs +0/−1
- src/Language/Haskell/Liquid/Bare/Typeclass.hs +0/−2
- src/Language/Haskell/Liquid/Constraint/Env.hs +0/−8
- src/Language/Haskell/Liquid/Constraint/Generate.hs +2/−2
- src/Language/Haskell/Liquid/Constraint/Init.hs +4/−1
- src/Language/Haskell/Liquid/Constraint/Qualifier.hs +0/−1
- src/Language/Haskell/Liquid/Constraint/Relational.hs +32/−12
- src/Language/Haskell/Liquid/Constraint/Split.hs +0/−21
- src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +2/−2
- src/Language/Haskell/Liquid/Constraint/Types.hs +0/−3
- src/Language/Haskell/Liquid/GHC/Plugin.hs +2/−2
- src/Language/Haskell/Liquid/LHNameResolution.hs +11/−3
- src/Language/Haskell/Liquid/Measure.hs +1/−1
- src/Language/Haskell/Liquid/Parse.hs +11/−7
- src/Language/Haskell/Liquid/Transforms/RefSplit.hs +0/−111
- src/Language/Haskell/Liquid/Types/Dictionaries.hs +1/−1
- src/Language/Haskell/Liquid/Types/Equality.hs +0/−2
- src/Language/Haskell/Liquid/Types/Errors.hs +2/−2
- src/Language/Haskell/Liquid/Types/Fresh.hs +0/−12
- src/Language/Haskell/Liquid/Types/PredType.hs +0/−4
- src/Language/Haskell/Liquid/Types/PrettyPrint.hs +1/−19
- src/Language/Haskell/Liquid/Types/RType.hs +289/−61
- src/Language/Haskell/Liquid/Types/RTypeOp.hs +0/−16
- src/Language/Haskell/Liquid/Types/RefType.hs +2/−21
- src/Language/Haskell/Liquid/UX/CmdLine.hs +432/−370
- src/Language/Haskell/Liquid/UX/Config.hs +3/−13
- src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +0/−2
- src/Language/Haskell/Liquid/UX/Tidy.hs +0/−2
- tests/Parser.hs +16/−0
liquidhaskell-boot.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-boot-version: 0.9.14.1+version: 0.9.14.1.1 synopsis: Liquid Types for Haskell description: This package provides a plugin to verify Haskell programs. But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)@@ -81,7 +81,6 @@ Language.Haskell.Liquid.Transforms.ANF Language.Haskell.Liquid.Transforms.CoreToLogic Language.Haskell.Liquid.Transforms.QuestionMark- Language.Haskell.Liquid.Transforms.RefSplit Language.Haskell.Liquid.Transforms.Rewrite Language.Haskell.Liquid.Transforms.Simplify Language.Haskell.Liquid.Transforms.InlineAux@@ -130,7 +129,6 @@ , bytestring >= 0.10 , Cabal , cereal- , cmdargs >= 0.10 , containers >= 0.5 , deepseq >= 1.3 , directory >= 1.2@@ -143,9 +141,8 @@ , gitrev , hashable >= 1.3 && < 1.6 , hscolour >= 1.22- , liquid-fixpoint == 0.9.6.3.6+ , liquid-fixpoint == 0.9.6.3.7 , mtl >= 2.1- , optparse-applicative < 0.20 , githash , megaparsec >= 8 , pretty >= 1.1
src/Language/Haskell/Liquid/Bare/Check.hs view
@@ -597,7 +597,6 @@ L.foldl' (\merr t -> merr <|> go t) Nothing ts go (RFun _ _ t1 t2 _) = go t1 <|> go t2 go (RVar _ _) = Nothing- go (RAllE _ t1 t2) = go t1 <|> go t2 go (REx _ t1 t2) = go t1 <|> go t2 go (RAppTy t1 t2 _) = go t1 <|> go t2 go (RRTy _ _ _ t) = go t@@ -629,7 +628,6 @@ go t@(RApp c ts rs r) = check (toRSort t :: RSort) r <|> efold go ts <|> go' c rs go t@(RFun _ _ t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2 go t@(RVar _ r) = check (toRSort t :: RSort) r- go (RAllE _ t1 t2) = go t1 <|> go t2 go (REx _ t1 t2) = go t1 <|> go t2 go t@(RAppTy t1 t2 r) = check (toRSort t :: RSort) r <|> go t1 <|> go t2 go (RRTy xts _ _ t) = efold go (snd <$> xts) <|> go t@@ -812,8 +810,6 @@ isRefined ty hasInnerRefinement (RApp _ args _ _) = any isRefined args-hasInnerRefinement (RAllE _ allarg ty) =- isRefined allarg || isRefined ty hasInnerRefinement (REx _ allarg ty) = isRefined allarg || isRefined ty hasInnerRefinement (RAppTy arg res _) =
src/Language/Haskell/Liquid/Bare/DataType.hs view
@@ -608,7 +608,7 @@ checkDataDecl :: Ghc.TyCon -> DataDecl -> Bool checkDataDecl c d = F.notracepp _msg (isGADT || cN == dN || null (tycDCons d)) where- _msg = printf "checkDataDecl: D = %s, c = %s, cN = %d, dN = %d" (show d) (show c) cN dN+ _msg = printf "checkDataDecl: D = %s, c = %s, cN = %d, dN = %d" (showpp d) (show c) cN dN cN = length (GM.tyConTyVarsDef c) dN = length (tycTyVars d) isGADT = Ghc.isGadtSyntaxTyCon c@@ -732,7 +732,7 @@ getPsSig m pos (RHole r) = addps m pos r getPsSig _ _ z- = panic Nothing $ "getPsSig" ++ show z+ = panic Nothing $ "getPsSig" ++ showpp z getPsSigPs :: [(UsedPVar, a)] -> Bool -> SpecProp -> [(a, Bool)] getPsSigPs m pos (RProp _ (RHole r)) = addps m pos r
src/Language/Haskell/Liquid/Bare/Elaborate.hs view
@@ -151,12 +151,6 @@ , _rtf_reft :: !r } - | RAllEF {- _rtf_bind :: !F.Symbol- , _rtf_allarg :: !f- , _rtf_ty :: !f- }- | RExF { _rtf_bind :: !F.Symbol , _rtf_exarg :: !f@@ -199,7 +193,6 @@ project (RAllT tvbind ty ref ) = RAllTF tvbind ty ref project (RAllP pvbind ty ) = RAllPF pvbind ty project (RApp c args pargs reft ) = RAppF c args pargs reft-project (RAllE bind allarg ty ) = RAllEF bind allarg ty project (REx bind exarg ty ) = RExF bind exarg ty project (RExprArg e ) = RExprArgF e project (RAppTy arg res reft ) = RAppTyF arg res reft@@ -212,7 +205,6 @@ embed (RAllTF tvbind ty ref ) = RAllT tvbind ty ref embed (RAllPF pvbind ty ) = RAllP pvbind ty embed (RAppF c args pargs reft ) = RApp c args pargs reft-embed (RAllEF bind allarg ty ) = RAllE bind allarg ty embed (RExF bind exarg ty ) = REx bind exarg ty embed (RExprArgF e ) = RExprArg e embed (RAppTyF arg res reft ) = RAppTy arg res reft@@ -250,9 +242,6 @@ | isClassType tin -> collectSpecTypeBinders tout | otherwise -> let (bs, abs') = collectSpecTypeBinders tout in (bind : bs, abs')- RAllE b _ t ->- let (bs, abs') = collectSpecTypeBinders t- in (b : bs, abs') RAllT (RTVar (RTV ab) _) t _ -> let (bs, abs') = collectSpecTypeBinders t in (bs, F.symbol ab : abs')@@ -273,7 +262,6 @@ RFun bind _ tin tout _ | isClassType tin -> go tout | otherwise -> mkHsLam (noLocA [nlVarPat (varSymbolToRdrName bind)]) (go tout)- RAllE _ _ t -> go t RAllT _ t _ -> go t REx _ _ t -> go t RAppTy _ t _ -> go t@@ -435,11 +423,6 @@ ) ) -- todo: Existential support- RAllE bind allarg ty -> do- (eAllarg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify allarg- (eTy , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty- let (eTyRenamed, canonicalBinders) = canonicalizeDictBinder bs (eTy, bs')- pure (RAllE bind eAllarg eTyRenamed, canonicalBinders) REx bind allarg ty -> do (eAllarg, bs ) <- elaborateSpecType' partialTp coreToLogic simplify allarg (eTy , bs') <- elaborateSpecType' partialTp coreToLogic simplify ty@@ -706,7 +689,6 @@ RApp RTyCon { rtc_tc = tc } ts _ _ -> mkHsTyConApp (getRdrName tc) [ specTypeToLHsType t | t <- ts, notExprArg t ]- RAllE _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) REx _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) RAppTy _ (RExprArg _) _ -> impossible Nothing "RExprArg should not appear here"
src/Language/Haskell/Liquid/Bare/Expand.hs view
@@ -252,7 +252,6 @@ go (RApp c ts rs _) = go_alias (val $ btc_tc c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs) go (RFun _ _ t1 t2 _) = go t1 ++ go t2 go (RAppTy t1 t2 _) = go t1 ++ go t2- go (RAllE _ t1 t2) = go t1 ++ go t2 go (REx _ t1 t2) = go t1 ++ go t2 go (RAllT _ t _) = go t go (RAllP _ t) = go t@@ -420,7 +419,6 @@ go (RFun x i t1 t2 r) = RFun x i (go t1) (go t2) r go (RAllT a t r) = RAllT a (go t) r go (RAllP a t) = RAllP a (go t)- go (RAllE x t1 t2) = RAllE x (go t1) (go t2) go (REx x t1 t2) = REx x (go t1) (go t2) go (RRTy e r o t) = RRTy e r o (go t) go t@RHole{} = t@@ -474,7 +472,7 @@ go (RApp x [] [] _) = EVar (getLHNameSymbol $ val $ btc_tc x) go (RApp f ts [] _) = F.eApps (EVar (getLHNameSymbol $ val $ btc_tc f)) (go <$> ts) go (RAppTy t1 t2 _) = EApp (go t1) (go t2)- go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show z) msg+ go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (showpp z) msg sp = Just (GM.sourcePosSrcSpan l) isRExprArg :: RType c tv r -> Bool@@ -570,7 +568,6 @@ nGiven = length rs (_, rrest) = splitAt nExpected rs lambdaRest = [r | r@(RProp binds _) <- rrest, not (null binds)]- walkCheck sp (RAllE _ t1 t2) = walkCheck sp t1 `seq` walkCheck sp t2 walkCheck sp (REx _ t1 t2) = walkCheck sp t1 `seq` walkCheck sp t2 walkCheck sp (RAppTy t1 t2 _) = walkCheck sp t1 `seq` walkCheck sp t2 walkCheck sp (RRTy xts _ _ t) = foldWalk sp (snd <$> xts) `seq` walkCheck sp t
src/Language/Haskell/Liquid/Bare/Misc.hs view
@@ -81,8 +81,6 @@ put s' mapTyVars allowTC τ (RAllP _ t) = mapTyVars allowTC τ t-mapTyVars allowTC τ (RAllE _ _ t)- = mapTyVars allowTC τ t mapTyVars allowTC τ (RRTy _ _ _ t) = mapTyVars allowTC τ t mapTyVars allowTC τ (REx _ _ t)
src/Language/Haskell/Liquid/Bare/Plugged.hs view
@@ -275,7 +275,6 @@ go (RAllT _ t _) (RAllT a t' r) = RAllT a (go t t') r go (RAllT a t r) t' = RAllT a (go t t') r go t (RAllP p t') = RAllP p (go t t')- go t (RAllE b a t') = RAllE b a (go t t') go t (REx b x t') = REx b x (go t t') go t (RRTy e r o t') = RRTy e r o (go t t') go (RAppTy t1 t2 _) (RAppTy t1' t2' r) = RAppTy (go t1 t1') (go t2 t2') r
src/Language/Haskell/Liquid/Bare/Resolve.hs view
@@ -379,6 +379,7 @@ where goReft bs r = return (f bs r) goRFun bs x i t1 t2 r = RFun x i{permitTC = Just (typeclass (getConfig env))} <$> (rebind x <$> go bs t1) <*> go (x:bs) t2 <*> goReft bs r+ -- See the documentation of 'RFun' for what rebind accomplishes. rebind x t = F.subst1 t (x, F.EVar $ rTypeValueVar t) go bs (RAppTy t1 t2 r) = RAppTy <$> go bs t1 <*> go bs t2 <*> goReft bs r go bs (RApp tc ts rs r) = goRApp bs tc ts rs r@@ -388,7 +389,6 @@ where a' = dropTyVarInfo (mapTyVarValue RT.bareRTyVar a) go bs (RAllP a t) = RAllP a' <$> go bs t where a' = ofBPVar env l a- go bs (RAllE x t1 t2) = RAllE x <$> go bs t1 <*> go bs t2 go bs (REx x t1 t2) = REx x <$> go bs t1 <*> go (x:bs) t2 go bs (RRTy xts r o t) = RRTy <$> xts' <*> goReft bs r <*> pure o <*> go bs t where xts' = mapM (traverse (go bs)) xts
src/Language/Haskell/Liquid/Bare/ToBare.hs view
@@ -53,7 +53,6 @@ go (RAllT α t r) = RAllT (goRTV α) (go t) r go (RAllP π t) = RAllP (goPV π) (go t) go (RFun x i t t' r) = RFun x i (go t) (go t') r- go (RAllE x t t') = RAllE x (go t) (go t') go (REx x t t') = REx x (go t) (go t') go (RAppTy t t' r) = RAppTy (go t) (go t') r go (RApp c ts rs r) = RApp (cF c) (go <$> ts) (goRTP <$> rs) r
src/Language/Haskell/Liquid/Bare/Typeclass.hs view
@@ -301,8 +301,6 @@ | RApp tc ts tps r <- t -- TODO: handle rtprop properly = RApp tc (renameTvs rename <$> ts) tps r- | RAllE b allarg ty <- t- = RAllE b (renameTvs rename allarg) (renameTvs rename ty) | REx b exarg ty <- t = REx b (renameTvs rename exarg) (renameTvs rename ty) | RExprArg _ <- t
src/Language/Haskell/Liquid/Constraint/Env.hs view
@@ -79,7 +79,6 @@ import Language.Haskell.Liquid.Types.Types hiding (binds) import Language.Haskell.Liquid.Constraint.Types import Language.Haskell.Liquid.Constraint.Fresh ()-import Language.Haskell.Liquid.Transforms.RefSplit import qualified Language.Haskell.Liquid.UX.CTags as Tg -- import Debug.Trace (trace)@@ -177,13 +176,6 @@ y' <- fresh γ' <- addCGEnv tx γ (eMsg, y', tyy) addCGEnv tx γ' (eMsg, x, tyx `F.subst1` (y, F.EVar y'))--addCGEnv tx γ (eMsg, sym, RAllE yy tyy tyx)- = addCGEnv tx γ (eMsg, sym, t)- where- xs = localBindsOfType tyy (renv γ)- t = L.foldl' meet ttrue [ tyx' `F.subst1` (yy, F.EVar x) | x <- xs]- (tyx', ttrue) = splitXRelatedRefs yy tyx addCGEnv tx γ (_, x, t') = do idx <- fresh
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -1131,13 +1131,13 @@ return t -------------------------------------------------------------------------------- -checkUnbound :: (Show a, Show a2, F.Subable a, F.Variable a ~ F.Symbol)+checkUnbound :: (PPrint a, Show a2, F.Subable a, F.Variable a ~ F.Symbol) => CGEnv -> CoreExpr -> F.Symbol -> a -> a2 -> a checkUnbound γ e x t a | x `notElem` F.syms t = t | otherwise = panic (Just $ getLocation γ) msg where- msg = unlines [ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t+ msg = unlines [ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ showpp t , "In" , GM.showPpr e , "Arg = "
src/Language/Haskell/Liquid/Constraint/Init.hs view
@@ -82,7 +82,10 @@ let tcb = fmap (rTypeSort tce) <$> concat bs let cbs = giCbs . giSrc $ info rTrue <- mapM (traverse (true allowTC)) f6- let γ0 = measEnv sp (head bs) cbs tcb lt1s lt2s (f6 ++ bs!!3) (bs!!5) hs info+ -- Issue #2537: reflected sigs (f6) must come AFTER assumed sigs (bs!!3) so that+ -- when both exist for the same symbol (e.g., assume-reflect actual functions),+ -- the strengthened reflected sig wins in M.fromList (which keeps the last entry).+ let γ0 = measEnv sp (head bs) cbs tcb lt1s lt2s (bs!!3 ++ f6) (bs!!5) hs info γ <- globalize <$> foldM (+=) γ0 ( [("initEnv", x, y) | (x, y) <- concat (rTrue:tail bs)]) return γ {invs = is (invs1 ++ invs2)} where
src/Language/Haskell/Liquid/Constraint/Qualifier.hs view
@@ -178,7 +178,6 @@ go γ (RFun x _ t t' _) = go γ t ++ goBind x t γ t' go γ t@(RApp c ts rs _) = scrape γ t ++ concatMap (go γ') ts ++ goRefs c γ' rs where γ' = add (rTypeValueVar t) t γ- go γ (RAllE x t t') = go γ t ++ goBind x t γ t' go γ (REx x t t') = go γ t ++ goBind x t γ t' go _ _ = [] goRefs c g rs = concat $ zipWith (goRef g) rs (rTyConPVs c)
src/Language/Haskell/Liquid/Constraint/Relational.hs view
@@ -48,7 +48,7 @@ import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Types hiding (binds) import Language.Haskell.Liquid.UX.Config-import System.Console.CmdArgs.Verbosity (whenLoud)+import Language.Fixpoint.Verbosity (whenLoud) import System.IO.Unsafe (unsafePerformIO) data RelPred@@ -119,8 +119,6 @@ as' = map removeAbsRef as r' = MkUReft r mempty out = RApp c' as' [] r'-removeAbsRef (RAllE b a t)- = RAllE b (removeAbsRef a) (removeAbsRef t) removeAbsRef (REx b a t) = REx b (removeAbsRef a) (removeAbsRef t) removeAbsRef (RAppTy s t r)@@ -187,9 +185,29 @@ consRelCheckBind _ _ (Rec [(_, e1)]) (Rec [(_, e2)]) t1 t2 _ rp = F.panic $ "consRelCheckBind Rec: exprs, types, and pred should have same number of args " ++- show (args e1 e2 t1 t2 p)+ showppArgs (args e1 e2 t1 t2 p) where p = fromRelExpr rp+ showppArgs :: Maybe ([Var], [Var], [F.Symbol], [F.Symbol], [SpecType], [SpecType], [F.Expr]) -> String+ showppArgs Nothing = "Nothing"+ showppArgs (Just (xs1, xs2, vs1, vs2, ts1, ts2, qs)) =+ concat+ [ "Just ("+ , F.showpp xs1+ , ", "+ , F.showpp xs2+ , ", "+ , F.showpp vs1+ , ", "+ , F.showpp vs2+ , ", "+ , F.showpp ts1+ , ", "+ , F.showpp ts2+ , ", "+ , F.showpp qs+ , ")"+ ] consRelCheckBind _ _ b1@(Rec _) b2@(Rec _) _ _ _ _ = F.panic $ "consRelCheckBind Rec: multiple binders are not supported " ++ F.showpp (b1, b2)@@ -559,14 +577,16 @@ γ'' <- γ' += ("consRelSub Base R", rr, t2) let cstr = F.subst (F.mkSubst [(resL, F.EVar rl), (resR, F.EVar rr)]) $ F.PImp p1 p2 entl γ'' (traceWhenLoud ("consRelSub Base cstr " ++ F.showpp cstr) cstr) "consRelSub Base"-consRelSub _ t1@(RHole _) t2@(RHole _) _ _ = F.panic $ "consRelSub is undefined for RHole " ++ show (t1, t2)-consRelSub _ t1@(RExprArg _) t2@(RExprArg _) _ _ = F.panic $ "consRelSub is undefined for RExprArg " ++ show (t1, t2)-consRelSub _ t1@REx {} t2@REx {} _ _ = F.panic $ "consRelSub is undefined for REx " ++ show (t1, t2)-consRelSub _ t1@RAllE {} t2@RAllE {} _ _ = F.panic $ "consRelSub is undefined for RAllE " ++ show (t1, t2)-consRelSub _ t1@RRTy {} t2@RRTy {} _ _ = F.panic $ "consRelSub is undefined for RRTy " ++ show (t1, t2)-consRelSub _ t1@RAllP {} t2@RAllP {} _ _ = F.panic $ "consRelSub is undefined for RAllP " ++ show (t1, t2)-consRelSub _ t1@RAllT {} t2@RAllT {} _ _ = F.panic $ "consRelSub is undefined for RAllT " ++ show (t1, t2)-consRelSub _ t1 t2 _ _ = F.panic $ "consRelSub is undefined for different types " ++ show (t1, t2)+consRelSub _ t1@(RHole _) t2@(RHole _) _ _ = F.panic $ "consRelSub is undefined for RHole " ++ showppP (t1, t2)+consRelSub _ t1@(RExprArg _) t2@(RExprArg _) _ _ = F.panic $ "consRelSub is undefined for RExprArg " ++ showppP (t1, t2)+consRelSub _ t1@REx {} t2@REx {} _ _ = F.panic $ "consRelSub is undefined for REx " ++ showppP (t1, t2)+consRelSub _ t1@RRTy {} t2@RRTy {} _ _ = F.panic $ "consRelSub is undefined for RRTy " ++ showppP (t1, t2)+consRelSub _ t1@RAllP {} t2@RAllP {} _ _ = F.panic $ "consRelSub is undefined for RAllP " ++ showppP (t1, t2)+consRelSub _ t1@RAllT {} t2@RAllT {} _ _ = F.panic $ "consRelSub is undefined for RAllT " ++ showppP (t1, t2)+consRelSub _ t1 t2 _ _ = F.panic $ "consRelSub is undefined for different types " ++ showppP (t1, t2)++showppP :: (PPrint a, PPrint b) => (a, b) -> String+showppP (x, y) = "(" ++ showpp x ++ ", " ++ showpp y ++ ")" -------------------------------------------------------------- -- Helper Definitions ----------------------------------------
src/Language/Haskell/Liquid/Constraint/Split.hs view
@@ -93,12 +93,6 @@ ws'' <- concat <$> mapM (rsplitW γ) rs return $ ws ++ ws' ++ ws'' -splitW (WfC γ (RAllE x tx t))- = do ws <- splitW (WfC γ tx)- γ' <- γ += ("splitW1", x, tx)- ws' <- splitW (WfC γ' t)- return $ ws ++ ws'- splitW (WfC γ (REx x tx t)) = do ws <- splitW (WfC γ tx) γ' <- γ += ("splitW2", x, tx)@@ -173,20 +167,6 @@ γ' <- γ += ("addExBind 2", y, forallExprRefType γ tx) splitC allowTC (SubC γ' (F.subst1 t1 (x, F.EVar y)) t2) -splitC allowTC (SubC γ (RAllE x tx t1) (RAllE x2 _ t2)) | x == x2- = do γ' <- γ += ("addAllBind 3", x, forallExprRefType γ tx)- splitC allowTC (SubC γ' t1 t2)--splitC allowTC (SubC γ (RAllE x tx t1) t2)- = do y <- fresh- γ' <- γ += ("addAABind 1", y, forallExprRefType γ tx)- splitC allowTC (SubC γ' (t1 `F.subst1` (x, F.EVar y)) t2)--splitC allowTC (SubC γ t1 (RAllE x tx t2))- = do y <- fresh- γ' <- γ += ("addAllBind 2", y, forallExprRefType γ tx)- splitC allowTC (SubC γ' t1 (F.subst1 t2 (x, F.EVar y)))- splitC allowTC (SubC cgenv (RRTy env _ OCons t1) t2) = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) cgenv xts c1 <- splitC allowTC (SubC γ' t1' t2')@@ -288,7 +268,6 @@ traceTy (RAllP _ t) = parens ("RAllP " ++ traceTy t) traceTy (RAllT _ t _) = parens ("RAllT " ++ traceTy t) traceTy (RFun _ _ t t' _) = parens ("RFun " ++ parens (traceTy t) ++ parens (traceTy t'))-traceTy (RAllE _ tx t) = parens ("RAllE " ++ parens (traceTy tx) ++ parens (traceTy t)) traceTy (REx _ tx t) = parens ("REx " ++ parens (traceTy tx) ++ parens (traceTy t)) traceTy (RExprArg _) = "RExprArg" traceTy (RAppTy t t' _) = parens ("RAppTy " ++ parens (traceTy t) ++ parens (traceTy t'))
src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs view
@@ -13,7 +13,6 @@ import qualified Liquid.GHC.API as Ghc import Liquid.GHC.API (Var, Id, TyCon) import qualified Language.Fixpoint.Types.Config as FC-import System.Console.CmdArgs.Default (def) import qualified Language.Fixpoint.Types as F import Language.Fixpoint.Solver.Rewrite (unify) import Language.Haskell.Liquid.Constraint.Types@@ -38,12 +37,13 @@ import Language.Haskell.Liquid.Types.Types hiding ( binds ) fixConfig :: FilePath -> Config -> FC.Config-fixConfig tgt cfg = def+fixConfig tgt cfg = FC.defConfig { FC.solver = Mb.fromJust (smtsolver cfg) , FC.linear = linear cfg , FC.eliminate = eliminate cfg , FC.nonLinCuts = not (higherOrderFlag cfg) -- eliminate cfg /= FC.All , FC.save = saveQuery cfg+ , FC.saveBfqOnError = saveBfqOnError cfg , FC.srcFile = tgt , FC.cores = cores cfg , FC.minPartSize = minPartSize cfg
src/Language/Haskell/Liquid/Constraint/Types.hs view
@@ -128,9 +128,6 @@ instance PPrint CGEnv where pprintTidy k = pprintTidy k . renv -instance Show CGEnv where- show = showpp- getLocation :: CGEnv -> SrcSpan getLocation = srcSpan . cgLoc
src/Language/Haskell/Liquid/GHC/Plugin.hs view
@@ -413,7 +413,7 @@ continue :: TcM (Either LiquidCheckException a) continue = pure $ Left (ErrorsOccurred []) - reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcM (Either LiquidCheckException a)+ reportErrs :: F.PPrint e => [TError e] -> TcM (Either LiquidCheckException a) reportErrs = LH.filterReportErrors thisFile GHC.failM continue (getFilters cfg) Full checkLiquidHaskellContext :: LiquidHaskellContext -> TcM (Either LiquidCheckException LiquidLib)@@ -561,7 +561,7 @@ dependencies let continue = pure $ Left (ErrorsOccurred [])- reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult)+ reportErrs :: F.PPrint e => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult) reportErrs = LH.filterReportErrors file GHC.failM continue (getFilters moduleCfg) Full (case result of
src/Language/Haskell/Liquid/LHNameResolution.hs view
@@ -209,8 +209,17 @@ checkErrors + -- Rebuild the logic map with fully-resolved define bodies from sp3.+ -- lmap1 was built before resolveLogicNames, so body symbols (e.g. "len")+ -- are bare/unresolved. sp3 has gone through logic name resolution and+ -- fromBareSpecLHName, so its defines carry properly qualified symbols.+ let lmap2 = lmap <> mkLogicMap (HM.fromList+ [ (F.val $ lhNameToResolvedSymbol <$> k,+ v { lmVar = lhNameToResolvedSymbol <$> k })+ | (k, v) <- defines sp3 ])+ dcs <- gets roUsedDataCons- return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1)+ return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap2) where -- Early exit name resolution if errors are found and pass them to the output. checkErrors :: ExceptT [Error] (StateT RenameOutput Identity) ()@@ -490,7 +499,6 @@ go (RFun x i t1 t2 r) = RFun <$> pure x <*> pure i <*> go t1 <*> go t2 <*> pure r go (RAllT a t r) = RAllT <$> pure a <*> go t <*> pure r go (RAllP a t) = RAllP a <$> go t- go (RAllE x t1 t2) = RAllE x <$> go t1 <*> go t2 go (REx x t1 t2) = REx x <$> go t1 <*> go t2 go (RRTy e r o t) = RRTy e r o <$> go t go t@RHole{} = pure t@@ -536,7 +544,7 @@ go (RApp x [] [] _) = EVar (getLHNameSymbol <$> btc_tc x) go (RApp f ts [] _) = eApps (EVar (renameAmbiguousCtor . getLHNameSymbol <$> btc_tc f)) (go <$> ts) go (RAppTy t1 t2 _) = EApp (go t1) (go t2)- go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show $ parsedToBareType z) msg+ go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (showpp $ parsedToBareType z) msg sp = Just (LH.sourcePosSrcSpan l) renameAmbiguousCtor :: Symbol -> Symbol
src/Language/Haskell/Liquid/Measure.hs view
@@ -187,7 +187,7 @@ = Just $ mkSubst $ zipWith (\y x -> (fst x, EVar $ fst y)) xts1' xts2' | otherwise = panic (Just $ sourcePosSrcSpan lc) ("The types for the wrapper and worker data constructors cannot be merged\n"- ++ show t1 ++ "\n" ++ show t2 ++ "\n"+ ++ showpp t1 ++ "\n" ++ showpp t2 ++ "\n" ++ "If there are UNPACK pragmas in effect, consider compiling with\n" ++ "-fomit-interface-pragmas to ignore them.\n" ++ "See https://github.com/ucsd-progsys/liquidhaskell/issues/2629")
src/Language/Haskell/Liquid/Parse.hs view
@@ -494,6 +494,7 @@ <|> try (braces $ RExprArg <$> located exprP) <|> try bareAtomNoAppP <|> try (parens bareTypeP)+ <|> try (parens $ RExprArg <$> located exprP) <?> "bareTyArgP" bareAtomNoAppP :: Parser BareTypeParsed@@ -1316,17 +1317,20 @@ aliasP :: Parser (RTAlias Symbol BareTypeParsed)-aliasP = rtAliasP id bareTypeP <?> "aliasP"+aliasP =+ rtAliasP id (locUpperIdLHNameP LHLogicNameBinder) bareTypeP <?> "aliasP" ealiasP :: Parser (RTAlias Symbol (ExprV LocSymbol))-ealiasP = try (rtAliasP symbol predP)- <|> rtAliasP symbol exprP- <?> "ealiasP"+ealiasP = rtAliasP symbol locBinderLogicNameP exprP <?> "ealiasP" -- | Parser for a LH type synonym.-rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (RTAlias tv ty)-rtAliasP f bodyP- = do lname <- locBinderLogicNameP+rtAliasP+ :: (Symbol -> tv)+ -> Parser (Located LHName)+ -> Parser ty+ -> Parser (RTAlias tv ty)+rtAliasP f nameP bodyP+ = do lname <- nameP args <- many aliasIdP reservedOp "=" body <- bodyP
− src/Language/Haskell/Liquid/Transforms/RefSplit.hs
@@ -1,111 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}--{-# OPTIONS_GHC -Wno-orphans #-}--module Language.Haskell.Liquid.Transforms.RefSplit (-- splitXRelatedRefs-- ) where--import Prelude hiding (error)--import Data.List (partition)--import Language.Haskell.Liquid.Types.RType-import Language.Haskell.Liquid.Types.PrettyPrint ()--import Language.Fixpoint.Types hiding (Predicate)-import Language.Fixpoint.Misc--splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType)-splitXRelatedRefs x t = splitRType x t----splitRType :: Symbol- -> RType c tv (UReft Reft)- -> (RType c tv (UReft Reft), RType c tv (UReft Reft))-splitRType f (RVar a r) = (RVar a r1, RVar a r2)- where- (r1, r2) = splitRef f r-splitRType f (RFun x i tx t r) = (RFun x i tx1 t1 r1, RFun x i tx2 t2 r2)- where- (tx1, tx2) = splitRType f tx- (t1, t2) = splitRType f t- (r1, r2) = splitRef f r-splitRType f (RAllT v t r) = (RAllT v t1 r1, RAllT v t2 r2)- where- (t1, t2) = splitRType f t- (r1, r2) = splitRef f r-splitRType f (RAllP p t) = (RAllP p t1, RAllP p t2)- where- (t1, t2) = splitRType f t-splitRType f (RApp c ts rs r) = (RApp c ts1 rs1 r1, RApp c ts2 rs2 r2)- where- (ts1, ts2) = unzip (splitRType f <$> ts)- (rs1, rs2) = unzip (splitUReft f <$> rs)- (r1, r2) = splitRef f r-splitRType f (RAllE x tx t) = (RAllE x tx1 t1, RAllE x tx2 t2)- where- (tx1, tx2) = splitRType f tx- (t1, t2) = splitRType f t-splitRType f (REx x tx t) = (REx x tx1 t1, REx x tx2 t2)- where- (tx1, tx2) = splitRType f tx- (t1, t2) = splitRType f t-splitRType _ (RExprArg e) = (RExprArg e, RExprArg e)-splitRType f (RAppTy tx t r) = (RAppTy tx1 t1 r1, RAppTy tx2 t2 r2)- where- (tx1, tx2) = splitRType f tx- (t1, t2) = splitRType f t- (r1, r2) = splitRef f r-splitRType f (RRTy xs r o rt) = (RRTy xs1 r1 o rt1, RRTy xs2 r2 o rt2)- where- (xs1, xs2) = unzip (go <$> xs)- (r1, r2) = splitRef f r- (rt1, rt2) = splitRType f rt-- go (x, t) = let (t1, t2) = splitRType f t in ((x,t1), (x, t2))-splitRType f (RHole r) = (RHole r1, RHole r2)- where- (r1, r2) = splitRef f r---splitUReft :: Symbol -> RTProp c tv (UReft Reft) -> (RTProp c tv (UReft Reft), RTProp c tv (UReft Reft))-splitUReft x (RProp xs (RHole r)) = (RProp xs (RHole r1), RProp xs (RHole r2))- where- (r1, r2) = splitRef x r-splitUReft x (RProp xs t) = (RProp xs t1, RProp xs t2)- where- (t1, t2) = splitRType x t--splitRef :: Symbol -> UReft Reft -> (UReft Reft, UReft Reft)-splitRef f (MkUReft r p) = (MkUReft r1 p1, MkUReft r2 p2)- where- (r1, r2) = splitReft f r- (p1, p2) = splitPred f p--splitReft :: Symbol -> Reft -> (Reft, Reft)-splitReft f (Reft (v, xs)) = (Reft (v, pAnd xs1), Reft (v, pAnd xs2))- where- (xs1, xs2) = partition (isFree f) (unPAnd xs)-- unPAnd (PAnd ps) = concatMap unPAnd ps- unPAnd p = [p]---splitPred :: Symbol -> Predicate -> (Predicate, Predicate)-splitPred f (Pr ps) = (Pr ps1, Pr ps2)- where- (ps1, ps2) = partition g ps- g p = any (isFree f) (thd3 <$> pargs p)---class IsFree a where- isFree :: Variable a -> a -> Bool--instance (Subable x) => (IsFree x) where- isFree x p = x `elem` syms p
src/Language/Haskell/Liquid/Types/Dictionaries.hs view
@@ -53,7 +53,7 @@ dlookup (DEnv denv) x = M.lookup x denv -dhasinfo :: (F.Symbolic a1, Show a) => Maybe (M.HashMap F.Symbol a) -> a1 -> Maybe a+dhasinfo :: F.Symbolic a1 => Maybe (M.HashMap F.Symbol a) -> a1 -> Maybe a dhasinfo Nothing _ = Nothing dhasinfo (Just xts) x = M.lookup x' xts where
src/Language/Haskell/Liquid/Types/Equality.hs view
@@ -48,8 +48,6 @@ | x1 == x2 && r1 =*= r2 && and (zipWith (=*=) ps1 ps2) = and <$> zipWithM go ts1 ts2- go (RAllE x1 t11 t12) (RAllE x2 t21 t22) | x1 == x2- = liftM2 (&&) (go t11 t21) (go t12 t22) go (REx x1 t11 t12) (REx x2 t21 t22) | x1 == x2 = liftM2 (&&) (go t11 t21) (go t12 t22) go (RExprArg e1) (RExprArg e2)
src/Language/Haskell/Liquid/Types/Errors.hs view
@@ -645,7 +645,7 @@ -- type CtxError = Error ---------------------------------------------------------------------------------ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc+ppError :: PPrint a => Tidy -> Doc -> TError a -> Doc -------------------------------------------------------------------------------- ppError k dCtx e = ppError' k dCtx e @@ -800,7 +800,7 @@ go _ = Nothing ---------------------------------------------------------------------------------ppError' :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc+ppError' :: PPrint a => Tidy -> Doc -> TError a -> Doc -------------------------------------------------------------------------------- ppError' td dCtx (ErrAssType _ o _ cid c p) = pprintTidy td o
src/Language/Haskell/Liquid/Types/Fresh.hs view
@@ -103,12 +103,6 @@ trueRefType allowTC (RVar a r) = RVar a <$> true allowTC r -trueRefType allowTC (RAllE y ty tx)- = do y' <- fresh- ty' <- true allowTC ty- tx' <- true allowTC tx- return $ RAllE y' ty' (tx' `F.subst1` (y, F.EVar y'))- trueRefType allowTC (RRTy e o r t) = RRTy e o r <$> trueRefType allowTC t @@ -151,12 +145,6 @@ refreshRefType allowTC (RAppTy t t' r) = RAppTy <$> refresh allowTC t <*> refresh allowTC t' <*> refresh allowTC r--refreshRefType allowTC (RAllE y ty tx)- = do y' <- fresh- ty' <- refresh allowTC ty- tx' <- refresh allowTC tx- return $ RAllE y' ty' (tx' `F.subst1` (y, F.EVar y')) refreshRefType allowTC (RRTy e o r t) = RRTy e o r <$> refreshRefType allowTC t
src/Language/Haskell/Liquid/Types/PredType.hs view
@@ -302,7 +302,6 @@ | otherwise = RAllP q (go t) go (RAllT a t r) = RAllT a (go t) (goRR r) go (RFun x i t t' r) = RFun x i (go t) (go t') (goRR r)- go (RAllE x t t') = RAllE x (go t) (go t') go (REx x t t') = REx x (go t) (go t') go (RRTy e r o rt) = RRTy e' (goRR r) o (go rt) where e' = [(x, go t) | (x, t) <- e] go (RAppTy t1 t2 r) = RAppTy (go t1) (go t2) (goRR r)@@ -354,7 +353,6 @@ -- ps has , pargs :: ![(t, Symbol, Expr)] substPred msg su (RRTy e r o t) = RRTy (fmap (substPred msg su) <$> e) r o (substPred msg su t)-substPred msg su (RAllE x t t') = RAllE x (substPred msg su t) (substPred msg su t') substPred msg su (REx x t t') = REx x (substPred msg su t) (substPred msg su t') substPred _ _ t = t @@ -435,8 +433,6 @@ | otherwise = freeArgsPs p t freeArgsPs p (RApp _ ts _ r) = L.nub $ freeArgsPsRef p r ++ concatMap (freeArgsPs p) ts-freeArgsPs p (RAllE _ t1 t2)- = L.nub $ freeArgsPs p t1 ++ freeArgsPs p t2 freeArgsPs p (REx _ t1 t2) = L.nub $ freeArgsPs p t1 ++ freeArgsPs p t2 freeArgsPs p (RAppTy t1 t2 r)
src/Language/Haskell/Liquid/Types/PrettyPrint.hs view
@@ -125,9 +125,6 @@ pprintTidy F.Lossy = shortModules . pprDoc pprintTidy F.Full = pprDoc -instance Show Predicate where- show = showpp- instance (PPrint t) => PPrint (Annot t) where pprintTidy k (AnnUse t) = text "AnnUse" <+> pprintTidy k t pprintTidy k (AnnDef t) = text "AnnDef" <+> pprintTidy k t@@ -137,9 +134,6 @@ instance PPrint a => PPrint (AnnInfo a) where pprintTidy k (AI m) = vcat $ pprAnnInfoBinds k <$> M.toList m -instance PPrint a => Show (AnnInfo a) where- show = showpp- pprAnnInfoBinds :: (PPrint a, PPrint b) => F.Tidy -> (SrcSpan, [(Maybe a, b)]) -> Doc pprAnnInfoBinds k (l, xvs) = vcat $ pprAnnInfoBind k . (l,) <$> xvs@@ -248,8 +242,6 @@ pprRtype bb p t@REx{} = ppExists bb p t-pprRtype bb p t@RAllE{}- = ppAllExpr bb p t pprRtype _ _ (RExprArg e) = braces $ pprint e pprRtype bb p (RAppTy t t' r)@@ -302,16 +294,6 @@ split zs (REx x t t') = split ((x,t):zs) t' split zs t = (reverse zs, t) -ppAllExpr- :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b)))- => PPEnv -> Prec -> RTypeBV b v c tv r -> Doc-ppAllExpr bb p rt- = text "forall" <+> brackets (intersperse comma [pprDbind bb topPrec x t | (x, t) <- ws]) <-> dot <-> pprRtype bb p rt'- where- (ws, rt') = split [] rt- split zs (RAllE x t t') = split ((x,t):zs) t'- split zs t = (reverse zs, t)- ppReftPs :: (OkRTBV b v c tv r, PPrint (RTypeBV b v c tv r), PPrint (RTypeBV b v c tv (NoReftB b))) => t -> t1 -> [RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv r)] -> Doc@@ -474,7 +456,7 @@ -- are unexpected errors, or will call @continue@ otherwise. -- -- An error is expected if there is any filter that matches it.-filterReportErrors :: forall e' a. (Show e', F.PPrint e') => FilePath -> Ghc.TcRn a -> Ghc.TcRn a -> [Filter] -> F.Tidy -> [TError e'] -> Ghc.TcRn a+filterReportErrors :: forall e' a. F.PPrint e' => FilePath -> Ghc.TcRn a -> Ghc.TcRn a -> [Filter] -> F.Tidy -> [TError e'] -> Ghc.TcRn a filterReportErrors path failure continue filters k = filterReportErrorsWith FilterReportErrorsArgs { errorReporter = \errs ->
src/Language/Haskell/Liquid/Types/RType.hs view
@@ -228,14 +228,11 @@ , tcpVarianceTs :: !VarianceInfo , tcpVariancePs :: !VarianceInfo , tcpSizeFun :: !(Maybe SizeFun)- } deriving (Generic, Data)+ } deriving (Generic, Data, Show) instance F.Loc TyConP where srcSpan tc = F.SS (tcpLoc tc) (tcpLoc tc) -instance Show TyConP where- show = F.showpp- instance F.PPrint TyConP where pprintTidy k tc = "data" <+> F.pprintTidy k (tcpCon tc) <+> ppComm k (tcpFreeTyVarsTy tc)@@ -255,15 +252,11 @@ data SizeFunV v = IdSizeFun -- ^ \x -> F.EVar x | SymSizeFun (F.Located v) -- ^ \x -> f x- deriving (Data, Generic, Eq, Functor, Foldable, Traversable)+ deriving (Data, Generic, Eq, Functor, Foldable, Show, Traversable) deriving (B.Binary, Hashable) via Generically (SizeFunV v) instance NFData v => NFData (SizeFunV v) -instance Show v => Show (SizeFunV v) where- show IdSizeFun = "IdSizeFun"- show (SymSizeFun x) = "SymSizeFun " ++ show (F.val x)- szFun :: SizeFun -> Symbol -> Expr szFun IdSizeFun = F.EVar szFun (SymSizeFun f) = \x -> F.mkEApp f [F.EVar x]@@ -279,6 +272,48 @@ type PVar t = PVarV Symbol t type PVarV v t = PVarBV Symbol v t++-- | A predicate variable with arguments, e.g. @p :: x:a -> z:a -> Bool@.+--+-- A 'PVarBV' appears in two roles:+--+-- 1. As a __binder__ inside 'RAllP', declaring the predicate variable and its+-- signature. Here each @pargs@ entry has the form @(t, x, EVar x)@: the+-- expression is the canonical variable itself (identity).+--+-- 2. As a __use site__ inside 'ur_pred' of a 'UReftBV' (as 'UsedPVarBV'),+-- recording which abstract refinement is applied and with which actual+-- argument expressions.+--+-- Example: given+--+-- @{-\@ foo :: forall a \<p :: x:a -> z:a -> Bool\>. y:a -> a\<p y\> \@-}@+--+-- * At the __binder__ (inside 'RAllP'):+-- @PV{pname="p", ptype=a, parg="LIQUID$dummy", pargs=[(a, "x", EVar "x")]}@+-- * At the __use site__ @a\<p y\>@ (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 <z :: Nat, w :: Int> . TYPE"- -- ^^^^^^^^^^^^^^^^^^^ (rt_pvbind)+ -- | A universally quantified type over predicate variables, e.g.+ -- @forall \<p :: Int -> 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\<p (i+1)\>@ of+ --+ -- > assume next :: forall a <p :: Int -> a -> Bool>. i:Int -> a<p i> -> a<p (i+1)>+ --+ -- is A-normalised to:+ --+ -- @REx "ex#0" {v:Int | v == i+1} (RApp a [] [RProp [("ex#0",_)] (a<p ex#0>)] _)@+ --+ -- * @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\<p ex#0\>@, 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\<p m\>@ 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 α)
src/Language/Haskell/Liquid/Types/RTypeOp.hs view
@@ -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
src/Language/Haskell/Liquid/Types/RefType.hs view
@@ -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
src/Language/Haskell/Liquid/UX/CmdLine.hs view
@@ -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 . (:[])
src/Language/Haskell/Liquid/UX/Config.hs view
@@ -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
src/Language/Haskell/Liquid/UX/QuasiQuoter.hs view
@@ -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) =
src/Language/Haskell/Liquid/UX/Tidy.hs view
@@ -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
tests/Parser.hs view
@@ -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+ [ "<test>:1:6:"+ , " |"+ , "1 | type t = Nat"+ , " | ^"+ , "unexpected 't'"+ , "expecting aliasP"+ ]+ ]