Moved parse' from Num to Parser

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)

Re-use Util.index_of

Code clean-up

Less casts and casts in the right place

Tidying up problems.ml

New failing problem, which shows that we need to change special_k

Added assert false

Fixed bug in eta_subterm

Remove FORCE option in Makefile

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

More problems

return type of simplify_match improved (no `Match in output)

Added safety check for step on n-th argument with n > 1

Avoid stepping on n if there is a div/number that would be turned into
a Lambda

Improved error messages

Failing problems commented out

New tests

Fix (??): some broken tests with Div = variable used to pass

Tentative commit: tactics dropped and clean-up

Fix: max_arity_tms was using wrong comparison

Fixed try in aux_conv + Added test in pure for divergence of conv

Fixes to printing

Added more problems with bombs, all working

Disabled some chars as variable names in the parser

Removed bomb variable

In Pure:
- Added constructor B to Pure.t
- Added rule corresponding to B (bottom) in Pure.mwhd
In Lambda4:
- Instantiating the bomb now actually uses subst_in_problem
- Two new exceptions: Bottom and Pacman
- Fixed subst_in_problem by making expand_match raise these two exceptions,
  which are caught when tolerated

Prettier-printing: string_of_problem outputs OCaml code

Added second problem with bombs and pacmans: it works!

Added new (passing) problem with a bomb (o1)

Towards `Bottom and `Pacman

1) Num updated to handle them
2) lambda4 compiles: safety conditions for projections hopefully
   implemented; strategy code not changed, therefore it will step over
   bombs and friends

New: simple backtracking with trail

auto_instantiate replaced by choose_step and first

Fixed if-then-else

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

-666 -> min_int

Fixed indentation and logging

instantiate takes an additional argument which is the number of the argument to the variable on which to step

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