type atome = string;;

type clause = {
  p : atome list; (* atomes apparaissant positivement *)
  n : atome list; (* atomes apparaissant négativement *)
};;

type clauses = { liste : clause list; };;
let trie l = Sort.list (fun x y -> x <= y) l;;

(* enleve les valeurs identiques successives d'une liste
   Précondition : l est triée (peu importe pour quel ordre).
*)
let rec enleve_doublons l = match l with
  | [] -> []
  | [x] -> [x]
  | x :: y :: r -> if x = y then enleve_doublons (y::r)
                   else x::enleve_doublons (y::r)
;;

(* met sous forme canonique un ensemble. Pour cela, le trie puis
   enlève les doublons: *)
let ensemble l = enleve_doublons (trie l);;

(* construit une clause en s'assurant que celle-ci est bien sous forme
   canonique. *)
let cons_clause p n = { p = ensemble p; n = ensemble n; };;

(* met sous forme canonique une clause qui aurait été mal construite *)
let canonise_clause { p = p; n = n; } = cons_clause p n;;

(* construit un ensemble de clauses en s'assurant que chaque clause
   est bien sous forme canonique et que l'ensemble est bien lui-même
   trié, sans doublon. *)
let cons_clauses cl = { liste = (ensemble (List.map canonise_clause cl)) };;
let print_atomes l =
  List.iter (fun a -> print_string " "; print_string a) l;;
  
let print_clause c =
  print_string "(conj";
  print_atomes c.p;
  print_string ") => (disj";
  print_atomes c.n;
  print_string ")\n"
;;

let print_clauses cl =
  List.iter (fun c -> print_clause c) cl.liste;
  print_string "\n"
;;