prog_synthesis/escher.hs

import Control.Monad (guard)

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

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

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

data Expr = Expr :&&: Expr -- Bool
          | Expr :||: Expr
          | NotE 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 Expr
    deriving (Read, Show, Eq)

data Conf = Conf { confInput :: [Value], confOracle :: [Value] -> Maybe Value, confProg :: Expr }

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

typeOf :: Value -> Type
typeOf (BoolV {}) = BoolT
typeOf (IntV {}) = IntT
typeOf (ListV {}) = ListT
typeOf (TreeV {}) = TreeT

isBool = (== BoolT) . typeOf
isInt = (== IntT) . typeOf
isList = (== ListT) . typeOf
isTree = (== TreeT) . typeOf

eval :: Conf -> Expr -> Maybe Value
eval conf (left :&&: right) = do BoolV leftB <- eval conf left
                                 BoolV rightB <- eval conf right
                                 return $ BoolV $ leftB && rightB
eval conf (left :||: right) = do BoolV leftB <- eval conf left
                                 BoolV rightB <- eval conf right
                                 return $ BoolV $ leftB || rightB
eval conf (NotE e) = do BoolV b <- eval conf conf e
                        return $ BoolV $ not b
eval conf (left :+: right) = do IntV leftI <- eval conf left
                                IntV rightI <- eval conf right
                                return $ IntV $ leftI + rightI
eval conf (left :-: right) = do IntV leftI <- eval conf left
                                IntV rightI <- eval conf right
                                return $ IntV $ leftI - rightI
eval conf (IncE e) = do IntV i <- eval conf e
                        return $ IntV $ i + 1
eval conf (DecE e) = do IntV i <- eval conf e
                        return $ IntV $ i - 1
eval conf ZeroE = Just $ IntV 0
eval conf (Div2E e) = do IntV i <- eval conf e
                         return $ IntV $ i `div` 2
eval conf (TailE e) = do ListV (_ : t) <- eval conf e
                         return $ ListV t
eval conf (HeadE e) = do ListV (h : _) <- eval conf e
                         return h
eval conf (left :++: right) = do ListV leftL <- eval conf left
                                 ListV rightL <- eval conf right
                                 return $ ListV $ leftL ++ rightL
eval conf (left ::: right) = do leftV <- eval conf left
                                ListV rightL <- eval conf right
                                return $ ListV $ leftV : rightL
eval conf EmptyListE = Just $ ListV []
eval conf (IsLeafE e) = do TreeV t <- eval conf e
                           return $ BoolV $ case t of
                             TNode {} ->  False
                             TLeaf {} -> True
eval conf (TreeValE e) = do TreeV t <- eval conf e
                            return $ case t of
                              n@TNode {}  -> treeRoot n
                              TLeaf e -> e
eval conf (TreeLeftE e) = do TreeV n@(TNode {}) <- eval conf e
                             return $ TreeV $ treeLeft n
eval conf (TreeRightE e) = do TreeV n@(TNode {}) <- eval conf e
                              return $ TreeV $ treeRight n
eval conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeV treeLeft <- eval conf nodeLeft
                                                             treeRoot <- eval conf nodeRoot
                                                             TreeV treeRight <- eval conf nodeRight
                                                             return $ TreeV $ TNode { treeLeft, treeRoot, treeRight }
eval conf (CreateLeafE e) = do v <- eval conf e
                               return $ TreeV $ TLeaf v
eval conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolV condB <- eval conf ifCond
                                                  if condB then eval conf ifDoThen else eval conf ifDoElse
eval conf (SelfE e) = do ListV newInput <- eval conf e
                         guard $ length newInput < length (confInput conf)
                         expectedV <- confOracle conf newInput -- TODO: add expected to Goal values list (if none), reset goal
                         eval conf{ confInput = newInput } (confProg conf)
eval conf (InputE e) = do IntV i <- eval conf e
                          guard $ i >= 0 && i < length (confInput conf)
                          return $ confInput conf !! i -- use !? instead (?)
-- eval _ = Nothing

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

-- bipartite graph, root is Goal
data Goal = Goal [Resolver] [Maybe Value]
data Resolver = Resolver { resolverCond :: Goal, resolverThen :: Goal, resolverElse :: Goal }

splitGoal :: Goal -> [Bool] -> Goal
splitGoal (Goal resolvers outputs) selector | length outputs == length selector =
  let resolverCond = Goal [] $ map (Just . BoolV) selector in
  let resolverThen = Goal [] $ zipWith (\v b -> if b then v else Nothing) outputs selector in
  let resolverElse = Goal [] $ zipWith (\v b -> if b then Nothing else v) outputs selector in
  let r = Resolver { resolverCond, resolverThen, resolverElse } in
  Goal (r : resolvers) outputs

-- Inputs - vector of values

-- forwardStep
-- resolveStep
-- splitGoalStep
-- saturateStep