(* Exprssion.mli *)
type term
val str : term -> string

(* Expression.ml *)
open String;;
type term =
  | Const of bool
  | Var of string
  | Not of term
  | Imp of (term * term)
  | Or of (term * term)
  | And of (term * term);;
let rec formula_to_string = function
  | Const c -> string_of_bool c
  | Var s -> s
  | Not (Var v) -> "!"^v
  | Not (Const c) -> "!"^ string_of_bool c
  | Not formula -> ("!"^ formula_to_string formula)
  | Or (a,b) -> ((formula_to_string a) ^ " | " ^ (formula_to_string b))
  | And (a,b) -> ((formula_to_string a) ^ " & " ^ (formula_to_string b) )
  | Imp (a , b) -> ( "(" ^ (formula_to_string a) ^ " > " ^ (formula_to_string b)^")" ) ;;

(* Parser.mly*)

%{
        open Expression
%}
%token <bool> CONST
%token <string> VAR
%token NOT
%token AND
%token OR
%token IMP
%token LPAREN
%token RPAREN
%token EOF

%right IMP
%left OR
%left AND
%right NOT

%start <Expression.term> prog
%%
prog:
        | e = expr; EOF{ e }

expr:
        | cnst = CONST { Const cnst }
        | v = VAR { Var v }
        | NOT; e1 = expr { Not e1 }
        | e1 = expr; AND; e2 = expr { And ( e1 , e2) }
        | e1 = expr; OR; e2 = expr { Or ( e1 , e2) }
        | e1 = expr; IMP; e2 = expr { Imp ( e1 , e2) }
        | LPAREN; e = expr; RPAREN { e }
        ;