Implementing entanglement of terms

FIXME usage of flags b' in subst and mk_app
 must be understood and fixed!

One garbage

More evil problems

Replaced eat with andrea's finish
(fixes examples failing for measure)

Added flag to lam and app, their propagation during subst, and a measure

(may fail after eat steps)

Embarassing bug in eta_eq fixed

Append the eaten arg + leftmost order in find_eta_difference

simple.evil example works.

Fix bug traces of old constructor B

Real evil problem found!

One must store arguments for later usage :-(

Removed B and C from t, stepped from problem

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)

Code clean-up

Less casts and casts in the right place

(cherry picked from commit 6bf723ba426a04a3ae5d36baf8a9fe4bffebc635)

Tidying up problems.ml

(cherry picked from commit c8d9c2fda6b135b29e81e3bea95520ba449b86e3)

Tentative commit: tactics dropped and clean-up

(cherry picked from commit 0991fc5486c3158fc361e84cbba5aefa67893ba4)

Include codice di pure.ml che implementa Pure.B da commit
 "Removed bomb variable"

Added assert false

(cherry picked from commit ba6f0ecd9531b266361674d76423c24381dc72ee)

Fixed bug in eta_subterm

(cherry picked from commit 09ecd6ebdb7d96386bd79a7117930aba4635f778)

Remove FORCE option in Makefile

(cherry picked from commit 6ba14f58fa4c8f93fc2a398bdee030cd2217adea)

Fix: missing check to avoid stepping on vars of non positive arity

(cherry picked from commit 58f1518398346a81ccd8d0b14a14565b8bff5276)

Fix: max_arity_tms was using wrong comparison

(cherry picked from commit a104858f2dd754e5d086c3884823f3f39d716691)

Added variable convergent_dummy

Fixes to printing

(cherry picked from commit 4627d2b89b5a96e09b1921e033a5c1d7dd50dbc6)

Disabled some chars as variable names in the parser

(cherry picked from commit bfd8f8a98a7392ac8cbd9070a8e4ff4d06e09510)

Prettier-printing: string_of_problem outputs OCaml code

(cherry picked from commit d97b1a852472085bf3449e34f3b25aee349686fd)

Fixed if-then-else

(cherry picked from commit 588a00cd5ae861a2f366df992f758f285265a34a)

Fix: nested `Lambda(false,_) were not handled correctly

(cherry picked from commit 0147bacbe2db4055ae6f991aaa64a9fb1047edc6)