TODO

- xif sans argument pour pouvoir le forcer

- xlet_keep 
		let H := cfml_get_precondition tt in
		xlet (... \*+ H)

- "xapp as x"  pratique sur xlet
- "xapps as x"  pratique sur xlet

- xlet Q => xif Q mais avec branche


MAJOR TODAY


- rename xextract to xpull;  and xgen to xpush.

- Sys.max_array_length 


MAJOR NEXT

- xchanges

- patterns and when clauses

- add support for pure records

- record with

- partial/over application

- xabstract => reimplement and rename as xgen


MAJOR NEXT NEXT

- xwhile: error reporting when arguments don't have the right types.

- eliminate notations for tags

- record single field and array single cell notation
   Notation "x `. f '~>' S" := 
   Notation "x `[ i ] '~>' S" := 

- realize array specification using single-cell array specifications

- see if we can get rid of make_cmj

- mutually recursive polymorhpic functions have too many type variables
  quantified: we need one set of fvs for each def in the recursion.

MAJOR POSTPONED

- support char
- support float

- implement the work around for type abbreviations:
   type typerecb1 = | Typerecb_1 of typerecb2
    and typerecb2 = typerecb1 list

- would it be better to perform all renaming during normalization phase?

- have a flag to control whether functions such as "min", "max", "abs", etc.. 
  should be systematically let-bound; this would allow binding these names.


- mutual recursive definitions, polymophic type variables should be more precise


##################################################################
# FUTURE WORK


OTHER LANGUAGES

- semantics for records|arrays  passed by value / passed by reference

- support null pointers


CODE BEAUTIFY

- better error message when calling [xapp] on a record application 
  in which the record is not unfocused.

- make sure that check_var is called where needed 

- unify the source code in main.ml and makecmj.ml

- check that there are no uses of labels in input source files

- Ltac xcf_core tt  
  should be able to test whether Spec is a top val, and then do rewrite.


MAKEFILE BEAUTIFY

- no longer rely on myocamldep

- make systematic use of    || (rm -f $@; exit 1)   in cfml calls

- In the makefile.Coq, when building the .vq and obtaining
    "Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
  => then delete the .vio file
    (useful for compilations interrupted using CTRL+C)
  => even better, wrap "coqc -quick" with an atomic commit of its result.


##################################################################
# PROPOSAL FOR DEFENSIVE CODE

  - VStack.ml  contains a verified stack implemementation using CFML.
    (not polluted by any runtime checks).

  - SStack.ml  is a wrapper for VStack which adds asserts; 
    e.g.    let pop s = assert (!s <> nil); VStack.pop s

  - The file SStack.ml is processed using a special mode of CFML,
    in which "assert t" is interpreted as "t needs to run safely
    and produce some boolean; and the rest of the code may
    assume this boolean to be true". Formally:

        (Assert F) H Q := 
          exists (P:Prop),
            (F H (fun (b:bool) => [b = true <-> P] \* H)) 
          /\ (H \* [P] ==> Q tt)

    During the proof, the user needs to provide the proposition
	 [P] that is tested by the assertion. This proposition can
	 be assumed to be true after the assert is executed.