{ -- wird einfach in den Quelltext copiert
module Parse where
import Char
}

-- die Parserfunktion heißt <parseTerm> und startet mit Startproduktion <Term> 
%name parseTerm Term

-- In der übernächsten Zeile den Kommentar entfernen. Die StartProduktion heißt
-- hier <Formel>
%name parseFormel Formel
  
%tokentype { Token }

-- Die Tokens 

%token 
  P        { TokenP }
  f        { Tokenf }
  x        { Tokenx }
  '('      { TokenKL }
  ')'      { TokenKR }
  ','      { TokenKomma }
  '^'      { TokenODER }
  'v'      { TokenUND }
  '-'      { TokenNOT }
  'A'      { TokenAll }    -- Allquantor
  'E'      { TokenExi }    -- Existenzquantor
  int      { TokenInt $$ } 

 %%  -- nicht entfernen!


----------------------------------------------------------------------------
-- Die Produktionen                                 die Datentypen 
----------------------------------------------------------------------------

-- Im Nachfolgenden steht $i für das i-te Token der Produktion  

Term : Variablensymbol                              { VarTerm $1 }
     | Funktionssymbol '(' Term Termrest            { FunkTerm $1 ($3:$4)}

Termrest : ')'                                      { [] }
         | ',' Term Termrest                        { $2:$3 }

Formel :  Praedikatsymbol '(' Term Termrest    { Atom $1 ($3:$4)} 
       |  Formel '^' Formel                    { And $1 $3}
       |  Formel 'v' Formel                    { Or $1 $3}
       |  '-' Formel                           { Negate $2} 
       |  'A' Variablensymbol Formel           { Forall $2 $3}
       |  'E' Variablensymbol Formel           { Exists $2 $3}

Variablensymbol : x int                           { Variable $2 }
Praedikatsymbol  : P int                           { Praedikat $2}
Funktionssymbol : f int                           { Funktion $2 } 




{ -- wird einfach in den Quelltext kopiert... 

-- eine ziemlich nutzlose Fehlermeldung
 
happyError :: [Token] -> a
happyError ts = error ("Fehler bei:\n"++(show ts))
 
----------------------------------------------------------------------------
-- Hier nun die Datentypen 
----------------------------------------------------------------------------

data Symbol = Variable Int 
            | Funktion Int 
            | Praedikat Int deriving (Eq, Read, Show)

data Term = VarTerm Symbol
          | FunkTerm Symbol [Term] deriving (Eq, Read, Show)

data Formel = Atom Symbol [Term]
            | Negate Formel
            | And Formel Formel
            | Or Formel Formel
            | Forall Symbol Formel
            | Exists Symbol Formel  deriving (Eq,Read,Show)  



----------------------------------------------------------------------------
-- Ab hier der Datentyp Token
----------------------------------------------------------------------------

data Token =  TokenP 
           | Tokenf 
           | Tokenx 
           | TokenKL 
           | TokenKR 
           | TokenKomma 
           | TokenODER 
           | TokenUND 
           | TokenNOT 
           | TokenAll 
           | TokenExi 
           | TokenInt Int deriving (Eq,Show,Read) 

----------------------------------------------------------------------------
-- ein einfacher Lexer, sollte für alles reichen
----------------------------------------------------------------------------
lexer :: String -> [Token]
lexer [] = []
lexer (c:cs)
      | isSpace c = lexer cs
      | isDigit c = lexNum (c:cs)
lexer ('P':cs) = TokenP  :    lexer cs
lexer ('f':cs) = Tokenf  :    lexer cs
lexer ('x':cs) = Tokenx  :    lexer cs
lexer ('(':cs) = TokenKL :    lexer cs
lexer (')':cs) = TokenKR :    lexer cs
lexer (',':cs) = TokenKomma : lexer cs
lexer ('v':cs) = TokenODER :  lexer cs
lexer ('^':cs) = TokenUND  :  lexer cs  
lexer ('-':cs) = TokenNOT  :  lexer cs
lexer ('A':cs) = TokenAll  :  lexer cs
lexer ('E':cs) = TokenExi  :  lexer cs
      
lexNum cs = TokenInt (read num) : lexer rest
  where (num,rest) = span isDigit cs

----------------------------------------------------------------------------
-- Ein einfacher Test (ein Akzeptor der Grammatik)
----------------------------------------------------------------------------

test = getContents >>= print . parseFormel . lexer  
}

-- ende