Formel/eseltree.mli

   1 (*TeX
   2   \section{Module \module{Eseltree}}
   3   On définit ici des QUAST étendus, c'est-à-dire des QUAST avec des
   4   paramètres définis par une forme affine modulo un entier. Ces
   5   structures sont définies car elles sont le résultat de \pip. Comme
   6   lors de la définition des QUAST (module \module{Seltree}) on a
   7   paramétré les \texttt{ARBRE}s par des \texttt{TAG}s, on paramètre
   8   ici les \texttt{EARBRE}s par des \texttt{ARBRE}s.
   9
  10   \subsection{Signature}
  11 *)
  12 open Num;;
  13 open Forme;;
  14 open Systeme;;
  15 open Seltree;;
  16 open Gen_syst;;
  17
  18 (*TeX
  19   Définissons d'abord les paramètres. Le type \texttt{New\_par.t} est
  20   un ensemble d'associations de noms (chaînes de caractères) et de
  21   paramètres qu'on peut manipuler de diverses façons. On peut y
  22   ajouter un élément (fonction \texttt{New\_par.add}), y rechercher la
  23   valeur d'un nom (fonction \texttt{New\_par.find}), en effacer un nom
  24   (fonction \texttt{New\_par.remove}) ou le combiner, en faire l'union
  25   avec un autre ensemble (fonction \texttt{New\_par.combine}). On a de
  26   plus la possibilité de transformer un paramètre ou unensemble de
  27   paramètres en un système d'inéquations équivalent avec les fonctions
  28   \texttt{systeme\_of\_divi} et \texttt{systeme\_of\_np}.
  29 *)
  30 module New_par :
  31   sig
  32     type divi = {lin : forme; div : num};;
  33     type t;;
  34     val make_divi : forme -> num -> divi;;
  35     val simpl_divi : divi -> divi;;
  36     val empty : t;;
  37     val add : string -> divi -> t -> t;;
  38     val find : string -> t -> divi;;
  39     val remove : string -> t -> t;;
  40     val iter : (string -> divi -> unit) -> t -> unit
  41     val fold : (string -> divi -> 'b -> 'b) -> t -> 'b -> 'b
  42     val combine : t -> t -> t;;
  43     val expr_of_divi : divi -> expr
  44     val ineq_of_divi : string -> divi -> gen_ineq
  45     val systeme_of_divi : string -> divi -> gen_syst;;
  46     val systeme_of_np : t -> gen_syst;;
  47
  48     val print_divi : divi -> unit;;
  49     val print_new_par : t -> unit;;
  50   end;;
  51
  52 (*TeX
  53   Le type de module \texttt{EARBRE} propose en plus des fonctions du
  54   même nom du type de module \texttt{ARBRE} quelques fonctions
  55   manipulant les paramètres :
  56   \begin{itemize}
  57     \item on ajoute un paramètre avec \texttt{add\_np} ;
  58     \item \texttt{unifie} permet de regrouper sous un même nom les
  59     paramètres ayant la même valeur, ce qui permet plus de
  60     simplifications ;
  61     \item \texttt{liste\_var\_np} retourne la liste des variables
  62     apparaissant dans les paramètres.
  63   \end{itemize}
  64 *)
  65 module type EARBRE =
  66   sig
  67     type arbre;;
  68     type feuille;;
  69     type earbre = {qu : arbre; np : New_par.t};;
  70
  71     val earbre_of_quast : arbre -> earbre;;
  72
  73     val subst : earbre -> (string * forme) list -> earbre;;
  74
  75     val add_np : string -> New_par.divi -> earbre -> earbre;;
  76
  77     val unifie : earbre -> earbre;;
  78
  79     val simpl : systeme -> earbre -> earbre;;
  80     val simpl_withcontextquast : systeme -> arbre -> earbre -> earbre;;
  81
  82     val liste_var_np : earbre -> string list;;
  83     val liste_var_earbre : earbre -> string list;;
  84     val tronque : earbre -> int -> earbre;;
  85
  86 (*TeX
  87   La fonction \texttt{mapq\_earbre} correspond à la fonction
  88   \texttt{map} du type de modules \texttt{ARBRE}.
  89 *)
  90     val mapq_earbre :
  91       (feuille -> arbre) -> earbre -> earbre;;
  92
  93     val branche_earbre : forme -> num -> earbre -> earbre -> earbre;;
  94
  95     val min : systeme -> earbre -> earbre -> earbre;;
  96     val max : systeme -> earbre -> earbre -> earbre;;
  97     val min_withcontextquast : systeme -> arbre -> earbre -> earbre -> earbre;;
  98     val max_withcontextquast : systeme -> arbre -> earbre -> earbre -> earbre;;
  99
 100 (*TeX
 101   Les trois fonctions suivantes sont des fonctions utilitaires pour le
 102   module \module{Pip}. \texttt{part\_ent} simplifie les paramètres
 103   alors qu'ils sont encore sous forme de division entière, elle
 104   factorise la partie entière. \texttt{subst\_earbre\_div} fait la
 105   même chose que \texttt{subst\_earbre} lorsque les paramètres sont
 106   des divisions entières. Enfin, \texttt{mod\_of\_div} transforme la
 107   reprèsentation par divisions entières en celle par modulos qui lui
 108   est équivalente mais simplifie les calculs suivants (en particulier
 109   la simplification de QUAST étendus).
 110 *)
 111     val part_ent : earbre -> earbre;;
 112     val subst_earbre_div : earbre -> (string * forme) list -> earbre;;
 113     val mod_of_div : earbre -> earbre;;
 114
 115     val print : earbre -> unit;;
 116   end;;
 117
 118 (*TeX
 119   Le foncteur \module{Etend} de type \texttt{ETEND} prend comme
 120   argument un module de type \texttt{ARBRE} et retourne un module de
 121   type \texttt{EARBRE} qui implémente les QUAST étendus avec les mêmes
 122   étiquettes que les QUAST du module argument.
 123 *)
 124 module type ETEND =
 125   functor(A : ARBRE) ->
 126     (EARBRE with type arbre = A.quast
 127             and type feuille = A.feuille);;
 128
 129 module Etend : ETEND;;
 130
 131 (*TeX
 132  Cas particulier : QUAST étendus sans tags, c'est le résultat de \pip.
 133 *)
 134 module Equast : (EARBRE with type arbre = Quast.quast
 135                         and type feuille = Quast.feuille);;