type formule = 
	| Var of int
	| Not of formule
	| Imply of formule*formule
	| Equiv of formule*formule
	| And of formule list
	| Or of formule list;;

let f = And [Or [Var 0; Var 1; Var 2]; Not (Var 0)];;
let g = Equiv (Var 0, And [Var 1; Var 2]);;
let rec evaluer_tab t form = match form with
	| Var i -> t.(i)
	| Not f -> not (evaluer_tab t f)
	| Imply (f1,f2) -> (not (evaluer_tab t f1)) || (evaluer_tab t f2)
	| Equiv (f1,f2) -> (evaluer_tab t f1) = (evaluer_tab t f2)
	| And [] -> true
	| And (h::tail) -> (evaluer_tab t h) && (evaluer_tab t (And tail))
	| Or [] -> false
	| Or (h::tail) -> (evaluer_tab t h) || (evaluer_tab t (Or tail));;
5 lsr 1;;

let contexte_from_int n c =
	let contexte = Array.make n false in
	let j = ref c in
	for i = 0 to n-1 do
		contexte.(i) <- !j mod 2 <> 0;
		j := !j lsr 1
	done;
	contexte;;

let evaluer n c f =
	let contexte = contexte_from_int n c in
	evaluer_tab contexte f;;

evaluer 3 3 g;;

let table_de_verite n f = 
	let rec puis n a = match n with
		| 0 -> 1
		| _ -> a * (puis (n-1) a) in
	let res = Array.make (puis	n 2) false in
	for c=0 to ((Array.length res) -1) do
		res.(c) <- evaluer n c f
	done;
	res;;
table_de_verite 3 g;;

let forme_normale_disjonctive n f =
	let rec puis n a = match n with
		| 0 -> 1
		| _ -> a * (puis (n-1) a) in

	let rec disjonction c conjs =

		let rec conjonction cont conj n = match n with
			| -1 -> And conj
			| _ -> conjonction cont ((if cont.(n) then (Var n) else Not (Var n))::conj) (n-1) in

		match c with
			| -1 -> Or conjs
			| _ -> let contexte = context_from_int n c in
					 if evaluer_tab contexte f then
					 	disjonction (c-1) ((conjonction contexte [] (n-1))::conjs)
					 else
					 	disjonction (c-1) conjs in
	disjonction ((puis n 2) -1) [];;
forme_normale_disjonctive 3 g;;