2019-06-04 18:26:42 +03:00
|
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
|
|
|
|
|
|
|
module Generators
|
|
|
|
( literal
|
|
|
|
, name
|
|
|
|
, variable
|
|
|
|
, boolean
|
|
|
|
, lambda
|
|
|
|
, apply
|
|
|
|
, ifthenelse
|
|
|
|
) where
|
|
|
|
|
|
|
|
import Prelude hiding (span)
|
|
|
|
|
|
|
|
import Hedgehog hiding (Var)
|
|
|
|
import qualified Hedgehog.Gen as Gen
|
|
|
|
import qualified Hedgehog.Range as Range
|
|
|
|
|
|
|
|
import Data.Core
|
|
|
|
import Data.Name
|
2019-07-17 19:44:27 +03:00
|
|
|
import Data.Term
|
2019-06-04 18:26:42 +03:00
|
|
|
|
|
|
|
-- The 'prune' call here ensures that we don't spend all our time just generating
|
|
|
|
-- fresh names for variables, since the length of variable names is not an
|
|
|
|
-- interesting property as they parse regardless.
|
2019-07-17 19:55:05 +03:00
|
|
|
name :: MonadGen m => m (Named User)
|
|
|
|
name = Gen.prune ((Named . Ignored <*> id) <$> names) where
|
2019-06-25 21:21:36 +03:00
|
|
|
names = Gen.text (Range.linear 1 10) Gen.lower
|
2019-06-04 18:26:42 +03:00
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
boolean :: MonadGen m => m (Term Core User)
|
2019-07-17 19:44:27 +03:00
|
|
|
boolean = bool <$> Gen.bool
|
2019-06-04 18:26:42 +03:00
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
variable :: MonadGen m => m (Term Core User)
|
2019-07-17 19:44:27 +03:00
|
|
|
variable = pure . namedValue <$> name
|
2019-06-04 18:26:42 +03:00
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
ifthenelse :: MonadGen m => m (Term Core User) -> m (Term Core User)
|
2019-07-17 19:44:27 +03:00
|
|
|
ifthenelse bod = Gen.subterm3 boolean bod bod if'
|
2019-06-04 18:26:42 +03:00
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
apply :: MonadGen m => m (Term Core User) -> m (Term Core User)
|
2019-06-04 18:26:42 +03:00
|
|
|
apply gen = go where
|
|
|
|
go = Gen.recursive
|
|
|
|
Gen.choice
|
2019-07-17 19:44:27 +03:00
|
|
|
[ Gen.subterm2 gen gen ($$)]
|
|
|
|
[ Gen.subterm2 go go ($$) -- balanced
|
|
|
|
, Gen.subtermM go (\x -> lam <$> name <*> pure x)
|
2019-06-04 18:26:42 +03:00
|
|
|
]
|
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
lambda :: MonadGen m => m (Term Core User) -> m (Term Core User)
|
2019-06-04 18:26:42 +03:00
|
|
|
lambda bod = do
|
|
|
|
arg <- name
|
2019-07-17 19:44:27 +03:00
|
|
|
Gen.subterm bod (lam arg)
|
2019-06-04 18:26:42 +03:00
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
atoms :: MonadGen m => [m (Term Core User)]
|
2019-07-17 19:44:27 +03:00
|
|
|
atoms = [boolean, variable, pure unit, pure frame]
|
2019-06-04 18:26:42 +03:00
|
|
|
|
2019-07-17 19:55:05 +03:00
|
|
|
literal :: MonadGen m => m (Term Core User)
|
2019-06-04 18:26:42 +03:00
|
|
|
literal = Gen.recursive Gen.choice atoms [lambda literal]
|