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
|
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
module Minilang.Lambda.ParserSpec where
import Data.Text (Text, pack)
import qualified Data.Text as Text
import Minilang.Lambda.Parser (AST (..), initialChars, parse, pretty, restChars)
import Test.Hspec (Spec, parallel, shouldBe)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (Arbitrary (..), Gen, NonEmptyList (..), elements, listOf, oneof, resize, sized, (===), (==>))
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" $ \ast ->
parse (pretty ast) === Right ast
newtype Identifier = Identifier {unIdent :: Text}
deriving (Eq, Show)
instance Arbitrary Identifier where
arbitrary =
Identifier . pack
<$> ((:) <$> elements initialChars <*> listOf (elements restChars))
instance Arbitrary AST where
arbitrary = genAst 10
shrink = \case
Sym _ -> []
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]
genAst :: Int -> Gen AST
genAst 0 = Sym . unIdent <$> arbitrary
genAst depth =
oneof
[ Sym . unIdent <$> arbitrary,
genAbstraction depth,
genApplication depth
]
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
|
