Copied old code back in parser, to make andrea8 great again

Merge branch 'permutations' into andrea

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

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

Removed num_more_args

Fixing the bug when eating triggers the reduction of a match

Added problem failing because of order of step

Test --with-pac fails if unseparable+uncomplete

Allow comments (#) at the end of terms

Logging options to display measure of single terms in string_of_problem

Fixed bug in Scott.mk_match when no branches (Fixes problem 1 in solved)

Fixed bug in computing special k

Added exception Lambda, which may be caught when a conv becomes a lambda

Added very simple generator of tests with bombs/pacmans, run it with --with-pac

Fixed eta_compare in the case Lam vs. Bot

Removed special strategies in choose_step

Better error messages in parser

Check for absence of bombs and pacmans

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).

Cleanup in w, added names, uncommented test for low special_k

Change to compute_special_k

Now the special_k taked into account the number or arguments (arity) of
terms. This solves problem "low special_k" in problems/w

Comments, fix indentation and

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

Simplified arity_of, precompute_edible_data, critical_showsteppers

Fixed computation of arity for top-level inerts

Simplified not-working example

Missing parenthesis fixed

Failing case found

Hack to reserve var 0 to purify it to BOM removed

String ==> Bytes to make recent ocaml compilers happy

Extracting solutions of 3-coloring problems

Added sample unsat problems found on the internet

subst does not replace anymore in branches of maches

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

Commented out problem, it is (still) failing because div occurs in conv

Printing now preserves the names of the original free variables

Fixed typo in problem

Improved parsing

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

Improved pretty-printing

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

Added problem wrongly backtracking

Forgot one "Z"

Code clean-up

Code clean-up

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

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

Encoding of SAT problems and 3-colorability of graphs

Fixes to parser

Added problems encoded from 3-colorability of graphs

Fixed "$" in parser

Command line arguments to ./a.out

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

Moved "o"-problems to problems/o

Fixed problems separator in parser: now it is $

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

Added label to problem

Removed invalid problems

Failure in case of empty problem, to be fixed

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

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

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

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

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

andrea7 -> new andrea9

- Removed Stuck and Pointer
- Added again bool flag to match entries to recall if coming from div or conv
- branches coming from div may diverge
- branches whose continuation is still a variable are completed

Fixed bug where entries in matches were not counted in all_terms
Still crashing

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