Synbit (Demo)
The system Synbit synthesizes bidirectional programs using unidirectional (i.e., "get") sketches. Interested readers may refer to
our OOPSLA 21 paper
and/or
its code repository in GitHub
.
"Get" definition (with components)
append :: ([a], [a]) -> [a] append l = let (l1, l2) = l in append_ l1 l2 append_ :: [a] -> [a] -> [a] append_ l1 l2 = case l1 of [] -> l2 x:xs -> x:append_ xs l2
Examples for "put"
-- Examples are given by variables starting with "ex". ex1 = (([1, 2, 3, 4], [5]), [6, 2], ([6, 2], [])) ex2 = (([1, 2, 3, 4], [5]), [1, 2, 3, 4, 5, 6], ([1, 2, 3, 4], [5, 6]))
Entrypoint function
Non-component functions (separated by comma; should include functions called from the entrypoint)