Home - roboguy13/suslik GitHub Wiki
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](/roboguy13/suslik/wiki/1,2,3],-[4,5,6)) :arrow_right: [-23,1,2,3],[-23,4,5,6](/roboguy13/suslik/wiki/-23,1,2,3],[-23,4,5,6) |
map (x:) |
filter.sus |
:heavy_check_mark: | Limitation: AbduceBranch only generates the conditions where both lhs and rhs are variables. | 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](/roboguy13/suslik/wiki/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](/roboguy13/suslik/wiki/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 |
:heavy_check_mark: | 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 |
:heavy_check_mark: | Uses subseq_of predicate. [1,2,3,4] :arrow_right: [1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[]] ](/roboguy13/suslik/wiki/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 |
:heavy_check_mark: | ([1,2,3], [10,100,1000]) :arrow_right: [1,10], [2,100], [3,100](/roboguy13/suslik/wiki/1,10],-[2,100],-[3,100) |
zip xs ys |
zipWith_add.sus |
:heavy_check_mark: | ([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 | Spec |
|---|---|---|---|
| :book: :large_orange_diamond: | xs ++ ys |
foldr cons ys xs |
foldr f e (app xs ys) = foldr f (foldr f e ys) xs |
| :book: :large_orange_diamond: | map sum |
map sum |
... |
| :book: :large_orange_diamond: | reverse |
... | rev (append xs ys) = append (rev ys) (rev xs) & rev (rev xs) = xs |
| :book: :large_orange_diamond: | sort |
... | (srt . srt) = srt & srt = flatten . mkTree |
| :book: :large_orange_diamond: | subseqs |
foldr (\x xss -> append (map (cons x) xss) xss) [](/roboguy13/suslik/wiki/) |
implies (ifElemThenBefore x y zs) (all (ifElemThenBefore x y) (subseqs zs)) |
| :book: | concat xs |
foldr append [] xs |
|
| :book: | filter (>7) xs |
foldr (\x acc -> ifThenElse (x > 7) (x :: acc) acc) [] xs |
|
| :book: | sum xs |
foldr (+) 0 xs |