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)

-666 -> min_int

(cherry picked from commit 5da7cf1322998c8965455264249f12ac4400f49d)

Fixed indentation and logging

(cherry picked from commit 4985769db038aa060b47ab40f673aaaacea54742)

clean removes *.o files

Removed old .ar files

Run tests with: make run

Fix: conv : x:min_int (.... y:1 ...)  y was not considered for stepping

When no other choice is available, step on any >0 variable that occurs in
a conv.

New problems n1, n2 used to debug the problem with dangerous variables fixed in the last commits

Bug fix: x (y z) where y was conv_dangerous did not make x so

Additional fix to last commit: args' where no longer checked for dangerous
variables. Fixed by passing three arguments to dangerous_invert_conv in
place of two.

Fix bug in dangerous_conv with arity of arguments of matches.
Next bug: variable replaced twice

The measure finally works on all problems in problems.ml!
Added in logs/fail.txt a fragment of a failing problem

Experimenting with a combined measure

Instantiate now uses a global initialSpecialK (ignoring the local one)
This fixes the bug in the previous commit, and makes the problem pass

Arity inherited only in the case (true, min_int)
Problem 25 fails because a fake variable becomes
critical step.

new_arity = old_arity + 1

Fixes to how arities are assigned and propagated
- added truelam to subst (useless, can be removed)
- TODO: to measure the problem, count the `fake` variables
        which are the ones with arity = min_int

Minor fixes

still stepping on negative variables

Problems pass, but still missing computation of arities of fresh applicative vars

New representation of arities in variables

Removed traces of lambda3

Removed lambda3 + Fixed lambda4

Updated type of terms with arities in lambda and matche

Moved andrea's stuff to its branch

Copy ocaml folder from sacerdot's svn repository, rev 4907

Initial commit