(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(*               Pierre Weis, projet Cristal, INRIA Rocquencourt       *)
(*                                                                     *)
(*  Copyright 2001 Institut National de Recherche en Informatique et   *)
(*  en Automatique.  All rights reserved.  This file is distributed    *)
(*  only by permission.                                                *)
(*                                                                     *)
(***********************************************************************)
open List;;

type proposition =
   | Vrai
   | Faux
   | Non of proposition
   | Et of proposition * proposition
   | Ou of proposition * proposition
   | Implique of proposition * proposition
   | Équivalent of proposition * proposition
   | Variable of string;;

exception Réfutation of (string * bool) list;;

let rec évalue_dans liaisons = function
  | Vrai -> true
  | Faux -> false
  | Non p -> not (évalue_dans liaisons p)
  | Et (p, q) -> (évalue_dans liaisons p) &&  (évalue_dans liaisons q)
  | Ou (p, q) -> (évalue_dans liaisons p) || (évalue_dans liaisons q)
  | Implique (p, q) ->
      (not (évalue_dans liaisons p)) || (évalue_dans liaisons q)
  | Équivalent (p, q) ->
      évalue_dans liaisons p = évalue_dans liaisons q
  | Variable v -> assoc v liaisons;;

let rec vérifie_lignes proposition liaisons variables =
  match variables with
  | [] ->
     if not (évalue_dans liaisons proposition)
     then raise (Réfutation liaisons)
  | var :: autres ->
     vérifie_lignes proposition ((var, true) :: liaisons) autres;
     vérifie_lignes proposition ((var, false) :: liaisons) autres;;

let vérifie_tautologie proposition variables =
  vérifie_lignes proposition [] variables;;
let rec variables accu proposition =
  match proposition with
  | Variable v -> if mem v accu then accu else v::accu
  | Non p -> variables accu p
  | Et (p, q) -> variables (variables accu p) q
  | Ou (p, q) -> variables (variables accu p) q
  | Implique (p, q) -> variables (variables accu p) q
  | Équivalent (p, q) -> variables (variables accu p) q
  | _ -> accu;;

let variables_libres proposition = variables [] proposition;;