{-# LANGUAGE TupleSections #-}
module Conjure.Defn
( Defn
, Bndn
, toDynamicWithDefn
, devaluate
, deval
, devl
, devalFast
, showDefn
, defnApparentlyTerminates
, module Conjure.Expr
)
where
import Conjure.Utils
import Conjure.Expr
import Data.Express
import Data.Express.Express
import Data.Express.Fixtures
import Data.Dynamic
import Control.Applicative ((<$>))
import Test.LeanCheck.Utils ((-:>))
type Defn = [Bndn]
type Bndn = (Expr,Expr)
showDefn :: Defn -> String
showDefn :: Defn -> String
showDefn = [String] -> String
unlines ([String] -> String) -> (Defn -> [String]) -> Defn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr) -> String) -> Defn -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> String
show1
where
show1 :: (Expr, Expr) -> String
show1 (Expr
lhs,Expr
rhs) = Expr -> String
showExpr Expr
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
rhs
toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn Expr -> Expr
exprExpr Int
n Defn
cx = ((Int, Int, Dynamic) -> Dynamic)
-> Maybe (Int, Int, Dynamic) -> Maybe Dynamic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
_,Int
_,Dynamic
d) -> Dynamic
d) (Maybe (Int, Int, Dynamic) -> Maybe Dynamic)
-> (Expr -> Maybe (Int, Int, Dynamic)) -> Expr -> Maybe Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Expr, Expr) -> Int) -> Defn -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Int
size (Expr -> Int) -> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd) Defn
cx)) Int
n
where
(Expr
ef':[Expr]
_) = Expr -> [Expr]
unfoldApp (Expr -> [Expr])
-> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Expr) -> [Expr]) -> (Expr, Expr) -> [Expr]
forall a b. (a -> b) -> a -> b
$ Defn -> (Expr, Expr)
forall a. [a] -> a
head Defn
cx
rev :: Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev :: Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
e = case Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
e of
Maybe (Int, Int, Dynamic)
Nothing -> Maybe (Int, Int, a)
forall a. Maybe a
Nothing
Just (Int
m,Int
n,Dynamic
d) -> case Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
Maybe a
Nothing -> Maybe (Int, Int, a)
forall a. Maybe a
Nothing
Just a
x -> (Int, Int, a) -> Maybe (Int, Int, a)
forall a. a -> Maybe a
Just (Int
m, Int
n, a
x)
re :: Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re :: Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
_ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> Maybe (Int, Int, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: recursion limit reached"
re Int
m Int
n Expr
_ | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> Maybe (Int, Int, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: evaluation limit reached"
re Int
m Int
n (Value String
"if" Dynamic
_ :$ Expr
ec :$ Expr
ex :$ Expr
ey) = case Int -> Int -> Expr -> Maybe (Int, Int, Bool)
forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
ec of
Maybe (Int, Int, Bool)
Nothing -> Maybe (Int, Int, Dynamic)
forall a. Maybe a
Nothing
Just (Int
m,Int
n,Bool
True) -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
ex
Just (Int
m,Int
n,Bool
False) -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
ey
re Int
m Int
n (Value String
"||" Dynamic
_ :$ Expr
ep :$ Expr
eq) = case Int -> Int -> Expr -> Maybe (Int, Int, Bool)
forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
ep of
Maybe (Int, Int, Bool)
Nothing -> Maybe (Int, Int, Dynamic)
forall a. Maybe a
Nothing
Just (Int
m,Int
n,Bool
True) -> (Int
m,Int
n,) (Dynamic -> (Int, Int, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Int, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic (Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True)
Just (Int
m,Int
n,Bool
False) -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
eq
re Int
m Int
n (Value String
"&&" Dynamic
_ :$ Expr
ep :$ Expr
eq) = case Int -> Int -> Expr -> Maybe (Int, Int, Bool)
forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
ep of
Maybe (Int, Int, Bool)
Nothing -> Maybe (Int, Int, Dynamic)
forall a. Maybe a
Nothing
Just (Int
m,Int
n,Bool
True) -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
eq
Just (Int
m,Int
n,Bool
False) -> (Int
m,Int
n,) (Dynamic -> (Int, Int, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Int, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic (Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False)
re Int
m Int
n Expr
e = case Expr -> [Expr]
unfoldApp Expr
e of
[] -> String -> Maybe (Int, Int, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: empty application unfold"
[Expr
e] -> (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
n,) (Dynamic -> (Int, Int, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Int, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic Expr
e
(Expr
ef:[Expr]
exs) | Expr
ef Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ef' -> Maybe (Int, Int, Dynamic)
-> [Maybe (Int, Int, Dynamic)] -> Maybe (Int, Int, Dynamic)
forall a. a -> [a] -> a
headOr (String -> Maybe (Int, Int, Dynamic)
forall a. HasCallStack => String -> a
error (String -> Maybe (Int, Int, Dynamic))
-> String -> Maybe (Int, Int, Dynamic)
forall a b. (a -> b) -> a -> b
$ String
"toDynamicWithDefn: unhandled pattern " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e)
[ Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Expr -> Maybe (Int, Int, Dynamic))
-> Expr -> Maybe (Int, Int, Dynamic)
forall a b. (a -> b) -> a -> b
$ Expr
e' Expr -> Defn -> Expr
//- Defn
bs
| let e :: Expr
e = [Expr] -> Expr
foldApp (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:(Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
exprExpr [Expr]
exs)
, (Expr
a',Expr
e') <- Defn
cx
, Just Defn
bs <- [Expr
e Expr -> Expr -> Maybe Defn
`match` Expr
a']
]
| Bool
otherwise -> (Maybe (Int, Int, Dynamic) -> Expr -> Maybe (Int, Int, Dynamic))
-> Maybe (Int, Int, Dynamic) -> [Expr] -> Maybe (Int, Int, Dynamic)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Maybe (Int, Int, Dynamic) -> Expr -> Maybe (Int, Int, Dynamic)
($$) (Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
ef) [Expr]
exs
Just (Int
m,Int
n,Dynamic
d1) $$ :: Maybe (Int, Int, Dynamic) -> Expr -> Maybe (Int, Int, Dynamic)
$$ Expr
e2 = case Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
e2 of
Maybe (Int, Int, Dynamic)
Nothing -> Maybe (Int, Int, Dynamic)
forall a. Maybe a
Nothing
Just (Int
m', Int
n', Dynamic
d2) -> (Int
m',Int
n',) (Dynamic -> (Int, Int, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Int, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic -> Dynamic -> Maybe Dynamic
dynApply Dynamic
d1 Dynamic
d2
Maybe (Int, Int, Dynamic)
_ $$ Expr
_ = Maybe (Int, Int, Dynamic)
forall a. Maybe a
Nothing
devaluate :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
devaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
devaluate Expr -> Expr
ee Int
n Defn
fxpr Expr
e = (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn Expr -> Expr
ee Int
n Defn
fxpr Expr
e Maybe Dynamic -> (Dynamic -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic
deval :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval :: (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval Expr -> Expr
ee Int
n Defn
fxpr a
x = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x (Maybe a -> a) -> (Expr -> Maybe a) -> Expr -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
devaluate Expr -> Expr
ee Int
n Defn
fxpr
devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
devalFast :: (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
devalFast Expr -> Expr
_ Int
n [(Expr, Expr)
defn] a
x = (Expr, Expr) -> Int -> a -> Expr -> a
forall a. Typeable a => (Expr, Expr) -> Int -> a -> Expr -> a
reval (Expr, Expr)
defn Int
n a
x
devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a
devl :: (Expr -> Expr) -> Int -> Defn -> Expr -> a
devl Expr -> Expr
ee Int
n Defn
fxpr = (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval Expr -> Expr
ee Int
n Defn
fxpr (String -> a
forall a. HasCallStack => String -> a
error String
"devl: incorrect type?")
defnApparentlyTerminates :: Defn -> Bool
defnApparentlyTerminates :: Defn -> Bool
defnApparentlyTerminates [(Expr
efxs, Expr
e)] = Expr -> Expr -> Bool
apparentlyTerminates Expr
efxs Expr
e
defnApparentlyTerminates Defn
_ = Bool
True