diff --git a/escher.hs b/escher.hs index aaf1011..df5a91f 100644 --- a/escher.hs +++ b/escher.hs @@ -1,3 +1,5 @@ +import Control.Monad (guard) + data Value = BoolV Bool | IntV Int | ListV [Value] @@ -34,8 +36,15 @@ data Expr = Expr :&&: Expr -- Bool | 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 @@ -47,55 +56,85 @@ isInt = (== IntT) . typeOf isList = (== ListT) . typeOf isTree = (== TreeT) . typeOf -eval :: Expr -> Maybe Value -eval (left :&&: right) = do BoolV leftB <- eval left - BoolV rightB <- eval right - return $ BoolV $ leftB && rightB -eval (left :||: right) = do BoolV leftB <- eval left - BoolV rightB <- eval right - return $ BoolV $ leftB || rightB -eval (NotE e) = do BoolV b <- eval e - return $ BoolV $ not b -eval (left :+: right) = do IntV leftI <- eval left - IntV rightI <- eval right - return $ IntV $ leftI + rightI -eval (left :-: right) = do IntV leftI <- eval left - IntV rightI <- eval right - return $ IntV $ leftI - rightI -eval (IncE e) = do IntV i <- eval e - return $ IntV $ i + 1 -eval (DecE e) = do IntV i <- eval e - return $ IntV $ i - 1 -eval ZeroE = Just $ IntV 0 -eval (Div2E e) = do IntV i <- eval e - return $ IntV $ i `div` 2 -eval (TailE e) = do ListV (_ : t) <- eval e - return $ ListV t -eval (HeadE e) = do ListV (h : _) <- eval e - return h -eval (left :++: right) = do ListV leftL <- eval left - ListV rightL <- eval right - return $ ListV $ leftL ++ rightL -eval (left ::: right) = do leftV <- eval left - ListV rightL <- eval right - return $ ListV $ leftV : rightL -eval EmptyListE = Just $ ListV [] -eval (IsLeafE e) = do TreeV t <- eval e - return $ BoolV $ case t of - TNode {} -> False - TLeaf {} -> True -eval (TreeValE e) = do TreeV t <- eval e - return $ case t of - n@TNode {} -> treeRoot n - TLeaf e -> e -eval (TreeLeftE e) = do TreeV n@(TNode {}) <- eval e - return $ TreeV $ treeLeft n -eval (TreeRightE e) = do TreeV n@(TNode {}) <- eval e - return $ TreeV $ treeRight n -eval (CreateNodeE { nodeLeft, nodeRoot, nodeRight }) = do TreeV treeLeft <- eval nodeLeft - treeRoot <- eval nodeRoot - TreeV treeRight <- eval nodeRight - return $ TreeV $ TNode { treeLeft, treeRoot, treeRight } -eval (CreateLeafE e) = do v <- eval e - return $ TreeV $ TLeaf v +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