mirror of
https://codeberg.org/ProgramSnail/prog_synthesis.git
synced 2025-12-05 21:18:42 +00:00
02: use one expr type
This commit is contained in:
parent
597f34e709
commit
5e7729e4ac
1 changed files with 62 additions and 41 deletions
103
02.hs
103
02.hs
|
|
@ -3,35 +3,45 @@ import Data.Maybe (isJust)
|
|||
|
||||
infixl 4 :+:
|
||||
|
||||
data IntExpr = Zero
|
||||
| Succ IntExpr
|
||||
| Len ListExpr
|
||||
| FirstZero ListExpr
|
||||
data Expr = Zero
|
||||
| Succ Expr
|
||||
| Len Expr
|
||||
| FirstZero Expr
|
||||
| Sort Expr
|
||||
| SubList Expr Expr Expr
|
||||
| Expr :+: Expr
|
||||
| Recursive Expr
|
||||
| ZeroList
|
||||
| InList
|
||||
deriving (Read, Show, Eq)
|
||||
|
||||
data ListExpr = Sort ListExpr
|
||||
| SubList ListExpr IntExpr IntExpr
|
||||
| ListExpr :+: ListExpr
|
||||
| Recursive ListExpr
|
||||
| ZeroList
|
||||
| InList
|
||||
data Type = IntT | ListT
|
||||
deriving (Read, Show, Eq)
|
||||
data Value = IntV Int | ListV [Int]
|
||||
deriving (Read, Show, Eq)
|
||||
|
||||
data Env = Env {input :: [Int], prog :: ListExpr, steps :: Int}
|
||||
typeOf :: Expr -> Type
|
||||
typeOf Zero = IntT
|
||||
typeOf (Succ {}) = IntT
|
||||
typeOf (Len {}) = IntT
|
||||
typeOf (FirstZero {}) = IntT
|
||||
typeOf _ = ListT
|
||||
|
||||
data Env = Env {input :: [Int], prog :: Expr, steps :: Int}
|
||||
|
||||
stepInEnv :: Env -> Env
|
||||
stepInEnv env@(Env {input, prog, steps}) = env { steps = steps - 1 }
|
||||
|
||||
execInt :: Env -> IntExpr -> Maybe Int
|
||||
execInt :: Env -> Expr -> Maybe Int
|
||||
execInt (Env {input, prog, steps=0}) _ = Nothing
|
||||
execInt _ Zero = Just 0
|
||||
execInt env (Succ expr) = (+) 1 <$> execInt (stepInEnv env) expr
|
||||
execInt env (Len listExpr) = length <$> execList (stepInEnv env) listExpr
|
||||
execInt env (FirstZero listExpr) = do value <- execList (stepInEnv env) listExpr
|
||||
0 `elemIndex` value
|
||||
execInt _ _ = Nothing
|
||||
|
||||
-- TODO: limit execution steps
|
||||
execList :: Env -> ListExpr -> Maybe [Int]
|
||||
execList :: Env -> Expr -> Maybe [Int]
|
||||
execList (Env {input, prog, steps=0}) _ = Nothing
|
||||
execList env (Sort listExpr) = sort <$> execList (stepInEnv env) listExpr
|
||||
execList env (SubList listExpr exprFrom exprTo) = do valFrom <- execInt (stepInEnv env) exprFrom
|
||||
|
|
@ -45,51 +55,62 @@ execList env (Recursive listExpr) = do listValue <- execList (stepInEnv env) lis
|
|||
if null listValue then Just [] else execList (stepInEnv $ env {input = listValue}) (prog env)
|
||||
execList _ ZeroList = Just [0]
|
||||
execList (Env {input, prog, steps}) InList = Just input
|
||||
execList _ _ = Nothing
|
||||
|
||||
execProg :: [Int] -> ListExpr -> Maybe [Int]
|
||||
-- TODO: union
|
||||
execProg :: [Int] -> Expr -> Maybe [Int]
|
||||
execProg input expr = execList (Env {input, prog=expr, steps=20}) expr
|
||||
|
||||
data AllExprs = AllExprs {ints :: [IntExpr], lists :: [ListExpr]}
|
||||
deriving (Read, Show, Eq)
|
||||
terminals :: [Expr]
|
||||
terminals = [Zero, ZeroList, InList]
|
||||
|
||||
terminals :: AllExprs
|
||||
terminals = AllExprs {ints = [Zero], lists = [ZeroList, InList]}
|
||||
concatShuffle :: [[Expr]] -> [Expr]
|
||||
concatShuffle xxs = let xxs' = filter (not . null) xxs in
|
||||
if null xxs' then [] else
|
||||
map head xxs' ++ concatShuffle (map tail xxs')
|
||||
|
||||
nextExprs :: AllExprs -> AllExprs
|
||||
nextExprs (AllExprs {ints, lists}) = AllExprs {ints = map Succ ints ++ map Len lists ++ map FirstZero lists ++ ints,
|
||||
lists = map Sort lists ++
|
||||
[SubList list from to | list <- lists, from <- ints, to <- ints] ++
|
||||
[left :+: right | left <- lists, right <- lists] ++
|
||||
map Recursive lists ++
|
||||
lists}
|
||||
nextExprs :: [Expr] -> [Expr]
|
||||
nextExprs exprs = concatShuffle $ [exprs]
|
||||
++ [[Succ e | e <- exprs, typeOf e == IntT]]
|
||||
++ [[Sort e, Recursive e, FirstZero e, Len e] | e <- exprs, typeOf e == ListT]
|
||||
++ [[e :+: e' |
|
||||
e <- exprs, typeOf e == ListT,
|
||||
e' <- exprs, typeOf e' == ListT]]
|
||||
++ [[SubList InList from to |
|
||||
-- e <- exprs, typeOf e == ListT,
|
||||
from <- exprs, typeOf from == IntT,
|
||||
to <- exprs, typeOf to == IntT]]
|
||||
|
||||
data Example = Example {exampleInput :: [Int], exampleOutput :: [Int]}
|
||||
|
||||
-- check expr on all examples
|
||||
isCorrect :: [Example] -> ListExpr -> Bool
|
||||
isCorrect :: [Example] -> Expr -> Bool
|
||||
isCorrect examples expr = all (\Example {exampleInput, exampleOutput} -> execProg exampleInput expr == Just exampleOutput) examples
|
||||
|
||||
isValid :: [Example] -> ListExpr -> Bool
|
||||
isValid examples expr = all (\Example {exampleInput, exampleOutput} -> isJust $ execProg exampleInput expr) examples
|
||||
isValid :: [Example] -> Expr -> Bool
|
||||
isValid examples expr | typeOf expr == IntT = True
|
||||
| otherwise = all (\Example {exampleInput, exampleOutput} -> isJust $ execProg exampleInput expr) examples
|
||||
|
||||
-- check are exprs produce same results on all the examples
|
||||
areSame :: [Example] -> ListExpr -> ListExpr -> Bool
|
||||
areSame examples exprLeft exprRight = all (\Example {exampleInput, exampleOutput} -> execProg exampleInput exprLeft == execProg exampleInput exprRight ) examples
|
||||
areSame :: [Example] -> Expr -> Expr -> Bool
|
||||
areSame examples exprLeft exprRight | typeOf exprLeft == IntT = False
|
||||
| typeOf exprRight == IntT = False
|
||||
| otherwise = all (\Example {exampleInput, exampleOutput} -> execProg exampleInput exprLeft == execProg exampleInput exprRight ) examples
|
||||
|
||||
upSyntesisStep :: [Example] -> AllExprs -> Either AllExprs ListExpr
|
||||
upSyntesisStep examples allExprs@(AllExprs {ints, lists}) = let lists' = filter (isValid examples) lists in -- exclude invalid fragments
|
||||
let lists'' = foldl (\acc expr -> if any (areSame examples expr) acc then acc else expr : acc) [] lists' in -- merge same values
|
||||
case find (isCorrect examples) lists'' of
|
||||
Just answer -> Right answer
|
||||
Nothing -> Left $ nextExprs allExprs{lists=lists''}
|
||||
upSyntesisStep :: [Example] -> [Expr] -> Either [Expr] Expr
|
||||
upSyntesisStep examples exprs = let exprs' = filter (isValid examples) exprs in -- exclude invalid fragments
|
||||
let exprs'' = foldl (\acc expr -> if any (areSame examples expr) acc then acc else expr : acc) [] exprs' in -- merge same values
|
||||
case find (isCorrect examples) exprs'' of
|
||||
Just answer -> Right answer
|
||||
Nothing -> Left $ nextExprs exprs''
|
||||
|
||||
upSyntesisRec :: [Example] -> Int -> AllExprs -> Maybe ListExpr
|
||||
upSyntesisRec :: [Example] -> Int -> [Expr] -> Maybe Expr
|
||||
upSyntesisRec _ 0 _ = Nothing
|
||||
upSyntesisRec examples steps exprs = case upSyntesisStep examples exprs of
|
||||
Right answer -> Just answer
|
||||
Left exprs' -> upSyntesisRec examples (steps - 1) exprs'
|
||||
|
||||
upSyntesis :: [Example] -> Int -> Maybe ListExpr
|
||||
upSyntesis :: [Example] -> Int -> Maybe Expr
|
||||
upSyntesis examples steps = upSyntesisRec examples steps terminals
|
||||
|
||||
-----
|
||||
|
|
@ -97,9 +118,9 @@ upSyntesis examples steps = upSyntesisRec examples steps terminals
|
|||
exampleOf :: [Int] -> [Int] -> Example
|
||||
exampleOf input output = Example {exampleInput = input, exampleOutput = output}
|
||||
|
||||
-- InList
|
||||
sameExamplesExpected = InList
|
||||
sameExamples = [exampleOf [1] [1], exampleOf [1,2] [1,2], exampleOf [1,2,3] [1,2,3], exampleOf [1,2,3,4] [1,2,3,4]]
|
||||
-- (Recursive $ SubList InList (Suc Zero) (Len InList)) :+: (SubList InList Zero Zero)
|
||||
revExamplesExpected = Recursive (SubList InList (Succ Zero) (Len InList)) :+: SubList InList Zero Zero
|
||||
revExamples = [exampleOf [1] [1], exampleOf [1,2] [2,1], exampleOf [1,2,3] [3,2,1], exampleOf [1,2,3,4] [4,3,2,1]]
|
||||
|
||||
main = print $ upSyntesis revExamples 5
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue