TODO

Notations:
==========

  <- : means easy
   * : means a bit more involving
  ** : means more complex
Done : means that this item has been done.
   ? : open question

TODO list:
=========

2011-11-04 (post-release todo)
-----------------------------

* Division by absorbent generated in test though there is no inverse
  generator for the generator that has an absorbent element (hence division
  by absorbent cannot occur!)

2011-11-03 (pre-release todo)
-----------------------------

* Update doc/tutorial
* Reorganize test directory and execute test in subdir (lpi, tableaux,
  lambda-sigma) by default
** Reorganize tableaux subdir

Done * ``Cannot generate test for equation'' was due to a bad treatment of
       combination of listary and fixed arity generators rules to test
Done * Division by absorbent generated in test though there is no absorbent element ...
Done * Chase down and remove spurious module openings in generated test files (see
       biocham test for example)
Done * Same for message "unknown generator ::" in test generations

2011-03-01
----------

* Alternativity

(x x) y = x (x y)
x (y y) = (x y) y

Implies (x y) x = x (y x) ?

* Power ???

(x x) x = x (x x)
(Autorise x^n)

In the number fields, we get the following hierarchy

R dim 1
C dime 2 -> on perd l'ordre
Qu 4 -> on perd la com de *
O 8 (Octonion) -> on perd l'assoc de *
S 16 (Sédénion) -> on perd l'alternativité de *

2010-09-09
----------

* Generate a compare_ty comparison predicate for any moca type ty:
  Presumably:
  - constant constructors are ordered by their order of presentation and
  lesser than any unary or binary constructor tree
  - a unary constructor tree is lesser than any binary constructor tree
  - unary and binary trees are ordered lexicographically by the presentation
  order of their head constructor.

* Rewrite the genr_binary and genr_unary to use the new scheme for fields (as
  in test/field_math_rewritten_by_hand.ml

<- Check the error messages in check.ml to verify that the name of the
generator that has a problem is always properly reported.

* Automatic generation of ml and mli files from a single mlm where exported
  functions/modules are marked up ("export" keyword?)

<- fix code generation pp for polymorphic types of form ('a, 'b) t (ie " 'a, 'b t ")
(see code generated for monoid_modules.* in test directory)

<- add a unique integer in the info record for providing efficient
ordering of shared values (see
http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz)

? Is it correct to complete a set of mutually defined types by
completing each type independently?

<- When mocac fails unlink the generated files if any (.mli, .ml, _test.ml).

<- Generate a header in each generated file:
     (* Warning: DO NOT EDIT.
        Your modifications could be unadvertently discarded, since
        this file is automatically generated by mocac
        from file foo.mlm. *)

<- Turn generated file readonly to prevent manual editing.

* give corresponding faulty line in .mlm source file when OCaml reports an
error in the .ml file produced by Moca. Need to generate #line directives in
the .ml (and .mli) generated source files.

* allow the user to specify the functions used for creating a new
  value (default is the caml constructor of the type declaration) in
  order to build hierarchies of moca types.

<- generation for nilpotent and absorbent for varyadic is ok ?

<- user rules on records

<- distribute gentest.ml and provide a script for running generated
  test files

* test non algebraic user rules (just use them to deduce an equality
  to test them!)

* generalize tests to ``non matching patterns'': if Neutral (Zero) for Plus is
  correctly implemented then no value matches Plus (Zero, x) nor Plus (x,
  Zero).
  Generate a checking function such as:
  let unmatch v =
    let ok =
      match v with
      | Plus (Zero, _x) -> false
      | Plus (_x, Zero) -> false
      | _ -> true in
    ok, v
  ;;

  This way we can (generically) test the unmatch function result and have a
  witness in case of failure. We can just perform the test systematically for
  each value creation for the type being tested.
  (Something like f (test_unmatch x) instead of f (x), with
   let test_unmatch x =
     let x, b = unmatch x in
     if b then x else begin
       prerr_endline "Unmatch test failed";
       failwith "error"
     end
   ;;
   or the like)

* understand (and ameliorate?) the deduction of type variables from
  environment.

<- defining a precedence from the order of constructors in the source code ?

** take into account includes when parsing files

** allow modules and functors defining moca types

** allow left associativity

<- produce an error in case of sharing if the type definition
has objects or functions

? ** extend add_type_decls to modules and functors

? ** allow builtin relations on record fields

<- the user should know the rules added by completion

<- complete printast.ml in compiler/ocaml_src/parsing/printast.ml to print
relations in type variant definitions (insert and complete
and relations i ppf relations =
  ...
at (to be completed) line
and string_x_core_type_list_x_location i ppf (s, l, _relations, _loc) =
  ...

** Revise generation functions for conformance with side arguments of
relations.

** Revise completion.

? <- rename otype into ocaml and pr_otype into ocamlpr

? <- split check into error and table, and move them into comp/

? ** Generate non-fragile construction functions

<- Restore OCamldoc doc generation

Removed from the TODO list:
---------------------------

<- replace [lmr]po comparison function by gt function
  since only gt is necessary for completion ?
=> not a good idea

? <- define relations as RelSet.t instead of relation list

<- because of the new .mlms file extension, do not replace in user rules
a constructor name by the corresponding construction function ?
=> not a good idea

** Revise check.ml to reintroduce proper checks (in particular for
user's rules if possible).
=> only successful completion should be required
(names, arities and types will be checked by ocaml)

** For user's rules with when clauses,
  = should be replaced by == in case of sharing
  (see the examples lpi and vector).
=> not useful anymore with the extension .mlms

* extend add_underscore to expressions
and add an underscore only for the constructors of the current type
=> not useful anymore with the extension .mlms

** finish structure example ?
=> the system is not adapted: it is not confluent and we must use a
breadth-first search to investigate the prooftree: definitely not moca-like

Canceled list:
--------------

Cancelled <- Trace normalization function calls (and pattern-matching cases)
in generated ml files. It generates too huge logs: this is unusable in fact.

Done list:
----------

Done * Memoization of normalization function calls (-memo command line
  option)

Done * Check in type definitions of mlm files that zeroary generators are
  listed first, then unary ones, then binary ones, then n-ary.

Where should listary generators be declared?

Otherwise, the Pervasives.compare primitive would not be compatible with the
so-called "intuitive" order used in the generated code. (See the remarks in
test/field_math_rewritten_by_hand for further information).  The "good" way
to handle it would be to generate a specialized version of compare.

Done * fix bug in rpo and define a function rpo_gt

Mult(Opp(Mult(x28,x29)),x3) n'est pas plus grand que
Mult(Opp x29, Mult(x12,Mult(Opp(Mult(x28,x12)),x3)))

Done * fix bug in rulset equality: group.mlm with neutral left and
  inverse left.

Done <- user rules on 0-ary

Done <- remove the side argument of Commutative ?

Done * turn pr_otype into a Format pretty printer

Done <- remove option -order and use rpo only

Done <- fix bug in printing of version number

Done * completion of pr_code to print lists.

Done * test algebraic user rules

Done <- repeat some values in the generation of test substitutions
  when not enough values are generated ?

Done ** generation of values for concrete types

Done ** generation of equation instances

Done ** generation of test files

Done <- remove Distributive_Inverse as a special case of Distributive

Done <- remove constructor Pair in Code.exp as a special case of Tuple

Done <- check user rule left hand-side declared for C are headed by C
  + no two commutativity/associativity declarations

Done <- add gi_priv_flag : Asttypes.private_flag;

Done <- name variables as moca_*

Done ** Complete genr_vary with inverse, etc.

Done ** Define a new test with a relational type specific comparison
and verify that the compiler indeed uses it in the generation
of the code for the generation function for the type.

Done <- respect order of user rule's in the precedence

Done <- generation of equations in the type used by completion
from moca relations

Done <- add a "-complete n" option

Done * in genr_rule, lowercase only the constructors of the current type

Done <- fix bug: in case of "open" module M, M may not be a file
but may be defined in the current file (M = f(N))

Done ** Get the vector test example working.

Done * add comments to explain precedence on relations

Done * parse open modules too

Done <- instead of putting every letter in lowercase, just put the first

Done * In genr_*, change the generated calls to ( = ) in order to call the
equality function relevant to the case (for instance, in case of maximal
sharing, this function is ( == )).

Done * in genr_binary, fix error in distributivity (case D varyadic)

Done ** Systematically generate an equality function.
Done ** replace mocac script by ocaml program

Done <- rename Nilpotent by Nilpotent_unary
and add Nilpotent for binary and  varyadic constructors

Done <- replace spec.type_def by OCaml type

Done <- Change predicate abs_neutr into absorbing_or_neutral.
Done <- Change predicate commutative_neutr into has_commutative.
Done <- In genr_base change cons_fun to name_of_construction_function
Done <- move prefix_cname from genr_bin to genr_base

Done <- Check that relation arguments are indeed constructors
of the current type.

Done <- Rules should be pattern -> expression and we continue
to change Constructors into construction functions.

Done <- nilpotent and idempotent have the same left-hand side as rewrite
rules: hence they are mutually exclusive (except when there is no element
distinct from the nilpotent generator). This exception is not relevant : the
user just have to choose one of the relation to get the same semantics.
Anyway, we must forbid both nilpotent and idempotent applied to the same
generator.

Done <-<- Add Ocaml annotation generation (this can be used to check the
   element types when using the appropriate Emacs mode)

Efficiency:
-----------

Done * Use compare and matching on the result of compare in order to perform
only one comparison instead of a cascade of comparisons.
  For instance:

  delete_C x = function
  | Plus (y, _) when x < y -> raise Not_found
  | Plus (y, t) when x = y -> t
  | Plus (y, t) -> C (y, delete_C x t)
  | y when y = x -> E
  | _ -> raise Not_found

  can be rewritten as:

  delete_C x = function
  | Plus (y, t) ->
    (match compare x y with
     | 0 -> t
     | k when k < 0 -> raise Not_found
     | _ -> C (y, delete_C x t))
  | y when y = x -> E
  | _ -> raise Not_found

Done* OK if (compare x y = 0) implies x=y (or x==y with sharing)

Done (there are no more insert functions) What for the insert function case ?

Long term goals (in order of urgency):
--------------------------------------

Done *  generate tests for correctness and irreducibility of canonical forms.

** generate completeness rules for user's rules and built-in rules.

** generate input files for CIME to complete and test termination and
confluence.

** Rewrite the test examples with user's rules only (not using the built in
   annotations).

Theoretical questions and problems:
-----------------------------------

? To which rewriting system, with which strategy do the generated programs
  correspond to ?

? User's rules completion: in the non-AC case, we can use the program
  written in directory completion/. What in the modulo-AC case ?

? To which extent rewriting modulo-AC or computation of normal forms
modulo-AC can be obtained without modulo-AC rewriting and matching ?

Remark: a pattern matching using the first match priority rule is
equivalent to a pattern matching (which can be different and can use
more or less clauses) using the most specific pattern rule.