Skip to content
David Young edited this page Jun 25, 2022 · 38 revisions

Main pages

Summary of functional specs status

(summarized from here)

Symbol Meaning
:heavy_check_mark: Synthesizes apparently correct code
:x: Does not synthesize
:grey_question: Synthesizes "incorrect" code
:large_orange_diamond: Partially working
N/A See notes

In the directory examples/functional-specs

Name Status Notes Haskell
append.sus :heavy_check_mark: ([1,2,3], [10,100,1000]) :arrow_right: [1,2,3,10,100,1000] xs ++ ys
concat.sus :heavy_check_mark: Flatten a list of lists into a list concat xs
cons_map.syn :grey_question: (-23, [[1,2,3], [4,5,6]]) :arrow_right: [[-23,1,2,3],[-23,4,5,6]] map (x:)
filter.sus :x: filter (>7) xs
fold.sus :heavy_check_mark: (can only produce a single int) [1,2,3] :arrow_right: 6 foldr (+) 0 xs
foldMap.sus :heavy_check_mark: [1,2,3] :arrow_right: 12 foldr (+) 0 (map (*2) xs)
foldScanr.sus :heavy_check_mark: Demonstration of composition sum (scanr (+) 0 xss)
intToNat.sus N/A Spec not yet done (ints to unary naturals) replicate n 0
map-times2.sus :heavy_check_mark: The code is partially given in the file. Synthesis fills in the hole map (*2)
map-sum.syn :heavy_check_mark: [[1,2], [3,4]] :arrow_right: [3, 7] map sum xss
map_single.sus :heavy_check_mark: [1, 2, 3] :arrow_right: [[1], [2], [3]] map (:[]) xs
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: Demonstration of composition maximum (map sum xss)
min_height.sus N/A Spec not yet done
mkSingletonList.sus :heavy_check_mark: 7 :arrow_right: [7] x : []
natToInt.sus :heavy_check_mark: "Unary naturals" to int (essentially a length function, using foldI) length xs
replicate.sus :x: 4 :arrow_right: [7, 7, 7, 7] replicate n 7
running_sum.sus :large_orange_diamond: Demonstrates scanr which partially working (see this issue) scanr (+) 0 xs
self_append.syn :x: [1,2,3] :arrow_right: [1,2,3,1,2,3] xs ++ xs
spatial_append.syn :heavy_check_mark: xs ++ ys
subseq.sus :x: Uses subseq_of predicate. [1,2,3,4] :arrow_right: [[1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[]] foldr (\x xss -> map (x:) ++ xss) [[]]
take.syn :grey_question: Synthesized code seems incorrect take n xs
zero-le7.sus :heavy_check_mark: While this synthesizes something that is spec-correct, its behavior might be unexpected
zip.sus :x: ([1,2,3], [10,100,1000]) :arrow_right: [[1,10], [2,100], [3,100]] zip xs ys
zipWith_add.sus :x: ([1,2,3], [10,100,1000]) :arrow_right: [11, 102, 1003] zipWith (+) xs ys

Structure of "fun-SuSLik" and the intermediate language

Intermediate language

top-level ::= ε | def top-level | ty-decl top-level
n ::= 0 | 1 | 2 | ...
e ::= n | v | let v = e in e | e e | e op e | comb
op ::= + | * | . | ...
args ::= ε | v args
def ::= v args := e | v args := ??
ty-decl ::= v : ty

where the . operator is function composition and comb is the list of combinators and primitives (TODO: Organize):

foldr : (a -> b -> b) -> b -> List a -> b
scanr : (a -> b -> b) -> b -> List a -> List b
map : Functor f => (a -> b) -> f a -> f b
(::) : a -> List a -> List a
[] : List a
fst : Pair a b -> a
snd : Pair a b -> b
pair : a -> b -> Pair a b
dup : a -> Pair a a
swap : Pair a b -> Pair b a
unmaybe : Maybe a -> a -> a
Just : a -> Maybe a
Nothing : Maybe a
uncons : List a -> Maybe (Pair a (List a))
True : Bool
False : Bool
ifThenElse : Bool -> a -> a -> a

Examples translated to "fun-SuSLik"

Status Haskell fun-SuSLik
:book: xs ++ ys foldr (::) xs ys
:book: concat xs foldr (++) [] xs
:book: filter (>7) xs foldr (\x acc -> ifThenElse (x > 7) (x :: acc) acc) [] xs
:book: sum xs foldr (+) 0 xs