prog_synthesis/escher/Syntesis.hs

module Syntesis where

import Expr
import Eval

import Control.Monad.State
import Data.Map.Lazy (Map)
import Data.Set (Set)
import Data.List (inits)
import qualified Data.Map.Lazy as Map
import qualified Data.Set as Set

-- bipartite graph, root is Goal
newtype Goal = Goal [Maybe Value] -- result or unimportant
  deriving (Read, Show, Eq, Ord)
-- Map sovled :: Goal -> Expr
-- Set unsolved
-- List Resolvers
data Resolver = Resolver { resolverGoal :: Goal,
                           resolverCond :: Goal,
                           resolverThen :: Goal,
                           resolverElse :: Goal } -- ids ??
  deriving (Read, Show, Eq, Ord)

data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])],
                   syntSolvedGoals :: Map Goal Expr,
                   syntUnsolvedGoals :: Set Goal,
                   syntResolvers :: [Resolver], -- Set Resolver,
                   syntExamples :: [[Value]],
                   syntOracle :: Oracle,
                   syntCache :: Cache,
                   syntRoot :: Goal}
type SyntState a = State Synt a


--fill holes in expr with top-level holes
fillHoles :: Expr -> [Expr] -> Expr
fillHoles (Hole :&&: Hole) [left, right] = left :&&: right
fillHoles (Hole :||: Hole) [left, right] = left :||: right
fillHoles (NotE Hole) [e] = NotE e
fillHoles (Hole :=: Hole) [left, right] = left :=: right
fillHoles (Leq0 Hole) [e] = Leq0 e
fillHoles (IsEmptyE Hole) [e] = IsEmptyE e
fillHoles (Hole :+: Hole) [left, right] = left :+: right
fillHoles (Hole :-: Hole) [left, right] = left :-: right
fillHoles (IncE Hole) [e] = IncE e
fillHoles (DecE Hole) [e] = DecE e
fillHoles ZeroE [] = ZeroE
fillHoles (Div2E Hole) [e] = Div2E e
fillHoles (TailE Hole) [e] = TailE e
fillHoles (HeadE Hole) [e] = HeadE e
fillHoles (Hole :++: Hole) [left, right] = left :++: right
fillHoles (Hole ::: Hole) [left, right] = left ::: right
fillHoles EmptyListE [] = EmptyListE
fillHoles (IsLeafE Hole) [e] = IsLeafE e
fillHoles (TreeValE Hole) [e] = TreeValE e
fillHoles (TreeLeftE Hole) [e] = TreeLeftE e
fillHoles (TreeRightE Hole) [e] = TreeRightE e
fillHoles (CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole})
          [nodeLeft, nodeRoot, nodeRight] = CreateNodeE {nodeLeft, nodeRoot, nodeRight}
fillHoles (CreateLeafE Hole) [e] = CreateLeafE e
fillHoles (IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole})
          [ifCond, ifDoThen, ifDoElse] = IfE {ifCond, ifDoThen, ifDoElse}
fillHoles (SelfE hs) es | all (== Hole) hs && length hs == length es = SelfE es
                        -- | otherwise = error $ show hs ++ show es
fillHoles (InputE i) [] = InputE i
fillHoles e es = error $ "Can't fill holes in " ++ show e ++ " with " ++ show es

confBySynt :: [Value] -> Expr -> Bool -> Synt -> Conf
confBySynt input expr newEx st = Conf {confInput = input,
                                       confOracle = syntOracle st,
                                       confExamples = syntExamples st,
                                       confTryFindExamples = newEx}


------ patterns

patterns0 :: [Expr]
patterns0 = [ZeroE, EmptyListE, InputE 0] -- TMP: NOTE: for faster search

patterns1 :: [Expr]
patterns1 = [NotE Hole, Leq0 Hole,
             IsEmptyE Hole, IncE Hole,
             DecE Hole, Div2E Hole,
             TailE Hole, HeadE Hole,
--             IsLeafE Hole, TreeValE Hole,
--             TreeLeftE Hole, TreeRightE Hole,
--             CreateLeafE Hole,
             SelfE [Hole]
            ]

patterns2 :: [Expr]
patterns2 = [Hole :&&: Hole,
             Hole :||: Hole,
             Hole :=: Hole,
             Hole :+: Hole,
             Hole :-: Hole,
             Hole :++: Hole,
             Hole ::: Hole]

patterns3 :: [Expr]
patterns3 = []
-- [CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole},
-- IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}]

------ generation

concatShuffle :: [[a]] -> [a]
concatShuffle xxs = let xxs' = filter (not . null) xxs in
                    if null xxs' then [] else
                    map head xxs' ++ concatShuffle (map tail xxs')

-- -> n, +1 for top expression
genNext1 :: [[Expr]] -> [Expr]
genNext1 = head

-- 1 2 3 ... (n - 1) + (n - 1) ... 1 -> n, +1 for top expression
genNext2 :: [[Expr]] -> [(Expr, Expr)]
genNext2 exprs = let len = length exprs in
                 let exprs' = tail exprs in
                 concatShuffle $
                 zipWith (\xs ys -> ([(x, y) | x <- xs, y <- ys])) exprs' $
                 reverse exprs'

-- map genNext2 [1, 1 2, 1 2 3, ..., 1 2 ... (n - 1)] + (n - 1) (n - 2) ... 1 -> n, +1 for top expression
genNext3 :: [[Expr]] -> [(Expr, Expr, Expr)]
genNext3 exprs = let exprs' = tail exprs in
                 let prefixes = map genNext2 $ tail $ inits exprs' in
                 let ends = reverse exprs' in
                 concatShuffle $
                 zipWith (\xys zs -> ([(x, y, z) | (x, y) <- xys, z <- zs])) prefixes ends

-- get list of patterns and holes for forward steps
genStep :: [[Expr]] -> [(Expr, [Expr])]
genStep [] = map (, []) patterns0
genStep xs = concatShuffle [[(p, [x]) | p <- patterns1, x <- genNext1 xs],
                            [(p, [x, y]) | p <- patterns2, (x, y) <- genNext2 xs],
                            [(p, [x, y, z]) | p <- patterns3, (x, y, z) <- genNext3 xs]]

------ algorithm

createSynt :: Oracle -> [([Value], Value)] -> Synt
createSynt oracle goals = let root = Goal $ map (Just . snd) goals in
                          Synt { syntExprs = [],
                                 syntSolvedGoals = Map.empty,
                                 syntUnsolvedGoals = Set.singleton root,
                                 syntResolvers = [], -- Set.empty
                                 syntExamples = map fst goals,
                                 syntOracle = oracle,
                                 syntCache = Map.empty, -- ??
                                 syntRoot = root}

initSynt :: Oracle -> [([Value], Value)] -> SyntState ()
initSynt oracle goals = put $ createSynt oracle goals