Skip to content

Commit 378476b

Browse files
matheussbernardomatheussbernardo
committed
Add new version detect synthesis
1 parent fc3f3b9 commit 378476b

File tree

10 files changed

+194
-45
lines changed

10 files changed

+194
-45
lines changed

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

Lines changed: 2 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -72,9 +72,7 @@ import Language.Haskell.Liquid.UX.Config
7272
patternFlag,
7373
higherOrderFlag, warnOnTermHoles )
7474
import qualified GHC.Data.Strict as Strict
75-
import Debug.Trace (traceM)
76-
import Data.Generics (gshow)
77-
import qualified Text.Printf as Text
75+
7876

7977
--------------------------------------------------------------------------------
8078
-- | Constraint Generation: Toplevel -------------------------------------------
@@ -112,8 +110,6 @@ emitConsolidatedHoleWarnings :: CG ()
112110
emitConsolidatedHoleWarnings = do
113111
holes <- gets hsHoles
114112
holeExprs <- gets hsHolesExprs
115-
mapAnfs <- gets hsANFHoles
116-
let mapAnfs' = M.fromList $ map (\(k, (v, _)) -> (F.symbol k, F.symbol v)) $ M.toList mapAnfs
117113

118114
let mergedHoles
119115
= [(h
@@ -125,25 +121,9 @@ emitConsolidatedHoleWarnings = do
125121

126122
forM_ mergedHoles $ \(h, holeInfo, anfs) -> do
127123
let γ = snd . info $ holeInfo
128-
let anfs' = map (\(v, x, t) -> (F.symbol v, x, prettifySpecType t mapAnfs')) anfs
124+
let anfs' = map (\(v, x, t) -> (F.symbol v, x, t)) anfs
129125
addWarning $ ErrHole (hloc holeInfo) "hole found" (reLocal $ renv γ) (F.symbol h) (htype holeInfo) anfs'
130126

131-
where
132-
prettifySpecType :: SpecType -> M.HashMap F.Symbol F.Symbol -> SpecType
133-
prettifySpecType t anfs = mapReft undoANF' t
134-
where
135-
undoANF' :: RReft -> RReft
136-
undoANF' (MkUReft (F.Reft (v, e)) p) =
137-
MkUReft (F.Reft (v, undoANFExpr anfs e)) p
138-
undoANFExpr :: M.HashMap F.Symbol F.Symbol -> F.Expr -> F.Expr
139-
undoANFExpr anfMap expr =
140-
F.mapExpr substAnf expr
141-
where
142-
substAnf e@(F.EVar x) =
143-
case M.lookup x anfMap of
144-
Just e' -> undoANFExpr anfMap (F.EVar e')
145-
Nothing -> e
146-
substAnf e = e
147127

148128
--------------------------------------------------------------------------------
149129
-- | Ensure that the instance type is a subtype of the class type --------------
@@ -268,7 +248,6 @@ consCB _ γ (NonRec x e)
268248
let isItHole = detectTypedHole e
269249
case isItHole of
270250
Just (srcSpan, var) -> do
271-
traceM $ Text.printf "HOLE DETECTED LET %s: %s: %s" (show x) (show var) (show srcSpan)
272251
linkANFToHole x (var, RealSrcSpan srcSpan Strict.Nothing)
273252
_ -> return ()
274253
grepDictionary :: CoreExpr -> Maybe (Var, [Type])
@@ -388,7 +367,6 @@ isVarHole x = isHoleStr (F.symbolString (F.symbol x))
388367
cconsE :: CGEnv -> CoreExpr -> SpecType -> CG ()
389368
--------------------------------------------------------------------------------
390369
cconsE g e t = do
391-
_ <- 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)
392370
checkANFHoleInExpr e t
393371
cconsE' g e t
394372

@@ -468,7 +446,6 @@ cconsE' γ e t
468446
let isItHole = detectTypedHole e
469447
case isItHole of
470448
Just (srcSpan, x) -> do
471-
traceM $ Text.printf "HOLE DETECTED CHECKING: %s" (show x)
472449
addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
473450
_ -> return ()
474451

@@ -602,10 +579,8 @@ consE γ e'@(App _ _) =
602579
synthesizeWithHole = do
603580
let isItHole = detectTypedHole e'
604581
t <- consEApp γ e'
605-
traceM $ Text.printf "SYNTHESIZING EXPRESSION: %s\n TYPE: [ %s ]\n" (showpp e') (show t)
606582
_ <- case isItHole of
607583
Just (srcSpan, x) -> do
608-
traceM $ Text.printf "HOLE DETECTED SYNTHESIS: %s" (show x)
609584
addHole (RealSrcSpan srcSpan Strict.Nothing) x t γ
610585
_ -> return ()
611586
return t

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

Lines changed: 0 additions & 2 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 Debug.Trace (traceM)
2423

2524

2625
--------------------------------------------------------------------------------
@@ -120,7 +119,6 @@ addA _ _ _ !a
120119

121120
addHole :: SrcSpan -> Var -> SpecType -> CGEnv -> CG ()
122121
addHole loc x t γ = do
123-
traceM $ "addHole: " ++ show x
124122
modify $ \s -> s { hsHoles = M.insert (x, loc) (holeInfo (s, γ)) $ hsHoles s }
125123
where
126124
holeInfo = HoleInfo t loc env

‎tests/tests.cabal‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2800,6 +2800,12 @@ executable typed-holes
28002800

28012801
ghc-options: -fplugin=LiquidHaskell
28022802
other-modules: Example0
2803+
, Example1
2804+
, Example2
2805+
, Example3
2806+
, Example4
2807+
, Example5
2808+
, Example6
28032809
build-depends: base
28042810
, liquid-prelude
28052811
, liquidhaskell

‎tests/typed-holes/Example0.hs‎

Lines changed: 5 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,10 @@
1-
{-@ LIQUID "--expect-error-containing=AAAAA" @-}
1+
{-@ LIQUID "--expect-error-containing=Hole Found" @-}
22
{-@ LIQUID "--warn-on-term-holes" @-}
33

44
module Example0 where
55
hole = undefined
66

7-
{-@ foo :: {v : Int | v == 1} @-}
8-
foo :: Int
9-
foo = hole + 1
10-
11-
{-@ bar :: {v : Int | v == 1} @-}
12-
bar :: Int
13-
bar = hole - 1
14-
15-
-- {-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
16-
-- listLength :: [a] -> Int
17-
-- listLength [] = hole
18-
-- listLength (_:xs) = 1 + listLength xs
7+
{-@ listLength :: xs:[a] -> {v : Nat | v == len xs} @-}
8+
listLength :: [a] -> Int
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

‎tests/typed-holes/Example3.hs‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
{-@ LIQUID "--expect-error-containing=Hole Found" @-}
2+
{-@ LIQUID "--exact-data-cons" @-}
3+
{-@ LIQUID "--warn-on-term-holes" @-}
4+
-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
5+
6+
module Example3 where
7+
import Prelude hiding ((<>), reverse, length, (++))
8+
import Language.Haskell.Liquid.ProofCombinators ((===), (***), QED(QED), Proof)
9+
10+
hole = undefined
11+
12+
{-@ length :: [a] -> {v:Int | 0 <= v } @-}
13+
length :: [a] -> Int
14+
length [] = 0
15+
length (_:xs) = 1 + length xs
16+
{-@ measure length @-}
17+
18+
{-@ reverse :: is:[a] -> {os:[a] | length is == length os} @-}
19+
reverse :: [a] -> [a]
20+
reverse [] = []
21+
reverse (x:xs) = reverse xs ++ [x]
22+
23+
{-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-}
24+
(++) :: [a] -> [a] -> [a]
25+
[] ++ ys = ys
26+
(x:xs) ++ ys = x : (xs ++ ys)
27+
{-@ infixl ++ @-}
28+
29+
{-@ reflect reverse @-}
30+
{-@ reflect ++ @-}
31+
32+
33+
--- Structural Induction will be needed. It could suggest as the next step.
34+
{-@ involutionProof :: xs:[a] -> { reverse (reverse xs) == xs } @-}
35+
involutionProof :: [a] -> Proof
36+
involutionProof xs = hole
37+
38+
{-@ distributivityP :: xs:[a] -> ys:[a] -> { reverse (xs ++ ys) == reverse ys ++ reverse xs } @-}
39+
distributivityP :: [a] -> [a] -> Proof
40+
distributivityP xs ys = hole

‎tests/typed-holes/Example4.hs‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
{-@ LIQUID "--expect-error-containing=Hole Found" @-}
2+
{-@ LIQUID "--exact-data-cons" @-}
3+
{-@ LIQUID "--warn-on-term-holes" @-}
4+
-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
5+
6+
module Example4 where
7+
import Prelude hiding ((<>), reverse, length, (++))
8+
import Language.Haskell.Liquid.ProofCombinators ((===), (***), (?), QED(QED), Proof)
9+
10+
hole = undefined
11+
{-@ length :: [a] -> {v:Int | 0 <= v } @-}
12+
length :: [a] -> Int
13+
length [] = 0
14+
length (_:xs) = 1 + length xs
15+
{-@ measure length @-}
16+
17+
{-@ reverse :: is:[a] -> {os:[a] | length is == length os} @-}
18+
reverse :: [a] -> [a]
19+
reverse [] = []
20+
reverse (x:xs) = reverse xs ++ [x]
21+
22+
{-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-}
23+
(++) :: [a] -> [a] -> [a]
24+
[] ++ ys = ys
25+
(x:xs) ++ ys = x : (xs ++ ys)
26+
{-@ infixl ++ @-}
27+
28+
{-@ reflect reverse @-}
29+
{-@ reflect ++ @-}
30+
31+
{-@ reverseApp :: xs:[a] -> ys:[a] -> {zs:[a] | zs == reverse xs ++ ys} @-}
32+
reverseApp :: [a] -> [a] -> [a]
33+
reverseApp [] ys
34+
= reverse [] ++ ys
35+
=== [] ++ ys
36+
=== ys
37+
reverseApp (x:xs) ys
38+
= reverse (x:xs) ++ ys
39+
=== (reverse xs ++ [x]) ++ ys
40+
=== (reverse xs ++ [x] ++ ys) ? hole -- I need a lemma here! Can the hole help me?
41+
=== reverse xs ++ ([x] ++ ys)
42+
-- It continues here following the

‎tests/typed-holes/Example5.hs‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
{-@ LIQUID "--expect-error-containing=Hole Found" @-}
2+
{-@ LIQUID "--exact-data-cons" @-}
3+
{-@ LIQUID "--warn-on-term-holes" @-}
4+
-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
5+
6+
module Example5 where
7+
import Prelude hiding ((<>), reverse, length, (++))
8+
import Language.Haskell.Liquid.ProofCombinators ((===), (***), (?), QED(QED), Proof)
9+
10+
hole = undefined
11+
12+
data Tree = Leaf Int | Node Tree Tree
13+
14+
{-@ reflect flatten @-}
15+
flatten :: Tree -> [Int]
16+
flatten (Leaf x) = [x]
17+
flatten (Node l r) = flatten l ++ flatten r
18+
19+
20+
{-@ length :: [a] -> {v:Int | 0 <= v } @-}
21+
length :: [a] -> Int
22+
length [] = 0
23+
length (_:xs) = 1 + length xs
24+
{-@ measure length @-}
25+
26+
{-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-}
27+
(++) :: [a] -> [a] -> [a]
28+
[] ++ ys = ys
29+
(x:xs) ++ ys = x : (xs ++ ys)
30+
{-@ infixl ++ @-}
31+
{-@ reflect ++ @-}
32+
33+
34+
{-@ flattenApp :: t:Tree -> ns:[Int] -> { v:[Int] | v == flatten t ++ ns } @-}
35+
flattenApp :: Tree -> [Int] -> [Int]
36+
flattenApp t ns = hole -- Structural Induction

‎tests/typed-holes/Example6.hs‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
{-@ LIQUID "--expect-error-containing=Hole Found" @-}
2+
{-@ LIQUID "--exact-data-cons" @-}
3+
{-@ LIQUID "--warn-on-term-holes" @-}
4+
-- Based on paper: Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
5+
{-@ infix : @-}
6+
7+
module Example6 where
8+
import Prelude hiding ((<>), reverse, length, (++))
9+
import Language.Haskell.Liquid.ProofCombinators ((===), (***), (?), QED(QED), Proof)
10+
hole = undefined
11+
{-@ length :: [a] -> {v:Int | 0 <= v } @-}
12+
length :: [a] -> Int
13+
length [] = 0
14+
length (_:xs) = 1 + length xs
15+
{-@ measure length @-}
16+
17+
{-@ (++) :: xs:[a] -> ys:[a] -> {zs:[a] | length zs == length xs + length ys} @-}
18+
(++) :: [a] -> [a] -> [a]
19+
[] ++ ys = ys
20+
(x:xs) ++ ys = x : (xs ++ ys)
21+
{-@ infixl ++ @-}
22+
{-@ reflect ++ @-}
23+
24+
25+
data Expr = Val Int | Add Expr Expr
26+
27+
{-@ reflect eval @-}
28+
eval :: Expr -> Int
29+
eval (Val n) = n
30+
eval (Add e1 e2) = eval e1 + eval e2
31+
32+
type Stack = [Int]
33+
type Code = [Op]
34+
data Op = PUSH Int | ADD
35+
36+
{-@ reflect exec @-}
37+
exec :: Code -> Stack -> Maybe Stack
38+
exec [] s = Just s
39+
exec (PUSH n : c) s = exec c (n:s)
40+
exec (ADD : c) (m:n:s) = exec c (m+n:s)
41+
exec _ _ = Nothing
42+
43+
{-@ reflect comp @-}
44+
comp :: Expr -> Code
45+
comp (Val n) = [PUSH n]
46+
comp (Add x y) = comp x ++ comp y ++ [ADD]
47+
48+
{-@ generalizedCorrectness
49+
:: e:Expr -> s:Stack -> {exec (comp e) s == Just ((eval e):s) }
50+
@-}
51+
generalizedCorrectness :: Expr -> Stack -> Proof
52+
generalizedCorrectness e s = hole -- Structural Induction

0 commit comments

Comments
 (0)