TODO

  - think about static flow analysis à la PML1

  - go back to original representation of calls as substitutions (+result) using C- and projections

  - add functions (fun x -> ...) as a syntactic sugar in definitions???

  - file christophe.ch is very slow (test12)

  - flags
      --minimal -> unary, no structs
      --only-termination

  - better exceptions than "Not_found" for utils.ml functions

  - change type used for representing function clauses:
       type clause = (var_name * term list) * term

  - without memoizing, reduction with case is slower than rewritting!!!

  - use lexing positions for parsing errors:
      - update "file" field
      - print buffer with error underlined ???

  - use type weight for priorities???

  - allow parser to read priorities in terms (for testing)???

  - add some assert tests

  - remove "continue_on_error" option (stop when loading files, continue in interactive mode)

  - try sorting the CASE clauses so that recursive clauses come first

  - use DeCap?

  - remove Proj variant and use Const everywhere (requires thinking about
    priority None: there should be a data and codata version)

  - think again about n-ary application
        type atomic_term = Var | Proj | Const | Angel
        type term = App of atomic_term * term list | Special ...

  - allow "{ proj1 = u1 ; ... ; projn = un }" in terms and patterns (=> lexer,
    parser, term, ...) unification now has
        { proj1 = u1 ; ... ; projn = un } ~ t   ==>   u1 ~ t.proj1, ..., un ~ t.projn

    In the end, the substitution should only contain "simple" patterns, and
    substitution should use "simple pattern matching"