-*- outline -*-

* Mots clés

DONE  - fun -> proc
DONE  - lambda -> fun
DONE  - eqobs_in -> sim
DONE  - datatype -> type
DONE  - record -> type
DONE  - bd_hoare -> phoare
DONE  - bdhoare_* -> phoare_*
DONE  - *_deno -> bydeno (byphoare | byequiv)

WONT  - fst -> .`1
WONT  - snd -> .`2

DONE * Comportement par défaut devrait etre `proof strict' (ceci est une décision unilatérale de François)

* Discuter la syntaxe des opérateurs

* Type de retour optionnel pour les procédures
DONE  + inférence pour les var. locales
DONE
DONE * Chainage pour les déclarations abstraites:
DONE
DONE   type t1, ..., tn.
DONE   var  x1, ..., xn.
DONE
DONE   result: with comma (Avec ou sans virgule ?)
DONE
DONE * Permettre les accès directs aux fonctions dans les foncteurs
DONE   (via `x <- call')
DONE * interface de module / proc.
DONE
DONE   proc * id(arg...) : t { restr } (* `*' est maintenant en dehors - 16082 *)
DONE 
DONE   + `arg' peut maintenant être de la forme `_ : t1 * ... * tn'
DONE      actuellement, la syntaxe est ,t1 * ... * tn

WONT * if / while -> parenthèses sur la condition ? (interaction avec les accolades)
       Wont because braces are not mandatory for the body

* intro-pattern ->>, <<- pour substitution d'une variable par un terme (voir pour un rewrite in *)

* rewrite in
DONE  + apply in à la Coq

* by < ; < first, last -> cas t; first by (t2; t3); t4

DONE * cut by t -> currently cut; first t. Should be cut; first by t.
DONE   idem for lemma ... by ...
DONE
DONE * by [] everywhere
DONE
DONE * apply -> gestion de <=>
DONE
DONE * t1 || t2 -> or-else

    ; < || < first, last

* case pour PHL -> à lier à celui de la logique ambiente

DONE * bd_hoare / hoare à top-level

* bd_hoare -> phoare / phl
	bd_hoare [fident ...] relation form // pas sform
	conseq aussi

HALF-DONE (only for non-exported functions) * détection du code mort

* Syntaxe des tactiques

    wp side? cpos?
    sp side? cpos?

    seq side? cpos : sform tacdir appbdinfo -> voir si `:' sert
	en fait, on veut: seq side? cpos : sform sform? tacdir? appbdinfo' (ou appbdinfo' est appbdinfo sans le dernier sform optionnel)
    while side : wtacinfo

    proc sform sform sform? -> proc LBRACKET form RBRACKET sform sform?
    call side? fpattern(callinfo) -> call side? fpattern(callinfo')  et call LBRACKET form RBRACKET sform sform?
    callinfo' = form LONGARROW form | form

    rcondt / rcondf -> UINT => singlecpos

    swap icpos -> unifier avec les code-positions + intervals à la rewrite
      + enlever la 1ère règle (SKbase)

    cfold -> voir si peut-être enlevé

    rnd -> mettre ou enlever le `:' (rnd_info)

    DONE inline * -> inline tout le monde d'un niveau

    kill -> utiliser la syntaxe des intervals pour rewrite

    split_while expr : side? cpos => split_while side? cpos : expr

    exfalso : si la pred. n'est pas False, devrait faire une coupure

    transivity transkind transkind transheap
      transkind : side stmt | id
      transheap : ...

    eager
      eager_seq -> utiliser les cpos
      à la fin : `:' entre eager_info && sform

    pr_bounded -> à virer

    DONE hoare / bdhoare -> fusionner en hoare
    DONE
    DONE rewrite Pr -> intégrer dans rewrite
    DONE
    DONE pr_false -> à enlever
    DONE
    DONE pr_eq -> à enlever (* Ce fait avec conseq *)
	
	exists* -> utilise alias

	alias ?side slist(alias_dec,COMMA)

	alias_dec = codepos | codepos AS lident | codepos lident EQ expr | UNDERSCORE list(sform)
	
X : tacdir : << | >> | ε

DONE * Semantique des tactiques:
DONE    eqobs_in, hoare devraient sur les procedures, pas seulement les statements

    Pr[...] sur les statements et pas seulement sur les procedures?

* equiv, phoare, hoare devraient pouvoir prendre des invariants plutot que des paires pre/post.