Status of functional specs - roboguy13/suslik Wiki

Note: This could get out of sync with Home. First priority will go towards updating Home.

Symbol Meaning
:heavy_check_mark: Synthesizes apparently correct code
:x: Does not synthesize
:grey_question: Synthesizes "incorrect" code
:eight_spoked_asterisk: Example with an unusual aspect
:large_orange_diamond: Partially working
N/A See notes

In the directory examples/functional-specs

Name Status Notes Haskell
append.sus :heavy_check_mark: xs ++ ys
append_cons_map.syn :x:
concat.sus :heavy_check_mark: Flatten a list of lists into a list concat xs
cons_map.syn :heavy_check_mark: :grey_question: map (x:) map (x:)
div.sus :x: Filename should be updated
duplicate.syn :heavy_check_mark: (x, x)
filter.sus :x: filter (>7) xs
flatten_leaf_tree.sus :x:
flatten_leaf_tree.syn :x:
fold.sus :heavy_check_mark: fold list of ints into a single int foldr (+) 0 xs
foldMap.sus :heavy_check_mark: map and then fold over the resulting list using foldMap predicate foldr (+) 0 (map (*2) xs)
foldScanr.sus :heavy_check_mark: A demonstration of composition sum (scanr (+) 0 xss)
free_leaf_tree.syn :heavy_check_mark:
intToNat.sus N/A Spec not yet done (ints to unary naturals)
lookup.syn :x:
map-times2.sus :heavy_check_mark: :eight_spoked_asterisk: The code is partially given in the file. Synthesis fills in the hole map (*2)
map-sum.syn :heavy_check_mark: :grey_question: :eight_spoked_asterisk: map sum xss
maximum.syn :heavy_check_mark: maximum xs
maximum_map_sum.syn :grey_question: Synthesizes "incorrect" code (no summing) maximum (map sum xss)
maximum_map_sum_seq.sus :heavy_check_mark: Uses extra arguments as intermediate storage maximum (map sum xss)
min_height.sus :x:
mkSingletonList.sus :heavy_check_mark: x : []
natToInt.sus :heavy_check_mark: "Unary naturals" to int (essentially a length function, using foldI)
replicate.sus :x: replicate n 7
running_sum.sus :large_orange_diamond: Demonstrates scanr which partially working (see this issue) scanr (+) 0 xs
self_append.syn :x: xs ++ xs
spatial_append.syn :heavy_check_mark:
subseq.sus :x: This uses a subseq_of predicate
subseqs.sus N/A Specification incomplete
take.syn :grey_question: Synthesized code seems incorrect
unfold.sus N/A Currently used as a scratchpad
zero-le7.sus :heavy_check_mark: While this synthesizes something that is spec-correct, its behavior might be unexpected
zip.sus :x: