{-# LANGUAGE InstanceSigs #-}

module Funcons.Operations.Expr where

import Funcons.Operations.Values
import Control.Monad (ap)

type OP = String

data Result t = SortErr           String -- sort mismatch
              | DomErr            String -- domain mismatch (in case of partial op)
              | ArityErr          String
              | ProjErr           String -- cannot project to a value
              | Normal            t
              | Nondeterministic  [Result t] 
              deriving Int -> Result t -> ShowS
[Result t] -> ShowS
Result t -> String
(Int -> Result t -> ShowS)
-> (Result t -> String) -> ([Result t] -> ShowS) -> Show (Result t)
forall t. Show t => Int -> Result t -> ShowS
forall t. Show t => [Result t] -> ShowS
forall t. Show t => Result t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result t] -> ShowS
$cshowList :: forall t. Show t => [Result t] -> ShowS
show :: Result t -> String
$cshow :: forall t. Show t => Result t -> String
showsPrec :: Int -> Result t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Result t -> ShowS
Show

choice :: [Result t] -> Result t
choice []  = String -> Result t
forall a. HasCallStack => String -> a
error String
"Nondeterministic: no choice given"
choice [Result t
t] = Result t
t
choice [Result t]
ts  = [Result t] -> Result t
forall t. [Result t] -> Result t
Nondeterministic [Result t]
ts
 
type NullaryOp t  = Result t
type UnaryOp t    = t -> Result t
type BinaryOp t   = t -> t -> Result t
type TernaryOp t  = t -> t -> t -> Result t
type NaryOp t     = [t] -> Result t

type NullaryVOp t  = Result t
type UnaryVOp t    = Values t -> Result t
type BinaryVOp t   = Values t -> Values t -> Result t
type TernaryVOp t  = Values t -> Values t -> Values t -> Result t
type NaryVOp t     = [Values t] -> Result t

data OpExpr t  
      = ValExpr         (Values t)
      | TermExpr        t  
      | NullaryOp   OP  (NullaryOp t)                                    
      | UnaryOp     OP  (UnaryOp t)     (OpExpr t)                       
      | BinaryOp    OP  (BinaryOp t)    (OpExpr t) (OpExpr t)            
      | TernaryOp   OP  (TernaryOp t)   (OpExpr t) (OpExpr t) (OpExpr t) 
      | NaryOp      OP  (NaryOp t)      [OpExpr t]  
      | InvalidOp   OP  String          [OpExpr t]
      | RewritesTo  OP  (OpExpr t)      [OpExpr t]

vNullaryOp :: OP -> NullaryVOp t -> OpExpr t
vNullaryOp :: String -> NullaryVOp t -> OpExpr t
vNullaryOp String
nm NullaryVOp t
op = String -> NullaryVOp t -> OpExpr t
forall t. String -> NullaryOp t -> OpExpr t
NullaryOp String
nm NullaryVOp t
op

vUnaryOp :: HasValues t => OP -> UnaryVOp t -> OpExpr t -> OpExpr t
vUnaryOp :: String -> UnaryVOp t -> OpExpr t -> OpExpr t
vUnaryOp String
nm UnaryVOp t
op = String -> UnaryOp t -> OpExpr t -> OpExpr t
forall t. String -> UnaryOp t -> OpExpr t -> OpExpr t
UnaryOp String
nm UnaryOp t
op'
  where op' :: UnaryOp t
op' t
t = case t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project t
t of
                  Maybe (Values t)
Nothing -> String -> Result t
forall t. String -> Result t
ProjErr String
nm
                  Just Values t
v  -> UnaryVOp t
op Values t
v

vBinaryOp :: HasValues t => OP -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp :: String -> BinaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t
vBinaryOp String
nm BinaryVOp t
op = String -> BinaryOp t -> OpExpr t -> OpExpr t -> OpExpr t
forall t. String -> BinaryOp t -> OpExpr t -> OpExpr t -> OpExpr t
BinaryOp String
nm BinaryOp t
op'
  where op' :: BinaryOp t
op' t
x t
y = case (t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project t
x, t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project t
y) of
                  (Just Values t
v1,Just Values t
v2) -> BinaryVOp t
op Values t
v1 Values t
v2 
                  (Maybe (Values t), Maybe (Values t))
_                 -> String -> Result t
forall t. String -> Result t
ProjErr String
nm

vTernaryOp :: HasValues t => OP -> TernaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t
vTernaryOp :: String
-> TernaryVOp t -> OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t
vTernaryOp String
nm TernaryVOp t
op = String
-> TernaryOp t -> OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t
forall t.
String
-> TernaryOp t -> OpExpr t -> OpExpr t -> OpExpr t -> OpExpr t
TernaryOp String
nm TernaryOp t
op'
  where op' :: TernaryOp t
op' t
x t
y t
z = case (t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project t
x, t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project t
y, t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project t
z) of
                  (Just Values t
v1,Just Values t
v2, Just Values t
v3)  -> TernaryVOp t
op Values t
v1 Values t
v2 Values t
v3
                  (Maybe (Values t), Maybe (Values t), Maybe (Values t))
_                           -> String -> Result t
forall t. String -> Result t
ProjErr String
nm

vNaryOp :: HasValues t => OP -> NaryVOp t -> [OpExpr t] -> OpExpr t
vNaryOp :: String -> NaryVOp t -> [OpExpr t] -> OpExpr t
vNaryOp String
nm NaryVOp t
op = String -> NaryOp t -> [OpExpr t] -> OpExpr t
forall t. String -> NaryOp t -> [OpExpr t] -> OpExpr t
NaryOp String
nm NaryOp t
op'
  where op' :: NaryOp t
op' [t]
ts = case (t -> Maybe (Values t)) -> [t] -> Maybe [Values t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM t -> Maybe (Values t)
forall t. HasValues t => t -> Maybe (Values t)
project [t]
ts of
                  Just [Values t]
vs -> NaryVOp t
op [Values t]
vs
                  Maybe [Values t]
Nothing -> String -> Result t
forall t. String -> Result t
ProjErr String
nm

opName :: OpExpr t -> OP
opName :: OpExpr t -> String
opName (ValExpr Values t
_) = ShowS
forall a. HasCallStack => String -> a
error String
"opName val"
opName (TermExpr t
_) = ShowS
forall a. HasCallStack => String -> a
error String
"opName term"
opName (NullaryOp String
op NullaryOp t
_) = String
op
opName (UnaryOp String
op UnaryOp t
_ OpExpr t
_) = String
op
opName (BinaryOp String
op BinaryOp t
_ OpExpr t
_ OpExpr t
_) = String
op
opName (TernaryOp String
op TernaryOp t
_ OpExpr t
_ OpExpr t
_ OpExpr t
_) = String
op
opName (NaryOp String
op NaryOp t
_ [OpExpr t]
_) = String
op
opName (InvalidOp String
op String
_ [OpExpr t]
_) = String
op
opName (RewritesTo String
op OpExpr t
_ [OpExpr t]
_) = String
op

data ValueOp t      = NullaryExpr (NullaryExpr t)
                    | UnaryExpr (UnaryExpr t)
                    | BinaryExpr (BinaryExpr t)
                    | TernaryExpr (TernaryExpr t)
                    | NaryExpr (NaryExpr t)

type NullaryExpr t  = OpExpr  t
type UnaryExpr t    = OpExpr t -> OpExpr  t
type BinaryExpr t   = OpExpr t -> OpExpr t -> OpExpr  t
type TernaryExpr t  = OpExpr t -> OpExpr t -> OpExpr t -> OpExpr  t
type NaryExpr t     = [OpExpr t] -> OpExpr t

nullaryOp :: NullaryExpr t ->  [OpExpr t] -> OpExpr t
nullaryOp :: NullaryExpr t -> [NullaryExpr t] -> NullaryExpr t
nullaryOp NullaryExpr t
f [] = NullaryExpr t
f
nullaryOp NullaryExpr t
f [NullaryExpr t]
xs = Int -> String -> [NullaryExpr t] -> NullaryExpr t
forall t. Int -> String -> [OpExpr t] -> OpExpr t
arityErr Int
0 (NullaryExpr t -> String
forall t. OpExpr t -> String
opName NullaryExpr t
f) [NullaryExpr t]
xs

unaryOp :: UnaryExpr t ->  [OpExpr t] -> OpExpr t
unaryOp :: UnaryExpr t -> [OpExpr t] -> OpExpr t
unaryOp UnaryExpr t
f [OpExpr t
x] = UnaryExpr t
f OpExpr t
x
unaryOp UnaryExpr t
f [OpExpr t]
xs = Int -> String -> [OpExpr t] -> OpExpr t
forall t. Int -> String -> [OpExpr t] -> OpExpr t
arityErr Int
1 (OpExpr t -> String
forall t. OpExpr t -> String
opName (UnaryExpr t
f OpExpr t
forall a. HasCallStack => a
undefined)) [OpExpr t]
xs

binaryOp :: BinaryExpr t ->  [OpExpr t] -> OpExpr t
binaryOp :: BinaryExpr t -> [OpExpr t] -> OpExpr t
binaryOp BinaryExpr t
f [OpExpr t
x,OpExpr t
y] = BinaryExpr t
f OpExpr t
x OpExpr t
y
binaryOp BinaryExpr t
f [OpExpr t]
xs = Int -> String -> [OpExpr t] -> OpExpr t
forall t. Int -> String -> [OpExpr t] -> OpExpr t
arityErr Int
2 (OpExpr t -> String
forall t. OpExpr t -> String
opName (BinaryExpr t
f OpExpr t
forall a. HasCallStack => a
undefined OpExpr t
forall a. HasCallStack => a
undefined)) [OpExpr t]
xs

ternaryOp :: TernaryExpr t -> [OpExpr t] -> OpExpr t
ternaryOp :: TernaryExpr t -> [OpExpr t] -> OpExpr t
ternaryOp TernaryExpr t
f [OpExpr t
x,OpExpr t
y,OpExpr t
z] = TernaryExpr t
f OpExpr t
x OpExpr t
y OpExpr t
z 
ternaryOp TernaryExpr t
f [OpExpr t]
xs = Int -> String -> [OpExpr t] -> OpExpr t
forall t. Int -> String -> [OpExpr t] -> OpExpr t
arityErr Int
3 (OpExpr t -> String
forall t. OpExpr t -> String
opName (TernaryExpr t
f OpExpr t
forall a. HasCallStack => a
undefined OpExpr t
forall a. HasCallStack => a
undefined OpExpr t
forall a. HasCallStack => a
undefined)) [OpExpr t]
xs

arityErr :: Int -> OP -> [OpExpr t] -> OpExpr t
arityErr :: Int -> String -> [OpExpr t] -> OpExpr t
arityErr Int
i String
op = String -> String -> [OpExpr t] -> OpExpr t
forall t. String -> String -> [OpExpr t] -> OpExpr t
InvalidOp String
op (String
"not applied to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" arguments")

applyExpr :: HasValues t => OpExpr t -> Result t
applyExpr :: OpExpr t -> Result t
applyExpr OpExpr t
expr = case OpExpr t
expr of
  ValExpr Values t
v                     -> t -> Result t
forall t. t -> Result t
Normal (Values t -> t
forall t. HasValues t => Values t -> t
inject Values t
v)
  TermExpr t
t                    -> t -> Result t
forall t. t -> Result t
Normal t
t
  InvalidOp String
_ String
err [OpExpr t]
_             -> String -> Result t
forall t. String -> Result t
ArityErr String
err
  NullaryOp String
_ Result t
f                 -> Result t
f
  UnaryOp String
_ t -> Result t
f OpExpr t
x                 -> t -> Result t
f (t -> Result t) -> Result t -> Result t
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
x
  BinaryOp String
_ BinaryOp t
f OpExpr t
x OpExpr t
y              -> do   t
xv <- OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
x 
                                        t
yv <- OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
y
                                        BinaryOp t
f t
xv t
yv
  TernaryOp String
_ TernaryOp t
f OpExpr t
x OpExpr t
y OpExpr t
z           -> do   t
xv <- OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
x
                                        t
yv <- OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
y
                                        t
zv <- OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
z
                                        TernaryOp t
f t
xv t
yv t
zv
  NaryOp String
_ NaryOp t
f [OpExpr t]
xs                 -> NaryOp t
f NaryOp t -> Result [t] -> Result t
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (OpExpr t -> Result t) -> [OpExpr t] -> Result [t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr [OpExpr t]
xs
  RewritesTo String
_ OpExpr t
e1 [OpExpr t]
_             -> OpExpr t -> Result t
forall t. HasValues t => OpExpr t -> Result t
applyExpr OpExpr t
e1

instance Functor Result where
  fmap :: (a -> b) -> Result a -> Result b
fmap a -> b
f (SortErr String
err)          = String -> Result b
forall t. String -> Result t
SortErr String
err
  fmap a -> b
f (ProjErr String
err)          = String -> Result b
forall t. String -> Result t
ProjErr String
err
  fmap a -> b
f (DomErr String
err)           = String -> Result b
forall t. String -> Result t
DomErr String
err
  fmap a -> b
f (ArityErr String
err)         = String -> Result b
forall t. String -> Result t
ArityErr String
err
  fmap a -> b
f (Normal a
v)             = b -> Result b
forall t. t -> Result t
Normal (a -> b
f a
v)
  fmap a -> b
f (Nondeterministic [Result a]
vs)  = [Result b] -> Result b
forall t. [Result t] -> Result t
Nondeterministic ((Result a -> Result b) -> [Result a] -> [Result b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> Result a -> Result b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) [Result a]
vs)

instance Applicative Result where
  pure :: a -> Result a
pure = a -> Result a
forall t. t -> Result t
Normal
  <*> :: Result (a -> b) -> Result a -> Result b
(<*>) = Result (a -> b) -> Result a -> Result b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Result where
  return :: a -> Result a
return = a -> Result a
forall t. t -> Result t
Normal
  Result a
p >>= :: Result a -> (a -> Result b) -> Result b
>>= a -> Result b
q = case Result a
p of
    SortErr String
err           -> String -> Result b
forall t. String -> Result t
SortErr String
err
    ProjErr String
err           -> String -> Result b
forall t. String -> Result t
ProjErr String
err
    DomErr String
err            -> String -> Result b
forall t. String -> Result t
DomErr String
err
    ArityErr String
err          -> String -> Result b
forall t. String -> Result t
ArityErr String
err
    Normal a
f              -> a -> Result b
q a
f 
    Nondeterministic [Result a]
fs   -> [Result b] -> Result b
forall t. [Result t] -> Result t
Nondeterministic ((Result a -> Result b) -> [Result a] -> [Result b]
forall a b. (a -> b) -> [a] -> [b]
map (Result a -> (a -> Result b) -> Result b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Result b
q) [Result a]
fs)

-- helper / smart constructors
{-
nullaryOp :: OP -> Result t -> OpExpr t
nullaryOp = NullaryOp

unaryOp :: IsOperand o => OP -> o t -> UnaryOp t -> OpExpr t
unaryOp nm o res = UnaryOp nm (toOp o) res

binaryOp :: (IsOperand o1, IsOperand o2) => OP -> o1 t -> o2 t -> BinaryOp t -> OpExpr t
binaryOp nm x y res = BinaryOp nm (toOp x) (toOp y) res

ternaryOp :: IsOperand o => OP -> o t -> o t -> o t -> TernaryOp t -> OpExpr t
ternaryOp nm x y z op = TernaryOp nm (toOp x) (toOp y) (toOp z) op

naryOp :: IsOperand o => OP -> [o t] -> NaryOp t -> OpExpr t
naryOp nm xs op = NaryOp nm (map toOp xs) op

rewritesTo :: (IsOperand o1, IsOperand o2) => OP -> [o1 t] -> o2 t -> OpExpr t 
rewritesTo nm xs op = RewritesTo nm (map toOp xs) (toOp op)
-}