module DDF.PE where
import DDF.DBI
import DDF.Double
import qualified Prelude as M
data P repr h a where
Unk :: repr h a -> P repr h a
Static :: a -> (forall h'. repr h' a) -> P repr h a
StaFun :: (forall hout. EnvT repr (a, h) hout -> P repr hout b) -> P repr h (a -> b)
Open :: (forall hout. EnvT repr h hout -> P repr hout a) -> P repr h a
data EnvT repr hin hout where
Dyn :: EnvT repr hin hin
Arg :: P repr hout a -> EnvT repr (a, hout) hout
Weak :: EnvT repr h (a, h)
Next :: EnvT repr hin hout -> EnvT repr (a, hin) (a, hout)
dynamic:: DBI repr => P repr h a -> repr h a
dynamic (Unk x) = x
dynamic (Static _ x) = x
dynamic (StaFun f) = abs $ dynamic (f Dyn)
dynamic (Open f) = dynamic (f Dyn)
app_open :: DBI repr => P repr hin r -> EnvT repr hin hout -> P repr hout r
app_open e Dyn = Unk (dynamic e)
app_open (Static es ed) _ = Static es ed
app_open (Open fs) h = fs h
app_open (StaFun fs) h = abs (fs (Next h))
app_open (Unk env) h = Unk (app_unk env h) where
app_unk :: DBI repr => repr hin a -> EnvT repr hin hout -> repr hout a
app_unk e Dyn = e
app_unk e (Arg p) = app (abs e) (dynamic p)
app_unk e (Next h') = app (s (app_unk (abs e) h')) z
app_unk e Weak = s e
instance DBI r => DBI (P r) where
z = Open f where
f :: EnvT r (a,h) hout -> P r hout a
f Dyn = Unk z
f (Arg x) = x
f (Next _) = z
f Weak = s z
s :: forall h a any. P r h a -> P r (any, h) a
s (Unk x) = Unk (s x)
s (Static a ar) = Static a ar
s (StaFun fs) = abs (fs (Next Weak))
s p = Open f where
f :: EnvT r (any, h) hout -> P r hout a
f Dyn = Unk (s (dynamic p))
f (Arg _) = p
f (Next h) = s (app_open p h)
f Weak = s (s p)
abs (Unk f) = Unk (abs f)
abs (Static k ks) = StaFun $ \_ -> Static k ks
abs body = StaFun (app_open body)
app (Unk f) (Unk x) = Unk (app f x)
app (StaFun fs) p = fs (Arg p)
app (Static _ fs) p = Unk (app fs (dynamic p))
app e1 e2 = Open (\h -> app (app_open e1 h) (app_open e2 h))
instance Bool r => Bool (P r) where
bool x = Static x (bool x)
ite = lam3 (\l r b -> app2 (f b) l r)
where
f :: P r h M.Bool -> P r h (a -> a -> a)
f (Static M.True _) = const
f (Static M.False _) = const1 id
f (Unk x) = Unk (lam2 (\l r -> ite3 l r (s (s x))))
f x = Open (\h -> f (app_open x h))
instance Double r => Double (P r) where
double x = Static x (double x)
doublePlus = abs (abs (f (s z) z))
where
f :: P r h M.Double -> P r h M.Double -> P r h M.Double
f (Static l _) (Static r _) = double (l + r)
f (Static 0 _) r = r
f l (Static 0 _) = l
f (Unk l) (Unk r) = Unk (doublePlus2 l r)
f l r = Open (\h -> f (app_open l h) (app_open r h))
doubleMult = abs (abs (f (s z) z))
where
f :: P r h M.Double -> P r h M.Double -> P r h M.Double
f (Static l _) (Static r _) = double (l * r)
f (Static 0 _) _ = double 0
f _ (Static 0 _) = double 0
f l (Static 1 _) = l
f (Static 1 _) r = r
f (Unk l) (Unk r) = Unk (doubleMult2 l r)
f l r = Open (\h -> f (app_open l h) (app_open r h))
doubleMinus = abs (abs (f (s z) z))
where
f :: P r h M.Double -> P r h M.Double -> P r h M.Double
f (Static l _) (Static r _) = double (l r)
f l (Static 0 _) = l
f (Unk l) (Unk r) = Unk (doubleMinus2 l r)
f l r = Open (\h -> f (app_open l h) (app_open r h))
doubleDivide = abs (abs (f (s z) z))
where
f :: P r h M.Double -> P r h M.Double -> P r h M.Double
f (Static l _) (Static r _) = double (l / r)
f (Static 0 _) _ = double 0
f l (Static 1 _) = l
f (Unk l) (Unk r) = Unk (doubleDivide2 l r)
f l r = Open (\h -> f (app_open l h) (app_open r h))
doubleExp = abs (f z)
where
f :: P r h M.Double -> P r h M.Double
f (Static l _) = double (M.exp l)
f (Unk l) = Unk (doubleExp1 l)
f l = Open (\h -> f (app_open l h))
doubleEq = abs (abs (f (s z) z)) where
f :: P r h M.Double -> P r h M.Double -> P r h M.Bool
f (Static l _) (Static r _) = bool (l == r)
f (Unk l) (Unk r) = Unk (doubleEq2 l r)
f l r = Open (\h -> f (app_open l h) (app_open r h))
pe :: Double repr => P repr () a -> repr () a
pe = dynamic