mirror of
https://codeberg.org/ProgramSnail/prog_synthesis.git
synced 2025-12-06 21:48:43 +00:00
fix types, delete old escher
This commit is contained in:
ProgramSnail
parent
753ca23cbc
commit
f27f6c5559
2 changed files with 17 additions and 754 deletions
741
escher.hs
741
escher.hs
|
|
@ -1,741 +0,0 @@
|
||||||
-- NOTE: it will be important to remove gets on caching addition
|
|
||||||
|
|
||||||
import Control.Monad (guard, liftM, when, unless, foldM, foldM_)
|
|
||||||
import Control.Applicative
|
|
||||||
import Control.Monad.State as State
|
|
||||||
import Data.Map (Map)
|
|
||||||
import Data.Set (Set)
|
|
||||||
import qualified Data.Map as Map
|
|
||||||
import qualified Data.Set as Set
|
|
||||||
import Data.List (inits)
|
|
||||||
import Data.Maybe (fromMaybe, isJust, maybeToList)
|
|
||||||
|
|
||||||
import Debug.Trace (trace)
|
|
||||||
|
|
||||||
data Value = BoolV Bool
|
|
||||||
| IntV Int
|
|
||||||
| ListV [Value]
|
|
||||||
| TreeV (Tree Value)
|
|
||||||
deriving (Read, Show, Eq, Ord)
|
|
||||||
|
|
||||||
data Tree a = TNode { treeLeft :: Tree a, treeRoot :: a, treeRight :: Tree a }
|
|
||||||
| TLeaf a
|
|
||||||
deriving (Read, Show, Eq, Ord)
|
|
||||||
|
|
||||||
data Type = BoolT
|
|
||||||
| IntT
|
|
||||||
| ListT Type
|
|
||||||
| TreeT Type
|
|
||||||
| AnyT
|
|
||||||
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 Conf = Conf {confInput :: [Value],
|
|
||||||
confOracle :: Oracle,
|
|
||||||
confExamples :: [[Value]]}
|
|
||||||
|
|
||||||
------------
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
------------
|
|
||||||
|
|
||||||
typeOf :: Value -> Type
|
|
||||||
typeOf (BoolV {}) = BoolT
|
|
||||||
typeOf (IntV {}) = IntT
|
|
||||||
typeOf (ListV (v : _)) = ListT $ typeOf v
|
|
||||||
typeOf (ListV []) = ListT AnyT
|
|
||||||
typeOf (TreeV (TNode { treeLeft, treeRoot, treeRight })) = TreeT $ typeOf treeRoot
|
|
||||||
typeOf (TreeV (TLeaf v)) = TreeT $ typeOf v
|
|
||||||
|
|
||||||
isBool = (== BoolT) . typeOf
|
|
||||||
isInt = (== IntT) . typeOf
|
|
||||||
isList x | ListT {} <- typeOf x = True
|
|
||||||
| otherwise = False
|
|
||||||
isTree x | TreeT {} <- typeOf x = True
|
|
||||||
| otherwise = False
|
|
||||||
|
|
||||||
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)
|
|
||||||
|
|
||||||
-- TODO: check
|
|
||||||
structuralLess :: Value -> Value -> Bool
|
|
||||||
structuralLess (BoolV left) (BoolV right) = not left && right
|
|
||||||
structuralLess (IntV left) (IntV right) = left < right && left > 0 -- ??
|
|
||||||
-- TODO: require same elems ?
|
|
||||||
structuralLess (ListV left) (ListV right) = length left < length right
|
|
||||||
-- TODO: require subtree ?
|
|
||||||
structuralLess (TreeV left) (TreeV right) = treeHeight left < treeHeight right
|
|
||||||
structuralLess _ _ = False
|
|
||||||
|
|
||||||
eval :: Conf -> Expr -> Result 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 e
|
|
||||||
return $ BoolV $ not b
|
|
||||||
eval conf (left :=: right) = do leftV <- eval conf left
|
|
||||||
rightV <- eval conf right
|
|
||||||
return $ BoolV $ leftV == rightV
|
|
||||||
eval conf (Leq0 e) = do IntV i <- eval conf e
|
|
||||||
return $ BoolV $ i <= 0
|
|
||||||
eval conf (IsEmptyE e) = do v <- eval conf e
|
|
||||||
case v of
|
|
||||||
ListV [] -> return $ BoolV True
|
|
||||||
ListV _ -> return $ BoolV False
|
|
||||||
_ -> FatalError $ "Can't take empty not from list" ++ show v
|
|
||||||
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 = return $ 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 = return $ 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 es) = do recInput <- foldM (\es e -> consValsM es (eval conf e)) [] es
|
|
||||||
-- NOTE: replaced guards for better errors description
|
|
||||||
-- guard $ length newInput == length (confInput conf)
|
|
||||||
-- guard $ and $ zipWith structuralLess newInput (confInput conf)
|
|
||||||
if length recInput /= length (confInput conf)
|
|
||||||
then FatalError $ "self call different length, new=" ++ show recInput ++ " old=" ++ show (confInput conf) -- TODO: fatal ?
|
|
||||||
else do
|
|
||||||
if not $ and $ zipWith structuralLess recInput (confInput conf)
|
|
||||||
then RecError $ "self call on >= exprs, new=" ++ show recInput ++ " old=" ++ show (confInput conf)
|
|
||||||
else do
|
|
||||||
case confOracle conf recInput of
|
|
||||||
Just recOutput -> if recInput `elem` confExamples conf
|
|
||||||
then return recOutput
|
|
||||||
else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)]
|
|
||||||
Nothing -> FatalError $ "no oracle output on " ++ show recInput
|
|
||||||
where consValsM :: [Value] -> Result Value -> Result [Value]
|
|
||||||
consValsM vs (Result v) = Result $ v : vs
|
|
||||||
consValsM _ (FatalError err) = FatalError err
|
|
||||||
consValsM _ (RecError err) = RecError err
|
|
||||||
consValsM _ (NewExamples ex) = NewExamples ex
|
|
||||||
eval conf (InputE i) = do if i < 0 || i >= length (confInput conf) -- NOTE: replaced guard for better errors description
|
|
||||||
then FatalError $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i -- TODO: fatal ?
|
|
||||||
else return $ confInput conf !! i -- use !? instead (?)
|
|
||||||
eval _ Hole = FatalError "can't eval hole"
|
|
||||||
|
|
||||||
data TypeConf = TypeConf { typeConfInput :: [Type],
|
|
||||||
typeConfOutput :: Type }
|
|
||||||
|
|
||||||
checkType :: TypeConf -> Expr -> Maybe Type
|
|
||||||
checkType conf (left :&&: right) = do BoolT <- checkType conf left
|
|
||||||
BoolT <- checkType conf right
|
|
||||||
return BoolT
|
|
||||||
checkType conf (left :||: right) = do BoolT <- checkType conf left
|
|
||||||
BoolT <- checkType conf right
|
|
||||||
return BoolT
|
|
||||||
checkType conf (NotE e) = do BoolT <- checkType conf e
|
|
||||||
return BoolT
|
|
||||||
checkType conf (left :=: right) = do leftT <- checkType conf left
|
|
||||||
rightT <- checkType conf right
|
|
||||||
guard $ leftT == rightT
|
|
||||||
return BoolT
|
|
||||||
checkType conf (Leq0 e) = do IntT <- checkType conf e
|
|
||||||
return BoolT
|
|
||||||
checkType conf (IsEmptyE e) = do ListT _ <- checkType conf e
|
|
||||||
return BoolT
|
|
||||||
checkType conf (left :+: right) = do IntT <- checkType conf left
|
|
||||||
IntT <- checkType conf right
|
|
||||||
return IntT
|
|
||||||
checkType conf (left :-: right) = do IntT <- checkType conf left
|
|
||||||
IntT <- checkType conf right
|
|
||||||
return IntT
|
|
||||||
checkType conf (IncE e) = do IntT <- checkType conf e
|
|
||||||
return IntT
|
|
||||||
checkType conf (DecE e) = do IntT <- checkType conf e
|
|
||||||
return IntT
|
|
||||||
checkType conf ZeroE = return IntT
|
|
||||||
checkType conf (Div2E e) = do IntT <- checkType conf e
|
|
||||||
return IntT
|
|
||||||
checkType conf (TailE e) = do ListT t <- checkType conf e
|
|
||||||
return $ ListT t
|
|
||||||
checkType conf (HeadE e) = do ListT t <- checkType conf e
|
|
||||||
return t
|
|
||||||
checkType conf (left :++: right) = do ListT t <- checkType conf left
|
|
||||||
ListT u <- checkType conf right
|
|
||||||
guard $ t == u
|
|
||||||
return $ ListT t
|
|
||||||
checkType conf (left ::: right) = do t <- checkType conf left
|
|
||||||
ListT u <- checkType conf right
|
|
||||||
guard $ t == u
|
|
||||||
return $ ListT t
|
|
||||||
checkType conf EmptyListE = return $ ListT AnyT -- TODO
|
|
||||||
checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e
|
|
||||||
return BoolT
|
|
||||||
checkType conf (TreeValE e) = do TreeT t <- checkType conf e
|
|
||||||
return t
|
|
||||||
checkType conf (TreeLeftE e) = do TreeT t <- checkType conf e
|
|
||||||
return $ TreeT t
|
|
||||||
checkType conf (TreeRightE e) = do TreeT t <- checkType conf e
|
|
||||||
return $ TreeT t
|
|
||||||
checkType conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeT t <- checkType conf nodeLeft
|
|
||||||
u <- checkType conf nodeRoot
|
|
||||||
guard $ t == u
|
|
||||||
TreeT w <- checkType conf nodeRight
|
|
||||||
guard $ t == w
|
|
||||||
return $ TreeT t
|
|
||||||
checkType conf (CreateLeafE e) = do t <- checkType conf e
|
|
||||||
return $ TreeT t
|
|
||||||
checkType conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolT <- checkType conf ifCond
|
|
||||||
leftT <- checkType conf ifDoThen
|
|
||||||
rightT <- checkType conf ifDoElse
|
|
||||||
guard $ leftT == rightT
|
|
||||||
return leftT
|
|
||||||
checkType conf (SelfE es) = do let ts = typeConfInput conf
|
|
||||||
guard $ length ts == length es
|
|
||||||
guard $ and $ zipWith (\t e -> checkType conf e == Just t) ts es
|
|
||||||
return $ typeConfOutput conf
|
|
||||||
checkType conf (InputE i) = Just $ typeConfInput conf !! i
|
|
||||||
checkType _ Hole = Nothing
|
|
||||||
-- checkType _ _ = Nothing
|
|
||||||
|
|
||||||
type Cache = Map Expr (Result Value)
|
|
||||||
|
|
||||||
eval' :: Cache -> Conf -> Expr -> (Result Value, Cache)
|
|
||||||
eval' cache conf expr = case expr `Map.lookup` cache of
|
|
||||||
Just result -> (result, cache)
|
|
||||||
Nothing -> let result = eval conf expr in
|
|
||||||
(result, Map.insert expr result cache)
|
|
||||||
|
|
||||||
eval'' :: Conf -> Expr -> SyntState (Result Value)
|
|
||||||
eval'' conf expr = do cache <- gets syntCache
|
|
||||||
let (result, cache') = eval' cache conf expr
|
|
||||||
modify $ \st -> st {syntCache = cache'}
|
|
||||||
return result
|
|
||||||
|
|
||||||
------------
|
|
||||||
|
|
||||||
type Oracle = [Value] -> Maybe Value
|
|
||||||
|
|
||||||
-- 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
|
|
||||||
fillHoles (InputE i) [] = InputE i
|
|
||||||
fillHoles _ _ = undefined
|
|
||||||
|
|
||||||
confBySynt :: [Value] -> Expr -> Synt -> Conf
|
|
||||||
confBySynt input expr st = Conf {confInput = input,
|
|
||||||
confOracle = syntOracle st,
|
|
||||||
confExamples = syntExamples st}
|
|
||||||
|
|
||||||
matchGoal :: Goal -> Expr -> Synt -> Bool
|
|
||||||
matchGoal (Goal goal) expr st = let examples = syntExamples st in
|
|
||||||
foldl checkOnInput True $ zip examples goal
|
|
||||||
where checkOnInput False _ = False
|
|
||||||
checkOnInput acc (input, output) = let output' = eval (confBySynt input expr st) expr in
|
|
||||||
matchValue output' output -- TODO
|
|
||||||
matchValue (Result x) (Just y) = x == y
|
|
||||||
matchValue _ Nothing = True
|
|
||||||
matchValue _ _ = False
|
|
||||||
|
|
||||||
------ syntesis steps
|
|
||||||
|
|
||||||
calcExprOutputs :: Expr -> SyntState [Result Value]
|
|
||||||
calcExprOutputs expr = gets (\st -> map (\input -> eval (confBySynt input expr st) expr) $ syntExamples st)
|
|
||||||
|
|
||||||
matchAnyOutputs :: [Result Value] -> SyntState Bool
|
|
||||||
matchAnyOutputs outputs = do exprs <- gets syntExprs
|
|
||||||
foldM step False $ map fst exprs
|
|
||||||
where step :: Bool -> Expr -> SyntState Bool
|
|
||||||
step True _ = return True
|
|
||||||
step False expr = do exprOutputs <- calcExprOutputs expr
|
|
||||||
return $ outputs == exprOutputs -- and $ zipWith sameResults outputs exprOutputs
|
|
||||||
sameResults (Result left) (Result right) = left == right
|
|
||||||
sameResults (RecError {}) (RecError {}) = True
|
|
||||||
sameResults _ _ = False
|
|
||||||
|
|
||||||
-- generate next step of exprs, remove copies
|
|
||||||
forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
|
|
||||||
forwardStep comp args = do let expr = fillHoles comp args
|
|
||||||
outputs <- calcExprOutputs expr
|
|
||||||
matchedExisting <- gets $ evalState (matchAnyOutputs outputs)
|
|
||||||
-- TODO: all RecErrors example could be useful on future cases ?
|
|
||||||
if any isFatalError outputs || all isRecError outputs || matchedExisting then return Nothing else do
|
|
||||||
modify $ \st -> st { syntExprs = (expr, []) : syntExprs st}
|
|
||||||
return $ Just expr
|
|
||||||
|
|
||||||
splitGoal :: Goal -> [Bool] -> Resolver
|
|
||||||
splitGoal resolverGoal@(Goal 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
|
|
||||||
Resolver { resolverGoal, resolverCond, resolverThen, resolverElse }
|
|
||||||
|
|
||||||
-- split goal by its index and by expr (if any answers matched), check if there is same goals to generated
|
|
||||||
splitGoalStep :: Goal -> [Bool] -> SyntState Resolver
|
|
||||||
splitGoalStep goal selector = do let r = splitGoal goal selector
|
|
||||||
resolvers <- gets syntResolvers
|
|
||||||
unless (r `elem` resolvers) $ -- do not add existing resolvers
|
|
||||||
modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $
|
|
||||||
Set.insert (resolverThen r) $
|
|
||||||
Set.insert (resolverElse r) $
|
|
||||||
syntUnsolvedGoals st,
|
|
||||||
syntResolvers = r : syntResolvers st } -- Set.insert
|
|
||||||
return r
|
|
||||||
|
|
||||||
-- TODO: use expr evaluated outputs ?
|
|
||||||
trySolveGoal :: Expr -> Goal -> SyntState Bool
|
|
||||||
trySolveGoal expr goal = do doesMatch <- gets $ matchGoal goal expr
|
|
||||||
if doesMatch then do
|
|
||||||
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st --,
|
|
||||||
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st
|
|
||||||
}
|
|
||||||
return True
|
|
||||||
-- trace ("goal solved: " ++ show goal) -- Tmp: trace
|
|
||||||
else return False
|
|
||||||
|
|
||||||
isGoalSolved :: Goal -> SyntState Bool
|
|
||||||
isGoalSolved goal = gets (Map.member goal . syntSolvedGoals)
|
|
||||||
|
|
||||||
goalSolution :: Goal -> SyntState (Maybe Expr)
|
|
||||||
goalSolution goal = gets (Map.lookup goal . syntSolvedGoals)
|
|
||||||
|
|
||||||
-- find all goals solved by new expr, by expr id it's values on examples, remove solved goals
|
|
||||||
-- returns found expr
|
|
||||||
-- NOTE: goals expected to be resolved
|
|
||||||
resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState Expr
|
|
||||||
-- resolveStep r _ | trace ("resolution: " ++ show r) False = undefined -- TMP: trace
|
|
||||||
resolveStep (ifCond, ifDoThen, ifDoElse) r = do let expr = IfE { ifCond, ifDoThen, ifDoElse }
|
|
||||||
let goal = resolverGoal r
|
|
||||||
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st,
|
|
||||||
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st,
|
|
||||||
syntExprs = (expr, []) : syntExprs st }
|
|
||||||
return expr
|
|
||||||
|
|
||||||
tryResolve :: Resolver -> SyntState (Maybe Expr)
|
|
||||||
-- tryResolve r | trace ("try resolution: " ++ show r) False = undefined -- TMP: trace
|
|
||||||
tryResolve r = do condSol <- goalSolution $ resolverCond r
|
|
||||||
thenSol <- goalSolution $ resolverThen r
|
|
||||||
elseSol <- goalSolution $ resolverElse r
|
|
||||||
case (condSol, thenSol, elseSol) of
|
|
||||||
(Just condExpr, Just thenExpr, Just elseExpr) -> do
|
|
||||||
expr <- resolveStep (condExpr, thenExpr, elseExpr) r
|
|
||||||
return $ Just expr
|
|
||||||
_ -> return Nothing
|
|
||||||
|
|
||||||
remakeSynt :: [[Value]] -> [Value] -> SyntState ()
|
|
||||||
remakeSynt newInputs newOutputs = do st <- get
|
|
||||||
let Goal oldOutputs = syntRoot st
|
|
||||||
goals <- gets $ \st -> zip (newInputs ++ syntExamples st)
|
|
||||||
(newOutputs ++ map (fromMaybe undefined) oldOutputs)
|
|
||||||
initSynt (syntOracle st) goals
|
|
||||||
modify (\st' -> st' { syntExprs = syntExprs st })
|
|
||||||
|
|
||||||
-- clear goal tree up to root, add example, calculate exprs on input (could be recursive ?)
|
|
||||||
-- returns new example
|
|
||||||
saturateStep :: Expr -> SyntState [[Value]]
|
|
||||||
saturateStep expr = do (newInputs, newOutputs) <- gets $ \st -> unzip $ foldl (searchEx st) [] (syntExamples st)
|
|
||||||
let exFound = not . null $ newInputs
|
|
||||||
when exFound $ remakeSynt newInputs newOutputs
|
|
||||||
return newInputs
|
|
||||||
where searchEx st [] input = case eval (confBySynt input expr st) expr of
|
|
||||||
NewExamples exs -> exs
|
|
||||||
_ -> []
|
|
||||||
searchEx _ exs _ = exs
|
|
||||||
|
|
||||||
-- try to find terminating expr
|
|
||||||
terminateStep :: Expr -> SyntState (Maybe Expr)
|
|
||||||
terminateStep expr = do doesMatch <- gets $ \st -> matchGoal (syntRoot st) expr st
|
|
||||||
return $ if doesMatch then Just expr else Nothing
|
|
||||||
|
|
||||||
------ 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],
|
|
||||||
InputE 0
|
|
||||||
]
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
stepOnAddedExpr :: Expr -> SyntState (Maybe Expr)
|
|
||||||
stepOnAddedExpr expr = do newEx <- saturateStep expr
|
|
||||||
if not . null $ newEx then do -- redo prev exprs (including current)
|
|
||||||
st <- get
|
|
||||||
-- trace ("exFound: " ++ show newEx) $ -- TMP: trace
|
|
||||||
stepOnAddedExprs $ map fst $ syntExprs st
|
|
||||||
else do -- try resolve goals & resolvers, generate new resolvers
|
|
||||||
maybeResult <- terminateStep expr
|
|
||||||
if isJust maybeResult then return maybeResult else do
|
|
||||||
exprOutputs <- calcExprOutputs expr
|
|
||||||
-- NOTE: now done in fowardStep
|
|
||||||
-- when (foldl (compareExprOutputs exprOutputs) True $ map fst $ syntExprs st) $ modify $ \st -> st { syntExprs = tail $ syntExprs st }
|
|
||||||
unsolvedGoals <- gets syntUnsolvedGoals
|
|
||||||
foldM_ (const $ trySolveGoal expr) False unsolvedGoals -- solve existing goals
|
|
||||||
resolvers <- gets syntResolvers
|
|
||||||
foldM_ (const tryResolve) Nothing resolvers -- resolve existing goals
|
|
||||||
modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st [syntRoot st] -- TODO: use Set.toList $ syntUnsolvedGoals st ?
|
|
||||||
gets $ \st -> syntRoot st `Map.lookup` syntSolvedGoals st
|
|
||||||
where splitGoalsFold expr outputs st goal@(Goal expected) = let matches = zipWith matchResult outputs expected in
|
|
||||||
if not $ any (fromMaybe False) matches then st else
|
|
||||||
let matchesBool = map (fromMaybe True) matches in
|
|
||||||
execState (do r <- splitGoalStep goal matchesBool
|
|
||||||
exprs <- gets syntExprs
|
|
||||||
foldM_ (const $ flip trySolveGoal $ resolverCond r) False $ map fst exprs
|
|
||||||
exprs <- gets syntExprs
|
|
||||||
foldM_ (const $ flip trySolveGoal $ resolverElse r) False $ map fst exprs
|
|
||||||
-- TODO: replace with always solve goal
|
|
||||||
trySolveGoal expr (resolverThen r)) st
|
|
||||||
matchResult :: Result Value -> Maybe Value -> Maybe Bool -- Nothing for unimportant matches marked as Nothing
|
|
||||||
matchResult (NewExamples {}) _ = Just False
|
|
||||||
matchResult _ Nothing = Nothing
|
|
||||||
matchResult (RecError {}) _ = Just False
|
|
||||||
matchResult (Result x) (Just y) = Just $ x == y
|
|
||||||
-- compareExprOutputs outputs False _ = False
|
|
||||||
-- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e
|
|
||||||
-- outputs == eOutputs
|
|
||||||
|
|
||||||
stepOnAddedExprs :: [Expr] -> SyntState (Maybe Expr)
|
|
||||||
stepOnAddedExprs = foldM step Nothing
|
|
||||||
where step :: Maybe Expr -> Expr -> SyntState (Maybe Expr)
|
|
||||||
step res@(Just {}) _ = return res
|
|
||||||
step Nothing expr = stepOnAddedExpr expr
|
|
||||||
|
|
||||||
-- returns result and valid expr
|
|
||||||
stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr, Maybe Expr)
|
|
||||||
stepOnNewExpr comp args = do expr <- forwardStep comp args
|
|
||||||
case expr of
|
|
||||||
Just expr' -> do res <- stepOnAddedExpr expr'
|
|
||||||
return (res, expr)
|
|
||||||
Nothing -> return (Nothing, Nothing)
|
|
||||||
|
|
||||||
-- stages:
|
|
||||||
-- init state
|
|
||||||
-- 1. gen new step exprs
|
|
||||||
-- 2. process exprs by one
|
|
||||||
-- 3. try terminate / saturate
|
|
||||||
-- 4. try to solve existing goals
|
|
||||||
-- 5. make resolutions if goals solved
|
|
||||||
-- 6. split goals, where expr partially matched
|
|
||||||
syntesisStep :: Int -> [[Expr]] -> SyntState (Maybe Expr)
|
|
||||||
syntesisStep 0 _ = return Nothing
|
|
||||||
syntesisStep steps prevExprs = -- oracle should be defined on the provided emample inputs
|
|
||||||
do let genExprs = genStep prevExprs
|
|
||||||
(result, validExprs) <- foldM step (Nothing, []) genExprs
|
|
||||||
if isJust result
|
|
||||||
then return result
|
|
||||||
else trace ("steps left: " ++ show (steps - 1)) $ syntesisStep (steps - 1) (validExprs : prevExprs)
|
|
||||||
where step res@(Just {}, _) _ = return res
|
|
||||||
step (Nothing, exprs) expr = do (res, val) <- uncurry stepOnNewExpr expr
|
|
||||||
return (res, maybeToList val ++ exprs)
|
|
||||||
|
|
||||||
syntesis' :: [[Expr]] -> Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
|
|
||||||
syntesis' exprs steps oracle inputs = -- oracle should be defined on the providid examples
|
|
||||||
let outputs = map (fromMaybe undefined . oracle) inputs in
|
|
||||||
runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs)
|
|
||||||
|
|
||||||
syntesis :: Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
|
|
||||||
syntesis = syntesis' []
|
|
||||||
|
|
||||||
------ examples
|
|
||||||
|
|
||||||
mainExamples :: [[Value]]
|
|
||||||
mainExamples = [[ListV [IntV 1, IntV 2, IntV 3]]]
|
|
||||||
|
|
||||||
allExamples :: [[Value]]
|
|
||||||
-- allExamples = [[ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]]
|
|
||||||
allExamples = [[ListV [IntV 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]]
|
|
||||||
|
|
||||||
--- reverse
|
|
||||||
|
|
||||||
reverseOracle :: Oracle
|
|
||||||
-- reverseOracle [ListV xs] = Just $ ListV $ reverse xs
|
|
||||||
reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs
|
|
||||||
reverseOracle _ = Nothing
|
|
||||||
|
|
||||||
reverseExpr :: Expr
|
|
||||||
reverseExpr = IfE { ifCond = IsEmptyE (InputE 0),
|
|
||||||
ifDoThen = EmptyListE,
|
|
||||||
ifDoElse = SelfE [TailE (InputE 0)] :++: (HeadE (InputE 0) ::: EmptyListE) }
|
|
||||||
|
|
||||||
reverseConf :: Conf
|
|
||||||
reverseConf = Conf { confInput = head allExamples,
|
|
||||||
confOracle = reverseOracle,
|
|
||||||
confExamples = allExamples }
|
|
||||||
|
|
||||||
--- stutter
|
|
||||||
|
|
||||||
stutterOracle :: Oracle
|
|
||||||
stutterOracle [ListV (x : xs)] | isInt x = do ListV xs' <- stutterOracle [ListV xs]
|
|
||||||
return $ ListV $ x : x : xs'
|
|
||||||
stutterOracle [ListV []] = Just $ ListV []
|
|
||||||
stutterOracle _ = Nothing
|
|
||||||
|
|
||||||
stutterExpr :: Expr
|
|
||||||
stutterExpr = IfE { ifCond = IsEmptyE (InputE 0),
|
|
||||||
ifDoThen = EmptyListE,
|
|
||||||
ifDoElse = HeadE (InputE 0) ::: (HeadE (InputE 0) ::: SelfE [TailE (InputE 0)]) }
|
|
||||||
|
|
||||||
stutterConf :: Conf
|
|
||||||
stutterConf = Conf { confInput = head allExamples,
|
|
||||||
confOracle = stutterOracle,
|
|
||||||
confExamples = allExamples }
|
|
||||||
|
|
||||||
--- length
|
|
||||||
|
|
||||||
lengthOracle :: Oracle
|
|
||||||
lengthOracle [ListV xs] = Just $ IntV $ length xs
|
|
||||||
lengthOracle _ = Nothing
|
|
||||||
|
|
||||||
lengthExpr :: Expr
|
|
||||||
lengthExpr = IfE { ifCond = IsEmptyE (InputE 0),
|
|
||||||
ifDoThen = ZeroE,
|
|
||||||
ifDoElse = IncE $ SelfE [TailE (InputE 0)] }
|
|
||||||
|
|
||||||
lengthConf :: Conf
|
|
||||||
lengthConf = Conf { confInput = head allExamples,
|
|
||||||
confOracle = lengthOracle,
|
|
||||||
confExamples = allExamples }
|
|
||||||
|
|
||||||
---
|
|
||||||
|
|
||||||
idOracle :: Oracle
|
|
||||||
idOracle [x] = Just x
|
|
||||||
idOracle _ = Nothing
|
|
||||||
|
|
||||||
main = do steps <- readLn :: IO Int
|
|
||||||
print $ fst $ syntesis steps reverseOracle allExamples
|
|
||||||
|
|
||||||
-- main = print $ (SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE)) `elem` (map fst $ syntExprs $ snd $ syntesis 10 reverseOracle allExamples)
|
|
||||||
-- Just (IfE {ifCond = IsEmptyE (InputE ZeroE), ifDoThen = InputE ZeroE :++: TailE (InputE ZeroE :++: (InputE ZeroE :++: (ZeroE ::: EmptyListE))), ifDoElse = SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE)})
|
|
||||||
|
|
@ -19,8 +19,11 @@ isTree x | TreeT {} <- typeOf x = True
|
||||||
| otherwise = False
|
| otherwise = False
|
||||||
|
|
||||||
simpleUnify :: Type -> Type -> Maybe Type
|
simpleUnify :: Type -> Type -> Maybe Type
|
||||||
|
simpleUnify t u | t == u = Just t
|
||||||
simpleUnify AnyT u = Just u
|
simpleUnify AnyT u = Just u
|
||||||
simpleUnify t AnyT = Just t
|
simpleUnify t AnyT = Just t
|
||||||
|
simpleUnify (ListT t) (ListT u) = ListT <$> simpleUnify t u
|
||||||
|
simpleUnify (TreeT t) (TreeT u) = TreeT <$> simpleUnify t u
|
||||||
simpleUnify _ _ = Nothing
|
simpleUnify _ _ = Nothing
|
||||||
|
|
||||||
checkType :: TypeConf -> Expr -> Maybe Type
|
checkType :: TypeConf -> Expr -> Maybe Type
|
||||||
|
|
@ -34,7 +37,7 @@ checkType conf (NotE e) = do BoolT <- checkType conf e
|
||||||
return BoolT
|
return BoolT
|
||||||
checkType conf (left :=: right) = do leftT <- checkType conf left
|
checkType conf (left :=: right) = do leftT <- checkType conf left
|
||||||
rightT <- checkType conf right
|
rightT <- checkType conf right
|
||||||
guard $ leftT == rightT
|
eqT <- simpleUnify leftT rightT
|
||||||
return BoolT
|
return BoolT
|
||||||
checkType conf (Leq0 e) = do IntT <- checkType conf e
|
checkType conf (Leq0 e) = do IntT <- checkType conf e
|
||||||
return BoolT
|
return BoolT
|
||||||
|
|
@ -63,12 +66,12 @@ checkType conf (HeadE e) = do ListT t <- checkType conf e
|
||||||
return t
|
return t
|
||||||
checkType conf (left :++: right) = do ListT t <- checkType conf left
|
checkType conf (left :++: right) = do ListT t <- checkType conf left
|
||||||
ListT u <- checkType conf right
|
ListT u <- checkType conf right
|
||||||
w <- simpleUnify t u
|
u' <- simpleUnify t u
|
||||||
return $ ListT w
|
return $ ListT u'
|
||||||
checkType conf (left ::: right) = do t <- checkType conf left
|
checkType conf (left ::: right) = do t <- checkType conf left
|
||||||
ListT u <- checkType conf right
|
ListT u <- checkType conf right
|
||||||
w <- simpleUnify t u
|
u' <- simpleUnify t u
|
||||||
return $ ListT w
|
return $ ListT u'
|
||||||
checkType conf EmptyListE = return $ ListT AnyT -- NOTE: ListT AnyT - type of generic empty list
|
checkType conf EmptyListE = return $ ListT AnyT -- NOTE: ListT AnyT - type of generic empty list
|
||||||
checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e
|
checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e
|
||||||
return BoolT
|
return BoolT
|
||||||
|
|
@ -80,19 +83,20 @@ checkType conf (TreeRightE e) = do TreeT t <- checkType conf e
|
||||||
return $ TreeT t
|
return $ TreeT t
|
||||||
checkType conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeT t <- checkType conf nodeLeft
|
checkType conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeT t <- checkType conf nodeLeft
|
||||||
u <- checkType conf nodeRoot
|
u <- checkType conf nodeRoot
|
||||||
guard $ t == u
|
u' <- simpleUnify t u
|
||||||
TreeT w <- checkType conf nodeRight
|
TreeT w <- checkType conf nodeRight
|
||||||
guard $ t == w
|
w' <- simpleUnify u' w
|
||||||
return $ TreeT t
|
return $ TreeT w'
|
||||||
checkType conf (CreateLeafE e) = do t <- checkType conf e
|
checkType conf (CreateLeafE e) = do t <- checkType conf e
|
||||||
return $ TreeT t
|
return $ TreeT t
|
||||||
checkType conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolT <- checkType conf ifCond
|
checkType conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolT <- checkType conf ifCond
|
||||||
leftT <- checkType conf ifDoThen
|
leftT <- checkType conf ifDoThen
|
||||||
rightT <- checkType conf ifDoElse
|
rightT <- checkType conf ifDoElse
|
||||||
guard $ leftT == rightT
|
simpleUnify leftT rightT
|
||||||
return leftT
|
|
||||||
checkType conf (SelfE es) = do let ts = typeConfInput conf
|
checkType conf (SelfE es) = do let ts = typeConfInput conf
|
||||||
guard $ length ts == length es
|
if length ts /= length es then error $ "Recursive call: not enough args, " ++
|
||||||
|
show es ++ " provided while "++
|
||||||
|
show ts ++ " are required" else do
|
||||||
guard $ and $ zipWith (\t e -> checkType conf e == Just t) ts es
|
guard $ and $ zipWith (\t e -> checkType conf e == Just t) ts es
|
||||||
return $ typeConfOutput conf
|
return $ typeConfOutput conf
|
||||||
checkType conf (InputE i) = Just $ typeConfInput conf !! i
|
checkType conf (InputE i) = Just $ typeConfInput conf !! i
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue