Commit ece5566d authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Add QuickCheck wrappers to the code generator

Also make the output a bit prettier:
- Alternatives formatted onto their own line
- Use the <$> combinator instead of using 'pure ctor <*>'
parent 85be2d16
......@@ -30,15 +30,25 @@ instance Pretty Expression where
pretty (EQExpr a b) = parens (pretty a <+> pretty "==" <+> pretty b)
pretty (ListExpr l) = pretty "[" <> hcat (punctuate comma (map pretty l)) <> pretty "]"
pretty (LambdaExpr ps ex) = parens (pretty "\\" <> hsep (map pretty ps) <+> pretty "->" <+> pretty ex)
pretty (AppFnCall n ps) = parens $ hsep $ intersperse (pretty "<*>") ((pretty "pure") <+> (pretty $ lowerFirst n) : map pretty ps)
pretty (AppConstrInst n ps) = parens $ hsep $ intersperse (pretty "<*>") ((pretty "pure") <+> (pretty $ upperFirst n) : map pretty ps)
pretty (AltExpr l r) = parens $ hsep [pretty l, (pretty "<|>") <+> (pretty r)]
pretty (TupleExpr es) = parens $ hsep $ punctuate comma $ map pretty es
pretty (AppFnCall n []) = parens $ pretty "pure" <+> (pretty $ lowerFirst n)
pretty (AppFnCall n ps) = parens $ hsep $ (pretty $ lowerFirst n) : (pretty "<$>") : (intersperse (pretty "<*>") $ map pretty ps)
pretty (AppConstrInst n []) = parens $ pretty "pure" <+> (pretty $ upperFirst n)
pretty (AppConstrInst n ps) = parens $ hsep $ (pretty $ upperFirst n) : (pretty "<$>") : (intersperse (pretty "<*>") $ map pretty ps)
pretty a@(AltExpr l r) = parens $ align $ vsep $ _flattenAlt a
pretty (LetExpr bs e) = parens $ align $ ((pretty "let" <+> (align $ vsep [pretty p <+> pretty "=" <+> pretty be | (p, be) <- bs])) <> line <>
(pretty "in" <+> pretty e))
instance Pretty Function where
pretty (Fn n lns) = intoLines (map oneLine lns) where
oneLine :: ([Parameter], Expression) -> Doc a
oneLine (ps, ex) = hsep $ (pretty (lowerFirst n) : map pretty ps) ++ [pretty "=", pretty ex]
_flattenAlt :: Expression -> [Doc a]
_flattenAlt (AltExpr l r) = _flattenAlt l ++ (pretty "<|>" <+> rh) : rt
where (rh:rt) = _flattenAlt r
_flattenAlt expr = [pretty expr]
nl :: Doc a
nl = pretty "\n"
......@@ -49,7 +59,7 @@ printProgram :: String -> Program -> Doc String
printProgram name program =
intoLines [
printModuleDecl name,
printImports ([("Data.List", []), ("Control.Applicative", []), ("Comble", [])] ++ imports program),
printImports ([("Data.List", []), ("Control.Applicative", []), ("Comble", []), ("Test.QuickCheck", [])] ++ imports program),
printTypeDecls (types program),
nl,
printFunctions (functions program),
......
......@@ -34,9 +34,11 @@ data Expression
| EQExpr Expression Expression
| ListExpr [Expression]
| LambdaExpr [Parameter] Expression
| TupleExpr [Expression]
| AppFnCall Name [Expression] -- <$> and <*> from Applicative typeclass
| AppConstrInst Name [Expression] -- idem
| AltExpr Expression Expression -- <|> from Alternative typeclass
| LetExpr [(Parameter, Expression)] Expression
-- | Functions are made up of a name and multiple head (parameter list)
-- and body (expression) pairs
......
......@@ -248,18 +248,27 @@ generatorFunctions (nsd, sd, _, _) =
where
generators :: SortDef -> [Function]
generators s@(MkDefSort sname ctxs ctors rewrite) =
[Fn ("gen" ++ sname) -- Function that returns a datastructure representing every term of some size.
[(VarParam "env" : replaceParam s (IntParam 0) params, FnCall "empty" []),
(VarParam "env" : replaceParam s (IntParam 1) params, alternatives $ map genFromCtor $ filter ((== 0) . ctorSize) ctors),
(VarParam "env" : params , alternatives $ map genFromCtor $ filter ((/= 0) . ctorSize) ctors)],
Fn (sname ++ "Env") -- Function to 'cast' the contexts of one sort to another by discarding variables not in the target sort's contexts
([([ConstrParam ("S" ++ nsname) [VarParam "next"]],
ConstrInst ("S" ++ nsname) [FnCall (sname ++ "Env") [VarExpr "next"]]) | nsname <- map xnamespace ctxs]
++ [([ConstrParam ("S" ++ nsname) [VarParam "next"]],
FnCall (sname ++ "Env") [VarExpr "next"]) | nsname <- filter (not . flip elem (map xnamespace ctxs)) (map nname nsd)]
++ [([ConstrParam "Z" []],
ConstrInst "Z" [])])]
[Fn ("gen" ++ sname) -- Function that returns a datastructure representing every term of some size.
[(VarParam "env" : replaceParam s (IntParam 0) params, FnCall "empty" []),
(VarParam "env" : replaceParam s (IntParam 1) params, alternatives $ map genFromCtor $ filter ((== 0) . ctorSize) ctors),
(VarParam "env" : params , alternatives $ map genFromCtor $ filter ((/= 0) . ctorSize) ctors)],
Fn (sname ++ "Env") -- Function to 'cast' the contexts of one sort to another by discarding variables not in the target sort's contexts
([([ConstrParam ("S" ++ nsname) [VarParam "next"]],
ConstrInst ("S" ++ nsname) [FnCall (sname ++ "Env") [VarExpr "next"]]) | nsname <- map xnamespace ctxs]
++ [([ConstrParam ("S" ++ nsname) [VarParam "next"]],
FnCall (sname ++ "Env") [VarExpr "next"]) | nsname <- filter (not . flip elem (map xnamespace ctxs)) (map nname nsd)]
++ [([ConstrParam "Z" []],
ConstrInst "Z" [])]),
Fn ("for" ++ sname ++ "WithSize") -- Wrapper for QuickCheck's forAll
[(VarParam "env" : params ++ [VarParam "prop"],
LetExpr [(VarParam "c", FnCall ("gen" ++ sname) $ VarExpr "env" : (argsOf sname)),
(VarParam "n", FnCall "card" [VarExpr "c"]),
(VarParam "g", AppFnCall "(!)" [FnCall "pure" [VarExpr "c"],
FnCall "chooseInteger" [TupleExpr [IntExpr 0, Minus (VarExpr "n") (IntExpr 1)]]])]
$ FnCall "forAll" [VarExpr "g", VarExpr "prop"])]
]
where
params = paramsOf sname
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment