module Tip.Haskell.Translate where
#include "errors.h"
import Tip.Haskell.Repr as H
import Tip.Core as T hiding (Formula(..),globals,Type(..),Decl(..))
import Tip.Core (Type((:=>:),BuiltinType))
import qualified Tip.Core as T
import Tip.Pretty
import Tip.Utils
import Tip.Scope
import Data.Maybe (isNothing)
import Tip.CallGraph
import Control.Monad
import qualified Data.Foldable as F
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
import qualified Data.Map as M
import Data.Generics.Geniplate
import Data.List (nub,partition)
prelude :: String -> HsId a
prelude = Qualified "Prelude" (Just "P")
tipDSL :: String -> HsId a
tipDSL = Qualified "Tip" Nothing
quickCheck :: String -> HsId a
quickCheck = Qualified "Test.QuickCheck" (Just "QC")
quickCheckUnsafe :: String -> HsId a
quickCheckUnsafe = Qualified "Test.QuickCheck.Gen.Unsafe" (Just "QU")
quickCheckAll :: String -> HsId a
quickCheckAll = Qualified "Test.QuickCheck.All" (Just "QC")
quickSpec :: String -> HsId a
quickSpec = Qualified "QuickSpec" (Just "QS")
sysEnv :: String -> HsId a
sysEnv = Qualified "System.Environment" (Just "Env")
smtenSym :: String -> HsId a
smtenSym = Qualified "Smten.Symbolic" (Just "S")
smtenEnv :: String -> HsId a
smtenEnv = Qualified "Smten.System.Environment" (Just "Env")
smtenMinisat :: String -> HsId a
smtenMinisat = Qualified "Smten.Symbolic.Solver.MiniSat" (Just "S")
smtenMonad :: String -> HsId a
smtenMonad = Qualified "Smten.Control.Monad" (Just "S")
feat :: String -> HsId a
feat = Qualified "Test.Feat" (Just "F")
lsc :: String -> HsId a
lsc = Qualified "Test.LazySmallCheck" (Just "L")
typeable :: String -> HsId a
typeable = Qualified "Data.Typeable" (Just "T")
data HsId a
= Qualified
{ qual_module :: String
, qual_module_short :: Maybe String
, qual_func :: String
}
| Exact String
| Other a
| Derived (HsId a) String
deriving (Eq,Ord,Show,Functor,Traversable,Foldable)
instance PrettyVar a => PrettyVar (HsId a) where
varStr (Qualified _ (Just m) s) = m ++ "." ++ s
varStr (Qualified m Nothing s) = m ++ "." ++ s
varStr (Exact s) = s
varStr (Other x) = varStr x
varStr (Derived o s) = s ++ varStr o
addHeader :: String -> Decls a -> Decls a
addHeader mod_name (Decls ds) =
Decls (map LANGUAGE ["TemplateHaskell","DeriveDataTypeable","TypeOperators","ImplicitParams","RankNTypes"] ++ Module mod_name : ds)
addImports :: Ord a => Decls (HsId a) -> Decls (HsId a)
addImports d@(Decls ds) = Decls (QualImport "Text.Show.Functions" Nothing : imps ++ ds)
where
imps = usort [ QualImport m short | Qualified m short _ <- F.toList d ]
trTheory :: (Ord a,PrettyVar a) => Mode -> Theory a -> Decls (HsId a)
trTheory mode = fixup_prel . trTheory' mode . fmap Other
where
fixup_prel =
case mode of
Smten -> fmap fx
_ -> id
where
fx (Qualified "Prelude" u v) = Qualified "Smten.Prelude" (Just "S") v
fx u = u
data Kind = Expr | Formula deriving Eq
theorySigs :: Theory (HsId a) -> [HsId a]
theorySigs Theory{..} = map sig_name thy_sigs
ufInfo :: Theory (HsId a) -> (Bool,[H.Type (HsId a)])
ufInfo Theory{thy_sigs} = (not (null imps),imps)
where
imps = [TyImp (Derived f "imp") (H.TyCon (Derived f "") []) | Signature f _ <- thy_sigs]
data Mode = Feat | QuickCheck | LazySmallCheck Bool | Smten | QuickSpec | Plain
deriving (Eq,Ord,Show)
isLazySmallCheck LazySmallCheck{} = True
isLazySmallCheck _ = False
isSmten Smten{} = True
isSmten _ = False
trTheory' :: forall a b . (a ~ HsId b,Ord b,PrettyVar b) => Mode -> Theory a -> Decls a
trTheory' mode thy@Theory{..} =
Decls $
concat [space_decl | isSmten mode ] ++
concatMap tr_datatype thy_datatypes ++
map tr_sort thy_sorts ++
concatMap tr_sig thy_sigs ++
concatMap tr_func thy_funcs ++
tr_asserts thy_asserts ++
[makeSig thy | mode == QuickSpec ]
where
(translate_UFs,imps) = ufInfo thy
space_decl :: [Decl a]
space_decl =
[ ClassDecl [] (TyCon (Exact "Space") [TyVar (Exact "stv")])
[TySig (Exact "space") []
(TyArr (TyCon (prelude "Int") [])
(TyCon (smtenSym "Symbolic") [TyVar (Exact "stv")]))
]
, InstDecl [] (TyCon (Exact "Space") [TyCon (prelude "Bool") []])
[funDecl
(Exact "space")
[d]
(H.Case (Apply (prelude "<") [var d,H.Int 0])
[(H.ConPat (prelude "True") [], Apply (smtenMonad "mzero") [])
,(H.WildPat,
Apply (smtenMonad "msum")
[List
[ Apply (smtenMonad "return") [Apply (prelude "False") []]
, Apply (smtenMonad "return") [Apply (prelude "True") []]
]])
])
]
]
where d = Exact "d"
tr_datatype :: Datatype a -> [Decl a]
tr_datatype (Datatype tc tvs cons) =
[ DataDecl tc tvs
[ (c,map (trType . snd) args) | Constructor c _ args <- cons ]
(map prelude ["Eq","Ord","Show"]
++ [typeable "Typeable" | not (isSmten mode) ])
]
++
[ TH (Apply (feat "deriveEnumerable") [QuoteTyCon tc])
| any (== mode) [Feat, QuickCheck, QuickSpec] ]
++
[ InstDecl [H.TyCon (feat "Enumerable") [H.TyVar a] | a <- tvs]
(H.TyCon (quickCheck "Arbitrary") [H.TyCon tc (map H.TyVar tvs)])
[funDecl
(quickCheck "arbitrary") []
(Apply (quickCheck "sized") [Apply (feat "uniform") []])]
| any (== mode) [QuickCheck, QuickSpec] ]
++
[ InstDecl
[H.TyCon (lsc "Serial") [H.TyVar a] | a <- tvs]
(H.TyCon (lsc "Serial") [H.TyCon tc (map H.TyVar tvs)])
[funDecl
(lsc "series")
[]
(foldr1
(\ e1 e2 -> Apply (lsc "\\/") [e1,e2])
[ foldl
(\ e _ -> Apply (lsc "><") [e,Apply (lsc "series") []])
(Apply (lsc "cons") [Apply c []])
as
| Constructor c _ as <- cons
])]
| isLazySmallCheck mode ]
++
[ InstDecl
[H.TyCon (Exact "Space") [H.TyVar a] | a <- tvs]
(H.TyCon (Exact "Space") [H.TyCon tc (map H.TyVar tvs)])
[funDecl
(Exact "space")
[d]
(H.Case (Apply (prelude "<") [var d,H.Int 0])
[(H.ConPat (prelude "True") [], Apply (smtenMonad "mzero") [])
,(H.WildPat,
Apply (smtenMonad "msum")
[List
[ foldl (\ e1 _ ->
Apply (smtenMonad "ap")
[e1,Apply (Exact "space")
[Apply (prelude "-") [var d,H.Int 1]]])
(Apply (smtenMonad "return") [Apply c []])
args
| Constructor c _ args <- cons
]])
])
]
| let d = Exact "d"
, isSmten mode
]
tr_sort :: Sort a -> Decl a
tr_sort (Sort s i) | null i = TypeDef (TyCon s []) (TyCon (prelude "Int") [])
tr_sort (Sort _ _) = error "Haskell.Translate: Poly-kinded abstract sort"
tr_sig :: Signature a -> [Decl a]
tr_sig (Signature f pt) =
[ DataDecl (Derived f "") [] [ (Derived f "Mk",[tr_polyTypeArbitrary pt]) ] []
, FunDecl (Derived f "get")
[( [H.ConPat (Derived f "Mk") [VarPat (Derived f "x")]]
, var (Derived f "x")
)]
, TySig f [] (tr_polyType pt)
, funDecl f [] (Apply (Derived f "get") [ImpVar (Derived f "imp")])
, InstDecl [] (TyCon (quickCheck "Arbitrary") [TyCon (Derived f "") []])
[ funDecl (quickCheck "arbitrary") []
(mkDo [Bind (Derived f "x") (Apply (quickCheckUnsafe "capture") [])]
(H.Case (var (Derived f "x"))
[(H.ConPat (quickCheckUnsafe "Capture") [VarPat (Derived f "y")]
,Apply (prelude "return")
[Apply (Derived f "Mk")
[Apply (Derived f "y")
[Apply (quickCheck "arbitrary") []]]]
)]
)
)
]
, TySig (Derived f "gen") []
(TyCon (quickCheck "Gen")
[TyCon (quickSpec "Dict")
[TyImp (Derived f "imp") (TyCon (Derived f "") [])]])
, funDecl (Derived f "gen") []
(mkDo [Bind (Derived f "x") (Apply (quickCheck "arbitrary") [])]
(ImpLet (Derived f "imp") (var (Derived f "x"))
(Apply (prelude "return") [Apply (quickSpec "Dict") []])))
]
tr_func :: Function a -> [Decl a]
tr_func fn@Function{..} =
[ TySig func_name [] (tr_polyType (funcType fn))
, FunDecl
func_name
[ (map tr_deepPattern dps,tr_expr Expr rhs)
| (dps,rhs) <- patternMatchingView func_args func_body
]
] ++
[ FunDecl
(prop_version func_name)
[ (map tr_deepPattern dps,tr_expr Formula rhs)
| (dps,rhs) <- patternMatchingView func_args func_body
]
| isLazySmallCheck mode && func_res == boolType
]
prop_version f = Derived f "property"
tr_asserts :: [T.Formula a] -> [Decl a]
tr_asserts fms =
let (info,decls) = unzip (zipWith tr_assert [1..] fms)
in concat decls ++
case mode of
QuickCheck ->
[ TH (Apply (prelude "return") [List []])
, funDecl (Exact "main") []
(mkDo [ Stmt (THSplice (Apply (quickCheckAll "polyQuickCheck")
[QuoteName name]))
| (name,_) <- info ]
Noop)
]
LazySmallCheck md ->
[ funDecl (Exact "main") []
((`mkDo` Noop)
$ [Bind (Exact "args") (Apply (sysEnv "getArgs") [])]
++ [Stmt (fn name) | (name,_) <- info])
]
where
fn name = case md of
False -> Apply (lsc "test") [var name]
True -> Apply (lsc "depthCheck")
[read_head (var (Exact "args"))
,var name]
Feat ->
[ funDecl (Exact "main") []
(mkDo [Stmt (Apply (feat "featCheckStop")
[ H.Lam [TupPat (map VarPat vs)] (Apply name (map var vs))
])
| (name,vs) <- info ] Noop)
]
Smten | let [(name,vs)] = info ->
[ funDecl (Exact "main") []
$ mkDo [Bind (Exact "args") (Apply (smtenEnv "getArgs") [])
,Bind (Exact "r")
(Apply (smtenSym "run_symbolic")
[Apply (smtenMinisat "minisat") []
,mkDo (
[ Bind v (Apply (Exact "space") [read_head (var (Exact "args"))])
| v <- vs ]
++
[ Stmt $ Apply (smtenMonad "guard") [Apply (prelude "not") [Apply name (map var vs)]] ])
(Apply (smtenMonad "return") [nestedTup (map var vs)])
])
]
(Apply (prelude "print") [var (Exact "r")])
]
_ -> []
where
read_head e = Apply (prelude "read") [Apply (prelude "head") [e]]
tr_assert :: Int -> T.Formula a -> ((a,[a]),[Decl a])
tr_assert i (T.Formula r _ tvs b) =
((prop_name,args),
[ TySig prop_name []
(foldr TyArr
(case mode of LazySmallCheck{} -> H.TyCon (lsc "Property") []
_ -> H.TyCon (prelude "Bool") [])
[ trType (applyType tvs (replicate (length tvs) (intType)) t)
| Local _ t <- typed_args ])
| mode == Feat || isLazySmallCheck mode || mode == Smten ]
++
[ funDecl prop_name args (assume (tr_expr (if mode == Feat || isSmten mode then Expr else Formula) body)) ]
)
where
prop_name | i == 1 = Exact "prop"
| otherwise = Exact ("prop" ++ show i)
(typed_args,body) =
case b of
Quant _ Forall lcls term -> (lcls,term)
_ -> ([],b)
args = map lcl_name typed_args
assume e =
case r of
Prove -> e
Assert -> Apply (tipDSL "assume") [e]
tr_deepPattern :: DeepPattern a -> H.Pat a
tr_deepPattern (DeepConPat Global{..} dps) = H.ConPat gbl_name (map tr_deepPattern dps)
tr_deepPattern (DeepVarPat Local{..}) = VarPat lcl_name
tr_deepPattern (DeepLitPat (T.Int i)) = IntPat i
tr_deepPattern (DeepLitPat (Bool b)) = withBool H.ConPat b
tr_pattern :: T.Pattern a -> H.Pat a
tr_pattern Default = WildPat
tr_pattern (T.ConPat Global{..} xs) = H.ConPat gbl_name (map (VarPat . lcl_name) xs)
tr_pattern (T.LitPat (T.Int i)) = H.IntPat i
tr_pattern (T.LitPat (Bool b)) = withBool H.ConPat b
tr_expr :: Kind -> T.Expr a -> H.Expr a
tr_expr k e0 =
case e0 of
Builtin (Lit (T.Int i)) :@: [] -> H.Int i
Builtin (Lit (Bool b)) :@: [] -> lsc_lift (withBool Apply b)
Builtin Implies :@: [u,v] | mode == Smten -> tr_expr k (Builtin Or :@: [Builtin Not :@: [u],v])
hd :@: es -> let ((f,k'),lft) = tr_head (map exprType es) k hd
in lift_if lft (maybe_ty_sig e0 (Apply f (map (tr_expr k') es)))
Lcl x -> lsc_lift (var (lcl_name x))
T.Lam xs b -> H.Lam (map (VarPat . lcl_name) xs) (tr_expr Expr b)
Match e alts -> H.Case (tr_expr Expr e) [ (tr_pattern p,tr_expr brs_k rhs) | T.Case p rhs <- default_last alts ]
where
brs_k
| isLazySmallCheck mode = k
| otherwise = Expr
T.Let x e b -> H.Let (lcl_name x) (tr_expr Expr e) (tr_expr k b)
T.Quant _ q xs b ->
foldr
(\ x e ->
Apply (tipDSL (case q of Forall -> "forAll"; Exists -> "exists"))
[H.Lam [VarPat (lcl_name x)] e])
(tr_expr Formula b)
xs
where
maybe_ty_sig e@(hd@(Gbl Global{..}) :@: es) he
| isNothing (makeGlobal gbl_name gbl_type (map exprType es) Nothing)
= he ::: trType (exprType e)
maybe_ty_sig _ he = he
lift_if b e
| b && isLazySmallCheck mode = Apply (lsc "lift") [e]
| otherwise = e
lsc_lift = lift_if (k == Formula)
default_last (def@(T.Case Default _):alts) = alts ++ [def]
default_last alts = alts
tr_head :: [T.Type a] -> Kind -> T.Head a -> ((a,Kind),Bool)
tr_head ts k (Builtin b) = tr_builtin ts k b
tr_head ts k (Gbl Global{..})
| stay_prop = ((prop_version gbl_name,Expr),False)
| otherwise = ((gbl_name ,Expr),False)
where
stay_prop = k == Formula
&& isLazySmallCheck mode
&& polytype_res gbl_type == boolType
tr_builtin :: [T.Type a] -> Kind -> T.Builtin -> ((a,Kind),Bool)
tr_builtin ts k b =
case b of
At -> ((prelude "id",Expr),False)
Lit{} -> error "tr_builtin"
And -> case_kind (tipDSL ".&&.") (Just (lsc "*&*"))
Or -> case_kind (tipDSL ".||.") (Just (lsc "*|*"))
Not -> case_kind (tipDSL "neg") (Just (lsc "neg"))
Implies -> case_kind (tipDSL "==>") (Just (lsc "*=>*"))
Equal -> case_kind (tipDSL "===") $ case ts of
BuiltinType Boolean:_ -> Just (lsc "*=*")
_ -> Nothing
Distinct -> case_kind (tipDSL "=/=") Nothing
_ -> (prelude_fn,False)
where
Just prelude_str_ = lookup b hsBuiltins
prelude_fn = (prelude prelude_str_,Expr)
case_kind tip_version lsc_version =
case k of
Expr -> (prelude_fn,False)
Formula ->
case mode of
LazySmallCheck{} ->
case lsc_version of
Just v -> ((v,Formula),False)
Nothing -> (prelude_fn,True)
_ -> ((tip_version,Formula),False)
tr_polyType_inner :: T.PolyType a -> H.Type a
tr_polyType_inner (PolyType _ ts t) = trType (ts :=>: t)
tr_polyType :: T.PolyType a -> H.Type a
tr_polyType pt@(PolyType tvs _ _)
| translate_UFs = TyForall tvs (TyCtx (arb tvs ++ imps) (tr_polyType_inner pt))
| otherwise = tr_polyType_inner pt
tr_polyTypeArbitrary :: T.PolyType a -> H.Type a
tr_polyTypeArbitrary pt@(PolyType tvs _ _) = TyForall tvs (TyCtx (arb tvs) (tr_polyType_inner pt))
arb = arbitrary . map H.TyVar
arbitrary :: [H.Type (HsId a)] -> [H.Type (HsId a)]
arbitrary ts =
[ TyCon (quickCheck tc) [t]
| t <- ts
, tc <- ["Arbitrary","CoArbitrary"]
]
trType :: (a ~ HsId b) => T.Type a -> H.Type a
trType (T.TyVar x) = H.TyVar x
trType (T.TyCon tc ts) = H.TyCon tc (map trType ts)
trType (ts :=>: t) = foldr TyArr (trType t) (map trType ts)
trType (BuiltinType b) = trBuiltinType b
trBuiltinType :: BuiltinType -> H.Type (HsId a)
trBuiltinType t | Just s <- lookup t hsBuiltinTys = H.TyCon (prelude s) []
withBool :: (a ~ HsId b) => (a -> [c] -> d) -> Bool -> d
withBool k b = k (prelude (show b)) []
hsBuiltinTys :: [(T.BuiltinType,String)]
hsBuiltinTys =
[ (Integer, "Int")
, (Boolean, "Bool")
]
hsBuiltins :: [(T.Builtin,String)]
hsBuiltins =
[ (And , "&&" )
, (Or , "||" )
, (Not , "not")
, (Implies , "<=" )
, (Equal , "==" )
, (Distinct , "/=" )
, (IntAdd , "+" )
, (IntSub , "-" )
, (IntMul , "*" )
, (IntDiv , "div")
, (IntMod , "mod")
, (IntGt , ">" )
, (IntGe , ">=" )
, (IntLt , "<" )
, (IntLe , "<=" )
]
typeOfBuiltin :: Builtin -> T.Type a
typeOfBuiltin b = case b of
And -> bbb
Or -> bbb
Not -> bb
Implies -> bbb
Equal -> iib
Distinct -> iib
IntAdd -> iii
IntSub -> iii
IntMul -> iii
IntDiv -> iii
IntMod -> iii
IntGt -> iib
IntGe -> iib
IntLt -> iib
IntLe -> iib
_ -> __
where
bb = [boolType] :=>: boolType
bbb = [boolType,boolType] :=>: boolType
iii = [intType,intType] :=>: intType
iib = [intType,intType] :=>: boolType
makeSig :: forall a . (PrettyVar a,Ord a) => Theory (HsId a) -> Decl (HsId a)
makeSig thy@Theory{..} =
funDecl (Exact "sig") [] $
Tup
[ List
[ Tup
[ constant_decl ft
, List $
if use_cg
then
[ int_lit num
| (members,num) <- cg `zip` [0..]
, f `elem` members
]
else
[int_lit 0]
]
| ft@(f,_) <- func_constants
]
, Apply (quickSpec "signature") [] `Record`
[ (quickSpec "constants",
List $
builtin_decls ++
map constant_decl
(ctor_constants ++ builtin_constants))
, (quickSpec "instances", List $
[ mk_inst [] (mk_class (feat "Enumerable") (H.TyCon (prelude "Int") [])) ] ++
[ mk_inst (map (mk_class c1) tys) (mk_class c2 (H.TyCon t tys))
| (t,n) <- type_univ
, (c1, c2) <- [(prelude "Ord", prelude "Ord"),
(feat "Enumerable", feat "Enumerable"),
(feat "Enumerable",quickCheck "Arbitrary")]
, let tys = map trType (qsTvs n)
] ++
[ Apply (quickSpec "makeInstance") [H.Lam [TupPat []] (Apply (Derived f "gen") [])]
| Signature f _ <- thy_sigs
])
, (quickSpec "maxTermSize", Apply (prelude "Just") [H.Int (if translate_UFs then 15 else 7)])
, (quickSpec "maxTermDepth", Apply (prelude "Just") [H.Int 4])
, (quickSpec "testTimeout", Apply (prelude "Just") [H.Int 100000])
]
]
where
(translate_UFs,imps) = ufInfo thy
use_cg = True
int_lit x = H.Int x ::: H.TyCon (prelude "Int") []
mk_inst ctx res =
Apply (quickSpec ("inst" ++ concat [ show (length ctx) | length ctx >= 2 ]))
[ Apply (quickSpec "Sub") [Apply (quickSpec "Dict") []] :::
H.TyCon (quickSpec ":-") [TyTup ctx,res] ]
mk_class c x = H.TyCon c [x]
scp = scope thy
cg = map (map defines) (flatCallGraph (CallGraphOpts False False) thy)
poly_type (PolyType _ args res) = args :=>: res
constant_decl (f,t) =
Apply (quickSpec "constant") [H.String f,lam (Apply f []) ::: qs_type]
where
(pre,qs_type) = qsType t
lam | null pre = id
| otherwise = H.Lam (replicate (length pre) (H.ConPat (quickSpec "Dict") []))
int_lit_decl x =
Apply (quickSpec "constant") [H.String (Exact (show x)),int_lit x]
bool_lit_decl b =
Apply (quickSpec "constant") [H.String (prelude (show b)),withBool Apply b]
ctor_constants =
[ (f,poly_type (globalType g))
| (f,g@ConstructorInfo{}) <- M.toList (globals scp)
]
func_constants =
[ (f,poly_type (globalType g))
| (f,g@FunctionInfo{}) <- M.toList (globals scp)
]
type_univ =
[ (data_name, length data_tvs)
| (_,DatatypeInfo Datatype{..}) <- M.toList (types scp)
]
(builtin_lits,builtin_funs) =
partition litBuiltin $
usort
[ b
| Builtin b :@: args <- universeBi thy
, let is_int = case args of
a1:_ -> exprType a1 == (intType :: T.Type (HsId a))
_ -> __
, case b of
Equal -> is_int
Distinct -> is_int
_ -> True
]
used_builtin_types :: [BuiltinType]
used_builtin_types =
usort [ t | BuiltinType t :: T.Type (HsId a) <- universeBi thy ]
bool_used = Boolean `elem` used_builtin_types
int_used =
or [ op `elem` builtin_funs | op <- [IntAdd,IntSub,IntMul,IntDiv,IntMod] ]
builtin_decls
= [ bool_lit_decl b | bool_used, b <- [False,True] ]
++ [ int_lit_decl x | int_used, x <- [0,1] ++
[ x
| Lit (T.Int x) <- builtin_lits ]]
builtin_constants
= [ (prelude s,typeOfBuiltin b)
| b <- nub $
[ b | bool_used, b <- [And,Or,Not] ]
++ [ b | b <- builtin_funs, intBuiltin b || eqRelatedBuiltin b ]
, Just s <- [lookup b hsBuiltins]
]
qsType :: Ord a => T.Type (HsId a) -> ([H.Type (HsId a)],H.Type (HsId a))
qsType t = (pre,foldr TyArr inner [ TyCon (quickSpec "Dict") [p] | p <- pre ])
where
pre | translate_UFs = arbitrary (map trType qtvs) ++ imps
| otherwise = []
inner = trType (applyType tvs qtvs t)
qtvs = qsTvs (length tvs)
tvs = tyVars t
qsTvs :: Int -> [T.Type (HsId a)]
qsTvs n = take n (cycle [ T.TyCon (quickSpec qs_tv) [] | qs_tv <- ["A","B","C","D","E"] ])
theoryBuiltins :: Ord a => Theory a -> [T.Builtin]
theoryBuiltins = usort . universeBi