Skip to content

Commit 36b29ec

Browse files
matheussbernardomatheussbernardo
authored
Merge pull request #3 from matheussbernardo/detect_synthesis
Detect synthesis
2 parents 0961495 + 378476b commit 36b29ec

File tree

14 files changed

+327
-72
lines changed

14 files changed

+327
-72
lines changed

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

Lines changed: 104 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -99,12 +99,32 @@ consAct γ cfg info = do
9999
hws <- gets hsWfs
100100
fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
101101
fws <- concat <$> mapM splitW hws
102+
when (warnOnTermHoles cfg) emitConsolidatedHoleWarnings
102103
modify $ \st -> st { fEnv = fEnv st `mappend` feEnv (fenv γ)
103104
, cgLits = litEnv γ
104105
, cgConsts = cgConsts st `mappend` constEnv γ
105106
, fixCs = fcs
106107
, fixWfs = fws }
107108

109+
emitConsolidatedHoleWarnings :: CG ()
110+
emitConsolidatedHoleWarnings = do
111+
holes <- gets hsHoles
112+
holeExprs <- gets hsHolesExprs
113+
114+
let mergedHoles
115+
= [(h
116+
, holeInfo
117+
, M.findWithDefault [] (h, srcSpan) holeExprs
118+
)
119+
| ((h, srcSpan), holeInfo) <- M.toList holes
120+
]
121+
122+
forM_ mergedHoles $ \(h, holeInfo, anfs) -> do
123+
let γ = snd . info $ holeInfo
124+
let anfs' = map (\(v, x, t) -> (F.symbol v, x, t)) anfs
125+
addWarning $ ErrHole (hloc holeInfo) "hole found" (reLocal $ renv γ) (F.symbol h) (htype holeInfo) anfs'
126+
127+
108128
--------------------------------------------------------------------------------
109129
-- | Ensure that the instance type is a subtype of the class type --------------
110130
--------------------------------------------------------------------------------
@@ -219,9 +239,17 @@ consCB _ γ (NonRec x def)
219239

220240
consCB _ γ (NonRec x e)
221241
= do to <- varTemplate γ (x, Nothing)
242+
when (warnOnTermHoles (getConfig γ)) checkLetHole
222243
to' <- consBind False γ (x, e, to) >>= addPostTemplate γ
223244
extender γ (x, makeSingleton γ (simplify e) <$> to')
224-
245+
where
246+
checkLetHole =
247+
do
248+
let isItHole = detectTypedHole e
249+
case isItHole of
250+
Just (srcSpan, var) -> do
251+
linkANFToHole x (var, RealSrcSpan srcSpan Strict.Nothing)
252+
_ -> return ()
225253
grepDictionary :: CoreExpr -> Maybe (Var, [Type])
226254
grepDictionary = go []
227255
where
@@ -297,28 +325,49 @@ addPToEnv γ π
297325
= do γπ <- γ += ("addSpec1", pname π, pvarRType π)
298326
foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π]
299327

328+
detectTypedHole :: CoreExpr -> Maybe (RealSrcSpan, Var)
329+
detectTypedHole e =
330+
case stripTicks e of
331+
Var x | isVarHole x ->
332+
case lastTick e of
333+
Just (SourceNote src _) -> Just (src, x)
334+
_ -> Nothing
335+
_ -> Nothing
336+
337+
-- Remove Initial App and sequent Tick nodes from an expression.
338+
stripTicks :: CoreExpr -> CoreExpr
339+
stripTicks (App (Tick _ e) _) = stripTicks e
340+
stripTicks (Tick _ e) = stripTicks e
341+
stripTicks e = e
342+
343+
-- Traverse the expression to get the last Tick information.
344+
lastTick :: Expr b -> Maybe CoreTickish
345+
lastTick (Tick t e) =
346+
case lastTick e of
347+
Just t' -> Just t'
348+
Nothing -> Just t
349+
lastTick (App e a) =
350+
case lastTick a of
351+
Just ta -> Just ta
352+
Nothing -> lastTick e
353+
lastTick _ = Nothing
354+
355+
-- A helper to check if the variable name indicates a typed hole.
356+
isVarHole :: Var -> Bool
357+
isVarHole x = isHoleStr (F.symbolString (F.symbol x))
358+
where
359+
isHoleStr s =
360+
case break (== '.') s of
361+
(_, '.':rest) -> rest == "hole"
362+
_ -> False
300363

301-
detectTypedHole :: CGEnv -> CoreExpr -> CG (Maybe (RealSrcSpan, Var))
302-
detectTypedHole _ (App (Tick genTick (Var x)) _) | isVarHole x
303-
= return (Just (getSrcSpanFromTick, x))
304-
where
305-
getSrcSpanFromTick =
306-
case genTick of
307-
SourceNote src _ -> src
308-
_ -> panic Nothing "Not a Source Note"
309-
isStrHole s =
310-
case break (=='.') s of
311-
(_, '.':rest) -> rest == "hole"
312-
_ -> False
313-
isVarHole = isStrHole . F.symbolString . F.symbol
314-
detectTypedHole _ _ = return Nothing -- NOT A TYPED HOLE
315364
--------------------------------------------------------------------------------
316365
-- | Bidirectional Constraint Generation: CHECKING -----------------------------
317366
--------------------------------------------------------------------------------
318367
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
319368
--------------------------------------------------------------------------------
320369
cconsE g e t = do
321-
-- _ <- traceM $ Text.printf "cconsE:\n expr = %s\n GSHOW = %s \nexprType = %s\n lqType = %s\n" (showpp e) (gshow e) (showpp (exprType e)) (showpp t)
370+
checkANFHoleInExpr e t
322371
cconsE' g e t
323372

324373
--------------------------------------------------------------------------------
@@ -388,15 +437,16 @@ cconsE' γ e@(Cast e' c) t
388437

389438
cconsE' γ e t
390439
= do
391-
_ <- when (warnOnTermHoles (getConfig γ)) maybeAddHole
440+
when (warnOnTermHoles (getConfig γ)) maybeAddHole
392441
te <- consE γ e
393442
te' <- instantiatePreds γ e te >>= addPost γ
394443
addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e)
395444
where
396445
maybeAddHole = do
397-
isItHole <- detectTypedHole γ e
446+
let isItHole = detectTypedHole e
398447
case isItHole of
399-
Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
448+
Just (srcSpan, x) -> do
449+
addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
400450
_ -> return ()
401451

402452
lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft)
@@ -520,44 +570,20 @@ consE γ (Var x)
520570
consE _ (Lit c)
521571
= refreshVV $ uRType $ literalFRefType c
522572

523-
consE γ e'@(App e a@(Type τ))
524-
= do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e
525-
t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te
526-
then freshTyType (typeclass (getConfig γ)) TypeInstE e τ
527-
else trueTy (typeclass (getConfig γ)) τ
528-
addW $ WfC γ t
529-
t' <- refreshVV t
530-
tt0 <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te)
531-
let tt = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0
532-
return $ case rTVarToBind α of
533-
Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ)
534-
Nothing -> tt
535-
where
536-
isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α)
537-
538-
consE γ e'@(App e a) | Just aDict <- getExprDict γ a
539-
= case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of
540-
Just riSig -> return $ fromRISig riSig
541-
_ -> do
542-
([], πs, te) <- bkUniv <$> consE γ e
543-
te' <- instantiatePreds γ e' $ foldr RAllP te πs
544-
(γ', te''') <- dropExists γ te'
545-
te'' <- dropConstraints γ te'''
546-
updateLocA {- πs -} (exprLoc e) te''
547-
let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te''
548-
cconsE γ' a tx
549-
addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)
550-
551-
consE γ e'@(App e a)
552-
= do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e
553-
te1 <- instantiatePreds γ e' $ foldr RAllP te πs
554-
(γ', te2) <- dropExists γ te1
555-
te3 <- dropConstraints γ te2
556-
updateLocA (exprLoc e) te3
557-
let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3
558-
cconsE γ' a tx
559-
makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a))
560-
573+
consE γ e'@(App _ _) =
574+
do
575+
t <- if warnOnTermHoles (getConfig γ) then synthesizeWithHole else consEApp γ e'
576+
checkANFHoleInExpr e' t
577+
return t
578+
where
579+
synthesizeWithHole = do
580+
let isItHole = detectTypedHole e'
581+
t <- consEApp γ e'
582+
_ <- case isItHole of
583+
Just (srcSpan, x) -> do
584+
addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
585+
_ -> return ()
586+
return t
561587
consE γ (Lam α e) | isTyVar α
562588
= do γ' <- updateEnvironment γ α
563589
t' <- consE γ' e
@@ -603,6 +629,27 @@ consE γ e@(Coercion _)
603629

604630
consE _ e@(Type t)
605631
= panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t)
632+
633+
checkANFHoleInExpr :: CoreExpr -> SpecType -> CG ()
634+
checkANFHoleInExpr e t = do
635+
let vars = collectVars e
636+
forM_ vars $ \var -> do
637+
isANF <- isANFInHole var
638+
case isANF of
639+
Just uniqueVar -> addHoleANF uniqueVar var e t
640+
_ -> return ()
641+
collectVars :: CoreExpr -> [Var]
642+
collectVars (Var x) = [x]
643+
collectVars (App e1 e2) = collectVars e1 ++ collectVars e2
644+
collectVars (Lam x e) = x : collectVars e
645+
collectVars (Let (NonRec x e1) e2) = x : collectVars e1 ++ collectVars e2
646+
collectVars (Let (Rec xes) e) =
647+
let (xs, es) = unzip xes
648+
in xs ++ concatMap collectVars es ++ collectVars e
649+
collectVars (Case e x _ alts) =
650+
x : collectVars e ++ concatMap collectAltVars alts
651+
where collectAltVars (Alt _ xs e') = xs ++ collectVars e'
652+
collectVars _ = []
606653

607654
consEApp :: CGEnv -> CoreExpr -> CG SpecType
608655
consEApp γ e'@(App e a@(Type τ))

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -302,6 +302,8 @@ initCGI cfg info = CGInfo {
302302
, ghcI = info
303303
, unsorted = F.notracepp "UNSORTED" $ F.makeTemplates $ gsUnsorted $ gsData spc
304304
, hsHoles = M.empty
305+
, hsANFHoles = M.empty
306+
, hsHolesExprs = M.empty
305307
}
306308
where
307309
tce = gsTcEmbeds nspc

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

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ import Language.Haskell.Liquid.Constraint.Env
2020
import Language.Fixpoint.Misc hiding (errorstar)
2121
import Language.Haskell.Liquid.GHC.Misc -- (concatMapM)
2222
import Liquid.GHC.API as Ghc hiding (panic, showPpr)
23-
import qualified Language.Fixpoint.Types as FT
2423

2524

2625
--------------------------------------------------------------------------------
@@ -120,15 +119,20 @@ addA _ _ _ !a
120119

121120
addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG ()
122121
addHole loc x t γ = do
123-
modify $ \s -> s { hsHoles = M.insert x (holeInfo (s, γ)) $ hsHoles s }
124-
addWarning $ ErrHole loc ("hole found") (reLocal $ renv γ) x' t
122+
modify $ \s -> s { hsHoles = M.insert (x, loc) (holeInfo (s, γ)) $ hsHoles s }
125123
where
126124
holeInfo = HoleInfo t loc env
127125
env = mconcat [renv γ, grtys γ, assms γ, intys γ]
128-
x' = FT.symbol x
129126

130-
isVarInHole :: Var -> CG Bool
131-
isVarInHole x = gets (M.member x . hsHoles)
127+
addHoleANF :: (Var, SrcSpan) -> Var -> CoreExpr -> SpecType -> CG ()
128+
addHoleANF uniqueVar anfVar e t =
129+
modify $ \s -> s { hsHolesExprs = M.insertWith (++) uniqueVar [(anfVar, e, t)] (hsHolesExprs s) }
130+
131+
linkANFToHole :: Var -> (Var, SrcSpan) -> CG ()
132+
linkANFToHole anf h = modify $ \s -> s { hsANFHoles = M.insert anf h $ hsANFHoles s }
133+
134+
isANFInHole :: Var -> CG (Maybe (Var, SrcSpan))
135+
isANFInHole anf = gets (M.lookup anf . hsANFHoles)
132136

133137
lookupNewType :: Ghc.TyCon -> CG (Maybe SpecType)
134138
lookupNewType tc

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -239,7 +239,9 @@ data CGInfo = CGInfo
239239
, ghcI :: !TargetInfo
240240
, dataConTys :: ![(Var, SpecType)] -- ^ Refined Types of Data Constructors
241241
, unsorted :: !F.Templates -- ^ Potentially unsorted expressions
242-
, hsHoles :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms
242+
, hsHoles :: !(M.HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms
243+
, hsANFHoles :: !(M.HashMap Var (Var, SrcSpan))
244+
, hsHolesExprs :: !(M.HashMap (Var, SrcSpan) [(Var, CoreExpr, SpecType)])
243245
}
244246

245247

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

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -250,8 +250,9 @@ data TError t =
250250
, ctx :: !(M.HashMap Symbol t)
251251
, svar :: !Symbol
252252
, thl :: !t
253+
, anf :: ![(Symbol, CoreExpr, t)]
253254
} -- ^ hole type
254-
255+
255256
| ErrHoleCycle
256257
{ pos :: !SrcSpan
257258
, holesCycle :: [Symbol] -- Var?
@@ -786,12 +787,25 @@ ppError' _td _dCtx (ErrHoleCycle _ holes)
786787
= "Cycle of holes found"
787788
$+$ pprint holes
788789

789-
ppError' td dCtx (ErrHole _ msg c x t)
790+
ppError' td dCtx (ErrHole _ msg c x t a)
790791
= "Hole Found"
791792
$+$ pprint x <+> "::" <+> pprint t
792793
$+$ dCtx
793794
$+$ ppContext td c
794795
$+$ msg
796+
$+$ "Extra Constraints where hole appears as ANF var"
797+
$+$ (if null a
798+
then empty
799+
else nests 2 [ text "with expression types"
800+
, vsep (
801+
map (
802+
\(v, e, t') ->
803+
text "ANF VAR is" <+> pprint v
804+
$+$ text "Expression is [" <+> ppCoreExpr e <+> text "] and has type:"
805+
$+$ pprint t'
806+
) a
807+
)
808+
])
795809

796810
ppError' td dCtx (ErrSubType _ _ cid c tA tE)
797811
= text "Liquid Type Mismatch"
@@ -1095,6 +1109,9 @@ ppList :: (PPrint a) => Doc -> [a] -> Doc
10951109
ppList d ls
10961110
= nest 4 (sepVcat blankLine (d : [ text "*" <+> pprint l | l <- ls ]))
10971111

1112+
ppCoreExpr :: CoreExpr -> Doc
1113+
ppCoreExpr = text . showSDocQualified . ppr
1114+
10981115
-- | Convert a GHC error into a list of our errors.
10991116

11001117
sourceErrors :: String -> SourceError -> [TError t]

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -484,7 +484,8 @@ printWarning logger (Warning srcSpan doc) = GHC.putWarnMsg logger srcSpan doc
484484
type ErrorResult = F.FixResult UserError
485485
type Error = TError SpecType
486486

487-
487+
instance NFData CoreExpr where
488+
rnf _ = () -- Simple implementation that doesn't traverse the structure
488489
instance NFData a => NFData (TError a)
489490

490491
--------------------------------------------------------------------------------

‎tests/tests.cabal‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2802,6 +2802,10 @@ executable typed-holes
28022802
other-modules: Example0
28032803
, Example1
28042804
, Example2
2805+
, Example3
2806+
, Example4
2807+
, Example5
2808+
, Example6
28052809
build-depends: base
28062810
, liquid-prelude
28072811
, liquidhaskell

‎tests/typed-holes/Example0.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,5 @@ module Example0 where
66

77
{-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
88
listLength :: [a] -> Int
9-
listLength [] = hole
10-
listLength (_:xs) = 1 + listLength xs
9+
listLength [] = 0
10+
listLength (_:xs) = 1 + hole

‎tests/typed-holes/Example1.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@
33

44
module Example1 where
55
import Language.Haskell.Liquid.ProofCombinators (Proof)
6-
76
hole = undefined
87

98
{-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
109
listLength :: [a] -> Int
1110
listLength [] = 0
1211
listLength (_:xs) = 1 + listLength xs
12+
1313
{-@ measure listLength @-}
1414

1515
{-@ listLengthProof :: xs:[a] -> {listLength xs == len xs} @-}

‎tests/typed-holes/Example2.hs‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,5 +24,13 @@ module Example2 where
2424
leftId x
2525
= empty <> x
2626
=== hole
27-
=== x
28-
*** QED
27+
=== x
28+
*** QED
29+
30+
{-@ rightId :: x:[a] -> { (x <> empty) == x } @-}
31+
rightId :: [a] -> Proof
32+
rightId x = hole
33+
34+
{-@ assoc :: x:[a] -> y:[a] -> z:[a] -> { (x <> (y <> z)) == ((x <> y) <> z) } @-}
35+
assoc :: [a] -> [a] -> [a] -> Proof
36+
assoc x y z = hole

0 commit comments

Comments
 (0)