open List
open Stream
open Genlex
open Printf
open Str

(* compilação com stream e com Str:

ocamlc str.cma -pp camlp4o .......

*)

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

 (*

leitura e manipulação de termos algébricos/indutivos (aqui expressões lógicas simples) com streams


Este método de leitura implementa um lexer/parser descendente (para
detalhes: disciplina de Processamento de Linguagem) para a
gramática LL(1) das expressões lógicas seguinte (N -> {TRUE , FALSE}, V
-> Variáveis):

E  ::= T E'
E' ::= -> T E'
E' ::= <-> T E'
E' ::= \epsilon
T  ::= F T'
T' ::= & F T'
T' ::= | F T'
T' ::= \epsilon
F  ::= N
F  ::= V
F  ::= ! E
F  ::= ( E )
*)



(*

Analise léxica usando a biblioteca Genlex.
*)

let lexer = make_lexer ["("; ")"; "<->"; "->"; "|"; "&" ; "!"; "TRUE"; "FALSE"];;


(*Analise Sintáctica: dado uma lista de tokens verificar se esta lista
segue a gramática das expressões lógicas e no caso positivo
  construir/devolver a expressão lógica contida *)

let rec parse_expr = parser (* corresponde a entrada E da gramática *)
    [< e1 = parse_conj; e = parse_more_imps e1 >] -> e
and parse_more_imps e1 = parser (* corresponde a entrada E' da gramática *)
    [< 'Kwd "->"; e2 = parse_conj; e = parse_more_imps (Implica(e1, e2)) >] -> e
  | [< 'Kwd "<->"; e2 = parse_conj; e = parse_more_imps (Equivale(e1, e2)) >] -> e
  | [< >] -> e1
and parse_conj = parser (* corresponde a entrada T da gramática *)
    [< e1 = parse_simple; e = parse_more_conjs e1 >] -> e
and parse_more_conjs e1 = parser (* corresponde a entrada T' da gramática *)
    [< 'Kwd "&"; e2 = parse_simple; e = parse_more_conjs (E(e1, e2)) >] -> e
  | [< 'Kwd "|"; e2 = parse_simple; e = parse_more_conjs (Ou(e1, e2)) >] -> e
  | [< >] -> e1
and parse_simple = parser (* corresponde a entrada F da gramática *)
    [< 'Ident s >] -> Var s
  | [< 'Kwd "TRUE" >] -> Verdade
  | [< 'Kwd "FALSE" >] -> Falso
  | [< 'Kwd "!";  'Kwd "("; e = parse_expr; 'Kwd ")" >] -> Nao e 
  | [< 'Kwd "("; e = parse_expr; 'Kwd ")" >] -> e;;




let parse_expression = parser [< e = parse_expr; _ = Stream.empty >] -> e;;

(* função principal de leitura usando streams*)
let expression_of_string s = 
  parse_expression
    (lexer
       (Stream.of_string (Str.global_replace (Str.regexp "!") "! " s)
       ));;


let rec do_n_times f n acc =
if n<=0
then rev acc
else
let v= f () in
(do_n_times f (n-1) (v::acc))

let read_expression () =  expression_of_string (read_line ());;

let read_n_expression n =
  do_n_times
    (fun () -> expression_of_string (read_line ()))
    n [];;

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 (Var v)          ->  ("!("^ v ^")" )
  | Nao f          ->  ("!"^ string_of_formula f)