CRADT20090630

Compte-rendu de la journée ADT tactiques du 30 juin 2009

Voir aussi la page ADT.

Nombre de participants: environ 15

Questions d'ordre général

Workshop Coq: 6 articles acceptés, il reste quelques possibilités pour financer une mission à Munich.

Ssreflect

(cf exposé)

Yves souligne l'aspect méthodologique de la démarche de Georges (utilisation de noms pertinents plutôt que H1, H2, ...; indentation des scripts; ...) qui va au delà de la structure propre de Ssreflect.

Nommage obligatoire des hypothèses dans Ssreflect : pourquoi l'imposer systématiquement et pas seulement dans la phase de stabilisation du code ?

Introduction automatique des paramètres dans une configuration Theorem thm x y : T. Arnaud dit que Matthieu l'a implanté mais est revenu en arrière pour raisons de compatibilité.

MLtac + notes sur les tactiques de Coq

Beaucoup de suggestions/demandes (cf exposé 1 et exposé 2).

Commentaires pêle-mêle:

Utiliser les notations Coq pour les termes au niveau ML nécessiterait de pouvoir compiler des fichiers .ml après avoir chargé des fichiers .v (ce que le chargement dynamique de code natif de OCaml 3.11 permet).

Exemple d'implémentation possible d'une macro camlp4 permettant de parser de la syntaxe Coq au niveau ML:

<<
match t with
| u1 -> body1
| u2 -> ...
>>

s'expanserait en

try
  let l =
    Matching.matches t
     (snd (Constrintern.intern_constr_pattern Evd.empty (Global.env()) u1)) in
  (* on suppose que u fait référence à trois variables ?x, ?y et ?z *)
  let x = List.assoc (id_of_string "x") l in
  let y = List.assoc (id_of_string "y") l in
  let z = List.assoc (id_of_string "z") l in
  body
with
  PatternMatchingFailure ->
  let l =
    Matching.matches t
     (snd (Constrintern.intern_constr_pattern Evd.empty (Global.env()) u2)) in
  ...

Benjamin rappelle le difficile positionnement de Ltac qui fut bridé (typage, types de données, ...) pour éviter d'être considéré comme une copie de ML au niveau Coq.

Analyse de Ltac

Plusieurs remarques et propositions intéressantes, cf transparents.

• généralisation de fail et || au niveau constr de Ltac.
• pouvoir contrôler le moment où le but est appliqué
• avoir des tactiques qui modifient le but par effet de bord et renvoie en même temps des données (e.g. intro pourrait retourner le nom créé)

...

Divers

Guillaume: transformer le wrapper gappa de dp en plugin.