The pml's discuss from rlepigre

Syntaxe revision (mantis #36)

Reexamine the syntax and see if the current choice are the best ...

Incompleteness of the termination checker that seems solvable

Here, we put all use case that seems to be solvable (or that even work in subml):
This issue should probably never be closed.

test/fifo.pml: with a pair of lists as argument
test/unfold.pml

pool optim, toward only head normal term added to the pool

insert_t_node should use a stack to avoid creating node for partially applied function.

For instance, adding [add n p] to the pool also adds [add n] which is a lambda, hence trigger a cloture construction.

This cost is dominating "equiv" when computation are really needed, with
probably a factor much greater that 2 (10 ?) to gain.

Incompleteness of typing/subtyping

Here we put reference to cases were the incompleteness of typing seems not reasonable.
This issue should probably never be closed.

test/fifo.pml: an annotation (x:a) is needed and this seems strange.

managment of unification variable in equivalence Description (mantis #50)

The current implementation seems to work but should be checked.
The risk is to loose some equivalence/normalisation propagation
when a unification variable gets instanciated.

HApp node are also concerned as their head is often an uninstanciated
unification variable.

Cyclic value should trigger contradiction in the pool.

An equation like x = S[x] learn in the pool does not yield a contradiction. Moreover,
using any function on x is likely to loop after that. We should detect such cycle.

Strangely, such cycle never appears in PML2 while they were frequent in PML1 ...

Do we need to learn ordinal relations in the pool

Probably not. Moreover, positivity is probably useless, relation o1 < o2 are enough (as it implies o2 > 0)

But still do we need to know in the pool that o1 < o2 is true ... Probably not ?

Theory

The document with the theory should be added to the git repository.

Checking for singleton type could be more complete (mantis #52)

Only very simple cases are handled by Typing.is_singleton.
Some quantification or Impl could be allowed.

PML can not always use function equalities that it learned

When we learn that functions are equal, we should keep that information:
VN_LAbs should contain a list of functions.

This would allow to always deduce f x = g x from f = g

Subtyping heuristic and auto case

Currently, we use in subtyping a heuristic testing is the term (int t : A < B) is a value.
This heuristic seems in fact to test if we already unrolled fixpoint ... And is
not so clear.

As a side effect, this heuristic forces subtyping of sums to use introduce a term
Preventing to replace the current term in a case anlysis with only one case with
a witness.

But this term with one case produce useless computation in the pool and useless
case analysis in auto_prove.

Contradiction is not always detected.

Use case in test/old_mccarthy91.pml

Printing of epsilons (mantis #53)

Epsilons should be prionted as the name of a bound variable that wes subsituted
with the epsilon. When epsilons are known to be equal, a "best" name should be chosen.

Deal with unification variables after type-checking (mantis #44)

Unification variable that remains after type-checking should
get a default instanciation.

Remark: if later we keep unification constraints, this would become very
important as there could be unsolvable contraints, or preferably, we should ensure all constraints have a default instanciation that we could use.

Add a syntaxtic sugar to extend record.

Minimal syntactic { include r1; include r2; ... } should use typing to know the field that are present.
The same notation for type is just some kind of higher order function performing some computation on type.

The general include for a record of unknown type (or default record value) seems too hard at the moment,
especially for compilation.

Cost of logging and Chrono

In function which are very frequently called, log and chrono can cost a lot.
If I uncomment the log in add_term and add_valu, the cost of log+chorno in Equiv and
Compare is a factor between 2 and 3.

we should create a binary "main.native" where this log/chrono on small function are disabled
(keeping still the main one like typing) and a main.debug with all log and chrono.

Improve type inference

Reference this issue in .pml file when we are not satisfied.

Reinforce completeness of auto and totality

When instantiating a unification variable of sort value with an expression
in the pool which is not a value, this does not trigger trying to prove that this a
value in auto_prove. Moreover, fixing this is not enough because one should
build a term which is a value to perform the instantiation.

Inequivalence clause are not stored in the pool (mantis #51)

Will only be useful when assuming inequivalence, which is not really possible currently.

Probably useless ... wait for a use case.

avoid canonical term in equiv.ml (mantis #41)

after #18 (mantis #40) is done, one should write an equality directly on
the pool, without using canonical term. canonical term should be kept for
debugging purpose only.

The Impl construct has no parse rule

auto cases! use information from typing

Some time, extra information comes from typing which allows to
restrict cases. This information is probably available in the type of the VWit ...
We should try to use it!

See lib/int.pml for a use case.

use closure in the pool Description (mantis #40)

the binder in all pool node (equiv.ml module) should be replaced
by closure.

This will allow to know that

a = b => (fun x y -> y x) a = (fun x y -> y x) b

without using an oracle

Mutually inductive types

Mutually inductive types can be encoded using extra parameters, but this result
in a notion of sized type which is not the one we want, and leads to failure
of the termination checker.