(Almost-)Correct handling of garbage in Simple

- subst_in_problem, step now return a list of terms from garbages
  that were activated, i.e. brought on toplevel after a reduction
- auto iterated on that garbage

TODO:
- remove sanity function
- problems/simple.constants.1 fails :-(

Using C instead of @ to combine more convergents in p.conv

Improved definition of eta_eq

Probably still not just right

Step possible beyond the args of p.div

Improved backtracking in Simple

- Removed Fail exception, replaced by combination
  of Failure, Backtrack, Unseparable
- Added label to problem

Implemented garbage in Num

- Implemented parsing of garbage
  e.g. (x. x x , A , B , ...) where the garbage is A and B and ...
- Garbage is not implemented in Lambda4, but implemented in Num (except in subst i.e. reduction)
  (see `assert g = []`)
- Added sample problems with garbage

Fix: bug in printing garbage, did not consider the level

Added garbage to L

Note: eta_eq ignores garbage at the moment

Removed eat, p.stepped, p.phase and t.B

More randomness in test generation

Added problems that fail when eat is done incorrectly

i.e. on arguments before the max arity in the conv

Using andrea's finish instead of eat. All tests succeed.

But again, most generated tests are solved in one step.

Trailing constant args in p.div are removed by sanity

Because they cannot contribute to any usable eta-difference

It shows bug with new eat

New failing test

Added tests with constants

- Enabled with flag --with-const
- Stores failing problems in problems/ folder

Problems that are not distinct commented out.

Those problems can be separated, but picking a different
term to diverge

Fix: eating a lambda^n.C args is bad

I know eat an argument which is a flexible inert.
What to do if there is none? I think we should backtrack;
for the time being I raise an assert false.

All output to stdout (in place of stderr).

This commit could be cherry-picked in the other branches as well.

Fix: find_eta_difference now works with inerts of arbitrary length

All simple.x tests now pass (same for automatically generated ones)

Forgot to commit yesterday file with problems with constants

Experimenting with backtracking and stepping on "all" possible subterms

Implementing constants

auto now iterates the eta differences and backtracks if no more available

Removed parameter from C

More comments and improved find_eta_difference

More comments and better variable names

Renamed output files

Removed warning

Fix lifting bug in unwind

problems/simple.* now pass

Simplified divergent problem

C diverges in pure

Make the code OCaml-4.06.1-friendly

Updated simple with current parser

- Removed parser_andrea
- Generalized problems.ml
- Moved sample problems from simple.ml to problems/simple.0

Simpler tests in simple_test.ml + Added diverging tests in simple.1

Eat was erasing terms from C that made it diverge

Bug in mk_app with C

Fix no_leading_lambdas to account for a step on x on an argument starting with x

New (in-)decision procedure for termination

More bound vars in simple_test

Clean up, improve comments, move functions

`run' is the new entrypoint in simple.ml

Added check for eta_subterm in `solve'

Reverted sanity to old syntax

Added simple_test.ml

Moved andrea.ml to simple.ml

Added constructor for constants

TODO: correctly translate constants to pure terms in `purify'

Made bombs more explosive (strongly)

Restored good check for Done

Simple strong separation implemented!

- Two phases for eat
- Moved code
- Reduction does not diverge (replaces DD with B)

Added check with purification to andrea.ml

Note! It now diverges because it uses B (bottoms)

Moved function, fix indentation, removed parsing of bombs

Clean-up step function; move code

Removed pacman

Clean up

get_subterm_with_head_and_args goes under lambdas

Removed useless `isdiv' flag

Clean-up to examples. Removed tests.

Simple algorithm by Andrea

Cherry-picked from f260

Moved env_of_sigma to Pure

Tentative implementation of strong separation algorithm

- A `Match from num is translated to pure by masking branches
  with underscore lambdas
- The eating step on the divergent does not create a substitution in sigma
  (to be understood...)
- In the branch of matches, \_. !divergent is translated to delta
- The checks in dangerous must still be fixed to go under lambdas

Machine implements strong reduction

The machine is very inefficient (uses unwind under lambdas)

Detection of divergents

Bug fixed in pretty-printing of original names under lambdas

Fix in pretty-printing of match

Implemented parsing of "nominal" variables (`@`)

Each occurrence of `@` is parsed as a fresh free variable

Allow comments (#) at the end of terms

Logging options to display measure of single terms in string_of_problem

Fixed bug in computing special k

Removed special strategies in choose_step

Better error messages in parser

(cherry picked from commit 54e55518261ee5f3c68758ea070b1bac41400e54)

Revert subst in branches of matches

Actually, it could be moved in susbt_in_problem,
hence doing it only once (on the deltas), instead
of replacing multiple times like now (useless).

(cherry picked from commit bd3a8ee424e495ab4003f6d4cb88579f29e3bc3a)

Comments, fix indentation and

(cherry picked from commit 0a50c398d9eef65620f18f99ef675770b50a920c)

Renamed in critical_showstoppers: showstoppers -> inedible (I don't know why)

(cherry picked from commit dc829653c03f7bf0977addabe480e7c8b178bad1)

Simplified arity_of, precompute_edible_data, critical_showsteppers

(cherry picked from commit 4c81587c5f911c4d5f818765106bb5373967d715)

Added a couple of tests which MUST fail

Fixed computation of arity for top-level inerts

(cherry picked from commit 5682bf463b89edb7756020fe7b838eb846d6c771)

Simplified not-working example

(cherry picked from commit 180710db0f9d6f81edd7a5cc1bfce41e3b3e620a)

Missing parenthesis fixed

(cherry picked from commit aa18ab71f3030f746de14168b9dae21c255e9b81)

Failing case found

(cherry picked from commit 42eb14bc4443ce5a9bb893654db97a9c41486f06)

Hack to reserve var 0 to purify it to BOM removed

(cherry picked from commit 1fdb461d0bc4056ade8a05c482142984dbda735c)

subst does not replace anymore in branches of maches

It was unnecessary: a match cannot expand to a previous branch

(cherry picked from commit 8a90160900bb95133b8e204a4fcadaa2db2f11dd)

Printing now preserves the names of the original free variables

(cherry picked from commit 7051416c234181eaf79dedfd18005cdf0a3e0863)

Improved parsing

- removed unused parse'
- fixed bug which was ignoring the first problems in some files

(cherry picked from commit 2d56686ea25883e77d0a69f1245e6e840fc8be5f)

Improved pretty-printing

- Num does not use print_name anymore
- Original names of free variables are preserved
- bound variables' names start with x

(cherry picked from commit 137e2373f8875992898f8be0e07c4299ffbf3516)

Added problem wrongly backtracking

(cherry picked from commit a34071ed728b8de44b198de4e73a52207557ed81)

Forgot one "Z"

(cherry picked from commit 572c25c8db51bd571c7f4810500074bac8c37c31)

Code clean-up

(cherry picked from commit 8fcb433208ce608350ea554dd1d92fa5a45fd463)

Code clean-up

(cherry picked from commit 5d8249a042beefbe21bfeed48619ed1917ebbcb7)

Important: added special variable "Z" for zero.

- Removed append_zero in Lambda4
- Now tests append "Z" at the end of ps'
- Manually appended "Z" at the end of all problems
- Removed tmp function in Lambda4, renamed to problem_of

(cherry picked from commit 82dd1911598932af386c4de46398624453e1fc31)

Moved all problems in problems folder. Last ones in "w"

(cherry picked from commit f7a60345135a4032bf63a7dc650bcc9fe30aa30a)

Fixes to parser

(cherry picked from commit 666a228779e465d08a0deea2e35c0cccf5722b40)

Fixed "$" in parser

(cherry picked from commit db562ac015ffc6c1a08c226b4eef7790b21661cd)

Command line arguments to ./a.out

For example:
 ./a.out problems/*
 ./a.out problems/p

Moved "o"-problems to problems/o

(cherry picked from commit dfad242808c3525a0d9e3420565551964fcf0832)

Fixed problems separator in parser: now it is $

A separable problem's label may start with '!', a not separable's with '?'

(cherry picked from commit 71f8eb7befd85ff4911658136597b41ed177ff8c)

Added label to problem

(cherry picked from commit c7e39970b94c93db45f2629af3fdb1e08371eca1)

Failure in case of empty problem, to be fixed

(cherry picked from commit 605ae9159149e42a17f044bbfad94f7dc2de79c2)

Parser.from_file, and p* problems moved to problems/p

(cherry picked from commit 032edbca0cd6654adae5b5f06620723e74847435)

problems now contain a label and the names of the original free variables

(cherry picked from commit 15c305b0d106b39616bdeea9aec9febc7539c2c1)

First draft of Parser.problem_of_string

- problem_of_string should unify old Lambda4.problem_of and Parser.parse'
- Lambda4.problem_of was temporarily factored in problem_of_2
  and problem_of_String_tmp

(cherry picked from commit 8b69a4c59242b64294c7065a4e85437ce3cbc32d)

Changed logic of entrypoint in Lambda4

- removed exception Fail
- added "check",which checks if we are in a subproblem
  of separation on which we know to be complete
- "solve" does not raise particular exceptions anymore,
  and the program raise failure only if there is some bug

(cherry picked from commit 608c40045f651c6402b17c437f997de4d63f6afd)

Moved parse' from Num to Parser

(cherry picked from commit 123d64bb5ae7127f6a51cbf44b63341de001a187)

Fixed: was using compare in place of eta_eq

in particular, eta_eq ignores arities of variables

there used to be cases of duplicate entries in PS (up to arities of variables)

(cherry picked from commit 79e9bd64d15490dd5abc353cc5b09378d3c640d1)

Re-use Util.index_of

(cherry picked from commit 52947a60467ebb10cec57ffc1725644ad605c671)