1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Minilang.Lambda.ParserSpec where
import Data.Either (isLeft, isRight)
import Data.Function ((&))
import Data.Text (Text, pack)
import qualified Data.Text as Text
import Minilang.Lambda.Eval (Term (Lam))
import qualified Minilang.Lambda.Eval as Eval
import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars)
import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (
Arbitrary (..),
Gen,
NonEmptyList (..),
Positive (..),
counterexample,
elements,
forAll,
forAllShrink,
listOf,
oneof,
resize,
sized,
suchThat,
vectorOf,
(===),
(==>),
)
-- ((f x) y) --> (f x y)
-- (lam (x) (lam (y) y)) --> (lam (x y) y)
spec :: Spec
spec = parallel $ do
prop "parses an identifier as a variable" $ \(Identifier ident) ->
parse ident `shouldBe` Right (Sym ident)
prop "parses a lambda-expression as an abstraction" $ \(Identifier ident) (Identifier body) ->
parse ("(lam (" <> ident <> ") " <> body <> ")") `shouldBe` Right (Abs [ident] (Sym body))
prop "parses a lambda-expression with multiple bindings as an abstraction" $ \(NonEmpty idents) (Identifier body) ->
let vars = unIdent <$> idents
abs = Abs vars (Sym body)
in parse ("(lam (" <> Text.unwords vars <> ") " <> body <> ")") `shouldBe` Right abs
prop "parses an application" $ \(Identifier ident1) (Identifier ident2) ->
parse ("(" <> ident1 <> " " <> ident2 <> ")") `shouldBe` Right (App (Sym ident1) (Sym ident2) [])
prop "parses multiple applications" $ \(NonEmpty idents) ->
(length idents >= 2) ==>
let vars = unIdent <$> idents
(a : b : rest) = vars
app = App (Sym a) (Sym b) (Sym <$> rest)
in parse ("(" <> Text.unwords vars <> ")") `shouldBe` Right app
prop "parses is inverse to pretty" $
forAllShrink (oneof [genAst 5, genDef 5]) shrink $ \ast ->
parse (pretty ast) === Right ast
prop "desugars abstractions to λ-terms" $ forAll (genAbstraction 5) $ \ast ->
let term = desugar ast
ar = arity ast
nestedAbs (Lam _ body) = 1 + nestedAbs body
nestedAbs _ = 0
in nestedAbs term === ar
& counterexample ("Desugared term: " <> show term)
prop "desugars applications to app-terms" $ forAllShrink (genApplication 5) shrink $ \ast ->
let term = desugar ast
ar = spine ast
nestedApp (Eval.App l _) = 1 + nestedApp l
nestedApp _ = 0
in nestedApp term === ar
& counterexample ("Desugared term: " <> show term)
prop "parses multiple let-binding as a function application" $
forAll arbitrary $ \(NonEmpty idents) ->
forAll (vectorOf (length idents) $ genAst 3) $ \(binding : bindings) ->
forAll (genAst 2) $ \body ->
let fun = Abs (unIdent <$> idents) body
app = App fun binding bindings
bound = zip idents (binding : bindings)
in parse
( "(let ("
<> Text.concat
( map
( \(Identifier v, t) ->
"(" <> v <> " " <> pretty t <> ")"
)
bound
)
<> ") "
<> pretty body
<> ")"
)
`shouldSatisfy` isRight
prop "parses a definition" $
forAll (genDef 5) $ \ast ->
let text = pretty ast
in parse text `shouldBe` Right ast
describe "integer literals" $ do
prop "any integer rendered by pretty parses back to the same Lit" $ \n ->
parse (pretty (Lit n)) === Right (Lit (n :: Int))
prop "a '-' separated from digits by spaces does not parse as an integer literal" $
forAll (getPositive <$> (arbitrary :: Gen (Positive Int))) $ \n ->
let spaced = "- " <> Text.pack (show n)
in parse spaced `shouldSatisfy` (/= Right (Lit (negate n)))
it "parses multiline program with blank lines" $ do
let program =
"(def id (lam (x) x))\n\
\\n\
\(def const (lam (x y) x))\n\
\(def apply (lam (f x) (f x)))\n\
\(apply id const)"
expected =
[ Def "id" (Abs ["x"] (Sym "x"))
, Def "const" (Abs ["x", "y"] (Sym "x"))
, Def "apply" (Abs ["f", "x"] (App (Sym "f") (Sym "x") []))
, App
(Sym "apply")
(Sym "id")
[Sym "const"]
]
parseProgram program `shouldBe` Right expected
spine :: AST -> Int
spine = \case
App x _ rest -> 1 + spine x + length rest
_ -> 0
arity :: AST -> Int
arity = \case
Abs bind body -> length bind + arity body
_ -> 0
newtype Identifier = Identifier {unIdent :: Text}
deriving (Eq, Show)
instance Arbitrary Identifier where
arbitrary =
( Identifier . pack
<$> ((:) <$> elements initialChars <*> listOf (elements restChars))
)
`suchThat` (not . isIntLiteral . unIdent)
where
-- An identifier whose first characters would be consumed as an integer
-- literal by the parser must be excluded: the parser tries `lit` before
-- `sym`, so any string starting with digits, or with '-' immediately
-- followed by digits, would produce a Lit rather than a Sym.
isIntLiteral t =
case Text.unpack t of
('-' : d : _) -> isDigit d
(d : _) -> isDigit d
[] -> False
isDigit c = c >= '0' && c <= '9'
instance Arbitrary AST where
arbitrary = genAst 10
shrink = \case
Sym _ -> []
Lit _ -> []
Abs bind body -> case shrink (Identifier <$> bind) of
[] -> shrink body
bind' ->
[ shrunkAbs (unIdent <$> bound) body'
| bound <- bind'
, body' <- shrink body
]
where
shrunkAbs [] b = b
shrunkAbs bound b = Abs bound b
App x y [] -> [x, y]
App x y rest -> (App x y <$> shrink rest) <> [x, y]
Def _name body -> shrink body -- never generated
genAst :: Int -> Gen AST
genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary]
genAst depth =
oneof
[ Sym . unIdent <$> arbitrary
, Lit <$> arbitrary
, genAbstraction depth
, genApplication depth
]
genDef :: Int -> Gen AST
genDef n = Def . unIdent <$> arbitrary <*> genAst n
genApplication :: Int -> Gen AST
genApplication depth = do
App <$> genAst d <*> genAst d <*> reasonablySized (listOf $ genAst d)
where
d = depth - 1
genAbstraction :: Int -> Gen AST
genAbstraction depth = do
x <- unIdent <$> arbitrary
xs <- fmap unIdent <$> reasonablySized arbitrary
Abs (x : xs) <$> reasonablySized (genAst $ depth - 1)
reasonablySized :: Gen a -> Gen a
reasonablySized gen = sized $ \size ->
resize (floor $ sqrt $ fromIntegral @_ @Double size) gen
|
