Include examples from various sources

[EmilyOng]

I have included several examples from: (more to come.)

Examples

Prusti Closure Examples

Summary

| Prusti | Heifer | |--------|--------| | [all](https://github.com/FabianWolff/closure-examples/blob/master/all.rs) | [src/prusti/all.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/all.ml) | | [any](https://github.com/FabianWolff/closure-examples/blob/master/any.rs) | [src/prusti/any.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/any.ml) | | [blameassgn](https://github.com/FabianWolff/closure-examples/blob/master/blameassgn.rs) | [src/prusti/blameassgn.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/blameassgn.ml) | | [cl_returned](https://github.com/FabianWolff/closure-examples/blob/master/cl_returned.rs) | [src/prusti/cl_returned.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/cl_returned.ml) | | [counter](https://github.com/FabianWolff/closure-examples/blob/master/counter.rs) | [src/prusti/counter.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/counter.ml) | | [delegation](https://github.com/FabianWolff/closure-examples/blob/master/delegation.rs) | [src/prusti/delegation.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/delegation.ml) | | [filter](https://github.com/FabianWolff/closure-examples/blob/master/filter.rs) | [src/examples/later/filter.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/examples/later/filter.ml) | | [fold](https://github.com/FabianWolff/closure-examples/blob/master/fold.rs) | [src/examples/later/fold.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/examples/later/fold.ml) | | [for_each](https://github.com/FabianWolff/closure-examples/blob/master/for_each.rs) | [src/examples/later/foreach.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/examples/later/foreach.ml) | | [map](https://github.com/FabianWolff/closure-examples/blob/master/map_vec.rs) | [src/examples/map.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/examples/map.ml) | | [repeat_with_n](https://github.com/FabianWolff/closure-examples/blob/master/repeat_with_n.rs) | [src/prusti/repeat_with_n.ml](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/prusti/repeat_with_n.ml) |

CS1101S Programs

Summary

- [Scoping section in Reading Assessment 1 20/21 S1](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/cs1/scoping.ml) - [Correctness section in Reading Assessment 1 18/19 S1](https://github.com/EmilyOng/AlgebraicEffect/blob/EmilyOng/examples/src/cs1/correctness.ml)

Program Proofs Book

Summary

Selection of examples and exercises in - [Chapter 6](https://github.com/EmilyOng/AlgebraicEffect/tree/EmilyOng/examples/src/program-proofs/chapter06) - [Chapter 8](https://github.com/EmilyOng/AlgebraicEffect/tree/EmilyOng/examples/src/program-proofs/chapter08)

Papers

Summary

- [Modular Specification and Verification of Closures in Rust](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/closure.ml#L34-L77)

Misc.

Summary

- [min_max_plus](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/closure.ml#L80-L86) from https://ilyasergey.net/CS6217/_static/slides/04-FunLog.pdf - [interleave](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/list.ml#L14-L19) from https://cs3110.github.io/textbook/chapters/ds/exercises.html - [subsequence](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/list.ml#L2-L7) - [replace](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/list.ml#L9-L12) - [find_index](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/list.ml#L25-L28) from https://v2.ocaml.org/api/List.html#VALfind_index - [exists](https://github.com/EmilyOng/AlgebraicEffect/blob/49364407136c7fea04a2e5387c8aee69f28837a2/src/examples/list.ml#L30-L33) from https://v2.ocaml.org/api/List.html#VALexists

Tests

Tested with TEST=1 dune test.

[dariusf]

Thanks so much. Before merging, could you just check that everything in src/examples is working? That directory is published to the web demo, so it'd be good to keep it tidy.

It's fine for other directories to be WIP, though if they're done, feel free to add them to run.t or the web demo later.

To check the things in run.t, you can run tests using dune test (2 mins) and PROVER=WHY3 dune test (about 12 mins).

[dariusf]

I fixed the substitution issue from earlier and made the tests more reliable. Also added some notes on configuring Why3 and some experimental tracing features, which help a lot when diving into the system.

[EmilyOng]

I fixed the substitution issue from earlier and made the tests more reliable. Also added some notes on configuring Why3 and some experimental tracing features, which help a lot when diving into the system.

Thanks! I have checked the programs in examples/ are working using (PROVER=WHY3) DEBUG=0 dune exec parsing/hip.exe src/examples/*.ml. Will try to make more progress with fixing the program-proofs programs and using pure functions.

[dariusf]

Looks good! Feel free to merge whenever you're ready.