prog_synthesis/escher/Expr.hs

module Expr where

import Control.Applicative
import Control.Monad (liftM)

data Tree a = TNode { treeLeft :: Tree a, treeRoot :: a, treeRight :: Tree a }
            | TLeaf a
    deriving (Read, Show, Eq, Ord)

data Expr = Expr :&&: Expr -- Bool
          | Expr :||: Expr
          | NotE Expr
          | Expr :=: Expr
          | Leq0 Expr
          | IsEmptyE Expr
          | Expr :+: Expr -- Int
          | Expr :-: Expr
          | IncE Expr
          | DecE Expr
          | ZeroE
          | Div2E Expr
          | TailE Expr -- List
          | HeadE Expr
          | Expr :++: Expr -- cat 
          | Expr ::: Expr -- cons
          | EmptyListE
          | IsLeafE Expr -- Tree
          | TreeValE Expr
          | TreeLeftE Expr
          | TreeRightE Expr
          | CreateNodeE { nodeLeft :: Expr, nodeRoot :: Expr, nodeRight :: Expr }
          | CreateLeafE Expr
          | IfE { ifCond :: Expr, ifDoThen :: Expr, ifDoElse :: Expr }-- Control
          | SelfE [Expr]
          | InputE Int
          | Hole
    deriving (Read, Show, Eq, Ord)

data Value = BoolV Bool
           | IntV Int
           | ListV [Value]
           | TreeV (Tree Value)
    deriving (Read, Show, Eq, Ord)

data Type = BoolT
          | IntT
          | ListT Type
          | TreeT Type
          | AnyT
    deriving (Read, Show, Eq, Ord)

data TypeConf = TypeConf { typeConfInput  :: [Type],
                           typeConfOutput :: Type }

data Result a = Result a
              | NewExamples [([Value], Value)]
              | RecError String
              | FatalError String
    deriving (Read, Show, Eq)

instance Applicative Result where
  Result f <*> Result x = Result $ f x
  NewExamples es <*> NewExamples es' = NewExamples $ es ++ es'
  RecError err <*> _ = RecError err
  _ <*> RecError err = RecError err
  FatalError err <*> _ = FatalError err
  _ <*> FatalError err = FatalError err
  NewExamples es <*> _ = NewExamples es
  _ <*> NewExamples es = NewExamples es
  pure = Result

-- m1 <*> m2 = m1 >>= (\x1 -> m2 >>= (\x2 -> return (x1 x2)))
instance Monad Result where
  Result x >>= f = f x
  NewExamples es >>= _ = NewExamples es
  RecError err >>= _ = RecError err
  FatalError err >>= _ = FatalError err
  return = pure

instance Alternative Result where
  empty = undefined -- TMP: no guards used -- FatalError "empty"  -- TODO: rec ?
  RecError err <|> y = y
  FatalError err <|> y = y
  NewExamples es <|> _ = NewExamples es
  r@(Result x) <|> _ = r

instance Functor Result where
  fmap = liftM

instance MonadFail Result where
  fail _ = RecError "failure" -- TODO: fatal ?

-- instance (Foldable expr) ??

-- TODO: check all laws

------------

isResult (Result {}) = True
isResult _ = False
isNewExamples (NewExamples {}) = True
isNewExamples _ = False
isRecError (RecError {}) = True
isRecError _ = False
isFatalError (FatalError {}) = True
isFatalError _ = False

treeHeight :: Tree a -> Int
treeHeight (TLeaf {}) = 1
treeHeight TNode { treeLeft, treeRoot, treeRight } = 1 + (max (treeHeight treeLeft) (treeHeight treeRight) :: Int)