Formel/gen_syst.mli

   1 (*TeX
   2   \subsection{Module Gen\_syst}
   3   \subssubsection{Interface}
   4 *)
   5 (* DEBUG type expr;; *)
   6 type expr =
   7   | FORM of Forme.forme
   8   | MOD of modulo
   9   | DIV of division
  10   | NAE of non_aff_expr
  11 and non_aff_expr = {nae_operator : string; nae_args : expr list}
  12 and modulo = {mod_expr : expr; modulus : expr}
  13 and division = {div_expr : expr; divisor : expr};;
  14
  15 val eq_expr : expr -> expr -> bool;;
  16 val lt_expr : expr -> expr -> bool;;
  17 val leq_expr : expr -> expr -> bool;;
  18 val sort_args : expr list -> expr list;;
  19 (* FIN DEBUG *)
  20 type gen_ineq;;
  21 type gen_syst = gen_ineq list;;
  22
  23 val expr_of_forme : Forme.forme -> expr;;
  24 val add_expr : expr -> expr -> expr;;
  25 val add_expr_list : expr list -> expr;;
  26 val sub_expr : expr -> expr -> expr;;
  27 val sub_expr_list : expr list -> expr;;
  28 val minus_expr : expr -> expr;;
  29 val mult_expr : expr -> expr -> expr;;
  30 val mult_expr_list : expr list -> expr;;
  31 val div_expr : expr -> expr -> expr;;
  32 val div_expr_list : expr list -> expr;;
  33 val quo_expr : expr -> expr -> expr;;
  34 val mod_expr : expr -> expr -> expr;;
  35 val gen_expr : string -> expr list -> expr;;
  36 val destructor : expr -> string * expr list;;
  37
  38 val make_ineq_eq : expr -> expr -> gen_ineq;;
  39 val make_ineq_le : expr -> expr -> gen_ineq;;
  40 val make_ineq_lt : expr -> expr -> gen_ineq;;
  41 val make_ineq_ge : expr -> expr -> gen_ineq;;
  42 val make_ineq_gt : expr -> expr -> gen_ineq;;
  43
  44 val ineq_e_of_t : gen_ineq -> gen_ineq;;
  45 val ineq_t_of_e : gen_ineq -> gen_ineq;;
  46 val not_ineq : gen_ineq -> gen_ineq;;
  47
  48 exception Non_linear of expr;;
  49
  50 val expr_is_form : expr -> bool;;
  51 val form_of_expr : expr -> Forme.forme;;
  52 val gen_ineq_of_ineq : Systeme.ineq -> gen_ineq;;
  53 val ineq_of_gen_ineq : gen_ineq -> Systeme.ineq;;
  54 val norm_syst : gen_syst -> gen_syst;;
  55
  56 val ineq_is_eq : gen_ineq -> bool;;
  57 val ineq_is_ge : gen_ineq -> bool;;
  58 val ineq_is_gt : gen_ineq -> bool;;
  59 val expr_of_ineq : gen_ineq -> expr;;
  60
  61 val eq_expr : expr -> expr -> bool;;
  62 val eq_ineq : gen_ineq -> gen_ineq -> bool;;
  63
  64 val list_var_expr : expr -> string list;;
  65 val list_var_ineq : gen_ineq -> string list;;
  66 val list_var_syst : gen_syst -> string list;;
  67
  68 val subst_expr : expr -> (string * Forme.forme) list -> expr;;
  69 val subst_ineq : gen_ineq -> (string * Forme.forme) list -> gen_ineq;;
  70 val subst_syst : gen_syst -> (string * Forme.forme) list -> gen_syst;;
  71
  72 val split_gen_syst : string list -> gen_syst -> gen_syst * gen_syst;;
  73 val strict_split_gen_syst : string list -> gen_syst -> gen_syst * gen_syst;;
  74
  75 val simplify :
  76   string list -> string list -> gen_syst -> gen_syst;;
  77
  78 val simplify_vars : string list -> gen_syst -> gen_syst;;
  79
  80 val ineq_list_of_gen_syst : gen_syst -> Systeme.ineq list;;
  81 val systeme_of_gen_syst : gen_syst -> Systeme.systeme;;
  82 val gen_syst_of_systeme : Systeme.systeme -> gen_syst;;
  83
  84 (* printers *)
  85 val print_expr : expr -> unit;;
  86 val print_gen_ineq : gen_ineq -> unit;;
  87 val print_gen_syst : gen_syst -> unit;;
  88
  89
  90 (* DEBUG *)
  91 val factorize : expr -> expr;;