Update inner types of Oracles (PQ branch)
- remplacer le type
type channel = { cname : string }
par
type oracle =
{ oname : string;
oindices_type : param list;
oargs_type : typet list;
oreturn_type : typet list option }
Variantes possibles: oindices_type : typet list (en sachant que le type est forcément intervalle; peut-être plus simple pour les comparaisons de types). Ou remplacer les 3 derniers champs par otype : typet list * typet list * typet list option comme dans le type oracle_struct.
(Note: j'hésite un peu à mettre oindices : repl_index list à la place de oindices_type : param list Inconvénient : cela oblige toutes les définitions du même oracle à être sous des réplications avec les même indices, et non seulement à être sous des réplications avec des indices du même type. Mais on a déjà cette limitation pour les variables : le type binder contient args_at_creation : repl_index list; qui oblige toutes les définitions d'une même variable à être sous des réplications avec les mêmes indices... A priori, je dirais que je préfère oindices_type.
Autre note: on peut envisager des mettre les champs oindices_type, oargs_type, oreturn_type mutables si leur contenu n'est pas connu au moment où on crée l'oracle.)
-
dans le type inputprocess_desc, remplacer | Input of (channel * term list) * pattern * process par | OracleDecl of oracle * pattern list * process ("pattern list" est un découpage de la "pattern" de l'Input, qui actuellement est toujours un n-uplet. Les indices de réplication sont toujours les indices courants, donc je pense que ce n'est pas la peine de les mentionner comme argument de OracleDecl.)
-
dans le type process_desc, remplacer | Output of (channel * term list) * term * inputprocess par | Return of term list * inputprocess (Le "term list" est un découpage du "term" de l'Output, qui actuellement est toujours un n-uplet; la partie canal "(channel * term list)" disparaît.)