type variavel = string

type formula = 
  | Implica of formula*formula
  | Equivale of formula*formula
  | Ou of formula*formula
  | E of formula*formula
  | Nao of formula
  | Var of variavel
  | Verdade
  | Falso

(* Função (recursiva estrutural) de conversão de expressões para strings *)
let rec string_of_formula form =
match form with
  | Var v          ->  v
  | Verdade        -> "TRUE"
  | Falso          -> "FALSE"
  | Implica(f, g)  -> ("( "^ string_of_formula f ^ " -> " ^ string_of_formula g ^" )")
  | Equivale(f, g) -> ("( "^ string_of_formula f ^ " <-> " ^ string_of_formula g ^" )")
  | E(f, g)        -> ("( "^ string_of_formula f ^ " & " ^ string_of_formula g ^" )")
  | Ou(f, g)       -> ("( "^ string_of_formula f ^ " | " ^ string_of_formula g ^" )")
  | Nao f          ->  ("!"^ string_of_formula f )


type literal = Bot | Top |  V of variavel | N of variavel
type fnc = literal list list

(* alínea 3 *)

let rec implfree f =
  match f with 
  | Implica  (g, h) -> Ou ((Nao (implfree g)),(implfree h))
  | Equivale (g, h) -> E ((Ou (Nao (implfree g),(implfree h))),
                         (Ou (Nao (implfree h),(implfree g))))
  | E  (g, h)       -> E (implfree g, implfree  h) 
  | Ou (g, h)       -> Ou (implfree g, implfree  h) 
  | Nao g           -> Nao (implfree g)
  | _ -> f 
;;

let rec nnfc f = 
  match f with 
  | Nao (Nao g) -> nnfc g
  | Nao (E (g,h)) -> Ou (nnfc (Nao g), nnfc (Nao h))
  | Nao (Ou (g,h)) -> E (nnfc (Nao g), nnfc (Nao h))
  | E (g, h)        ->  E (nnfc g, nnfc  h) 
  | Ou (g, h)       ->  Ou (nnfc g, nnfc  h) 
  | _ -> f
;;

let rec distr f g =
match (f,g) with
(E (h,i), _ ) -> E ((distr h g), (distr i g))  
| (_ , E (h,i)) ->  E ((distr f h), (distr f i)) 
| _ -> Ou (f,g)

let rec cnfc  f =
match f with
  Ou (g,h) -> distr (cnfc g) (cnfc h)  
| E  (g,h) ->  E (cnfc g, cnfc h)
| _ -> f
;;

let t f = cnfc (nnfc (implfree f));;



let rec to_fnc_aux_ou f =
  match f with
  | Ou ((Ou (g,h)), (Ou (i,j))) -> to_fnc_aux_ou (Ou (g,h)) @ to_fnc_aux_ou (Ou (i,j))
  | Ou (Var g, Ou (i,j)) -> V g::to_fnc_aux_ou (Ou (i,j))
  | Ou ((Ou (g,h)), Var i) -> to_fnc_aux_ou (Ou (g,h)) @ [V i]
  | Ou (Nao (Var g), Ou (i,j)) -> N g::to_fnc_aux_ou (Ou (i,j))
  | Ou ((Ou (g,h)), Nao (Var i)) -> to_fnc_aux_ou (Ou (g,h)) @ [N i]
  | Ou (g,h) -> (to_fnc_aux_ou g) @ (to_fnc_aux_ou h)
  | Nao (Var x) -> [N x]
  | Var x -> [V x]
  | Verdade ->  [Top]
  | Falso ->  [Bot]
  | _ -> failwith "to_fnc_aux_ou: Formato invalido" 
;;


let rec to_fnc_aux f = 
  match f with
    | E (E (g,h),E (i,j))  -> to_fnc_aux (E (g,h)) @ to_fnc_aux (E (i,j)) 
    | E (Ou (g,h),E (i,j))  -> to_fnc_aux_ou (Ou (g,h)) :: to_fnc_aux (E (i,j)) 
    | E (E (g,h),Ou (i,j))  -> to_fnc_aux (E (g,h)) @ [to_fnc_aux_ou (Ou (i,j))] 
    | E (Ou (g,h),Ou (i,j))  ->  [to_fnc_aux_ou (Ou (g,h));to_fnc_aux_ou (Ou (i,j))]
    | Ou _ -> [to_fnc_aux_ou f]
    | Nao _ -> [to_fnc_aux_ou f]
    | Var _ -> [to_fnc_aux_ou f]
    | Verdade ->  [to_fnc_aux_ou f]
    | Falso ->  [to_fnc_aux_ou f]
    | _ -> failwith "to_fnc_aux: Formato invalido" 

let to_fnc f = to_fnc_aux (t f);;

(*
(*  (A/\ C) -> (~(B-> ~A) \/ (C /\ ~D)  *)
let exemplo = Implica (E (Var "A",Var "C"), Ou (Nao (Implica (Var "B", Nao (Var "A"))), E(Var "C", Nao (Var "D"))));;

let ex = t exemplo;;

(string_of_formula exemplo);;

(string_of_formula ex);;

let res = to_fnc exemplo;;
*)

This document was generated using caml2html