module Formula where

import ParseLib
import List

type Atomica = Char

data Formula = At Atomica
    | Op1 Op1 Formula
    | Op2 Op2 Formula Formula
    deriving Show

data Op1 = Neg
     deriving Show
     
data Op2 = And | Or | Implica | DobleImplica
     deriving Show
    
{-
    Gramatica de una formula:
    
        formula := termino | termino ConDer formula

        termino := factor | termino ConIzq factor
        
        factor := atomico |  Op1 factor | (formula)


    Conectivos que asocian a la izq:
        ConIzq := or | and 
    
    Conectivos que asocian a la der:
        ConDer := implica | doble_implica
    
    Conectivos Unarios
        Op1    := negacion
-}


parse0Espacio :: Parse Char [Char]
parse0Espacio = list (token ' ')


-- def. de formula
formula :: Parse Char Formula
formula = (parse0Espacio >*> (termino `alt` formula2) >*> parse0Espacio) `build`  \(_,(f,_)) -> f

formula2 :: Parse Char Formula
formula2 = (termino >*> parse0Espacio >*> conDer >*> parse0Espacio >*>formula) `build` \(t,(_,(op,(_,f)))) -> Op2 op t f

-- def de factor
factor :: Parse Char Formula  
factor = atomico `alt` factor1 `alt` parentesisFormula

factor1 :: Parse Char Formula
factor1 = (negacion >*> parse0Espacio >*> factor) `build` \(c,(_,f)) -> Op1 c f

parentesisFormula :: Parse Char Formula
parentesisFormula = (token '(' >*> parse0Espacio >*>formula  >*> parse0Espacio >*> token ')') `build` \(_,(_,(f,(_,_)))) -> f


-- def. de termino
termino :: Parse Char Formula  -- termino := factor | termino ConIzq factor
termino = factor `alt` termino2


termino2 :: Parse Char Formula
termino2 =  (factor >*> parse0Espacio >*> list (conIzq >*> parse0Espacio >*> factor >*> parse0Espacio))
        `build` mkTermino
        where
            mkTermino (a,(_,fs)) = foldl operar a fs
            operar e (op,(_,(a,_))) = Op2 op e a

termino1 :: Parse Char Formula
termino1 = (negacion >*> parse0Espacio >*> factor) `build` \(n,(_,f)) -> Op1 n f

conDer :: Parse Char Op2
conDer = implica `alt` doble_implica

conIzq :: Parse Char Op2
conIzq = con_or `alt` con_and


-- Terminales
implica :: Parse Char Op2
implica = (token '-' >*> token '>') `build` \(_,_) -> Implica

doble_implica :: Parse Char Op2
doble_implica = (token '<' >*> token '-' >*> token '>') `build` \(_,(_,_)) -> DobleImplica

con_or :: Parse Char Op2 
con_or = token '|' `build` const Or

con_and :: Parse Char Op2 
con_and = token '&' `build` const And

negacion :: Parse Char Op1
negacion = token '~' `build` const Neg

atomico :: Parse Char Formula
atomico = spot (\c -> c >='a' && c <= 'z') `build` At


----------------
-- Auxiliares
----------------

obtenerAtomicas :: Formula -> [Atomica]
obtenerAtomicas f = sort (obtenerAtomicas' f)

obtenerAtomicas' :: Formula -> [Atomica]
obtenerAtomicas' (At c) = c:[]
obtenerAtomicas' (Op1 op f) = obtenerAtomicas' f
obtenerAtomicas' (Op2 op f1 f2) = union (obtenerAtomicas' f1) (obtenerAtomicas' f2)

------------------
--  el parser tiene exito si se consume todo el string
parseFormula :: String -> Maybe Formula
parseFormula cs = devuelvoFormula (formula cs)

devuelvoFormula :: [(Formula,String)] -> Maybe Formula
devuelvoFormula (x:xs)
        | length (snd x) == 0 = Just (fst x)
        | otherwise = devuelvoFormula xs
devuelvoFormula [] = Nothing