From a633c4e6e363bf3f8336edc8a12f90cb19fe7ab5 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Wed, 12 Feb 2025 13:29:30 +0100 Subject: [PATCH 01/10] Initial version of typed holes support under allow-typed-holes flag --- .../Haskell/Liquid/Constraint/Generate.hs | 75 ++++++++++++------- .../Haskell/Liquid/Constraint/Init.hs | 1 + .../Haskell/Liquid/Constraint/Monad.hs | 13 ++++ .../Haskell/Liquid/Constraint/Types.hs | 1 + .../src/Language/Haskell/Liquid/Liquid.hs | 1 - .../src/Language/Haskell/Liquid/UX/CmdLine.hs | 5 ++ .../src/Language/Haskell/Liquid/UX/Config.hs | 1 + tests/tests.cabal | 18 +++++ tests/typed-holes/Example1.hs | 28 +++++++ 9 files changed, 117 insertions(+), 26 deletions(-) create mode 100644 tests/typed-holes/Example1.hs diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs index 98c2cb78c4..43014257a7 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -68,9 +68,11 @@ import Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConC import Language.Haskell.Liquid.UX.Config ( HasConfig(getConfig), Config(typeclass, gradual, checkDerived, extensionality, - nopolyinfer, noADT, dependantCase, exactDC, rankNTypes), + nopolyinfer, noADT, dependantCase, exactDC, rankNTypes, allowTypedHoles), patternFlag, - higherOrderFlag ) + higherOrderFlag, allowTypedHoles ) +import qualified GHC.Data.Strict as Strict + -------------------------------------------------------------------------------- -- | Constraint Generation: Toplevel ------------------------------------------- @@ -295,14 +297,23 @@ addPToEnv γ π = do γπ <- γ += ("addSpec1", pname π, pvarRType π) foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π] + +detectTypedHole :: CGEnv -> CoreExpr -> CG (Maybe (RealSrcSpan, Var)) +detectTypedHole _ (App (Tick genTick (Var x)) _) | isVarHole x + = return (Just (getSrcSpanFromTick, x)) + where + getSrcSpanFromTick = case genTick of + SourceNote src _ -> src + _ -> panic Nothing "Not a Source Note" + isVarHole = L.isInfixOf "hole" . F.symbolString . F.symbol +detectTypedHole _ _ = return Nothing -- NOT A TYPED HOLE -------------------------------------------------------------------------------- -- | Bidirectional Constraint Generation: CHECKING ----------------------------- -------------------------------------------------------------------------------- cconsE :: CGEnv -> CoreExpr -> SpecType -> CG () -------------------------------------------------------------------------------- cconsE g e t = do - -- NOTE: tracing goes here - -- traceM $ printf "cconsE:\n expr = %s\n exprType = %s\n lqType = %s\n" (showPpr e) (showPpr (exprType e)) (showpp t) + _ <- if (allowTypedHoles (getConfig g)) then (detectTypedHole g e) else return Nothing cconsE' g e t -------------------------------------------------------------------------------- @@ -319,9 +330,9 @@ cconsE' γ e t cconsE' γ e@(Let b@(NonRec x _) ee) t = do sp <- gets specLVars if x `S.member` sp - then cconsLazyLet γ e t - else do γ' <- consCBLet γ b - cconsE γ' ee t + then cconsLazyLet γ e t + else do γ' <- consCBLet γ b + cconsE γ' ee t cconsE' γ e (RAllP p t) = cconsE γ' e t'' @@ -456,12 +467,26 @@ cconsLazyLet γ (Let (NonRec x ex) e) t cconsLazyLet _ _ _ = panic Nothing "Constraint.Generate.cconsLazyLet called on invalid inputs" + +consE :: CGEnv -> CoreExpr -> CG SpecType +-------------------------------------------------------------------------------- +consE g e = do + t <- if (allowTypedHoles (getConfig g)) then synthesizeWithHole else consE' g e + return t + where + synthesizeWithHole = do + isItHole <- detectTypedHole g e + t <- consE' g e + _ <- case isItHole of + Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t g + _ -> return () + return t -------------------------------------------------------------------------------- -- | Bidirectional Constraint Generation: SYNTHESIS ---------------------------- -------------------------------------------------------------------------------- -consE :: CGEnv -> CoreExpr -> CG SpecType +consE' :: CGEnv -> CoreExpr -> CG SpecType -------------------------------------------------------------------------------- -consE γ e +consE' γ e | patternFlag γ , Just p <- Rs.lift e = consPattern γ (F.notracepp "CONSE-PATTERN: " p) (exprType e) @@ -476,7 +501,7 @@ consE γ e -- If datacon definitions have references to self for fancy termination, -- ignore them at the construction. -consE γ (Var x) | GM.isDataConId x +consE' γ (Var x) | GM.isDataConId x = do t0 <- varRefType γ x -- NV: The check is expected to fail most times, so -- it is cheaper than direclty fmap ignoreSelf. @@ -487,15 +512,15 @@ consE γ (Var x) | GM.isDataConId x addLocA (Just x) (getLocation γ) (varAnn γ x t) return t -consE γ (Var x) +consE' γ (Var x) = do t <- varRefType γ x addLocA (Just x) (getLocation γ) (varAnn γ x t) return t -consE _ (Lit c) +consE' _ (Lit c) = refreshVV $ uRType $ literalFRefType c -consE γ e'@(App e a@(Type τ)) +consE' γ e'@(App e a@(Type τ)) = do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te then freshTyType (typeclass (getConfig γ)) TypeInstE e τ @@ -510,7 +535,7 @@ consE γ e'@(App e a@(Type τ)) where isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α) -consE γ e'@(App e a) | Just aDict <- getExprDict γ a +consE' γ e'@(App e a) | Just aDict <- getExprDict γ a = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of Just riSig -> return $ fromRISig riSig _ -> do @@ -523,7 +548,7 @@ consE γ e'@(App e a) | Just aDict <- getExprDict γ a cconsE γ' a tx addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a) -consE γ e'@(App e a) +consE' γ e'@(App e a) = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e te1 <- instantiatePreds γ e' $ foldr RAllP te πs (γ', te2) <- dropExists γ te1 @@ -533,12 +558,12 @@ consE γ e'@(App e a) cconsE γ' a tx makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a)) -consE γ (Lam α e) | isTyVar α +consE' γ (Lam α e) | isTyVar α = do γ' <- updateEnvironment γ α t' <- consE γ' e return $ RAllT (makeRTVar $ rTyVar α) t' mempty -consE γ e@(Lam x e1) +consE' γ e@(Lam x e1) = do tx <- freshTyType (typeclass (getConfig γ)) LamE (Var x) τx γ' <- γ += ("consE", F.symbol x, tx) t1 <- consE γ' e1 @@ -550,33 +575,33 @@ consE γ e@(Lam x e1) where FunTy { ft_arg = τx } = exprType e -consE γ e@(Let _ _) +consE' γ e@(Let _ _) = cconsFreshE LetE γ e -consE γ e@(Case _ _ _ [_]) +consE' γ e@(Case _ _ _ [_]) | Just p@Rs.PatProject{} <- Rs.lift e = consPattern γ p (exprType e) -consE γ e@(Case _ _ _ cs) +consE' γ e@(Case _ _ _ cs) = cconsFreshE (caseKVKind cs) γ e -consE γ (Tick tt e) +consE' γ (Tick tt e) = do t <- consE (setLocation γ (Sp.Tick tt)) e addLocA Nothing (GM.tickSrcSpan tt) (AnnUse t) return t -- See Note [Type classes with a single method] -consE γ (Cast e co) +consE' γ (Cast e co) | Just f <- isClassConCo co = consE γ (f e) -consE γ e@(Cast e' c) +consE' γ e@(Cast e' c) = castTy γ (exprType e) e' c -consE γ e@(Coercion _) +consE' γ e@(Coercion _) = trueTy (typeclass (getConfig γ)) $ exprType e -consE _ e@(Type t) +consE' _ e@(Type t) = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t) caseKVKind ::[Alt Var] -> KVKind diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs index c8ed97a6e7..23f28f3661 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs @@ -301,6 +301,7 @@ initCGI cfg info = CGInfo { , allowHO = higherOrderFlag cfg , ghcI = info , unsorted = F.notracepp "UNSORTED" $ F.makeTemplates $ gsUnsorted $ gsData spc + , hsHoles = M.empty } where tce = gsTcEmbeds nspc diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs index 5a542e47a6..2b1ac9b4f4 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs @@ -20,6 +20,8 @@ import Language.Haskell.Liquid.Constraint.Env import Language.Fixpoint.Misc hiding (errorstar) import Language.Haskell.Liquid.GHC.Misc -- (concatMapM) import Liquid.GHC.API as Ghc hiding (panic, showPpr) +import qualified Language.Fixpoint.Types as FT + -------------------------------------------------------------------------------- -- | `addC` adds a subtyping constraint into the global pool. @@ -116,6 +118,17 @@ addA !l xo@Nothing !t (AI m) addA _ _ _ !a = a +addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG () +addHole loc x t γ = do + modify $ \s -> s { hsHoles = M.insert x (holeInfo (s, γ)) $ hsHoles s } + addWarning $ ErrHole loc ("hole found") (reGlobal env <> reLocal env) x' t + where + holeInfo = HoleInfo t loc env + env = mconcat [renv γ, grtys γ, assms γ, intys γ] + x' = FT.symbol x + +isVarInHole :: Var -> CG Bool +isVarInHole x = gets (M.member x . hsHoles) lookupNewType :: Ghc.TyCon -> CG (Maybe SpecType) lookupNewType tc diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs index 97c83843ec..aff7c5166e 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs @@ -239,6 +239,7 @@ data CGInfo = CGInfo , ghcI :: !TargetInfo , dataConTys :: ![(Var, SpecType)] -- ^ Refined Types of Data Constructors , unsorted :: !F.Templates -- ^ Potentially unsorted expressions + , hsHoles :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes } diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs index 1cbd69ad35..1b916b6c94 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs @@ -125,7 +125,6 @@ dumpCs cgi = do putStrLn $ render $ pprintMany (fixCs cgi) putStrLn "***************************** WfCs ********************************" putStrLn $ render $ pprintMany (hsWfs cgi) - pprintMany :: (PPrint a) => [a] -> Doc pprintMany xs = vcat [ F.pprint x $+$ text " " | x <- xs ] diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs index 35a09409a4..f26deb4f64 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -478,6 +478,10 @@ config = cmdArgsMode $ Config { = def &= help "Allow refining constructors with unsafe refinements" &= name "allow-unsafe-constructors" &= explicit + , allowTypedHoles + = def &= help "Allow typed holes in implementation" + &= name "allow-typed-holes" + &= explicit } &= program "liquid" &= help "Refinement Types for Haskell" &= summary copyright @@ -741,6 +745,7 @@ defConfig = Config , dumpOpaqueReflections = False , dumpPreNormalizedCore = False , allowUnsafeConstructors = False + , allowTypedHoles = False } -- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs index 8a10073b12..3fd5a4349e 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs @@ -125,6 +125,7 @@ data Config = Config , dumpOpaqueReflections :: Bool -- Dumps all opaque reflections to the stdout , dumpPreNormalizedCore :: Bool -- Dumps the prenormalized core (before a-normalization) , allowUnsafeConstructors :: Bool -- ^ Allow refining constructors with unsafe refinements + , allowTypedHoles :: Bool -- ^ Allow typed holes in the source code } deriving (Generic, Data, Show, Eq) allowPLE :: Config -> Bool diff --git a/tests/tests.cabal b/tests/tests.cabal index be81e6f58d..471bbc9e9a 100644 --- a/tests/tests.cabal +++ b/tests/tests.cabal @@ -2619,6 +2619,24 @@ executable typeclass-pos hs-source-dirs: app , typeclasses/pos + default-language: Haskell2010 + +flag typed-holes + default: False + +executable typed-holes + main-is: Main.hs + + ghc-options: -fplugin=LiquidHaskell + other-modules: Example1 + build-depends: base + , liquid-prelude + , liquidhaskell + + hs-source-dirs: app + , typed-holes + + default-language: Haskell2010 -- This test suite is for internal function unit tests, not for checking LH on -- source files. test-suite tasty diff --git a/tests/typed-holes/Example1.hs b/tests/typed-holes/Example1.hs new file mode 100644 index 0000000000..7626907833 --- /dev/null +++ b/tests/typed-holes/Example1.hs @@ -0,0 +1,28 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--exact-data-cons" @-} +{-@ LIQUID "--allow-typed-holes" @-} +-- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/ + +module Example1 where + import Prelude hiding ((<>)) + import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof) + + hole = undefined + + {-@ reflect empty @-} + empty :: [a] + empty = [] + + {-@ infix <> @-} + {-@ reflect <> @-} + (<>) :: [a] -> [a] -> [a] + [] <> xs = xs + (x:xs) <> ys = x : (xs <> ys) + + {-@ leftId :: x:[a] -> { (empty <> x) == x } @-} + leftId :: [a] -> Proof + leftId x + = empty <> x + === hole + === x + *** QED \ No newline at end of file From aa627f4f4e90e63751c417ceaaf8a7839e9f9e26 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Fri, 14 Feb 2025 14:38:59 +0100 Subject: [PATCH 02/10] Renames flag to warnOnTermHoles, also detect holes only in the Synthesis phase --- .../Haskell/Liquid/Constraint/Generate.hs | 147 +++++++++--------- .../src/Language/Haskell/Liquid/Liquid.hs | 1 + .../src/Language/Haskell/Liquid/UX/CmdLine.hs | 8 +- .../src/Language/Haskell/Liquid/UX/Config.hs | 2 +- tests/typed-holes/Example1.hs | 2 +- 5 files changed, 82 insertions(+), 78 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs index 43014257a7..e4d676f1fe 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -68,9 +68,9 @@ import Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConC import Language.Haskell.Liquid.UX.Config ( HasConfig(getConfig), Config(typeclass, gradual, checkDerived, extensionality, - nopolyinfer, noADT, dependantCase, exactDC, rankNTypes, allowTypedHoles), + nopolyinfer, noADT, dependantCase, exactDC, rankNTypes, warnOnTermHoles), patternFlag, - higherOrderFlag, allowTypedHoles ) + higherOrderFlag, warnOnTermHoles ) import qualified GHC.Data.Strict as Strict @@ -313,7 +313,7 @@ detectTypedHole _ _ = return Nothing -- NOT A TYPED HOLE cconsE :: CGEnv -> CoreExpr -> SpecType -> CG () -------------------------------------------------------------------------------- cconsE g e t = do - _ <- if (allowTypedHoles (getConfig g)) then (detectTypedHole g e) else return Nothing + -- _ <- 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) cconsE' g e t -------------------------------------------------------------------------------- @@ -330,9 +330,9 @@ cconsE' γ e t cconsE' γ e@(Let b@(NonRec x _) ee) t = do sp <- gets specLVars if x `S.member` sp - then cconsLazyLet γ e t - else do γ' <- consCBLet γ b - cconsE γ' ee t + then cconsLazyLet γ e t + else do γ' <- consCBLet γ b + cconsE γ' ee t cconsE' γ e (RAllP p t) = cconsE γ' e t'' @@ -468,25 +468,12 @@ cconsLazyLet _ _ _ = panic Nothing "Constraint.Generate.cconsLazyLet called on invalid inputs" -consE :: CGEnv -> CoreExpr -> CG SpecType --------------------------------------------------------------------------------- -consE g e = do - t <- if (allowTypedHoles (getConfig g)) then synthesizeWithHole else consE' g e - return t - where - synthesizeWithHole = do - isItHole <- detectTypedHole g e - t <- consE' g e - _ <- case isItHole of - Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t g - _ -> return () - return t --------------------------------------------------------------------------------- +--------------------------------------------------------- -- | Bidirectional Constraint Generation: SYNTHESIS ---------------------------- -------------------------------------------------------------------------------- -consE' :: CGEnv -> CoreExpr -> CG SpecType +consE :: CGEnv -> CoreExpr -> CG SpecType -------------------------------------------------------------------------------- -consE' γ e +consE γ e | patternFlag γ , Just p <- Rs.lift e = consPattern γ (F.notracepp "CONSE-PATTERN: " p) (exprType e) @@ -501,7 +488,7 @@ consE' γ e -- If datacon definitions have references to self for fancy termination, -- ignore them at the construction. -consE' γ (Var x) | GM.isDataConId x +consE γ (Var x) | GM.isDataConId x = do t0 <- varRefType γ x -- NV: The check is expected to fail most times, so -- it is cheaper than direclty fmap ignoreSelf. @@ -512,58 +499,33 @@ consE' γ (Var x) | GM.isDataConId x addLocA (Just x) (getLocation γ) (varAnn γ x t) return t -consE' γ (Var x) +consE γ (Var x) = do t <- varRefType γ x addLocA (Just x) (getLocation γ) (varAnn γ x t) return t -consE' _ (Lit c) +consE _ (Lit c) = refreshVV $ uRType $ literalFRefType c -consE' γ e'@(App e a@(Type τ)) - = do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e - t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te - then freshTyType (typeclass (getConfig γ)) TypeInstE e τ - else trueTy (typeclass (getConfig γ)) τ - addW $ WfC γ t - t' <- refreshVV t - tt0 <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te) - let tt = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0 - return $ case rTVarToBind α of - Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ) - Nothing -> tt - where - isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α) - -consE' γ e'@(App e a) | Just aDict <- getExprDict γ a - = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of - Just riSig -> return $ fromRISig riSig - _ -> do - ([], πs, te) <- bkUniv <$> consE γ e - te' <- instantiatePreds γ e' $ foldr RAllP te πs - (γ', te''') <- dropExists γ te' - te'' <- dropConstraints γ te''' - updateLocA {- πs -} (exprLoc e) te'' - let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te'' - cconsE γ' a tx - addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a) - -consE' γ e'@(App e a) - = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e - te1 <- instantiatePreds γ e' $ foldr RAllP te πs - (γ', te2) <- dropExists γ te1 - te3 <- dropConstraints γ te2 - updateLocA (exprLoc e) te3 - let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3 - cconsE γ' a tx - makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a)) +consE γ e'@(App _ _) = + do + t <- if (warnOnTermHoles (getConfig γ)) then synthesizeWithHole else consEApp γ e' + return t + where + synthesizeWithHole = do + isItHole <- detectTypedHole γ e' + t <- consEApp γ e' + _ <- case isItHole of + Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ + _ -> return () + return t -consE' γ (Lam α e) | isTyVar α +consE γ (Lam α e) | isTyVar α = do γ' <- updateEnvironment γ α t' <- consE γ' e return $ RAllT (makeRTVar $ rTyVar α) t' mempty -consE' γ e@(Lam x e1) +consE γ e@(Lam x e1) = do tx <- freshTyType (typeclass (getConfig γ)) LamE (Var x) τx γ' <- γ += ("consE", F.symbol x, tx) t1 <- consE γ' e1 @@ -575,35 +537,76 @@ consE' γ e@(Lam x e1) where FunTy { ft_arg = τx } = exprType e -consE' γ e@(Let _ _) +consE γ e@(Let _ _) = cconsFreshE LetE γ e -consE' γ e@(Case _ _ _ [_]) +consE γ e@(Case _ _ _ [_]) | Just p@Rs.PatProject{} <- Rs.lift e = consPattern γ p (exprType e) -consE' γ e@(Case _ _ _ cs) +consE γ e@(Case _ _ _ cs) = cconsFreshE (caseKVKind cs) γ e -consE' γ (Tick tt e) +consE γ (Tick tt e) = do t <- consE (setLocation γ (Sp.Tick tt)) e addLocA Nothing (GM.tickSrcSpan tt) (AnnUse t) return t -- See Note [Type classes with a single method] -consE' γ (Cast e co) +consE γ (Cast e co) | Just f <- isClassConCo co = consE γ (f e) -consE' γ e@(Cast e' c) +consE γ e@(Cast e' c) = castTy γ (exprType e) e' c -consE' γ e@(Coercion _) +consE γ e@(Coercion _) = trueTy (typeclass (getConfig γ)) $ exprType e -consE' _ e@(Type t) +consE _ e@(Type t) = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t) +consEApp :: CGEnv -> CoreExpr -> CG SpecType +consEApp γ e'@(App e a@(Type τ)) + = do + RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e + t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te + then freshTyType (typeclass (getConfig γ)) TypeInstE e τ + else trueTy (typeclass (getConfig γ)) τ + addW $ WfC γ t + t' <- refreshVV t + tt0 <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te) + let tt = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0 + return $ case rTVarToBind α of + Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ) + Nothing -> tt + where + isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α) + +consEApp γ e'@(App e a) | Just aDict <- getExprDict γ a + = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of + Just riSig -> return $ fromRISig riSig + _ -> do + ([], πs, te) <- bkUniv <$> consE γ e + te' <- instantiatePreds γ e' $ foldr RAllP te πs + (γ', te''') <- dropExists γ te' + te'' <- dropConstraints γ te''' + updateLocA {- πs -} (exprLoc e) te'' + let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te'' + cconsE γ' a tx + addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a) + +consEApp γ e'@(App e a) + = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e + te1 <- instantiatePreds γ e' $ foldr RAllP te πs + (γ', te2) <- dropExists γ te1 + te3 <- dropConstraints γ te2 + updateLocA (exprLoc e) te3 + let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3 + cconsE γ' a tx + makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a)) +consEApp _ _ = panic Nothing "Constraint.Generate.consEApp called on invalid inputs" + caseKVKind ::[Alt Var] -> KVKind caseKVKind [Alt (DataAlt _) _ (Var _)] = ProjectE caseKVKind cs = CaseE (length cs) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs index 1b916b6c94..1cbd69ad35 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Liquid.hs @@ -125,6 +125,7 @@ dumpCs cgi = do putStrLn $ render $ pprintMany (fixCs cgi) putStrLn "***************************** WfCs ********************************" putStrLn $ render $ pprintMany (hsWfs cgi) + pprintMany :: (PPrint a) => [a] -> Doc pprintMany xs = vcat [ F.pprint x $+$ text " " | x <- xs ] diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs index f26deb4f64..2fa90839f3 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -478,9 +478,9 @@ config = cmdArgsMode $ Config { = def &= help "Allow refining constructors with unsafe refinements" &= name "allow-unsafe-constructors" &= explicit - , allowTypedHoles - = def &= help "Allow typed holes in implementation" - &= name "allow-typed-holes" + , warnOnTermHoles + = def &= help "Warn about holes in terms" + &= name "warn-on-term-holes" &= explicit } &= program "liquid" &= help "Refinement Types for Haskell" @@ -745,7 +745,7 @@ defConfig = Config , dumpOpaqueReflections = False , dumpPreNormalizedCore = False , allowUnsafeConstructors = False - , allowTypedHoles = False + , warnOnTermHoles = False } -- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs index 3fd5a4349e..3ea14ca5fe 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs @@ -125,7 +125,7 @@ data Config = Config , dumpOpaqueReflections :: Bool -- Dumps all opaque reflections to the stdout , dumpPreNormalizedCore :: Bool -- Dumps the prenormalized core (before a-normalization) , allowUnsafeConstructors :: Bool -- ^ Allow refining constructors with unsafe refinements - , allowTypedHoles :: Bool -- ^ Allow typed holes in the source code + , warnOnTermHoles :: Bool -- ^ Warn about holes in the terms } deriving (Generic, Data, Show, Eq) allowPLE :: Config -> Bool diff --git a/tests/typed-holes/Example1.hs b/tests/typed-holes/Example1.hs index 7626907833..564f83e29e 100644 --- a/tests/typed-holes/Example1.hs +++ b/tests/typed-holes/Example1.hs @@ -1,6 +1,6 @@ {-@ LIQUID "--expect-error-containing=Hole Found" @-} {-@ LIQUID "--exact-data-cons" @-} -{-@ LIQUID "--allow-typed-holes" @-} +{-@ LIQUID "--warn-on-term-holes" @-} -- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/ module Example1 where From 93499c053cb8e93b4323ae59367424f7be5a5880 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Fri, 14 Feb 2025 14:41:49 +0100 Subject: [PATCH 03/10] Improving comment about the env hsHoles --- .../src/Language/Haskell/Liquid/Constraint/Types.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs index aff7c5166e..daf7b7b80f 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs @@ -239,7 +239,7 @@ data CGInfo = CGInfo , ghcI :: !TargetInfo , dataConTys :: ![(Var, SpecType)] -- ^ Refined Types of Data Constructors , unsorted :: !F.Templates -- ^ Potentially unsorted expressions - , hsHoles :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes + , hsHoles :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms } From 00ece27f0f5c7d360c8501cfd01fc00f652a2d85 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Fri, 14 Feb 2025 15:06:08 +0100 Subject: [PATCH 04/10] Adding Local Env to the Warning message of term hole --- .../src/Language/Haskell/Liquid/Constraint/Monad.hs | 2 +- .../src/Language/Haskell/Liquid/Types/Errors.hs | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs index 2b1ac9b4f4..104638132e 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs @@ -121,7 +121,7 @@ addA _ _ _ !a addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG () addHole loc x t γ = do modify $ \s -> s { hsHoles = M.insert x (holeInfo (s, γ)) $ hsHoles s } - addWarning $ ErrHole loc ("hole found") (reGlobal env <> reLocal env) x' t + addWarning $ ErrHole loc ("hole found") (reLocal $ renv γ) x' t where holeInfo = HoleInfo t loc env env = mconcat [renv γ, grtys γ, assms γ, intys γ] diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs index a42ad4ff9d..d0831d7c5c 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs @@ -785,9 +785,11 @@ ppError' _td _dCtx (ErrHoleCycle _ holes) = "Cycle of holes found" $+$ pprint holes -ppError' _td _dCtx (ErrHole _ msg _ x t) +ppError' td dCtx (ErrHole _ msg c x t) = "Hole Found" $+$ pprint x <+> "::" <+> pprint t + $+$ dCtx + $+$ ppContext td c $+$ msg ppError' td dCtx (ErrSubType _ _ cid c tA tE) From 4b9637e045bb73395e33f430bfb1ec52b5f666f1 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Fri, 14 Feb 2025 15:29:45 +0100 Subject: [PATCH 05/10] Adding docs about typed-holes --- docs/mkDocs/docs/options.md | 49 +++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 2549b52f45..3df432f59c 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -732,3 +732,52 @@ an import of a module coming from package `PACKAGE`. e.g. `--exclude-automatic-assumptions-for=vector` would stop loading `_LHAssumptions` modules for any imports coming from package `vector`. + +## Warn on Term Holes + +**Options:** `warn-on-term-holes` + +LiquidHaskell can be configured to emit warnings whenever it encounters incomplete terms, known as *holes*. + +This flag is particularly useful during development, ensuring that any placeholders in your specifications are reviewed and completed before final evaluation. + +To activate this behavior, use the `--warn-on-term-holes` flag either: + +1. As a pragma in your source file: + ```haskell + {-@ LIQUID "--warn-on-term-holes" @-} + ``` +2. As a plugin option: + ``` + ghc-options: -fplugin-opt=LiquidHaskell:--warn-on-term-holes + ``` + +When enabled, LiquidHaskell issues a warning for each term hole it discovers, for example: + +```haskell +typed-holes/Example1.hs:25:13: error: + Hole Found +Example1.hole :: {v : [a] | false} +in the context + Example1.<> : forall a . + x1:[a] -> x2:[a] -> {VV : [a] | VV == Example1.<> x1 x2} + + lq_anf$##7205759403792797257##dWZ : {v : [a] | v == Example1.<> lq_anf$##7205759403792797256##dWY x##aFc + && GHC.Types_LHAssumptions.len v >= 0} + + Example1.hole : forall a . a + + Example1.empty : forall a . + {VV : [a] | VV == Example1.empty + && VV == GHC.Types.[]} + + lq_anf$##7205759403792797256##dWY : {v : [a] | v == Example1.empty + && v == GHC.Types.[] + && GHC.Types_LHAssumptions.len v >= 0} + + x##aFc : {VV##1043 : [a] | GHC.Types_LHAssumptions.len VV##1043 >= 0} +hole found + | +25 | === hole + | ^^^^ +``` \ No newline at end of file From 1cad6919e72785eda6c1d310e335a45590a01e8f Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Tue, 25 Feb 2025 09:49:55 +0100 Subject: [PATCH 06/10] Improves documentation regarding how to use holes in terms --- docs/mkDocs/docs/options.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 3df432f59c..94cf1c90f4 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -739,6 +739,21 @@ an import of a module coming from package `PACKAGE`. e.g. LiquidHaskell can be configured to emit warnings whenever it encounters incomplete terms, known as *holes*. +To create a hole you need to have a binding with the name `hole` in the scope by adding: + + hole = undefined + +To use a hole you simply insert the `hole` in any place +where you want to get more type information. For example: +```haskell +hole = undefined + +{-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-} +listLength :: [a] -> Int +listLength [] = hole -- Hole inserted here +listLength (_:xs) = 1 + listLength xs +``` + This flag is particularly useful during development, ensuring that any placeholders in your specifications are reviewed and completed before final evaluation. To activate this behavior, use the `--warn-on-term-holes` flag either: From 5f8522d99cb6f292a3c051bb853cfb6b28b7f979 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Tue, 25 Feb 2025 10:04:09 +0100 Subject: [PATCH 07/10] Fix the string hole detection --- .../Language/Haskell/Liquid/Constraint/Generate.hs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs index e4d676f1fe..82dd866371 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -302,10 +302,15 @@ detectTypedHole :: CGEnv -> CoreExpr -> CG (Maybe (RealSrcSpan, Var)) detectTypedHole _ (App (Tick genTick (Var x)) _) | isVarHole x = return (Just (getSrcSpanFromTick, x)) where - getSrcSpanFromTick = case genTick of - SourceNote src _ -> src - _ -> panic Nothing "Not a Source Note" - isVarHole = L.isInfixOf "hole" . F.symbolString . F.symbol + getSrcSpanFromTick = + case genTick of + SourceNote src _ -> src + _ -> panic Nothing "Not a Source Note" + isStrHole s = + case break (=='.') s of + (_, '.':rest) -> rest == "hole" + _ -> False + isVarHole = isStrHole . F.symbolString . F.symbol detectTypedHole _ _ = return Nothing -- NOT A TYPED HOLE -------------------------------------------------------------------------------- -- | Bidirectional Constraint Generation: CHECKING ----------------------------- From d69052df19304ce56b47fd6c8fd4c3e002083a70 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Tue, 25 Feb 2025 10:13:28 +0100 Subject: [PATCH 08/10] Adding more examples to the warn on term holes tests --- tests/tests.cabal | 4 +++- tests/typed-holes/Example0.hs | 10 ++++++++++ tests/typed-holes/Example1.hs | 31 ++++++++++--------------------- tests/typed-holes/Example2.hs | 28 ++++++++++++++++++++++++++++ 4 files changed, 51 insertions(+), 22 deletions(-) create mode 100644 tests/typed-holes/Example0.hs create mode 100644 tests/typed-holes/Example2.hs diff --git a/tests/tests.cabal b/tests/tests.cabal index 471bbc9e9a..0ef92e5aab 100644 --- a/tests/tests.cabal +++ b/tests/tests.cabal @@ -2628,7 +2628,9 @@ executable typed-holes main-is: Main.hs ghc-options: -fplugin=LiquidHaskell - other-modules: Example1 + other-modules: Example0 + , Example1 + , Example2 build-depends: base , liquid-prelude , liquidhaskell diff --git a/tests/typed-holes/Example0.hs b/tests/typed-holes/Example0.hs new file mode 100644 index 0000000000..3804f2f333 --- /dev/null +++ b/tests/typed-holes/Example0.hs @@ -0,0 +1,10 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--warn-on-term-holes" @-} + +module Example0 where + hole = undefined + + {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-} + listLength :: [a] -> Int + listLength [] = hole + listLength (_:xs) = 1 + listLength xs diff --git a/tests/typed-holes/Example1.hs b/tests/typed-holes/Example1.hs index 564f83e29e..70f505a1e8 100644 --- a/tests/typed-holes/Example1.hs +++ b/tests/typed-holes/Example1.hs @@ -1,28 +1,17 @@ {-@ LIQUID "--expect-error-containing=Hole Found" @-} -{-@ LIQUID "--exact-data-cons" @-} {-@ LIQUID "--warn-on-term-holes" @-} --- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/ module Example1 where - import Prelude hiding ((<>)) - import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof) - - hole = undefined + import Language.Haskell.Liquid.ProofCombinators (Proof) - {-@ reflect empty @-} - empty :: [a] - empty = [] + hole = undefined - {-@ infix <> @-} - {-@ reflect <> @-} - (<>) :: [a] -> [a] -> [a] - [] <> xs = xs - (x:xs) <> ys = x : (xs <> ys) + {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-} + listLength :: [a] -> Int + listLength [] = 0 + listLength (_:xs) = 1 + listLength xs + {-@ measure listLength @-} - {-@ leftId :: x:[a] -> { (empty <> x) == x } @-} - leftId :: [a] -> Proof - leftId x - = empty <> x - === hole - === x - *** QED \ No newline at end of file + {-@ listLengthProof :: xs:[a] -> {listLength xs == len xs} @-} + listLengthProof :: [a] -> Proof + listLengthProof = hole diff --git a/tests/typed-holes/Example2.hs b/tests/typed-holes/Example2.hs new file mode 100644 index 0000000000..50509665d1 --- /dev/null +++ b/tests/typed-holes/Example2.hs @@ -0,0 +1,28 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--exact-data-cons" @-} +{-@ LIQUID "--warn-on-term-holes" @-} +-- Based on https://ucsd-progsys.github.io/liquidhaskell-blog/2016/10/06/structural-induction.lhs/ + +module Example2 where + import Prelude hiding ((<>)) + import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof) + + hole = undefined + + {-@ reflect empty @-} + empty :: [a] + empty = [] + + {-@ infix <> @-} + {-@ reflect <> @-} + (<>) :: [a] -> [a] -> [a] + [] <> xs = xs + (x:xs) <> ys = x : (xs <> ys) + + {-@ leftId :: x:[a] -> { (empty <> x) == x } @-} + leftId :: [a] -> Proof + leftId x + = empty <> x + === hole + === x + *** QED \ No newline at end of file From 1a2cc54cd50b4eebe92cbd7821355c713cce35a1 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Tue, 25 Feb 2025 11:08:25 +0100 Subject: [PATCH 09/10] Move hole detection from synthesis to checking --- .../Haskell/Liquid/Constraint/Generate.hs | 59 +++++++++++++++---- 1 file changed, 46 insertions(+), 13 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs index 82dd866371..634c8c5afa 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -387,9 +387,17 @@ cconsE' γ e@(Cast e' c) t addC (SubC γ (F.notracepp ("Casted Type for " ++ GM.showPpr e ++ "\n init type " ++ showpp t) t') t) ("cconsE Cast: " ++ GM.showPpr e) cconsE' γ e t - = do te <- consE γ e + = do + _ <- when (warnOnTermHoles (getConfig γ)) maybeAddHole + te <- consE γ e te' <- instantiatePreds γ e te >>= addPost γ addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e) + where + maybeAddHole = do + isItHole <- detectTypedHole γ e + case isItHole of + Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ + _ -> return () lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft) lambdaSingleton γ tce x e @@ -512,18 +520,43 @@ consE γ (Var x) consE _ (Lit c) = refreshVV $ uRType $ literalFRefType c -consE γ e'@(App _ _) = - do - t <- if (warnOnTermHoles (getConfig γ)) then synthesizeWithHole else consEApp γ e' - return t - where - synthesizeWithHole = do - isItHole <- detectTypedHole γ e' - t <- consEApp γ e' - _ <- case isItHole of - Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ - _ -> return () - return t +consE γ e'@(App e a@(Type τ)) + = do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e + t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te + then freshTyType (typeclass (getConfig γ)) TypeInstE e τ + else trueTy (typeclass (getConfig γ)) τ + addW $ WfC γ t + t' <- refreshVV t + tt0 <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te) + let tt = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0 + return $ case rTVarToBind α of + Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ) + Nothing -> tt + where + isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α) + +consE γ e'@(App e a) | Just aDict <- getExprDict γ a + = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of + Just riSig -> return $ fromRISig riSig + _ -> do + ([], πs, te) <- bkUniv <$> consE γ e + te' <- instantiatePreds γ e' $ foldr RAllP te πs + (γ', te''') <- dropExists γ te' + te'' <- dropConstraints γ te''' + updateLocA {- πs -} (exprLoc e) te'' + let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te'' + cconsE γ' a tx + addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a) + +consE γ e'@(App e a) + = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e + te1 <- instantiatePreds γ e' $ foldr RAllP te πs + (γ', te2) <- dropExists γ te1 + te3 <- dropConstraints γ te2 + updateLocA (exprLoc e) te3 + let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3 + cconsE γ' a tx + makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a)) consE γ (Lam α e) | isTyVar α = do γ' <- updateEnvironment γ α From 7037c59d4d54ce995dd5f186791c7bd3b06c16b0 Mon Sep 17 00:00:00 2001 From: Matheus de Sousa Bernardo Date: Sun, 11 May 2025 15:49:26 +0200 Subject: [PATCH 10/10] Detect synthesis (#5) * add detect synthesis * adding different warning strategy * consolidate anf holes warnings * more detect synthesis * more detect synthesis * Fixing nested hole bug * Add new version detect synthesis --- .../Haskell/Liquid/Constraint/Generate.hs | 161 +++++++++++------- .../Haskell/Liquid/Constraint/Init.hs | 2 + .../Haskell/Liquid/Constraint/Monad.hs | 18 +- .../Haskell/Liquid/Constraint/Types.hs | 4 +- .../Language/Haskell/Liquid/Types/Errors.hs | 21 ++- .../Language/Haskell/Liquid/Types/Types.hs | 3 +- tests/tests.cabal | 4 + tests/typed-holes/Example0.hs | 2 +- tests/typed-holes/Example1.hs | 2 +- tests/typed-holes/Example2.hs | 12 +- tests/typed-holes/Example3.hs | 40 +++++ tests/typed-holes/Example4.hs | 42 +++++ tests/typed-holes/Example5.hs | 36 ++++ tests/typed-holes/Example6.hs | 52 ++++++ 14 files changed, 328 insertions(+), 71 deletions(-) create mode 100644 tests/typed-holes/Example3.hs create mode 100644 tests/typed-holes/Example4.hs create mode 100644 tests/typed-holes/Example5.hs create mode 100644 tests/typed-holes/Example6.hs diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs index 634c8c5afa..7a8ddb9adb 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -99,12 +99,32 @@ consAct γ cfg info = do hws <- gets hsWfs fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs fws <- concat <$> mapM splitW hws + when (warnOnTermHoles cfg) emitConsolidatedHoleWarnings modify $ \st -> st { fEnv = fEnv st `mappend` feEnv (fenv γ) , cgLits = litEnv γ , cgConsts = cgConsts st `mappend` constEnv γ , fixCs = fcs , fixWfs = fws } +emitConsolidatedHoleWarnings :: CG () +emitConsolidatedHoleWarnings = do + holes <- gets hsHoles + holeExprs <- gets hsHolesExprs + + let mergedHoles + = [(h + , holeInfo + , M.findWithDefault [] (h, srcSpan) holeExprs + ) + | ((h, srcSpan), holeInfo) <- M.toList holes + ] + + forM_ mergedHoles $ \(h, holeInfo, anfs) -> do + let γ = snd . info $ holeInfo + let anfs' = map (\(v, x, t) -> (F.symbol v, x, t)) anfs + addWarning $ ErrHole (hloc holeInfo) "hole found" (reLocal $ renv γ) (F.symbol h) (htype holeInfo) anfs' + + -------------------------------------------------------------------------------- -- | Ensure that the instance type is a subtype of the class type -------------- -------------------------------------------------------------------------------- @@ -219,9 +239,17 @@ consCB _ γ (NonRec x def) consCB _ γ (NonRec x e) = do to <- varTemplate γ (x, Nothing) + when (warnOnTermHoles (getConfig γ)) checkLetHole to' <- consBind False γ (x, e, to) >>= addPostTemplate γ extender γ (x, makeSingleton γ (simplify e) <$> to') - + where + checkLetHole = + do + let isItHole = detectTypedHole e + case isItHole of + Just (srcSpan, var) -> do + linkANFToHole x (var, RealSrcSpan srcSpan Strict.Nothing) + _ -> return () grepDictionary :: CoreExpr -> Maybe (Var, [Type]) grepDictionary = go [] where @@ -297,28 +325,49 @@ addPToEnv γ π = do γπ <- γ += ("addSpec1", pname π, pvarRType π) foldM (+=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π] +detectTypedHole :: CoreExpr -> Maybe (RealSrcSpan, Var) +detectTypedHole e = + case stripTicks e of + Var x | isVarHole x -> + case lastTick e of + Just (SourceNote src _) -> Just (src, x) + _ -> Nothing + _ -> Nothing + +-- Remove Initial App and sequent Tick nodes from an expression. +stripTicks :: CoreExpr -> CoreExpr +stripTicks (App (Tick _ e) _) = stripTicks e +stripTicks (Tick _ e) = stripTicks e +stripTicks e = e + +-- Traverse the expression to get the last Tick information. +lastTick :: Expr b -> Maybe CoreTickish +lastTick (Tick t e) = + case lastTick e of + Just t' -> Just t' + Nothing -> Just t +lastTick (App e a) = + case lastTick a of + Just ta -> Just ta + Nothing -> lastTick e +lastTick _ = Nothing + +-- A helper to check if the variable name indicates a typed hole. +isVarHole :: Var -> Bool +isVarHole x = isHoleStr (F.symbolString (F.symbol x)) + where + isHoleStr s = + case break (== '.') s of + (_, '.':rest) -> rest == "hole" + _ -> False -detectTypedHole :: CGEnv -> CoreExpr -> CG (Maybe (RealSrcSpan, Var)) -detectTypedHole _ (App (Tick genTick (Var x)) _) | isVarHole x - = return (Just (getSrcSpanFromTick, x)) - where - getSrcSpanFromTick = - case genTick of - SourceNote src _ -> src - _ -> panic Nothing "Not a Source Note" - isStrHole s = - case break (=='.') s of - (_, '.':rest) -> rest == "hole" - _ -> False - isVarHole = isStrHole . F.symbolString . F.symbol -detectTypedHole _ _ = return Nothing -- NOT A TYPED HOLE -------------------------------------------------------------------------------- -- | Bidirectional Constraint Generation: CHECKING ----------------------------- -------------------------------------------------------------------------------- cconsE :: CGEnv -> CoreExpr -> SpecType -> CG () -------------------------------------------------------------------------------- cconsE g e t = do - -- _ <- 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) + checkANFHoleInExpr e t cconsE' g e t -------------------------------------------------------------------------------- @@ -388,15 +437,16 @@ cconsE' γ e@(Cast e' c) t cconsE' γ e t = do - _ <- when (warnOnTermHoles (getConfig γ)) maybeAddHole + when (warnOnTermHoles (getConfig γ)) maybeAddHole te <- consE γ e te' <- instantiatePreds γ e te >>= addPost γ addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e) where maybeAddHole = do - isItHole <- detectTypedHole γ e + let isItHole = detectTypedHole e case isItHole of - Just (srcSpan, x) -> addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ + Just (srcSpan, x) -> do + addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ _ -> return () lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> CG (UReft F.Reft) @@ -520,44 +570,20 @@ consE γ (Var x) consE _ (Lit c) = refreshVV $ uRType $ literalFRefType c -consE γ e'@(App e a@(Type τ)) - = do RAllT α te _ <- checkAll ("Non-all TyApp with expr", e) γ <$> consE γ e - t <- if not (nopolyinfer (getConfig γ)) && isPos α && isGenericVar (ty_var_value α) te - then freshTyType (typeclass (getConfig γ)) TypeInstE e τ - else trueTy (typeclass (getConfig γ)) τ - addW $ WfC γ t - t' <- refreshVV t - tt0 <- instantiatePreds γ e' (subsTyVarMeet' (ty_var_value α, t') te) - let tt = makeSingleton γ (simplify e') $ subsTyReft γ (ty_var_value α) τ tt0 - return $ case rTVarToBind α of - Just (x, _) -> maybe (checkUnbound γ e' x tt a) (F.subst1 tt . (x,)) (argType τ) - Nothing -> tt - where - isPos α = not (extensionality (getConfig γ)) || rtv_is_pol (ty_var_info α) - -consE γ e'@(App e a) | Just aDict <- getExprDict γ a - = case dhasinfo (dlookup (denv γ) aDict) (getExprFun γ e) of - Just riSig -> return $ fromRISig riSig - _ -> do - ([], πs, te) <- bkUniv <$> consE γ e - te' <- instantiatePreds γ e' $ foldr RAllP te πs - (γ', te''') <- dropExists γ te' - te'' <- dropConstraints γ te''' - updateLocA {- πs -} (exprLoc e) te'' - let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te'' - cconsE γ' a tx - addPost γ' $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a) - -consE γ e'@(App e a) - = do ([], πs, te) <- bkUniv <$> consE γ {- GM.tracePpr ("APP-EXPR: " ++ GM.showPpr (exprType e)) -} e - te1 <- instantiatePreds γ e' $ foldr RAllP te πs - (γ', te2) <- dropExists γ te1 - te3 <- dropConstraints γ te2 - updateLocA (exprLoc e) te3 - let RFun x _ tx t _ = checkFun ("Non-fun App with caller ", e') γ te3 - cconsE γ' a tx - makeSingleton γ' (simplify e') <$> addPost γ' (maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ $ simplify a)) - +consE γ e'@(App _ _) = + do + t <- if warnOnTermHoles (getConfig γ) then synthesizeWithHole else consEApp γ e' + checkANFHoleInExpr e' t + return t + where + synthesizeWithHole = do + let isItHole = detectTypedHole e' + t <- consEApp γ e' + _ <- case isItHole of + Just (srcSpan, x) -> do + addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ + _ -> return () + return t consE γ (Lam α e) | isTyVar α = do γ' <- updateEnvironment γ α t' <- consE γ' e @@ -603,6 +629,27 @@ consE γ e@(Coercion _) consE _ e@(Type t) = panic Nothing $ "consE cannot handle type " ++ GM.showPpr (e, t) + +checkANFHoleInExpr :: CoreExpr -> SpecType -> CG () +checkANFHoleInExpr e t = do + let vars = collectVars e + forM_ vars $ \var -> do + isANF <- isANFInHole var + case isANF of + Just uniqueVar -> addHoleANF uniqueVar var e t + _ -> return () +collectVars :: CoreExpr -> [Var] +collectVars (Var x) = [x] +collectVars (App e1 e2) = collectVars e1 ++ collectVars e2 +collectVars (Lam x e) = x : collectVars e +collectVars (Let (NonRec x e1) e2) = x : collectVars e1 ++ collectVars e2 +collectVars (Let (Rec xes) e) = + let (xs, es) = unzip xes + in xs ++ concatMap collectVars es ++ collectVars e +collectVars (Case e x _ alts) = + x : collectVars e ++ concatMap collectAltVars alts + where collectAltVars (Alt _ xs e') = xs ++ collectVars e' +collectVars _ = [] consEApp :: CGEnv -> CoreExpr -> CG SpecType consEApp γ e'@(App e a@(Type τ)) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs index 23f28f3661..e262a60aa8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs @@ -302,6 +302,8 @@ initCGI cfg info = CGInfo { , ghcI = info , unsorted = F.notracepp "UNSORTED" $ F.makeTemplates $ gsUnsorted $ gsData spc , hsHoles = M.empty + , hsANFHoles = M.empty + , hsHolesExprs = M.empty } where tce = gsTcEmbeds nspc diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs index 104638132e..9d16749b34 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Monad.hs @@ -20,7 +20,6 @@ import Language.Haskell.Liquid.Constraint.Env import Language.Fixpoint.Misc hiding (errorstar) import Language.Haskell.Liquid.GHC.Misc -- (concatMapM) import Liquid.GHC.API as Ghc hiding (panic, showPpr) -import qualified Language.Fixpoint.Types as FT -------------------------------------------------------------------------------- @@ -120,15 +119,22 @@ addA _ _ _ !a addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG () addHole loc x t γ = do - modify $ \s -> s { hsHoles = M.insert x (holeInfo (s, γ)) $ hsHoles s } - addWarning $ ErrHole loc ("hole found") (reLocal $ renv γ) x' t + exists <- gets (M.member (x, loc) . hsHoles) + unless exists $ + modify $ \s -> s { hsHoles = M.insert (x, loc) (holeInfo (s, γ)) $ hsHoles s } where holeInfo = HoleInfo t loc env env = mconcat [renv γ, grtys γ, assms γ, intys γ] - x' = FT.symbol x -isVarInHole :: Var -> CG Bool -isVarInHole x = gets (M.member x . hsHoles) +addHoleANF :: (Var, SrcSpan) -> Var -> CoreExpr -> SpecType -> CG () +addHoleANF uniqueVar anfVar e t = + modify $ \s -> s { hsHolesExprs = M.insertWith (++) uniqueVar [(anfVar, e, t)] (hsHolesExprs s) } + +linkANFToHole :: Var -> (Var, SrcSpan) -> CG () +linkANFToHole anf h = modify $ \s -> s { hsANFHoles = M.insert anf h $ hsANFHoles s } + +isANFInHole :: Var -> CG (Maybe (Var, SrcSpan)) +isANFInHole anf = gets (M.lookup anf . hsANFHoles) lookupNewType :: Ghc.TyCon -> CG (Maybe SpecType) lookupNewType tc diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs index daf7b7b80f..8b63226b85 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs @@ -239,7 +239,9 @@ data CGInfo = CGInfo , ghcI :: !TargetInfo , dataConTys :: ![(Var, SpecType)] -- ^ Refined Types of Data Constructors , unsorted :: !F.Templates -- ^ Potentially unsorted expressions - , hsHoles :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms + , hsHoles :: !(M.HashMap (Var, SrcSpan) (HoleInfo (CGInfo, CGEnv) SpecType)) -- Information about holes in terms + , hsANFHoles :: !(M.HashMap Var (Var, SrcSpan)) + , hsHolesExprs :: !(M.HashMap (Var, SrcSpan) [(Var, CoreExpr, SpecType)]) } diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs index d0831d7c5c..c8845bc6b1 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Errors.hs @@ -249,8 +249,9 @@ data TError t = , ctx :: !(M.HashMap Symbol t) , svar :: !Symbol , thl :: !t + , anf :: ![(Symbol, CoreExpr, t)] } -- ^ hole type - + | ErrHoleCycle { pos :: !SrcSpan , holesCycle :: [Symbol] -- Var? @@ -785,12 +786,25 @@ ppError' _td _dCtx (ErrHoleCycle _ holes) = "Cycle of holes found" $+$ pprint holes -ppError' td dCtx (ErrHole _ msg c x t) +ppError' td dCtx (ErrHole _ msg c x t a) = "Hole Found" $+$ pprint x <+> "::" <+> pprint t $+$ dCtx $+$ ppContext td c $+$ msg + $+$ "Extra Constraints where hole appears as ANF var" + $+$ (if null a + then empty + else nests 2 [ text "with expression types" + , vsep ( + map ( + \(v, e, t') -> + text "ANF VAR is" <+> pprint v + $+$ text "Expression is [" <+> ppCoreExpr e <+> text "] and has type:" + $+$ pprint t' + ) a + ) + ]) ppError' td dCtx (ErrSubType _ _ cid c tA tE) = text "Liquid Type Mismatch" @@ -1094,6 +1108,9 @@ ppList :: (PPrint a) => Doc -> [a] -> Doc ppList d ls = nest 4 (sepVcat blankLine (d : [ text "*" <+> pprint l | l <- ls ])) +ppCoreExpr :: CoreExpr -> Doc +ppCoreExpr = text . showSDocQualified . ppr + -- | Convert a GHC error into a list of our errors. sourceErrors :: String -> SourceError -> [TError t] diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs index dcd868014b..e369b4b9f1 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs @@ -483,7 +483,8 @@ printWarning logger (Warning srcSpan doc) = GHC.putWarnMsg logger srcSpan doc type ErrorResult = F.FixResult UserError type Error = TError SpecType - +instance NFData CoreExpr where + rnf _ = () -- Simple implementation that doesn't traverse the structure instance NFData a => NFData (TError a) -------------------------------------------------------------------------------- diff --git a/tests/tests.cabal b/tests/tests.cabal index 0ef92e5aab..82664eb654 100644 --- a/tests/tests.cabal +++ b/tests/tests.cabal @@ -2631,6 +2631,10 @@ executable typed-holes other-modules: Example0 , Example1 , Example2 + , Example3 + , Example4 + , Example5 + , Example6 build-depends: base , liquid-prelude , liquidhaskell diff --git a/tests/typed-holes/Example0.hs b/tests/typed-holes/Example0.hs index 3804f2f333..55193d629b 100644 --- a/tests/typed-holes/Example0.hs +++ b/tests/typed-holes/Example0.hs @@ -7,4 +7,4 @@ module Example0 where {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-} listLength :: [a] -> Int listLength [] = hole - listLength (_:xs) = 1 + listLength xs + listLength (_:xs) = 1 + hole diff --git a/tests/typed-holes/Example1.hs b/tests/typed-holes/Example1.hs index 70f505a1e8..0d87a3047a 100644 --- a/tests/typed-holes/Example1.hs +++ b/tests/typed-holes/Example1.hs @@ -3,13 +3,13 @@ module Example1 where import Language.Haskell.Liquid.ProofCombinators (Proof) - hole = undefined {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-} listLength :: [a] -> Int listLength [] = 0 listLength (_:xs) = 1 + listLength xs + {-@ measure listLength @-} {-@ listLengthProof :: xs:[a] -> {listLength xs == len xs} @-} diff --git a/tests/typed-holes/Example2.hs b/tests/typed-holes/Example2.hs index 50509665d1..6453d645b0 100644 --- a/tests/typed-holes/Example2.hs +++ b/tests/typed-holes/Example2.hs @@ -24,5 +24,13 @@ module Example2 where leftId x = empty <> x === hole - === x - *** QED \ No newline at end of file + === x + *** QED + + {-@ rightId :: x:[a] -> { (x <> empty) == x } @-} + rightId :: [a] -> Proof + rightId x = hole + + {-@ assoc :: x:[a] -> y:[a] -> z:[a] -> { (x <> (y <> z)) == ((x <> y) <> z) } @-} + assoc :: [a] -> [a] -> [a] -> Proof + assoc x y z = hole diff --git a/tests/typed-holes/Example3.hs b/tests/typed-holes/Example3.hs new file mode 100644 index 0000000000..48fe1af05d --- /dev/null +++ b/tests/typed-holes/Example3.hs @@ -0,0 +1,40 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--exact-data-cons" @-} +{-@ LIQUID "--warn-on-term-holes" @-} +-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) + +module Example3 where + import Prelude hiding ((<>), reverse, length, (++)) + import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof) + + hole = undefined + + {-@ length :: [a] -> {v:Int | 0 <= v } @-} + length :: [a] -> Int + length [] = 0 + length (_:xs) = 1 + length xs + {-@ measure length @-} + + {-@ reverse :: is:[a] -> {os:[a] | length is == length os} @-} + reverse :: [a] -> [a] + reverse [] = [] + reverse (x:xs) = reverse xs ++ [x] + + {-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-} + (++) :: [a] -> [a] -> [a] + [] ++ ys = ys + (x:xs) ++ ys = x : (xs ++ ys) + {-@ infixl ++ @-} + + {-@ reflect reverse @-} + {-@ reflect ++ @-} + + + --- Structural Induction will be needed. It could suggest as the next step. + {-@ involutionProof :: xs:[a] -> { reverse (reverse xs) == xs } @-} + involutionProof :: [a] -> Proof + involutionProof xs = hole + + {-@ distributivityP :: xs:[a] -> ys:[a] -> { reverse (xs ++ ys) == reverse ys ++ reverse xs } @-} + distributivityP :: [a] -> [a] -> Proof + distributivityP xs ys = hole diff --git a/tests/typed-holes/Example4.hs b/tests/typed-holes/Example4.hs new file mode 100644 index 0000000000..1fdac94991 --- /dev/null +++ b/tests/typed-holes/Example4.hs @@ -0,0 +1,42 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--exact-data-cons" @-} +{-@ LIQUID "--warn-on-term-holes" @-} +-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) + +module Example4 where + import Prelude hiding ((<>), reverse, length, (++)) + import Language.Haskell.Liquid.ProofCombinators ((===), (***), (?), QED(QED), Proof) + + hole = undefined + {-@ length :: [a] -> {v:Int | 0 <= v } @-} + length :: [a] -> Int + length [] = 0 + length (_:xs) = 1 + length xs + {-@ measure length @-} + + {-@ reverse :: is:[a] -> {os:[a] | length is == length os} @-} + reverse :: [a] -> [a] + reverse [] = [] + reverse (x:xs) = reverse xs ++ [x] + + {-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-} + (++) :: [a] -> [a] -> [a] + [] ++ ys = ys + (x:xs) ++ ys = x : (xs ++ ys) + {-@ infixl ++ @-} + + {-@ reflect reverse @-} + {-@ reflect ++ @-} + + {-@ reverseApp :: xs:[a] -> ys:[a] -> {zs:[a] | zs == reverse xs ++ ys} @-} + reverseApp :: [a] -> [a] -> [a] + reverseApp [] ys + = reverse [] ++ ys + === [] ++ ys + === ys + reverseApp (x:xs) ys + = reverse (x:xs) ++ ys + === (reverse xs ++ [x]) ++ ys + === (reverse xs ++ [x] ++ ys) ? hole -- I need a lemma here! Can the hole help me? + === reverse xs ++ ([x] ++ ys) + -- It continues here following the diff --git a/tests/typed-holes/Example5.hs b/tests/typed-holes/Example5.hs new file mode 100644 index 0000000000..93a93274a0 --- /dev/null +++ b/tests/typed-holes/Example5.hs @@ -0,0 +1,36 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--exact-data-cons" @-} +{-@ LIQUID "--warn-on-term-holes" @-} +-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) + +module Example5 where + import Prelude hiding ((<>), reverse, length, (++)) + import Language.Haskell.Liquid.ProofCombinators ((===), (***), (?), QED(QED), Proof) + + hole = undefined + + data Tree = Leaf Int | Node Tree Tree + + {-@ reflect flatten @-} + flatten :: Tree -> [Int] + flatten (Leaf x) = [x] + flatten (Node l r) = flatten l ++ flatten r + + + {-@ length :: [a] -> {v:Int | 0 <= v } @-} + length :: [a] -> Int + length [] = 0 + length (_:xs) = 1 + length xs + {-@ measure length @-} + + {-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-} + (++) :: [a] -> [a] -> [a] + [] ++ ys = ys + (x:xs) ++ ys = x : (xs ++ ys) + {-@ infixl ++ @-} + {-@ reflect ++ @-} + + + {-@ flattenApp :: t:Tree -> ns:[Int] -> { v:[Int] | v == flatten t ++ ns } @-} + flattenApp :: Tree -> [Int] -> [Int] + flattenApp t ns = hole -- Structural Induction diff --git a/tests/typed-holes/Example6.hs b/tests/typed-holes/Example6.hs new file mode 100644 index 0000000000..26dc2b79d9 --- /dev/null +++ b/tests/typed-holes/Example6.hs @@ -0,0 +1,52 @@ +{-@ LIQUID "--expect-error-containing=Hole Found" @-} +{-@ LIQUID "--exact-data-cons" @-} +{-@ LIQUID "--warn-on-term-holes" @-} +-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) +{-@ infix : @-} + +module Example6 where + import Prelude hiding ((<>), reverse, length, (++)) + import Language.Haskell.Liquid.ProofCombinators ((===), (***), (?), QED(QED), Proof) + hole = undefined + {-@ length :: [a] -> {v:Int | 0 <= v } @-} + length :: [a] -> Int + length [] = 0 + length (_:xs) = 1 + length xs + {-@ measure length @-} + + {-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-} + (++) :: [a] -> [a] -> [a] + [] ++ ys = ys + (x:xs) ++ ys = x : (xs ++ ys) + {-@ infixl ++ @-} + {-@ reflect ++ @-} + + + data Expr = Val Int | Add Expr Expr + + {-@ reflect eval @-} + eval :: Expr -> Int + eval (Val n) = n + eval (Add e1 e2) = eval e1 + eval e2 + + type Stack = [Int] + type Code = [Op] + data Op = PUSH Int | ADD + + {-@ reflect exec @-} + exec :: Code -> Stack -> Maybe Stack + exec [] s = Just s + exec (PUSH n : c) s = exec c (n:s) + exec (ADD : c) (m:n:s) = exec c (m+n:s) + exec _ _ = Nothing + + {-@ reflect comp @-} + comp :: Expr -> Code + comp (Val n) = [PUSH n] + comp (Add x y) = comp x ++ comp y ++ [ADD] + + {-@ generalizedCorrectness + :: e:Expr -> s:Stack -> {exec (comp e) s == Just ((eval e):s) } + @-} + generalizedCorrectness :: Expr -> Stack -> Proof + generalizedCorrectness e s = hole -- Structural Induction