{-# LANGUAGE DeriveDataTypeable #-}
module Test.Speculate.Expr.Core
( Expr (..)
, constant
, showConstant
, var
, hole
, holeOfTy
, ($$)
, evaluate
, eval
, typ
, etyp
, typeCorrect
, arity
, holes
, vars
, consts
, atomicConstants
, subexprs
, subexprsV
, isSub
, hasVar
, unfoldApp
, isTuple
, unfoldTuple
, isConstantNamed
, lengthE
, depthE
, countHoles
, countVar
, countVars
, unrepeatedVars
, isAssignment
, lexicompare
, lexicompareBy
, compareComplexity
, compareComplexityThen
, falseE
, showExpr
, showPrecExpr
, showsPrecExpr
, showOpExpr
, showsOpExpr
, eqExprCommuting
)
where
import Data.List (intercalate, find)
import Data.Maybe (fromMaybe, isJust, catMaybes)
import Data.Function (on)
import Data.Monoid ((<>))
import Data.Dynamic
import Test.LeanCheck
import Test.Speculate.Utils
data Expr = Constant String Dynamic
| Var String TypeRep
| Expr :$ Expr
deriving Typeable
constant :: Typeable a => String -> a -> Expr
constant s x = Constant s (toDyn x)
showConstant :: (Typeable a, Show a) => a -> Expr
showConstant x = constant (show x) x
var :: (Listable a, Typeable a) => String -> a -> Expr
var s a = Var s (typeOf a)
hole :: (Listable a, Typeable a) => a -> Expr
hole = holeOfTy . typeOf
holeOfTy :: TypeRep -> Expr
holeOfTy = Var ""
($$) :: Expr -> Expr -> Maybe Expr
e1 $$ e2 =
case typ e1 `funResultTy` typ e2 of
Nothing -> Nothing
Just _ -> Just $ e1 :$ e2
instance Show Expr where
showsPrec d e = showParen (d > 10)
$ showsPrecExpr 0 e
. showString " :: "
. shows (typ e)
. showString (showHoles e)
where
showHoles e = case holes e of
[] -> ""
hs -> " (holes: " ++ intercalate ", " (map show hs) ++ ")"
showsPrecExpr :: Int -> Expr -> String -> String
showsPrecExpr d (Constant s _) | isInfixedPrefix s = showString $ toPrefix s
showsPrecExpr d (Constant s _) | isNegativeLiteral s = showParen (d > 0) $ showString s
showsPrecExpr d (Constant s _) = showParen sp $ showString s
where sp = if atomic s then isInfix s else maybe True (d >) $ outernmostPrec s
showsPrecExpr d (Var "" _) = showString "_"
showsPrecExpr d (Var s _) = showParen (isInfix s) $ showString s
showsPrecExpr d ((Constant ":" _ :$ e1@(Constant _ _)) :$ e2)
| typ e1 == typeOf (undefined :: Char) =
case showsTailExpr e2 "" of
'\"':cs -> showString ("\"" ++ (init . tail) (showsPrecExpr 0 e1 "") ++ cs)
cs -> showParen (d > prec ":")
$ showsOpExpr ":" e1 . showString ":" . showString cs
showsPrecExpr d ((Constant ":" _ :$ e1) :$ e2) =
case showsTailExpr e2 "" of
"[]" -> showString "[" . showsPrecExpr 0 e1 . showString "]"
'[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs
cs -> showParen (d > prec ":")
$ showsOpExpr ":" e1 . showString ":" . showString cs
showsPrecExpr d ee | isTuple ee = id
showString "("
. foldr1 (\s1 s2 -> s1 . showString "," . s2)
(showsPrecExpr 0 `map` unfoldTuple ee)
. showString ")"
showsPrecExpr d ((Constant f _ :$ e1) :$ e2)
| isInfix f = showParen (d > prec f)
$ showsOpExpr f e1
. showString " " . showString f . showString " "
. showsOpExpr f e2
| otherwise = showParen (d > prec " ")
$ showString f
. showString " " . showsOpExpr " " e1
. showString " " . showsOpExpr " " e2
showsPrecExpr d (Constant f _ :$ e1)
| isInfix f = showParen True
$ showsOpExpr f e1 . showString " " . showString f
showsPrecExpr d (e1 :$ e2) = showParen (d > prec " ")
$ showsPrecExpr (prec " ") e1
. showString " "
. showsPrecExpr (prec " " + 1) e2
isTuple :: Expr -> Bool
isTuple = not . null . unfoldTuple
unfoldTuple :: Expr -> [Expr]
unfoldTuple = u . unfoldApp
where
u (Constant cs _:es) | not (null es) && cs == replicate (length es - 1) ','
= es
u _ = []
showsTailExpr :: Expr -> String -> String
showsTailExpr ((Constant ":" _ :$ e1@(Constant _ _)) :$ e2)
| typ e1 == typeOf (undefined :: Char) =
case showsPrecExpr 0 e2 "" of
'\"':cs -> showString ("\"" ++ (init . tail) (showsPrecExpr 0 e1 "") ++ cs)
cs -> showsOpExpr ":" e1 . showString ":" . showsTailExpr e2
showsTailExpr ((Constant ":" _ :$ e1) :$ e2) =
case showsPrecExpr 0 e2 "" of
"[]" -> showString "[" . showsPrecExpr 0 e1 . showString "]"
'[':cs -> showString "[" . showsPrecExpr 0 e1 . showString "," . showString cs
cs -> showsOpExpr ":" e1 . showString ":" . showsTailExpr e2
showsTailExpr e = showsOpExpr ":" e
showsOpExpr :: String -> Expr -> String -> String
showsOpExpr op = showsPrecExpr (prec op + 1)
showOpExpr :: String -> Expr -> String
showOpExpr op = showPrecExpr (prec op + 1)
showPrecExpr :: Int -> Expr -> String
showPrecExpr n e = showsPrecExpr n e ""
showExpr :: Expr -> String
showExpr = showPrecExpr 0
instance Eq Expr where (==) = eqExprCommuting []
eqExprCommuting :: [Expr] -> Expr -> Expr -> Bool
eqExprCommuting ces = e
where
e (Var s1 t1) (Var s2 t2) = t1 == t2 && s1 == s2
e (Constant s1 d1) (Constant s2 d2) = dynTypeRep d1 == dynTypeRep d2 && s1 == s2
e ((ef1 :$ ex1) :$ ey1) ((ef2 :$ ex2) :$ ey2)
| ef1 == ef2 && ef1 `elem` ces = eqExprCommuting ces ex1 ex2 && eqExprCommuting ces ey1 ey2
|| eqExprCommuting ces ex1 ey2 && eqExprCommuting ces ey1 ex2
e (ef1 :$ ex1) (ef2 :$ ex2) = ef1 == ef2 && ex1 == ex2
e _ _ = False
instance Ord Expr where
compare = compareComplexity
lexicompareBy :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering
lexicompareBy compareConstants = cmp
where
c1@(Constant _ _) `cmp` c2@(Constant _ _) = c1 `compareConstants` c2
e1 `cmp` e2 | typ e1 /= typ e2 = typ e1 `compareTy` typ e2
Var s1 _ `cmp` Var s2 _ = s1 `compare` s2
(f :$ x) `cmp` (g :$ y) = f `cmp` g `thn` x `cmp` y
(_ :$ _) `cmp` _ = GT
_ `cmp` (_ :$ _) = LT
_ `cmp` Var _ _ = GT
Var _ _ `cmp` _ = LT
lexicompareConstants :: Expr -> Expr -> Ordering
lexicompareConstants = cmp
where
e1 `cmp` e2 | typ e1 /= typ e2 = typ e1 `compareTy` typ e2
Constant s1 _ `cmp` Constant s2 _ = s1 `compare` s2
_ `cmp` _ = error "lexicompareConstants can only compare constants"
lexicompare :: Expr -> Expr -> Ordering
lexicompare = lexicompareBy lexicompareConstants
compareComplexityThen :: (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering
compareComplexityThen cmp = (compare `on` lengthE)
<> (flip compare `on` length . vars)
<> (flip compare `on` length . repVars)
<> (compare `on` length . consts)
<> cmp
compareComplexity :: Expr -> Expr -> Ordering
compareComplexity = compareComplexityThen lexicompare
falseE :: Expr
falseE = showConstant False
evaluate :: Typeable a => Expr -> Maybe a
evaluate e = v e >>= fromDynamic
where
v :: Expr -> Maybe Dynamic
v (Var _ _) = Nothing
v (Constant _ x) = Just x
v (e1 :$ e2) = do v1 <- v e1
v2 <- v e2
dynApply v1 v2
eval :: Typeable a => a -> Expr -> a
eval x e = fromMaybe x (evaluate e)
typ :: Expr -> TypeRep
typ (Constant _ d) = dynTypeRep d
typ (Var _ t) = t
typ (e1 :$ e2) = resultTy (typ e1)
etyp :: Expr -> Either Expr TypeRep
etyp (e1 :$ e2) =
case (et1,et2) of
(Right t1, Right t2) ->
case t1 `funResultTy` t2 of
Just t -> Right t
Nothing -> Left e
_ -> Left e
where
et1 = etyp e1
et2 = etyp e2
ettoe et = case et of Right t -> Var "" t
Left e -> e
e = ettoe et1 :$ ettoe et2
etyp e = Right (typ e)
typeCorrect :: Expr -> Bool
typeCorrect (e1 :$ e2) = typeCorrect e1
&& typeCorrect e2
&& isJust (typ e1 `funResultTy` typ e2)
typeCorrect _ = True
arity :: Expr -> Int
arity = tyArity . typ
holes :: Expr -> [TypeRep]
holes (e1 :$ e2) = holes e1 ++ holes e2
holes (Var "" t) = [t]
holes _ = []
vars :: Expr -> [(TypeRep,String)]
vars (e1 :$ e2) = vars e1 +++ vars e2
vars (Var s t) = [(t,s)]
vars _ = []
atomicConstants :: Expr -> [Expr]
atomicConstants (e1 :$ e2) = atomicConstants e1 +++ atomicConstants e2
atomicConstants e@(Constant _ _) = [e]
atomicConstants _ = []
hasVar :: Expr -> Bool
hasVar (e1 :$ e2) = hasVar e1 || hasVar e2
hasVar (Var s t) = True
hasVar _ = False
repVars :: Expr -> [(TypeRep,String)]
repVars (e1 :$ e2) = repVars e1 ++ repVars e2
repVars (Var s t) = [(t,s)]
repVars _ = []
consts :: Expr -> [Expr]
consts (e1 :$ e2) = consts e1 +++ consts e2
consts e@(Constant _ _) = [e]
consts _ = []
lengthE :: Expr -> Int
lengthE (e1 :$ e2) = lengthE e1 + lengthE e2
lengthE _ = 1
depthE :: Expr -> Int
depthE e@(_:$_) = 1 + maximum (map depthE $ unfoldApp e)
depthE _ = 1
countHoles :: TypeRep -> Expr -> Int
countHoles t = count t . holes
countVar :: TypeRep -> String -> Expr -> Int
countVar t n (e1 :$ e2) = countVar t n e1 + countVar t n e2
countVar t n (Var n' t') | t == t' && n == n' = 1
countVar _ _ _ = 0
countVars :: Expr -> [(TypeRep,String,Int)]
countVars e = map (\(t,n) -> (t,n,countVar t n e)) $ vars e
unrepeatedVars :: Expr -> Bool
unrepeatedVars = all (\(_,_,n) -> n == 1) . countVars
isAssignment :: Expr -> Bool
isAssignment ((Constant "==" _ :$ Var _ _) :$ e2) = True
isAssignment ((Constant "==" _ :$ e1) :$ Var _ _) = True
isAssignment _ = False
subexprs :: Expr -> [Expr]
subexprs e@(e1 :$ e2) = [e] +++ subexprs e1 +++ subexprs e2
subexprs e@(Constant _ _) = [e]
subexprs _ = []
subexprsV :: Expr -> [Expr]
subexprsV e@(e1 :$ e2) = [e] +++ subexprsV e1 +++ subexprsV e2
subexprsV e = [e]
isConstant :: Expr -> Bool
isConstant (Constant _ _) = True
isConstant _ = False
isSub :: Expr -> Expr -> Bool
isSub e e0 | e == e0 = True
isSub e (e1 :$ e2) = isSub e e1 || isSub e e2
isSub e e0 = e == e0
sub :: Expr -> Expr -> Expr -> Expr
sub ef et = s
where
s e | e == ef = et
s (e1 :$ e2) = s e1 :$ s e2
s e = e
isConstantNamed :: Expr -> String -> Bool
Constant n' _ `isConstantNamed` n = n' == n
_ `isConstantNamed` _ = False
unfoldApp :: Expr -> [Expr]
unfoldApp (ef :$ ex) = unfoldApp ef ++ [ex]
unfoldApp ef = [ef]