Formel/seltree.mli

   1 (*TeX
   2   \section{Module \module{Seltree}}
   3   On implémente ici des QUAST. Ces structures (de type \texttt{ARBRE})
   4   sont paramétrées par une structure de type \texttt{TAG} qui
   5   représente une étiquette caractérisant chaque feuille. Sont définis
   6   ici les modules \module{NoTag} et \module{Quast} représentant les
   7   QUAST ordinaires sans étiquettes.
   8
   9   Un utilisateur voulant créer un nouveau type d'étiquette devra créer
  10   un module \module{MyTag} du type \texttt{TAG} caractérisant ces
  11   étiquettes. Il obtiendra les QUAST étiquetés correspondants à ces
  12   étiquettes par l'appel : \texttt{module MyQuast =
  13   Make\_arbre(MyTag)}.
  14   \subsection{Signature}
  15   Le type de modules \texttt{TAG} définit les fonctions obligatoires
  16   de manipulation des étiquettes. On doit pouvoir comparer des
  17   étiquettes (fonction \texttt{eq}), y faire une substitution de
  18   variables (fonction \texttt{subst}), en obtenir la liste des
  19   variables (fonction \texttt{liste\_var}), les imprimer avec un
  20   imprimeur de la bibliothèque \module{Format} (fonction
  21   \texttt{print}). La fonction \texttt{minmax} permet de gérer le
  22   minimum et le maximum de deux feuilles étiquetées. Elle prend un
  23   argument entier qui précise la situation (on notera $f_1$ la feuille
  24   correspondant au premier argument et $f_2$ celle du deuxième) :
  25
  26   \begin{tabular}{|c|l|}
  27     \hline
  28     $0$ & égalité de $f_1$ et  $f_2$\\
  29     $1$ & choix de $f_2$\\
  30     $-1$ & choix de $f_1$\\
  31     $2$ & maximum, $f_1$ de dimension inférieure à $f_2$\\
  32     $-2$ & minimum, $f_1$ de dimension inférieure à $f_2$\\
  33     $3$ & maximum, $f_1$ de dimension supérieure à $f_2$\\
  34     $-3$ & minimum, $f_1$ de dimension supérieure à $f_2$\\
  35     \hline
  36   \end{tabular}
  37 *)
  38 open Num
  39 open Forme
  40 open Systeme
  41 module type TAG =
  42   sig
  43     type t
  44     val eq : t -> t -> bool
  45     val subst : t -> (string * Forme.forme) list -> t
  46     val list_var : t -> string list
  47     val minmax : t -> t -> int -> t
  48     val print : t -> unit
  49     val help : unit -> unit
  50   end;;
  51
  52 (*TeX
  53   Le type de modules \texttt{ARBRE} définit les fonctions disponibles
  54   affectant les QUAST étiquetés. Le type \texttt{tag} est ici abstrait
  55   mais est destiné à être instancié par le type \texttt{t} d'un module
  56   de type \texttt{TAG}.
  57 *)
  58 module type ARBRE =
  59   sig
  60     type tag
  61     type feuille = { point: forme list; tag: tag }
  62     type branchement =
  63       { predicat: forme;
  64         biais: num;
  65         sup: quast;
  66         inf: quast }
  67     and quast = Cond of branchement | Feuille of feuille | Bottom
  68     val quast_of_branchement : branchement -> quast
  69     val make_branchement :
  70       forme -> num -> quast -> quast -> branchement
  71     val eq_branchement : branchement -> branchement -> bool
  72     val eq : quast -> quast -> bool
  73 (*TeX
  74   La fonction \texttt{normalise} met un \texttt{quast} sous une forme
  75   normale. Ce processus permet des comparaisons plus précises par la
  76   fonction \texttt{equal}. Mais attention, la normalisation peut
  77   entraîner une explosion exponentielle de la taille du
  78   \texttt{quast}. Son utilisation est donc dangereuse. Cette fonction
  79   n'est utilisée que par \texttt{equal}.
  80 *)
  81     val normalise : quast -> quast
  82     val equal : quast -> quast -> bool
  83 (*TeX
  84   La fonction \texttt{liste\_var} retourne la liste des variables
  85   apparaissant dans son argument (étiquettes comprises).
  86 *)
  87     val liste_var : quast -> string list
  88 (*TeX
  89   La fonction \code{tronque} limite la taille des listes de formes
  90   d'un quast.
  91 *)
  92     val tronque : quast -> int -> quast
  93 (*TeX
  94   La fonction\texttt{to\_systeme} retourne la liste des contextes de chaque
  95   feuille, le systeme représentant le chemin parcouru dans l'arbre
  96   pour arriver à la feuille. Tous ces systèmes sont combinés aux
  97   contexte passé en premier argument.
  98 *)
  99     val to_systeme : Gen_syst.gen_syst -> quast -> Gen_syst.gen_syst list
 100     val flatten : Gen_syst.gen_syst -> quast -> (Gen_syst.gen_syst * feuille) list
 101 (*TeX
 102   La fonction \texttt{simpl} simplifie un quast en en supprimant
 103   certaines branches inaccessibles dans un contexte passé en argument
 104   (le \texttt{systeme}). Les tests effectués sont triviaux et la
 105   simplification est donc limitée. Le module \module{Tree\_pip}
 106   propose une simplification plus poussée mais plus coûteuse car
 107   faisant appel à \pip (voir page~\pageref{simplifie}).
 108 *)
 109     val simpl : systeme -> quast -> quast
 110     val simpl_withcontextquast : systeme -> quast -> quast -> quast
 111 (*TeX
 112   La fonction \texttt{subst} substitue des variables par de formes
 113   affines dans un \texttt{quast}.
 114 *)
 115     val subst : quast -> (string * forme) list -> quast
 116 (*TeX
 117   La fonction \texttt{map} applique une fonction à toutes les
 118   \texttt{Feuille}s d'un \texttt{quast}.
 119 *)
 120     val map : (feuille -> quast) -> quast -> quast
 121 (*TeX
 122   Les fonctions \texttt{min} et \texttt{max} calculent le minimum et
 123   le maximum de deux \texttt{quast}s dans un contexte donné par le
 124   premier argument.
 125 *)
 126     val min : systeme -> quast -> quast -> quast
 127     val max : systeme -> quast -> quast -> quast
 128     val min_withcontextquast : systeme -> quast -> quast -> quast -> quast
 129     val max_withcontextquast : systeme -> quast -> quast -> quast -> quast
 130
 131 (*TeX
 132   \texttt{print} imprime un \texttt{quast} avec la bibliothèque
 133   \module{Format}.
 134 *)
 135     val print : quast -> unit
 136   end;;
 137
 138 (*TeX
 139   Le foncteur \texttt{Make\_arbre} construit un module de QUAST
 140   étiquetés par son argument.
 141 *)
 142 module type MAKE_ARBRE =
 143   functor(T : TAG) -> (ARBRE with type tag = T.t);;
 144
 145 module Make_arbre : MAKE_ARBRE;;
 146
 147 (*TeX
 148   Cas particulier des QUAST ordinaires (sans tags).
 149 *)
 150 module NoTag : (TAG with type t = unit);;
 151
 152 module Quast : (ARBRE with type tag = NoTag.t);;
 153