sort generating system before printing

[sppoc.git] / Formel / gen_syst.ml

(*TeX
  \subsection{Implementation}
*)
open Forme;;
open Systeme;;
open Num;;
open Util.Nums;;
open Util.Lists;;

(*TeX
  \subsubsection{Type definitions}
*)
type expr =
  | FORM of forme
  | MOD of modulo
  | DIV of division
  | NAE of non_aff_expr
and non_aff_expr = {nae_operator : string; nae_args : expr list}
and modulo = {mod_expr : expr; modulus : expr}
and division = {div_expr : expr; divisor : expr};;

type gen_ineq = 
  | Strict of expr (* expr > 0 *)
  | Large of expr (* expr >= 0 *)
  | Eq of expr  (* expr = 0 *)
;;

type gen_syst = gen_ineq list;;

exception Non_linear of expr;;

(*TeX
  Comparison functions.
*)
let rec eq_expr e e' = match e, e' with
  | FORM f, FORM f' -> eq_forme f f'
  | MOD {mod_expr = me; modulus = m},
    MOD {mod_expr = me'; modulus = m'} -> 
      eq_expr m m' && eq_expr me me'
  | DIV {div_expr = de; divisor = d},
    DIV {div_expr = de'; divisor = d'} -> 
      eq_expr d d' && eq_expr de de'
  | NAE {nae_operator = op; nae_args = a},
    NAE {nae_operator = op'; nae_args = a'} ->
      op = op' && (eq_lists eq_expr a a')
  | _ -> false;;

let lt_lists lt_fun l l' =
  let rec iter = function
    | (e, e')::t ->
        if lt_fun e e' then true
        else if lt_fun e' e then false
        else iter t
    | [] -> false
  in
    if (List.length l) < (List.length l') then true
    else if (List.length l) = (List.length l') then
      iter (List.combine l l')
    else false;;

let rec lt_expr e e' = match e, e' with
  | FORM f, FORM f' -> lt_forme f f'
  | FORM _, _ -> true
  | _, FORM _ -> false
  | MOD {mod_expr = me; modulus = m},
    MOD {mod_expr = me'; modulus = m'} -> 
      lt_expr m m' || eq_expr m m' && lt_expr me me'
  | MOD _ , _ -> true
  | _, MOD _ -> false
  | DIV {div_expr = de; divisor = d},
    DIV {div_expr = de'; divisor = d'} -> 
      lt_expr d d' || eq_expr d d' && eq_expr de de'
  | DIV _, _ -> true
  | _, DIV _ -> false
  | NAE {nae_operator = op; nae_args = a},
    NAE {nae_operator = op'; nae_args = a'} ->
      op < op' || op = op' && (lt_lists lt_expr a a');;

let leq_expr e e' = lt_expr e e' || eq_expr e e';;

let sort_args l = Sort.list leq_expr l;;

(*TeX
  \subsubsection{Expression simplification}
*)
let expr_is_form = function
  | FORM _ -> true
  | _ -> false;;

let rec form_of_expr = function
  | FORM f -> f
  | NAE {nae_operator = _; nae_args = el} as e -> 
      ignore (List.map form_of_expr el);
      raise (Non_linear e)
  | e -> raise (Non_linear e);;

let modularify_forme f m =
  let fm = (forme_of_terme_list 
              (List.map 
                 (fun t -> let c = terme_get_coef t in
                    if (mod_num c m =/ zero) then
                      terme_of_num zero
                    else t)
                 (forme_to_terme_list f))) in
    if forme_is_num fm then
      FORM (forme_of_num (mod_num (get_const fm) m))
    else MOD {mod_expr = FORM fm; modulus = FORM (forme_of_num m)};;

let divide_forme f d =
  if forme_is_num f
  then FORM (forme_of_num (quo_num (get_const f) d))
  else
    begin match List.partition 
      (fun t -> mod_num (terme_get_coef t) d =/ zero)
      (forme_to_terme_list f) with
        | dt, [] -> FORM ((forme_of_terme_list dt) /| d)
        | [], ndt -> DIV {div_expr = FORM (forme_of_terme_list ndt);
                          divisor = FORM (forme_of_num d)}
        | dt, ndt -> 
            NAE {nae_operator = "+";
                 nae_args = [FORM ((forme_of_terme_list dt) /| d);
                             DIV {div_expr = FORM (forme_of_terme_list ndt);
                                  divisor = FORM (forme_of_num d)}]}
    end;;

let rec negate_formified_expression = function
  | FORM f -> FORM (minus_forme f)
  | MOD m -> NAE {nae_operator = "-"; nae_args = [MOD m]}
  | DIV d -> NAE {nae_operator = "-"; nae_args = [DIV d]}
  | NAE {nae_operator = op; nae_args = args} as nae -> 
      begin match op with
        | "+" -> NAE {nae_operator = "+";
                      nae_args = sort_args (List.map 
                                              negate_formified_expression 
                                              args)}
        | "-" -> 
            begin match args with
              | [] -> invalid_arg "Gen_syst.negate_formified_expression"
              | [e] -> e
              | h::t -> NAE {nae_operator = "+";
                             nae_args = 
                               (negate_formified_expression h)::t}
            end
        | "*" -> 
            begin match args with
              | [] -> invalid_arg "Gen_syst.negate_formified_expression"
              | [e] -> negate_formified_expression e
              | h::t -> NAE {nae_operator = "*";
                             nae_args = 
                               sort_args 
                                 ((negate_formified_expression h)::t)}
            end
        | "/" ->
            begin match args with
              | [] -> invalid_arg "Gen_syst.negate_formified_expression"
              | [e] -> negate_formified_expression e
              | h::t -> NAE {nae_operator = "/";
                             nae_args = 
                               (negate_formified_expression h)::t}
            end
        | _ -> NAE {nae_operator = "-";
                    nae_args = [nae]}
      end;;

let rec flatten_mult_args = function
  | [] -> []
  | NAE {nae_operator = "*"; nae_args = el}::t ->
      el@(flatten_mult_args t)
  | h::t -> h::(flatten_mult_args t);;

let powerify_mults = function
  | [] -> []
  | h::t ->
      let make_power e n =
        if n = 1 then e
        else NAE {nae_operator = "**";
                  nae_args = [e; FORM (forme_of_num
                                         (Num.num_of_int n))]} in
      let rec build_freq e n = function
        | e'::r when eq_expr e e' -> build_freq e (succ n) r
        | e'::r -> (make_power e n)::(build_freq e' 1 r)
        | [] -> [make_power e n] in
        build_freq h 1 t;;

let mult_formified_expressions el =
  match List.partition expr_is_form 
    (powerify_mults (sort_args (flatten_mult_args el))) with
    | fe, [] -> 
        begin match List.partition forme_is_num 
          (List.map form_of_expr fe) with
            | l, [] ->
                FORM (forme_of_num 
                        (List.fold_right mult_num
                           (List.map get_const l) un))
            | l, [f] ->
                FORM (List.fold_left mult_forme f
                        (List.map get_const l))
            | l, h::t ->
                NAE {nae_operator = "*";
                     nae_args = 
                       sort_args 
                         ((FORM (List.fold_left mult_forme h
                                   (List.map get_const l)))
                          ::(List.map (fun f -> FORM f) t))}
        end
    | [], [nf] -> nf
    | [], nfe -> NAE {nae_operator = "*";
                      nae_args = sort_args nfe}
    | fe, nfe ->
        begin match List.partition forme_is_num 
          (List.map form_of_expr fe) with
            | l, [] ->
                let n = (List.fold_right mult_num
                           (List.map get_const l) un) in
                  NAE {nae_operator = "*";
                       nae_args =
                         if n =/ un then sort_args nfe
                         else if n =/ moins_un then
                           begin match nfe with
                             | h::t -> 
                                 sort_args ((negate_formified_expression h)::t)
                             | _ ->
                                 failwith 
                                   "Gen_syst.mult_formified_expressions"
                           end
                         else sort_args ((FORM (forme_of_num n))::nfe)}
            | l, [f] ->
                NAE {nae_operator = "*";
                     nae_args =
                       sort_args ((FORM (List.fold_left mult_forme f
                                           (List.map get_const l)))
                                  ::nfe)}
            | l, h::t ->
                NAE {nae_operator = "*";
                     nae_args = 
                       sort_args (((FORM (List.fold_left mult_forme h
                                            (List.map get_const l)))
                                   ::(List.map (fun f -> FORM f) t))@nfe)}
        end;;

let div_formified_expressions = function
  | e::e'::r as el -> 
      begin match List.partition 
        (fun e -> expr_is_form e
           && forme_is_num (form_of_expr e)) (e'::r) with
          | ne, [] ->
              if expr_is_form e 
              then FORM (List.fold_left div_forme 
                           (form_of_expr e)
                           (List.map (fun e -> get_const
                                          (form_of_expr e)) ne))
              else let n = List.fold_left mult_num un
                             (List.map (fun e -> get_const
                                            (form_of_expr e)) ne) in
                if n =/ un then e
                else if n =/ moins_un 
                then negate_formified_expression e
                else NAE {nae_operator = "*";
                          nae_args = (sort_args [FORM (forme_of_num (un // n)); e])}
          | [], nne -> NAE {nae_operator = "/";
                            nae_args = e::(sort_args nne)}
          | ne, nne -> 
              if expr_is_form e 
              then NAE {nae_operator = "/";
                        nae_args =
                          (FORM (List.fold_left div_forme 
                                   (form_of_expr e)
                                   (List.map 
                                      (fun e -> get_const
                                           (form_of_expr e)) ne)))
                          ::(sort_args nne)}
              else let n = List.fold_left mult_num un
                             (List.map (fun e -> get_const
                                            (form_of_expr e)) ne) in
                if n =/ un
                then NAE {nae_operator = "/";
                          nae_args = e::(sort_args nne)}
                else if n =/ moins_un 
                then NAE {nae_operator = "/";
                          nae_args = (negate_formified_expression e)
                                     ::(sort_args nne)}
                else NAE {nae_operator = "/";
                          nae_args = e::(sort_args ((FORM (forme_of_num n))::nne))}
      end
  | _ -> invalid_arg "Gen_syst.div_formified_expressions";;

let power_formified_expressions e e' =
  if (expr_is_form e') && (forme_is_num (form_of_expr e'))
  then
    if (get_const (form_of_expr e')) = zero
    then FORM (forme_of_num un)
    else
      if (get_const (form_of_expr e')) = un
      then e
      else
        if (expr_is_form e) && (forme_is_num (form_of_expr e))
        then FORM (forme_of_num (power_num 
                                   (get_const (form_of_expr e))
                                   (get_const (form_of_expr e'))))
        else NAE {nae_operator = "**"; nae_args = [e; e']}
  else NAE {nae_operator = "**"; nae_args = [e; e']};;

let rec flatten_sums = function
  | (NAE {nae_operator = "+";
          nae_args = el})::t -> (flatten_sums el)@(flatten_sums t)
  | e::t -> e::(flatten_sums t)
  | [] -> []

let sum_exprs el =
  let name = ref ""
  and new_var () = Util.Name.gen "s" in
  let rec make_term_list tl defs el = 
    let check e c t =
      name := "";
      List.iter (fun (v, e') ->
                   if eq_expr e e' then name := v) defs;
      if !name = ""
      then begin
        List.iter (fun (v, e') ->
                     if eq_expr (negate_formified_expression e) e'
                     then name := v) defs;
        if !name = ""
        then begin
          name := new_var ();
          make_term_list ((make_terme !name c)::tl)
            ((!name, e)::defs) t
        end else
          make_term_list ((make_terme !name (minus_num c))::tl) defs t
      end else 
        make_term_list ((make_terme !name c)::tl) defs t
    in match el with
      | [] -> (forme_to_terme_list (forme_of_terme_list tl)), defs
      | (NAE {nae_operator = "*";
              nae_args = [FORM f; e]})::t when forme_is_num f ->
          check e (get_const f) t
      | h::t -> check h un t
  and rebuild defs tl = 
    List.map (fun t -> 
                let c, v = (terme_get_coef t), (terme_get_var t)
                in if c =/ un then List.assoc v defs
                  else if c =/ moins_un
                  then (negate_formified_expression 
                          (List.assoc v defs))
                  else mult_formified_expressions
                    [FORM (forme_of_num c);
                     List.assoc v defs]) tl
  in 
  let tl, defs = make_term_list [] [] el in
    rebuild defs tl;;

let add_formified_expressions el =
  match List.partition expr_is_form (flatten_sums el) with
    | fe, [] -> 
        FORM (List.fold_right 
                add_forme 
                (List.map form_of_expr fe) 
                (forme_of_num zero))
    | [], nfe -> 
        begin match sum_exprs nfe with
          | [] -> FORM (forme_of_num zero)
          | [e] -> e
          | s -> NAE {nae_operator = "+";
                      nae_args = sort_args s}
        end
    | fe, nfe ->
        let f = List.fold_right add_forme 
                  (List.map form_of_expr fe) 
                  (forme_of_num zero) in
          begin match sum_exprs nfe with
            | [] -> FORM f
            | [e] ->
                if forme_is_num f && (get_const f) =/ zero
                then e
                else NAE {nae_operator = "+";
                          nae_args = sort_args [FORM f; e]}
            | s -> 
                NAE {nae_operator = "+";
                     nae_args = 
                       if forme_is_num f && (get_const f) =/ zero
                       then sort_args s
                       else sort_args ((FORM f)::s)}
          end;;

let factorize = function
  | NAE {nae_operator = "+";
         nae_args = el} as sumexpr -> begin
      let build_sub_exprs = function
        | NAE {nae_operator = "*";
               nae_args = l} -> l
        | e -> [e] in
      let sub_exprs = Sort.list leq_expr 
                        (List.flatten (List.map build_sub_exprs el)) in
      let rec build_freq e n = function
        | e'::r when eq_expr e e' -> build_freq e (succ n) r
        | e'::r -> (e,n)::(build_freq e' 1 r)
        | [] -> [(e,n)] in
      let choose = function
        | [] -> None
        | (_,1)::_ -> None
        | (e,_)::_ -> Some e in
        match choose 
          (Sort.list
             (fun (e,n) (e',n') -> n > n' || (n = n' && (lt_expr e' e)))
             (build_freq (List.hd sub_exprs) 0 sub_exprs)) with
            | None -> sumexpr
            | Some factor -> begin
                let fact = function
                  | NAE {nae_operator = "*"; nae_args = el} 
                      when generic_mem eq_expr factor el ->
                      begin 
                        match
                          generic_remove_first eq_expr factor el
                        with
                          | [] -> Some (FORM (forme_of_num un)), None
                          | [e] -> Some e, None
                          | l -> Some (mult_formified_expressions
                                         (sort_args l)), None
                      end
                  | e when eq_expr factor e -> 
                      Some (FORM (forme_of_num un)), None
                  | e -> None, Some e in
                let rec split_and_remove_options = function
                  | (None, None)::t -> assert false
                  | (None, Some h)::t ->
                      let t1,t2 = split_and_remove_options t in
                        t1, (h::t2)
                  | (Some h, None)::t  ->
                      let t1,t2 = split_and_remove_options t in
                        (h::t1), t2
                  | (Some h1, Some h2)::t  ->
                      let t1,t2 = split_and_remove_options t in
                        (h1::t1), (h2::t2)
                  | [] -> [], [] in
                  match split_and_remove_options (List.map fact el) with
                    | [], _ -> assert false
                    | [e], [] -> mult_formified_expressions 
                          (sort_args [factor;e])
                    | [e], l -> add_formified_expressions
                          (sort_args 
                             ((mult_formified_expressions
                                 (sort_args [factor;e]))::l))
                    | l, [] -> mult_formified_expressions
                          (sort_args [factor;
                                      add_formified_expressions
                                        (sort_args l)])
                    | l, l' -> add_formified_expressions
                          (sort_args 
                             ((mult_formified_expressions
                                 (sort_args 
                                    [factor;
                                     add_formified_expressions
                                       (sort_args l)]))::l'))
              end
    end
  | e -> e;;

(*TeX
  formify\_expr is the main simplification function. It computes all
  the available linear forms.
*)
let rec formify_step formify_args = function
  | FORM f -> FORM f
  | MOD {mod_expr = e; modulus = m} ->
      let e' = formify_args e 
      and m' = formify_args m in
        if (expr_is_form e') && (expr_is_form m')
          && (forme_is_num (form_of_expr m'))
        then modularify_forme 
          (form_of_expr e') 
          (get_const (form_of_expr m'))
        else MOD {mod_expr = e'; modulus = m'}
  | DIV {div_expr = e; divisor = d} ->
      let e' = formify_args e 
      and d' = formify_args d in
        if (expr_is_form e') && (expr_is_form d')
          && (forme_is_num (form_of_expr d'))
        then divide_forme 
          (form_of_expr e') 
          (get_const (form_of_expr d'))
        else DIV {div_expr = e'; divisor = d'}
  | NAE nae -> formify_nae formify_args nae
and formify_nae formify_args {nae_operator = op; nae_args = args} =
  let fargs = List.map formify_args args in
    match op with
      | "+" -> factorize (add_formified_expressions (sort_args fargs))
      | "-" ->
          begin match fargs with
            | [] -> invalid_arg "Gen_syst.formify_nae"
            | [e] -> negate_formified_expression e
            | h::t -> add_formified_expressions 
                  (h::(List.map negate_formified_expression t))
          end
      | "*" -> mult_formified_expressions (sort_args fargs)
      | "/" -> div_formified_expressions fargs
      | "**" ->
          begin match fargs with
            | [e;e'] -> power_formified_expressions e e'
            | _ -> invalid_arg "Gen_syst.formify_nae"
          end
      | op -> NAE {nae_operator = op; nae_args = fargs};;

let rec formify_expr e = formify_step formify_expr e;;
let formify_top_expr e = formify_step (fun exp -> exp) e;;

(*TeX
  \subsubsection{Constructors}
*)
let expr_of_forme f = FORM f;;

let add_expr e1 e2 =
  formify_top_expr (NAE {nae_operator = "+"; 
                               nae_args = [e1; e2]});;

let add_expr_list el =
  formify_top_expr (NAE {nae_operator = "+"; 
                         nae_args = el});;

let sub_expr e1 e2 =
  formify_top_expr (NAE {nae_operator = "-";
                         nae_args = [e1; e2]});;

let sub_expr_list el =
  if List.length el = 0 then invalid_arg "Gen_syst.sub_expr_list";
  formify_top_expr (NAE {nae_operator = "-";
                         nae_args = (List.hd el)::(sort_args (List.tl el))});;

let minus_expr e = negate_formified_expression e;;

let mult_expr e1 e2 =
  formify_top_expr (NAE {nae_operator = "*";
                         nae_args = [e1; e2]});;

let mult_expr_list el =
  formify_top_expr (NAE {nae_operator = "*";
                         nae_args = el});;

let div_expr e1 e2 =
  formify_top_expr (NAE {nae_operator = "/";
                         nae_args = [e1; e2]});;

let div_expr_list el =
  if List.length el < 2 then invalid_arg "Gen_syst.div_expr_list";
  formify_top_expr (NAE {nae_operator = "/";
                         nae_args = (List.hd el)::(sort_args (List.tl el))});;

let quo_expr e1 e2 =
  formify_top_expr (DIV {div_expr = e1; divisor = e2});;

let mod_expr e1 e2 =
  formify_top_expr (MOD {mod_expr = e1; modulus = e2});;

let gen_expr op args = 
  formify_top_expr (NAE {nae_operator = Util.Strings.remove op ' ';
                         nae_args = args});;

(*TeX
  General destructor.
*)
let destructor = function
  | NAE {nae_operator = op; nae_args = args} -> op, args
  | FORM f -> "", [(expr_of_forme f)]
  | DIV {div_expr = n; divisor = d} -> "div", [n;d]
  | MOD {mod_expr = n; modulus = d} -> "mod", [n;d];;

(*TeX
  \texttt{gen\_syst\_to\_ineq\_list}.
*)
let linearize_expr defs e = 
  let name = ref ""
  and new_var () = Util.Name.gen "e" in
  let rec make_forme defs = function
    | FORM f -> (FORM f), defs
    | MOD {mod_expr = me; modulus = FORM f} as exp ->
        if forme_is_num f 
        then
          begin
            let mf, mdefs = make_forme defs me in
            let mm = MOD {mod_expr = mf; modulus = FORM f} in
              name := "";
              List.iter 
                (fun (v, e) -> if eq_expr mm e then name := v) defs;
              if !name = "" then begin
                List.iter
                  (fun (v, e) -> 
                   if eq_expr (negate_formified_expression mm) e 
                   then name := v) defs;
                if !name = "" then begin
                  name := new_var ();
                  FORM (forme_of_string !name), ((!name, mm)::mdefs)
                end else 
                  FORM (minus_forme (forme_of_string !name)), mdefs
              end else
                FORM (forme_of_string !name), mdefs
          end 
        else raise (Non_linear exp)
    | DIV {div_expr = de; divisor = FORM f} as exp ->
        if forme_is_num f 
        then
          begin
            let df, mdefs = make_forme defs de in
            let dd = DIV {div_expr = df; divisor = FORM f} in
              name := "";
              List.iter 
                (fun (v, e) -> if eq_expr dd e then name := v) defs;
              if !name = "" then begin
                List.iter
                  (fun (v, e) -> 
                   if eq_expr (negate_formified_expression dd) e 
                   then name := v) defs;
                if !name = "" then begin
                  name := new_var ();
                  FORM (forme_of_string !name), ((!name, dd)::mdefs)
                end else 
                  FORM (minus_forme (forme_of_string !name)), mdefs
              end else
                FORM (forme_of_string !name), mdefs
          end 
        else raise (Non_linear exp)
    | NAE {nae_operator = op; nae_args = el} as exp ->
        let defs', el' = List.fold_right 
                           (fun e (defs, el') -> 
                              let e', defs' = make_forme defs e in
                                defs', (e'::el'))
                           el (defs, [])
        in let f = formify_expr (NAE {nae_operator = op; nae_args = el'})
        in 
          (FORM (form_of_expr f)), defs'
    | exp -> raise (Non_linear exp)
  in
    make_forme defs e;;

let linearize_ineq defs = function
  | Large e -> 
      let e', defs' = linearize_expr defs e in
        (Large e'), defs'
  | Strict e ->
      let e', defs' = linearize_expr defs e in
        (Strict e'), defs'
  | Eq e -> begin
      match e with
        | NAE {nae_operator = "+";
               nae_args = [FORM v;
                           NAE {nae_operator = "-";
                                nae_args = [MOD {mod_expr = me; 
                                                 modulus = FORM f}]}]} 
            when forme_is_var v -> 
              if forme_is_num f 
              then
                let mf, mdefs = linearize_expr defs me in
                let mm = MOD {mod_expr = mf; modulus = FORM f} in
                  Eq (FORM (forme_of_num zero)), ((forme_to_var v, mm)::mdefs)
              else raise (Non_linear (MOD {mod_expr = me; modulus = FORM f}))
        | _ -> let e', defs' = linearize_expr defs e in
            (Eq e'), defs'
    end;;

let ineq_list_of_gen_syst s =
  let s', defs = List.fold_left 
                   (fun (il, d) i -> 
                      let i', d' = linearize_ineq d i in
                        (i'::il), d') ([], []) s
  in
    List.map (fun i -> match i with
                | Eq e -> make_ineq (form_of_expr e) EQ zero
                | Large e -> make_ineq (form_of_expr e) SUP zero
                | Strict e -> make_ineq (form_of_expr e) SUP un)
      (s'@
       (List.flatten 
          (List.map 
             (fun (v, e) -> match e with
                | MOD m -> 
                    let q, r = 
                      (FORM (forme_of_string (Util.Name.gen "div"))),
                      (FORM (forme_of_string v))
                    in [Eq (formify_expr 
                              (NAE {nae_operator = "+";
                                    nae_args = 
                                      [NAE {nae_operator = "*";
                                            nae_args = [m.modulus; q]};
                                       r;
                                       negate_formified_expression 
                                         m.mod_expr]}));
                        Large r;
                        Strict (formify_expr
                                  (NAE {nae_operator = "-";
                                        nae_args = [m.modulus; r]}))]
                | DIV d -> 
                    let q, r = 
                      (FORM (forme_of_string v)),
                      (FORM (forme_of_string (Util.Name.gen "mod")))
                    in [Eq (formify_expr 
                              (NAE {nae_operator = "+";
                                    nae_args = 
                                      [NAE {nae_operator = "*";
                                            nae_args = [d.divisor; q]};
                                       r;
                                       negate_formified_expression 
                                         d.div_expr]}));
                        Large r;
                        Strict (formify_expr
                                  (NAE {nae_operator = "-";
                                        nae_args = [d.divisor; r]}))]
                | e -> raise (Non_linear e))
             defs)));;

(*TeX
  Normalisation d'une inéquation.
*)
let norm_ineq = function
  | Eq (FORM f) -> Eq (FORM (div_forme f (pgcd_forme f)))
  | Strict (FORM f) -> Strict (FORM (div_forme f (pgcd_forme f)))
  | Large (FORM f) -> Large (FORM (div_forme f (pgcd_forme f)))
  | i -> i;;

let make_ineq_eq e1 e2 = norm_ineq (Eq (sub_expr e1 e2));;
let make_ineq_le e1 e2 = norm_ineq (Large (sub_expr e2 e1));;
let make_ineq_lt e1 e2 = norm_ineq (Strict (sub_expr e2 e1));;
let make_ineq_ge e1 e2 = norm_ineq (Large (sub_expr e1 e2));;
let make_ineq_gt e1 e2 = norm_ineq (Strict (sub_expr e1 e2));;

let ineq_e_of_t i = match norm_ineq i with
  | Eq e -> Eq e
  | Large e -> Large e
  | Strict e -> norm_ineq (Large (sub_expr e (FORM (forme_of_num un))));;

let ineq_t_of_e i = match norm_ineq i with
  | Eq e -> Eq e
  | Large e -> norm_ineq (Strict (add_expr e (FORM (forme_of_num un))))
  | Strict e -> Strict e;;

let not_ineq = function
  | Eq e -> invalid_arg "Gen_syst.not_ineq"
  | Large e -> Strict (minus_expr e)
  | Strict e -> Large (minus_expr e);;

let ineq_is_eq = function
  | Eq _ -> true
  | _ -> false;;

let ineq_is_ge = function
  | Large _ -> true
  | _ -> false;;

let ineq_is_gt = function
  | Strict _ -> true
  | _ -> false;;

let gen_ineq_of_ineq {in_forme = f; in_signe = s; in_biais = n} =
  match s with
    | EQ -> make_ineq_eq 
          (expr_of_forme f) 
          (expr_of_forme (forme_of_num n))
    | SUP -> make_ineq_ge
          (expr_of_forme f) 
          (expr_of_forme (forme_of_num n))
    | INF -> make_ineq_le
          (expr_of_forme f) 
          (expr_of_forme (forme_of_num n));;

let ineq_of_gen_ineq = function
  | Eq e -> make_ineq (form_of_expr e) EQ zero
  | Large e -> make_ineq (form_of_expr e) SUP zero
  | Strict e -> make_ineq (form_of_expr e) SUP un;;

let norm_syst s = (* Sort.list (>=) *) s;;

let eq_ineq i i' = match i, i' with
  | Strict e, Strict e' -> eq_expr e e'
  | Large e, Large e' -> eq_expr e e'
  | Eq e, Eq e' -> eq_expr e e' 
      or eq_expr (negate_formified_expression e) e'
      or eq_expr e (negate_formified_expression e')
  | _ -> false;;

let systeme_of_gen_syst s =
  systeme_of_ineq_list (ineq_list_of_gen_syst s);;

let gen_syst_of_systeme s =
  List.map 
    (fun {in_forme = f; in_signe = c; in_biais = n} ->
       begin match c with
         | EQ -> make_ineq_eq (FORM f) (FORM (forme_of_num n))
         | SUP -> make_ineq_ge (FORM f) (FORM (forme_of_num n))
         | INF -> make_ineq_le (FORM f) (FORM (forme_of_num n))
       end)
    (systeme_to_ineq_list s);;
                            
(*TeX
  \subsubsection{Variable manipulation}

  Itérateurs.
*)
let rec map_forme_expr f = function
    | FORM e -> FORM (f e)
    | MOD m -> MOD {mod_expr = map_forme_expr f m.mod_expr;
                    modulus = map_forme_expr f m.modulus}
    | DIV d -> DIV {div_expr = map_forme_expr f d.div_expr;
                    divisor = map_forme_expr f d.divisor}
    | NAE nae -> NAE {nae_operator = nae.nae_operator;
                      nae_args = List.map 
                                   (fun e -> map_forme_expr f e)
                                   nae.nae_args};;

let map_expr f e = formify_expr (map_forme_expr f e);;

let rec fold_expr f n = function
  | FORM e -> f n e
  | MOD m -> fold_expr f (fold_expr f n m.mod_expr) m.modulus
  | DIV d -> fold_expr f (fold_expr f n d.div_expr) d.divisor
  | NAE nae -> List.fold_left 
        (fun n' e -> fold_expr f n' e) n nae.nae_args;;

let apply_ineq f = function
  | Eq e -> Eq (f e)
  | Large e -> Large (f e)
  | Strict e -> Strict (f e);;

let list_var_expr e = 
  fold_expr (fun l f -> fusionne l (liste_var_forme f))
    [] e;;

let expr_of_ineq = function
  | Eq e -> e
  | Large e -> e
  | Strict e -> e;;

let list_var_ineq i = list_var_expr (expr_of_ineq i);;

let list_var_syst s =
  List.fold_left (fun l i -> fusionne l (list_var_ineq i))
    [] s;;

(*TeX
  Substitutions.
*)
let subst_expr e sfl = map_expr (fun f -> subst_forme f sfl) e;;

let subst_ineq i sfl = 
  norm_ineq (apply_ineq (fun e -> subst_expr e sfl) i);;

let subst_syst s sfl = 
  norm_syst (List.map (fun i -> subst_ineq i sfl) s);;

(*TeX
  Séparation en deux sous-systèmes d'un système avec d'une part les
    inéquations qui font référence à au moins une des variables de la
      liste passée en argument et les autres d'autre part.
      *)
let rec split_gen_syst l = function
  [] -> [],[]
| i::s -> let avec,sans = split_gen_syst l s
            in if (intersect (list_var_ineq i) l) = []
               then avec, (i::sans)
               else (i::avec), sans
  ;;

(*TeX
  Séparation en deux sous-systèmes d'un système avec d'une part les
    inéquations qui font référence uniquement aux variables de la
      liste passée en argument et les autres d'autre part.
      *)

let rec strict_split_gen_syst l = function
  [] -> [],[]
| i::s -> let avec,sans = strict_split_gen_syst l s
            in if (subtract (list_var_ineq i) l) = []
               then (i::avec), sans
               else avec, (i::sans)
  ;;
                                                                
(*TeX
  Structure tests and corresponding simplifications. A replacement
  function returns the simplified system and a boolean indicating if
  the inequation used for the simplification should be kept in the
  system or not. This inequation is not included in the system to be
  simplified. 
*)
let ineq_is_constant_def = function
  | Eq (FORM f) -> (List.length (liste_var_forme f)) = 1
  | _ -> false;;

let replace_constant_def iv i s = match i with 
  | Eq (FORM f) -> 
      let v = List.hd (liste_var_forme f) in
      let c = (minus_num (get_const f)) // (get_coef v f) in
        (subst_syst s [v, forme_of_num c]), not (List.mem v iv)
  | _ -> invalid_arg "Gen_syst.replace_constant_def";;

let ineq_is_scale = function
  | Eq (FORM f) ->
      (List.length (liste_var_forme f) = 2)
      && (get_const f =/ zero)
  | _ -> false;;

let replace_scale iv tv p i s = match i with
  | Eq (FORM f) ->
      let v, v' = match liste_var_forme f with
        | [v1; v2] -> 
            if List.mem v1 iv then v1, v2
            else if List.mem v2 iv then v2, v1
            else if List.mem v1 p && List.mem v2 tv then v2, v1
            else v1, v2
        | _ -> invalid_arg "Gen_syst.replace_scale"
      in let sf = div_forme 
                    (((forme_of_string v') *| (get_coef v' f))
                     +| (forme_of_num (get_const f)))
                    (minus_num (get_coef v f))
      in (subst_syst s [v, sf]), not (List.mem v iv)
  | _ -> invalid_arg "Gen_syst.replace_scale";;

let ineq_is_def vl pl = function
  | Eq (FORM f) ->
      let symbs = liste_var_forme f in
      let vars, os = List.partition (fun s -> List.mem s vl) symbs in
      let params, others =  List.partition (fun s -> List.mem s pl) os
      in 
        List.length vars = 1 && List.length others = 0
  | _ -> false;;

let replace_def keep vl pl i s = match i with
  | Eq (FORM f) ->
      let v = List.find 
                (fun v ->  List.mem v vl) 
                (liste_var_forme f) in
      let c = get_coef v f in
      let sf = (forme_of_string v) -| (f /| c)
      in (subst_syst s [v, sf]), keep
  | _ -> invalid_arg "Gen_syst.replace_def";;

let ineq_is_tautology = function
  | Eq (FORM f) -> (forme_is_num f) && (get_const f =/ zero)
  | Large (FORM f) -> (forme_is_num f) && (get_const f >=/ zero)
  | Strict (FORM f) -> (forme_is_num f) && (get_const f >/ zero)
  | _ -> false;;

let rec remove_tautologies = function
  | [] -> []
  | h::t -> 
      if ineq_is_tautology h 
      then remove_tautologies t
      else h::(remove_tautologies t);;

let ineq_is_antilogy = function
  | Eq (FORM f) -> (forme_is_num f) && (get_const f <>/ zero)
  | Large (FORM f) -> (forme_is_num f) && (get_const f </ zero)
  | Strict (FORM f) -> (forme_is_num f) && (get_const f >=/ zero)
  | _ -> false;;

let handle_antilogies system =
  let form = Forme.forme_of_num ( Num.minus_num one ) in
    if List.exists ineq_is_antilogy system then [ Eq (FORM form) ]
    else system
  ;;

let rec remove_duplicates = function
  | [] -> []
  | h::t -> h::(remove_duplicates 
                  (generic_subtract eq_ineq t [h]));;

(*TeX
  Removing of the inequalities with only intermediate variables that
  do not appear in any inequality with true variables or parameters.
*)
let remove_iv_only tv iv p s =
  let vars = fusionne (Sort.list (<=) tv) (Sort.list (<=) p) in
  let rec separate = function
    | i::s -> 
        let with_vars, iv_only = separate s in
          if intersect vars (list_var_ineq i) = [] then
            with_vars, (i::iv_only)
          else 
            (i::with_vars), iv_only
    | [] -> [], [] in
  let with_vars, iv_only = separate s in
  let keep_vars = ref (list_var_syst with_vars)
  and keep_ineq = ref with_vars in
  let rec trim = function
    | (i::to_scan , useless) -> 
        let ineq_vars = list_var_ineq i in
          if (ineq_vars <> []) && (intersect !keep_vars ineq_vars = []) then
            trim (to_scan , i::useless)
          else
            begin
              keep_ineq := i::!keep_ineq ;
              keep_vars := list_var_syst !keep_ineq ;
              trim (to_scan@useless , []) ;
            end
    | ([] , useless ) -> ([] , useless) in
  let _ = trim (iv_only , []) in
    !keep_ineq;; 

(*TeX
  Removing intermediate variable definition (any kind, not only
  linear) for which the defined variable only appears in other such
  definitions.
*)
let is_iv_def iv ineq =
  let get_unit_vars f =
    List.filter (fun v -> 
                   abs_num (Forme.get_coef v f) =/ un)
      (liste_var_forme f) in
    if ineq_is_eq ineq then
      match expr_of_ineq ineq with
        | NAE {nae_operator="+"; nae_args=el} ->
            begin
              let fe, nfe = List.partition expr_is_form el in
                match fe, nfe with
(* Attention, il ne faut prendre que les variables avec un
   coefficient de 1 ou -1, sinon ce n'est pas une definition
   mais une contrainte : nous sommes en nombres ENTIERS
*)
                  | [FORM f], [] -> intersect iv (get_unit_vars f)
                  | [FORM f], _ -> 
                      List.filter 
                        (fun v -> 
                           not (List.mem v (list_var_expr 
                                              (NAE {nae_operator="+";
                                                    nae_args=nfe})))) 
                        (intersect iv (get_unit_vars f))
                  | [], _ -> []
                  | _, _ -> failwith "Gen_syst.is_iv_def"
          end
        | _ -> []
  else [];;

let remove_iv_defs iv s =
  let syst = ref s
  and modif = ref true
  in let rec rem_defs before = function
    | i::l -> 
        begin
          match is_iv_def iv i with
            | [] -> rem_defs (i::before) l
            | vl -> 
                if List.exists 
                  (fun v -> not (List.mem v 
                                   (list_var_syst (before@l)))) vl
                then begin
                  modif := true;
                  rem_defs before l
                end else rem_defs (i::before) l
        end
    | [] -> before
  in 
    while !modif do
      modif := false;
      syst := rem_defs [] !syst
    done;
    !syst;;

(*TeX
  If an equality is a negation, take the opposite.
*)
let neg_trim = function
  | Eq (NAE {nae_operator="-"; nae_args=[e]}) -> Eq e
  | i -> i;;

(*TeX
  Simplification engine.
*)
let stage test replace s =
  let modif = ref true
  and global_mod = ref false
  and used_ineqs = ref []
  and syst = ref s
  in let register i (s, keep) =
    if keep then used_ineqs := i::(!used_ineqs);
    modif := true;
    global_mod := true;
    syst := norm_syst s
  in
  let rec scan before after =
    if not !modif 
    then match after with
      | [] -> ()
      | h::t -> 
          if test h 
          then register h (replace h (before@t))
          else scan (h::before) t
  in
    while !modif do
      modif := false;
      scan [] !syst
    done;
    !global_mod, !used_ineqs, !syst;;

let simplify_interne tv iv p s =
  let modif1 = ref true
  and modif2 = ref true
  and modif3 = ref true
  and used_ineqs = ref []
  and syst = ref s
  in let trim () =
      syst := List.map neg_trim !syst;
      syst := remove_iv_defs iv
        (remove_iv_only tv iv p (remove_duplicates !syst))
  in let register modifn (modified, used, new_syst) =
    modifn := modified;
    used_ineqs := used@(!used_ineqs);
    syst := new_syst
  in
    while !modif3 or !modif2 or !modif1 do
      modif3 := false;
      while !modif2 or !modif1 do
        modif2 := false;
        while !modif1 do
          register modif1
            (stage ineq_is_constant_def (replace_constant_def iv) !syst);
          register modif1
            (stage ineq_is_scale (replace_scale iv tv p) !syst)
        done;
        register modif2 
          (stage (ineq_is_def iv (tv@p)) (replace_def false iv (tv@p)) !syst)
      done;
      register modif3
        (stage (ineq_is_def tv p) (replace_def true tv p) !syst);
      trim ();
    done;
    let simple = remove_tautologies (remove_duplicates !syst) in
      handle_antilogies (!used_ineqs@simple);;

let simplify tv p s = 
  simplify_interne tv (subtract (list_var_syst s) (tv@p)) p s;;
let simplify_vars tv s = 
  simplify_interne tv (subtract (list_var_syst s) tv) [] s;;

(*TeX
  \subsubsection{Printers}
*)
open Format;;
open Formatters;;

let rec print_expr = function
  | FORM f -> print_forme f
  | MOD m -> print_modulo m
  | DIV d -> print_division d
  | NAE nae -> print_non_aff_expr nae
and print_expr_rec = function
  | FORM f -> print_forme_rec f
  | MOD m -> print_modulo_rec m
  | DIV d -> print_division_rec d
  | NAE nae -> print_non_aff_expr_rec nae
and print_forme_rec f =
  if List.length (forme_to_terme_list f) = 1 then
    print_forme f
  else begin
    pp_open_hovbox (!current_formatter) 2;
    pp_print_string (!current_formatter) "(";
    print_forme f;
    pp_print_string (!current_formatter) ")";
    pp_close_box (!current_formatter) ()
  end
and print_non_aff_infix_expr nae =
  pp_open_hvbox (!current_formatter) 2;
  begin match nae.nae_args with
    | [] -> invalid_arg "Gen_syst.print_non_aff_infix_expr"
    | [e] -> 
        pp_print_string (!current_formatter) nae.nae_operator;
        pp_print_cut (!current_formatter) ();
        print_expr_rec e;
    | e::t ->
        print_expr_rec e;
        List.iter 
          (fun e ->
             pp_print_cut (!current_formatter) ();
             pp_print_string (!current_formatter) nae.nae_operator;
             pp_print_cut (!current_formatter) ();
             print_expr_rec e)
          t
  end;
  pp_close_box (!current_formatter) ()
and print_non_aff_prefix_expr nae =
  pp_open_hvbox (!current_formatter) 2;
  pp_print_string (!current_formatter) nae.nae_operator;
  pp_print_space (!current_formatter) ();
  begin match nae.nae_args with
    | [] -> invalid_arg "Gen_syst.print_non_aff_prefix_expr"
    | e::t ->
        print_expr e;
        List.iter 
          (fun e ->
             pp_print_space (!current_formatter) ();
             print_expr_rec e)
          t
  end;
  pp_close_box (!current_formatter) ()
and print_non_aff_expr nae =
  if (String.uppercase nae.nae_operator) <> 
    (String.lowercase nae.nae_operator)
  then print_non_aff_prefix_expr nae
  else print_non_aff_infix_expr nae
and print_non_aff_expr_rec nae =
  if nae.nae_operator = "**" then print_non_aff_expr nae
  else begin
    pp_open_hvbox (!current_formatter) 1;
    pp_print_string (!current_formatter) "(";
    print_non_aff_expr nae;
    pp_print_string (!current_formatter) ")";
    pp_close_box (!current_formatter) ()
  end
and print_modulo m =
  pp_open_hovbox (!current_formatter) 2;
  print_expr_rec m.mod_expr;
  pp_print_space (!current_formatter) ();
  pp_print_string (!current_formatter) "mod";
  pp_print_space (!current_formatter) ();
  print_expr_rec m.modulus;
  pp_close_box (!current_formatter) ()
and print_modulo_rec m =
  pp_open_hovbox (!current_formatter) 1;
  pp_print_string (!current_formatter) "(";
  print_modulo m;
  pp_print_string (!current_formatter) ")";
  pp_close_box (!current_formatter) ()
and print_division d =
  pp_open_hovbox (!current_formatter) 2;
  print_expr_rec d.div_expr;
  pp_print_space (!current_formatter) ();
  pp_print_string (!current_formatter) "div";
  pp_print_space (!current_formatter) ();
  print_expr_rec d.divisor;
  pp_close_box (!current_formatter) ()
and print_division_rec d =
  pp_open_hovbox (!current_formatter) 1;
  pp_print_string (!current_formatter) "(";
  print_division d;
  pp_print_string (!current_formatter) ")";
  pp_close_box (!current_formatter) ();;

let print_form_ineq f comp =
  let neg_comp = function
    | "=" -> "="
    | ">=" -> "<="
    | ">" -> "<" 
    | _ -> assert false in
  let const = get_const f in
    if eq_num const zero then 
      let f', comp' =
        if (signature f) < 0 then
          minus_forme f, neg_comp comp
        else f, comp
      in begin
      match
        List.partition 
          (fun t -> gt_num (terme_get_coef t) zero)
          (forme_to_terme_list f')
      with
        | lp, [] ->
          print_forme f';
          pp_print_space (!current_formatter) ();
          pp_print_string (!current_formatter) comp';
          pp_print_space (!current_formatter) ();
          print_num zero
        | [], ln ->
          print_forme (minus_forme f');
          pp_print_space (!current_formatter) ();
          pp_print_string (!current_formatter) (neg_comp comp');
          pp_print_space (!current_formatter) ();
          print_num zero
        | lp, ln ->
          print_forme (forme_of_terme_list lp);
          pp_print_space (!current_formatter) ();
          pp_print_string (!current_formatter) comp';
          pp_print_space (!current_formatter) ();
          print_forme (minus_forme (forme_of_terme_list ln))
    end else
      let f' = sub_forme f (forme_of_num const) in
        if signature f' < 0 then begin
          print_forme (minus_forme f');
          pp_print_space (!current_formatter) ();
          pp_print_string (!current_formatter) (neg_comp comp);
          pp_print_space (!current_formatter) ();
          print_num const
        end else begin
          print_forme f';
          pp_print_space (!current_formatter) ();
          pp_print_string (!current_formatter) comp;
          pp_print_space (!current_formatter) ();
          print_num (minus_num const)
        end;;

let print_gen_ineq i =
  pp_open_hovbox (!current_formatter) 2;
  begin match i with
    | Eq (FORM f) -> print_form_ineq f "="
    | Large (FORM f) -> print_form_ineq f ">="
    | Strict (FORM f) -> print_form_ineq f ">"
    | Eq e -> 
        print_expr e;
        pp_print_space (!current_formatter) ();
        pp_print_string (!current_formatter) "= 0"
    | Large e ->
        print_expr e;
        pp_print_space (!current_formatter) ();
        pp_print_string (!current_formatter) ">= 0"
    | Strict e ->
        print_expr e;
        pp_print_space (!current_formatter) ();
        pp_print_string (!current_formatter) "> 0"
  end;
  pp_close_box (!current_formatter) ();;

let print_gen_syst s =
  pp_open_hovbox (!current_formatter) 1;
  pp_print_string (!current_formatter) "{";
  let ss = List.sort compare s in
    begin match ss with
      | [] -> ()
      | h::[] -> print_gen_ineq h
      | h::t -> print_gen_ineq h;
          List.iter (fun i ->
                       pp_print_string (!current_formatter) ",";
                       pp_print_space (!current_formatter) ();
                       print_gen_ineq i) t
    end;
  pp_print_cut (!current_formatter) ();
  pp_print_string (!current_formatter) "}";
  pp_close_box (!current_formatter) ();;