{
{-# OPTIONS_GHC -w #-}
{-
Copyright (C) HyLoRes 2002-2007. See AUTHORS file

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307,
USA.
-}

module HyLo.InputFile.Parser ( parse,
                               initParseState,
                               ParseState,
                               QueryType(..),
                               RelProperty(..),
                               ParseOutput(..), RelInfo, ProverInfo,InferenceTask,
                               relations, provers, theory, tasks)

where

import Control.Monad.State

import HyLo.InputFile.Lexer ( Token(..), FilePos, line, col )

import HyLo.Signature.String ( StringSignature,
                               PropSymbol(..),
                               NomSymbol(..),
                               RelSymbol(..))

import HyLo.Signature ( Signature,
                        emptySignature,
                        addNomToSig,
                        addPropToSig,
                        addRelToSig,
                        isNomInSig,
                        isPropInSig,
                        isRelInSig)

-- since ghc 6.10, "Down" is defined in GHC.Exts, that is included
-- (unqualified) in the parser. we need to use Formula.Down instead of
-- simply Down to avoid ambiguities...
import HyLo.Formula as Formula ( Formula(..), Where(..), CountOp(..) )

}

%name parse
%tokentype { (Token, FilePos) }
%monad { State ParseState }

%token
             signature       { (TokenSignature,    _) }
             propositions    { (TokenPropositions, _) }
             nominals        { (TokenNominals ,    _) }
             relations       { (TokenRelations,    _) }

             reflexive       { (TokenReflexive,    _) }
             universal       { (TokenUniversal,    _) }
             difference      { (TokenDifference,   _) }
             transitive      { (TokenTransitive,   _) }
             symmetric       { (TokenSymmetric,    _) }
             functional      { (TokenFunctional,   _) }
             injective       { (TokenInjective,    _) }

             inverseof       { (TokenInverseOf,    _) }
             subsetof        { (TokenSubsetOf,     _) }
             equals          { (TokenEquals,       _) }
             tclosureof      { (TokenTClosureOf   ,_) }
             trclosureof     { (TokenTRClosureOf,  _) }

             automatic       { (TokenAutomatic,    _) }

             proverparameters { (TokenProverParameters, _) }
             prover          { (TokenProver,       _) }

             theory          { (TokenTheory,       _) }
             query           { (TokenQuery,        _) }
             valid           { (TokenValid,        _) }
             satisfiable     { (TokenSatisfiable,  _) }
             retrieve        { (TokenRetrieve,     _) }
             count           { (TokenCount,        _) }
             integer         { (TokenInteger $$,   _) }
             variable        { (TokenVariable $$,  _) }
             label           { (TokenLabel $$,     _) }
             file            { (TokenFile $$,      _) }
             ':'             { (TokenColon    ,    _) }
             down            { (TokenDown     ,    _) }
             greaterEqual    { (TokenGE       ,    _) }
             lowerEqual      { (TokenLE       ,    _) }
             greater         { (TokenG        ,    _) }
             lower           { (TokenL        ,    _) }
             equal           { (TokenE        ,    _) }
             nonEqual        { (TokenNE       ,    _) }
             prop            { (TokenProp $$  ,    _) }
             nom             { (TokenNom $$   ,    _) }
             true            { (TokenTrue     ,    _) }
             false           { (TokenFalse    ,    _) }
             neg             { (TokenNeg      ,    _) }
             and             { (TokenAnd      ,    _) }
             or              { (TokenOr       ,    _) }
             dimp            { (TokenDimp     ,    _) }
             imp             { (TokenImp      ,    _) }
             box             { (TokenBox $$   ,    _) }
             ubox            { (TokenUBox     ,    _) }
             dbox            { (TokenDBox     ,    _) }
             dia             { (TokenDia $$   ,    _) }
             udia            { (TokenUDia     ,    _) }
             ddia            { (TokenDDia     ,    _) }
             '('             { (TokenOB       ,    _) }
             ')'             { (TokenCB       ,    _) }
             ';'             { (TokenSC       ,    _) }
             '.'             { (TokenDot      ,    _) }
             ','             { (TokenComma    ,    _) }
             '{'             { (TokenOC       ,    _) }
             '}'             { (TokenCC       ,    _) }
             '<'             { (TokenODia     ,    _) }
             '>'             { (TokenCDia     ,    _) }
             '['             { (TokenOBox     ,    _) }
             ']'             { (TokenCBox     ,    _) }
             '='             { (TokenEqual    ,    _) }
%right imp
%right dimp
%left or
%left and
%left box ubox dbox dia udia ddia neg
%right ':'
%right down

%%

Input :: { ParseOutput }
Input :
  signature '{' Signature '}'
  ProverSpecific
  Theory
  Queries { PO{relations = $3,
               provers   = $5,
               theory    = $6,
               tasks     = $7} }

Signature :: { [RelInfo] }
Signature :
  AutomaticSignature { $1 }
| ContentSignature { $1 }

Variable :: {String}
Variable :
  variable  { $1 }
| prop      { let PropSymbol x = $1 in x}
| nom       { let NomSymbol x  = $1 in x}

Theory :: { [Formula NomSymbol PropSymbol RelSymbol] }
Theory :
 theory '{' Formulas '}' { $3 }

Queries :: { [InferenceTask] }
Queries : { [] }
| Query Queries { $1:$2 }

Query :: { InferenceTask }
Query :
  query '(' valid File ')'       '{' Formulas '}' { (Valid,       $4, $7) }
| query '(' satisfiable File ')' '{' Formulas '}' { (Satisfiable, $4, $7) }
| query '(' retrieve File ')'    '{' Formulas '}' { (Retrieve,    $4, $7) }
| query '(' count File ')'       '{' Formulas '}' { (Counting,    $4, $7) }

File :: { Maybe String }
File :  { Nothing }
| ',' file  { Just $2 }

ProverSpecific :: { [ProverInfo] }
ProverSpecific : { [] }
| proverparameters '{' ProverList '}' { $3 }

ProverList :: { [ProverInfo] }
ProverList : { [] }
| prover '(' Variable ')' '{' OptionsList '}'  ProverList { ($3,$6):$8 }

OptionsList :: { [(String,String)] }
OptionsList : { [] }
| Variable '=' Value { [($1,$3)]  }
| Variable '=' Value ',' OptionsList { ($1,$3): $5 }

Value :: { String }
Value :
  Variable { $1 }
| label { $1 }
| true { "true" }
| false { "false" }

AutomaticSignature :: { [RelInfo] }
AutomaticSignature :
 automatic
 { % putType Automatic >>= \s -> return []}

ContentSignature :: { [RelInfo] }
ContentSignature :
  {% putType NotAutomatic >>= \s -> return []}
| propositions
  '{' VariableList '}' ContentSignature
  { % getSig >>= \s -> putSig (foldr addPToSig s $3)
             >>= \s -> putType NotAutomatic
             >>= \s -> return $5}
| nominals
  '{' VariableList '}' ContentSignature
  { % getSig >>= \s -> putSig (foldr addNToSig s $3)
             >>= \s -> putType NotAutomatic
             >>= \s -> return $5}
| relations
  '{' RelationList '}' ContentSignature
  { % getSig >>= \s -> putSig (foldr (addRToSig . fst) s $3)
             >>= \s -> putType NotAutomatic
             >>= \s -> return ($3++$5)}


RelationList :: { [RelInfo] }
RelationList : { [] }
| Variable { [($1, [])] }
| Variable ',' RelationList { ($1, []):$3 }
| Variable ':' '{' RelPropertyList '}' { [($1, $4)] }
| Variable ':' '{' RelPropertyList '}' ',' RelationList { ($1 , $4):$7  }

RelPropertyList :: { [RelProperty] }
RelPropertyList : { [] }
| UnaryRelProperty { [$1] }
| BinaryRelProperty { [$1] }
| UnaryRelProperty ',' RelPropertyList { $1:$3 }
| BinaryRelProperty ',' RelPropertyList {  $1:$3 }

UnaryRelProperty :: { RelProperty }
UnaryRelProperty :
  universal { Universal }
| difference { Difference }
| reflexive { Reflexive }
| transitive { Transitive }
| symmetric { Symmetric }
| functional { Functional }
| injective { Injective }

BinaryRelProperty :: { RelProperty }
BinaryRelProperty :
  subsetof Variable { SubsetOf [$2] }
| subsetof '{' VariableList '}' { SubsetOf $3 }
| equals Variable { Equals [$2] }
| equals '{' VariableList '}' { Equals $3 }
| inverseof Variable { InverseOf $2 }
| tclosureof Variable { TClosureOf $2 }
| trclosureof Variable { TRClosureOf $2 }

VariableList :: { [String] }
VariableList : { [] }
| Variable { [$1] }
| Variable ',' VariableList { $1:$3 }

Formulas :: { [Formula NomSymbol PropSymbol RelSymbol] }
Formulas : { [] }
| Formula                          { [$1] }
| Formula ';' Formulas             { $1:$3 }


Formula :: { Formula NomSymbol PropSymbol RelSymbol }
Formula :
  true                             { Top          }
| false                            { Bot          }
| nom
  { % get >>= \s -> if (isAutomatic s)
                    then return (Nom $1)
                    else if (isNomInSig $1 (pSig s))
                    then return (Nom $1)
                    else (error $ (show $1) ++ " not in Sig as Nominal")}
| prop
  { % get >>= \s -> if (isAutomatic s)
                    then return (Prop $1)
                    else if (isPropInSig $1 (pSig s))
                    then return (Prop $1)
                    else (error $ (show $1) ++ " not in Sig as Prop")      }
| variable
  { % getSig >>= \s -> if (isNomInSig (NomSymbol $1) s)
                       then return (Nom (NomSymbol $1))
                       else if (isPropInSig (PropSymbol $1) s)
                       then return (Prop (PropSymbol $1))
                       else if (isRelInSig (RelSymbol $1) s)
                       then error ($1 ++ " defined as Rel")
                       else (error $ "Symbol not in Sig : " ++ $1) }
| dia    Formula                   { Diam $1 $2   }
| udia   Formula                   { E $2         }
| ddia   Formula                   { D $2         }
| box    Formula                   { Box $1 $2    }
| ubox Formula                     { A $2         }
| dbox   Formula                   { B $2         }
| '<' Rel '>' Formula
  { % getSig >>= \s -> if (isRelInSig $2 s)
                       then return (Diam $2 $4)
                       else (error $ (show $2) ++ " not in Sig as Relation")}
| '[' Rel ']' Formula
  { % getSig >>= \s -> if (isRelInSig $2 s)
                       then return (Box $2 $4)
                       else (error $ (show $2) ++ " not in Sig as Relation")}
| Formula dimp Formula             { $1 :<-->: $3 }
| Formula imp Formula              { $1 :-->: $3  }
| neg Formula                      { Neg $2       }
| Formula and Formula              { $1 :&: $3    }
| Formula or Formula               { $1 :|: $3    }
| nom ':' Formula
  { % get >>= \s -> if (isAutomatic s)
                    then return (At $1 $3)
                    else if (isNomInSig $1 (pSig s))
                    then return (At $1 $3)
                    else (error $ (show $1) ++ " not defined as Nom in Sig")   }
| PropVar ':' Formula
  { % getSig >>= \s -> if (isNomInSig $1 s)
                       then return (At $1 $3)
                       else (error $ (show $1) ++ " not defined as Nom in Sig")   }
| down '(' nom Formula ')'
  { % get >>= \s -> if (isAutomatic s)
                    then return (Formula.Down $3 $4)
                    else if (isNomInSig $3 (pSig s))
                    then return (Formula.Down $3 $4)
                    else (error $ (show $3) ++ " not defined as Nom in Sig")   }
| down '(' PropVar Formula ')'
  { % getSig >>= \s -> if (isNomInSig $3 s)
                       then return (Formula.Down $3 $4)
                       else (error $ (show $3) ++ " not defined as Nom in Sig")   }
| down nom '.' Formula %prec down
  { % get >>= \s -> if (isAutomatic s)
                    then return (Formula.Down $2 $4)
                    else if (isNomInSig $2 (pSig s))
                    then return (Formula.Down $2 $4)
                    else (error $ (show $2) ++ " not defined as Nom in Sig")  }
| down PropVar '.' Formula %prec down
  { % getSig >>= \s -> if (isNomInSig $2 s)
                       then return (Formula.Down $2 $4)
                       else (error $ (show $2) ++ " not defined as Nom in Sig")  }
| CountSymbol integer '.' Formula        { Count $1 Global     $2 $4 }
| CountSymbol integer Rel '.' Formula
  { % getSig >>= \s -> if (isRelInSig $3 s)
                       then return (Count $1 (Local $3) $2 $5)
                       else (error $ (show $3) ++ " not in Sig as Relation")}
| '(' Formula ')'                        { $2           }

CountSymbol :: { CountOp }
CountSymbol :
  greaterEqual { :>=: }
| lowerEqual   { :<=: }
| greater      { :>:  }
| lower        { :<:  }
| equal        { :=:  }
| nonEqual     { :/=: }


Rel :: { RelSymbol }
Rel :
  prop     { let (PropSymbol l) = $1 in RelSymbol l }
| nom      { let (NomSymbol l) = $1 in RelSymbol l }
| variable { RelSymbol $1 }


PropVar :: { NomSymbol }
PropVar :
  prop     { let (PropSymbol l) = $1 in NomSymbol l }
| variable { NomSymbol $1 }


{
data ParseOutput = PO{relations :: [RelInfo],
                      provers   :: [ProverInfo],
                      theory    :: [Formula NomSymbol PropSymbol RelSymbol],
                      tasks     :: [InferenceTask]
                     } deriving (Show)

type RelInfo = (String,[RelProperty])
type ProverInfo = (String, [(String,String)])
type InferenceTask = (QueryType,
                      Maybe String,
                      [Formula NomSymbol PropSymbol RelSymbol])

data RelProperty   = Reflexive |
                     Symmetric |
                     Transitive |
                     Functional |
                     Injective |
                     Universal |
                     Difference |
                     --
                     InverseOf  String |
                     SubsetOf [String] |
                     Equals   [String] |
                     TClosureOf String |
                     TRClosureOf String
                     deriving (Eq, Show, Ord)

data QueryType = Valid | Satisfiable | Retrieve | Counting
                  deriving (Eq, Show)

data SignatureType = NotAutomatic | Automatic | NotSet deriving (Eq)

type ParseState = (StringSignature,SignatureType)

initParseState = (emptySignature, NotSet)

pSig = fst
pType = snd

isAutomatic s = (pType s) == Automatic


getSig :: State ParseState (StringSignature)
getSig = do
          state <- get
          return (fst state)

putSig :: StringSignature -> State ParseState ()
putSig s = do
            state <- get
            put (s,snd state)

getType :: State ParseState (SignatureType)
getType = do
           state <- get
           return (snd state)

putType :: SignatureType -> State ParseState ()
putType t = do
             state <- get
             put (fst state, t)

addPToSig l s =
  if (isNomInSig (NomSymbol l) s)
  then error $ l ++ " already declared as Nom"
  else if (isRelInSig (RelSymbol l) s)
  then error $ l ++ " already declared as Rel"
  else addPropToSig (PropSymbol l) s

addNToSig l s =
  if (isPropInSig (PropSymbol l) s)
  then error $ l ++ " already declared as Prop"
  else if (isRelInSig (RelSymbol l) s)
  then error $ l ++ " already declared as Rel"
  else addNomToSig (NomSymbol l) s

addRToSig l s =
  if (isPropInSig (PropSymbol l) s)
  then error $ l ++ " already declared as Prop"
  else if (isNomInSig (NomSymbol l) s)
  then error $ l ++ " already declared as Nom"
  else addRelToSig (RelSymbol l) s

happyError :: [(Token, FilePos)] -> a
happyError ((_, fp):_) = error ("Parse error near line " ++
                                   (show $ line fp) ++
                                   ", col. " ++
                                   (show $ col fp))
}