module SourceTest where
import Testbed
import StaticTest
import HaskellPrelude
main :: IO ()
main = test static imports testDefns
saveTest :: IO ()
saveTest = save "Test" static imports testDefns
Just static = (preludeClasses <:> testClasses) initialEnv
imports :: [Assump]
imports = defnsHaskellPrelude
testDefns :: [BindGroup]
testDefns
= map toBg
[
[("test",
Nothing,
[([PVar "x"],
ap [econst eqMfun, evar "x", evar "x"])])],
[("head'",
Nothing,
[([PCon consCfun [PVar "x", PVar "xs"]],
elet [[("dummy",
Nothing,
[([],
evar "tail'")])]]
(evar "x"))]),
("tail'",
Nothing,
[([PCon consCfun [PVar "x", PVar "xs"]],
elet [[("dummy",
Nothing,
[([],
evar "head'")])]]
(evar "xs"))])],
[("aFloat",
Just (Forall []
([] :=>
tFloat)),
[([],
elit (LitInt 23))])],
[("aNum",
Nothing,
[([],
elit (LitInt 42))])],
[("bNum",
Nothing,
[([],
ap [econst plusMfun, evar "aNum", evar "aFloat"])])],
[("cNum",
Nothing,
[([PVar "x"],
ap [evar "subtract", evar "aFloat", evar "x"])])],
[("oddMono",
Nothing,
[([],
ap [evar ".", evar "not", econst evenMfun])])],
[("sumMono",
Nothing,
[([],
ap [evar "foldl", econst plusMfun, elit (LitInt 0)])])],
[("sumEta",
Nothing,
[([PVar "xs"],
ap [evar "foldl", econst plusMfun, elit (LitInt 0), evar "xs"])])],
[("egg",
Just (Forall [Star]
([isIn1 cOrd (TGen 0)] :=>
(TGen 0 `fn` tBool))),
[([PVar "x"],
ap [evar "||", ap [econst leMfun, evar "x", evar "x"],
ap [evar "egg", econst trueCfun]])])],
[("egf",
Just (Forall [Star]
([isIn1 cEq (TGen 0)] :=>
(TGen 0 `fn` tBool))),
[([PVar "x"],
ap [evar "||", ap [econst eqMfun, evar "x", evar "x"],
ap [evar "egg", econst trueCfun]])])],
[("egf'",
Just (Forall [Star]
([isIn1 cEq (TGen 0)] :=>
(TGen 0 `fn` tBool))),
[([PVar "x"],
ap [evar "||", ap [econst eqMfun, evar "x", evar "x"],
ap [evar "egg'", econst trueCfun]])]),
("egg'",
Nothing,
[([PVar "x"],
ap [evar "||", ap [econst leMfun, evar "x", evar "x"],
ap [evar "egf'", econst trueCfun]])])],
[("egf''",
Nothing,
[([PVar "x"],
ap [evar "||", ap [econst eqMfun, evar "x", evar "x"],
ap [evar "egg''", econst trueCfun]])]),
("egg''",
Nothing,
[([PVar "x"],
ap [evar "||", ap [econst leMfun, evar "x", evar "x"],
ap [evar "egf''", econst trueCfun]])])],
[("myOdd",
Nothing,
[([PLit (LitInt 0)],
econst falseCfun),
([PVar "n"],
ap [evar "not", ap [evar "myEven",
ap [econst minusMfun, evar "n", elit (LitInt 1)]]])]),
("myEven",
Nothing,
[([PLit (LitInt 0)],
econst trueCfun),
([PVar "n"],
ap [evar "not",ap [evar "myOdd",
ap [econst minusMfun, evar "n", elit (LitInt 1)]]])])],
[("eqNull",
Just (Forall [Star]
([isIn1 cEq (TGen 0)] :=>
(TAp tList (TGen 0) `fn` tBool))),
[([PVar "xs"],
ap [econst eqMfun, evar "xs", econst nilCfun])])],
[("eqNull'",
Nothing,
[([PVar "xs"],
ap [econst eqMfun, evar "xs", econst nilCfun])])],
[("baz",
Nothing,
[([PVar "x"],
ap [econst tup2Cfun,
ap [econst tup2Cfun,
ap [econst eqMfun, evar "x"],
ap [econst leMfun, evar "x"]],
ap [econst tup2Cfun,
ap [econst remMfun, evar "x"],
ap [econst plusMfun, evar "x"]]])])]]