Skip to content

Commit f6c97e6

Browse files
facundominguezfacundominguez
authored
Merge pull request #2596 from ucsd-progsys/fd/show-non-cut-kvars
Show solutions of non-cut kvars in error messages
2 parents 534a54f + 521d645 commit f6c97e6

File tree

7 files changed

+64
-30
lines changed

7 files changed

+64
-30
lines changed

‎liquid-fixpoint‎

‎liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs‎

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ import Data.Bifunctor
1212
import qualified Data.HashSet as S
1313
import Text.PrettyPrint.HughesPJ
1414
import Control.Monad (when)
15+
import qualified Data.HashMap.Strict as HashMap
1516
import qualified Data.Maybe as Mb
1617
import qualified Data.List as L
1718
import qualified Language.Haskell.Liquid.UX.DiffCheck as DC
@@ -133,29 +134,30 @@ solveCs :: Config -> FilePath -> CGInfo -> TargetInfo -> Maybe [String] -> IO (O
133134
solveCs cfg tgt cgi info names = do
134135
finfo <- cgInfoFInfo info cgi
135136
let fcfg = fixConfig tgt cfg
136-
F.Result {resStatus=r0, resSolution=sol} <- solve fcfg finfo
137+
F.Result {resStatus=r0, resSolution=solCuts, resNonCutsSolution=solNonCuts} <- solve fcfg finfo
138+
let sol = HashMap.union (HashMap.map F.Delayed solCuts) solNonCuts
137139
let failBs = gsFail $ gsTerm $ giSpec info
138140
let (r,rf) = splitFails (S.map val failBs) r0
139-
let resErr = second (applySolution sol . cinfoError) <$> r
141+
let resErr = second (applySolution finfo sol . cinfoError) <$> r
140142
-- resModel_ <- fmap (e2u cfg sol) <$> getModels info cfg resErr
141-
let resModel_ = cidE2u cfg sol <$> resErr
142-
let resModel' = resModel_ `addErrors` (e2u cfg sol <$> logErrors cgi)
143+
let resModel_ = cidE2u cfg <$> resErr
144+
let resModel' = resModel_ `addErrors` (e2u cfg <$> logErrors cgi)
143145
`addErrors` makeFailErrors (S.toList failBs) rf
144146
`addErrors` makeFailUseErrors (S.toList failBs) (giCbs $ giSrc info)
145-
let lErrors = applySolution sol <$> logErrors cgi
146-
let resModel = resModel' `addErrors` (e2u cfg sol <$> lErrors)
147-
let out0 = mkOutput cfg resModel sol (annotMap cgi)
147+
let lErrors = applySolution finfo sol <$> logErrors cgi
148+
let resModel = resModel' `addErrors` (e2u cfg <$> lErrors)
149+
let out0 = mkOutput cfg resModel finfo sol (annotMap cgi)
148150
return $ out0 { o_vars = names }
149151
{ o_result = resModel }
150152

151153

152-
e2u :: Config -> F.FixSolution -> Error -> UserError
153-
e2u cfg s = fmap F.pprint . tidyError cfg s
154+
e2u :: Config -> Error -> UserError
155+
e2u cfg = fmap F.pprint . tidyError cfg
154156

155-
cidE2u :: Config -> F.FixSolution -> (Integer, Error) -> UserError
156-
cidE2u cfg s (subcId, e) =
157+
cidE2u :: Config -> (Integer, Error) -> UserError
158+
cidE2u cfg (subcId, e) =
157159
let e' = attachSubcId e
158-
in fmap F.pprint (tidyError cfg s e')
160+
in fmap F.pprint (tidyError cfg e')
159161
where
160162
attachSubcId es@ErrSubType{} = es { cid = Just subcId }
161163
attachSubcId es@ErrSubTypeModel{} = es { cid = Just subcId }

‎liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs‎

Lines changed: 25 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ import Text.Printf
107107
import Text.PrettyPrint.HughesPJ hiding ((<>), first)
108108
import Language.Fixpoint.Misc
109109
import Language.Fixpoint.Types hiding (DataDecl (..), DataCtor (..), panic, shiftVV, Predicate, isNumeric)
110-
import Language.Fixpoint.Types.Visitor (mapKVars, Visitable)
110+
import Language.Fixpoint.Types.Visitor (trans, Visitable)
111111
import qualified Language.Fixpoint.Types as F
112112
import Language.Haskell.Liquid.Types.Errors
113113
import Language.Haskell.Liquid.Types.PrettyPrint
@@ -1541,17 +1541,36 @@ rTypeSort :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ())
15411541
rTypeSort tce = typeSort tce . toType True
15421542

15431543
--------------------------------------------------------------------------------
1544-
applySolution :: (Functor f) => FixSolution -> f SpecType -> f SpecType
1544+
applySolution
1545+
:: (Functor f)
1546+
=> FInfo a -> M.HashMap KVar (Delayed Expr) -> f SpecType -> f SpecType
15451547
--------------------------------------------------------------------------------
1546-
applySolution = fmap . fmap . mapReft' . appSolRefa
1548+
applySolution si = fmap . fmap . mapReft' . appSolRefa si
15471549
where
15481550
mapReft' f (MkUReft (Reft (x, z)) p) = MkUReft (Reft (x, f z)) p
15491551

15501552
appSolRefa :: Visitable t
1551-
=> M.HashMap KVar Expr -> t -> t
1552-
appSolRefa s p = mapKVars f p
1553+
=> GInfo c a -> M.HashMap KVar (Delayed Expr) -> t -> t
1554+
appSolRefa si s = mapKVars f0
15531555
where
1554-
f k = Just $ M.lookupDefault PTop k s
1556+
f0 k = Just $ forceDelayed $ M.lookupDefault (Delayed PTop) k s
1557+
1558+
mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t
1559+
mapKVars f = trans txK
1560+
where
1561+
txK (PKVar k su)
1562+
| Just p' <- f k =
1563+
rapierSubstExpr (substSymbolsSet su) (renameDomain k su) p'
1564+
txK p = p
1565+
1566+
-- The parameters of kvars all seem to have prefix $ and suffix ##k_
1567+
-- at the point where mapKVars is used. We compensate for that here.
1568+
renameDomain k (Su m) =
1569+
Su $ M.fromList
1570+
[ (consSym '$' (suffixSymbol v "k_"), e)
1571+
| v <- kvarDomain si k
1572+
, let e = M.lookupDefault (EVar v) v m
1573+
]
15551574

15561575
--------------------------------------------------------------------------------
15571576
-- shiftVV :: Int -- SpecType -> Symbol -> SpecType

‎liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Annotate.hs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -78,9 +78,9 @@ import Language.Haskell.Liquid.Types.Types
7878

7979
-- | @output@ creates the pretty printed output
8080
--------------------------------------------------------------------------------------------
81-
mkOutput :: Config -> ErrorResult -> FixSolution -> AnnInfo (Annot SpecType) -> Output Doc
81+
mkOutput :: Config -> ErrorResult -> FInfo a -> FixDelayedSolution -> AnnInfo (Annot SpecType) -> Output Doc
8282
--------------------------------------------------------------------------------------------
83-
mkOutput cfg res sol anna
83+
mkOutput cfg res si sol anna
8484
= O { o_vars = Nothing
8585
-- , o_errors = []
8686
, o_types = toDoc <$> annTy
@@ -90,7 +90,7 @@ mkOutput cfg res sol anna
9090
}
9191
where
9292
annTmpl = closeAnnots anna
93-
annTy = tidySpecType Lossy <$> applySolution sol annTmpl
93+
annTy = tidySpecType Lossy <$> applySolution si sol annTmpl
9494
toDoc = rtypeDoc tidy
9595
tidy = if shortNames cfg then Lossy else Full
9696

‎liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Errors.hs‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,11 @@ type Ctx = M.HashMap F.Symbol SpecType
3434
type CtxM = M.HashMap F.Symbol (WithModel SpecType)
3535

3636
------------------------------------------------------------------------
37-
tidyError :: Config -> F.FixSolution -> Error -> Error
37+
tidyError :: Config -> Error -> Error
3838
------------------------------------------------------------------------
39-
tidyError cfg sol
39+
tidyError cfg
4040
= fmap (tidySpecType tidy)
41-
. tidyErrContext tidy sol
41+
. tidyErrContext tidy
4242
where
4343
tidy = configTidy cfg
4444

@@ -47,32 +47,32 @@ configTidy cfg
4747
| shortNames cfg = F.Lossy
4848
| otherwise = F.Full
4949

50-
tidyErrContext :: F.Tidy -> F.FixSolution -> Error -> Error
51-
tidyErrContext k _ e@(ErrSubType {})
50+
tidyErrContext :: F.Tidy -> Error -> Error
51+
tidyErrContext k e@(ErrSubType {})
5252
= e { ctx = c', tact = F.subst θ tA, texp = F.subst θ tE }
5353
where
5454
(θ, c') = tidyCtx k xs (ctx e)
5555
xs = F.syms tA ++ F.syms tE
5656
tA = tact e
5757
tE = texp e
5858

59-
tidyErrContext _ _ e@(ErrSubTypeModel {})
59+
tidyErrContext _ e@(ErrSubTypeModel {})
6060
= e { ctxM = c', tactM = fmap (F.subst θ) tA, texp = fmap (F.subst θ) tE }
6161
where
6262
(θ, c') = tidyCtxM xs $ ctxM e
6363
xs = F.syms tA ++ F.syms tE
6464
tA = tactM e
6565
tE = texp e
6666

67-
tidyErrContext k _ e@(ErrAssType {})
67+
tidyErrContext k e@(ErrAssType {})
6868
= e { ctx = c', cond = F.subst θ p }
6969
where
7070
m = ctx e
7171
(θ, c') = tidyCtx k xs m
7272
xs = F.syms p
7373
p = cond e
7474

75-
tidyErrContext _ _ e
75+
tidyErrContext _ e
7676
= e
7777

7878
--------------------------------------------------------------------------------

‎tests/errors/KVars.hs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{-@ LIQUID "--expect-error-containing=v < 0" @-}
2+
-- | Tests that KVar solutions show in error messages
3+
module KVars where
4+
5+
6+
{-@ intId :: forall <p :: Int -> Bool> . Int<p> -> Int<p> @-}
7+
intId :: Int -> Int
8+
intId x = x
9+
10+
{-@ test :: {x:Int | x < 0} -> {v:Int | v > 0} @-}
11+
test :: Int -> Int
12+
test x = intId x

‎tests/tests.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -641,6 +641,7 @@ executable errors
641641
, InlineSubExp0
642642
, InlineSubExp1
643643
, IrregularData
644+
, KVars
644645
, LiftMeasureCase
645646
, LocalHole
646647
, MissingAssume

0 commit comments

Comments
 (0)