{
module Parser where
    
import Data.Char
import Data.Data
import Control.Monad
import Data.List as L
import Lexer
import Data.Set as S
import Codec.TPTP.Base
import System.IO
import System.IO.Unsafe
import Control.Monad.Identity
}

%name parseTPTP
%tokentype { Token }
%error { 
          
          ((\xs -> case xs of
                    xs -> error ("Parse error, pos: "++show (take 25 xs))))
       }


%token
 tok_lp                 { LP }
 tok_rp                 { RP }
 tok_lbra               { Lbrack }
 tok_rbra               { Rbrack }
 tok_comma              { Comma }
 tok_dot                { Dot }
 tok_star               { Star }
 tok_plus               { Plus }
 tok_rangle             { Rangle }
 tok_colon              { Oper ":" }

 tok_iff                { Oper "<=>"}
 tok_implies            { Oper "=>"}
 tok_xor                { Oper "<~>"}
 tok_nor                { Oper "~|"}
 tok_nand               { Oper "~&"}
 tok_impliedby          { Oper "<=" }
 tok_equals             { Oper "=" }
 tok_nequals            { Oper "!=" }

 tok_exclam             { Oper "!" }
 tok_question           { Oper "?" }
 tok_ampersand          { Oper "&" }
 tok_vline              { Oper "|" }
 tok_tilde              { Oper "~" }

 tok_fof                { LowerWord "fof" }
 tok_cnf                { LowerWord "cnf" }
 tok_include_           { LowerWord "include" }

 tok_single_quoted      { SingleQuoted $$ }
 tok_distinct_object    { DoubleQuoted $$ }
 tok_dollar_word        { DollarWord $$ }
 tok_dollar_dollar_word { DollarDollarWord $$ }
 tok_upper_word         { UpperWord $$ }
 tok_lower_word         { LowerWord $$ }
 tok_signed_integer     { SignedInt $$ }
 tok_unsigned_integer   { UnsignedInt $$ }
 tok_real               { Real $$ }

 comment            { CommentToken $$ }

     
%% 

TPTP_file  :: {[TPTP_Input]}
TPTP_file  : {[]} | TPTP_input TPTP_file  {$1 : $2}
           
TPTP_input  :: {TPTP_Input}
TPTP_input  : annotated_formula  {$1} 
             | include  { $1 }
             | comment { Comment $1 }

annotated_formula  :: {TPTP_Input}
annotated_formula  :  fof_annotated  {$1} 
                    | cnf_annotated  {$1}

fof_annotated  :: {TPTP_Input}
fof_annotated  : fof lp name  comma formula_role  comma fof_formula  annotations  rp dot
       { AFormula        $3               $5                $7           $8 }
                
cnf_annotated  :: {TPTP_Input}
cnf_annotated  : cnf lp name  comma formula_role  comma cnf_formula  annotations  rp dot
       { AFormula          $3              $5  (univquant_free_vars $7) $8 }
       
       
annotations  :: { Annotations }
annotations  :  comma source optional_info  { Annotations $2 $3 } 
    | { NoAnnotations }

formula_role  :: {Role}
formula_role  : lower_word_ { Role $1 }


fof_formula  :: {Formula}
fof_formula  : binary_formula  { $1 }
              | unitary_formula  { $1 }
      
binary_formula  :: {Formula}
binary_formula  : nonassoc_binary  {$1}
                 | assoc_binary  {$1}
                 
nonassoc_binary  :: {Formula}
nonassoc_binary  : unitary_formula  binary_connective  unitary_formula 
                  { $2 $1 $3 }

                  
assoc_binary  :: {Formula}
assoc_binary  : or_formula  { $1 }
               | and_formula  { $1 }
    
                 
or_formula  :: {Formula}
or_formula  : unitary_formula   vline  unitary_formula  more_or_formula
               { foldl (.|.) ($1 .|. $3) $4 }
             
more_or_formula  :: {[Formula]}
more_or_formula  : {[]} | vline  unitary_formula more_or_formula 
                  { $2 : $3 }
                  
and_formula  :: {Formula}
and_formula  : unitary_formula  ampersand unitary_formula  more_and_formula
               { foldl (.&.) ($1 .&. $3) $4 }


more_and_formula  :: {[Formula]}
more_and_formula  : {[]} | ampersand unitary_formula more_and_formula 
                   { $2 : $3 }
                   
unitary_formula  :: {Formula}
unitary_formula  :  quantified_formula  {$1}
                  | unary_formula       {$1}
                  | atomic_formula      {$1}
                  | lp fof_formula  rp  {$2}
                   
quantified_formula  :: {Formula}
quantified_formula  : quantifier  lbra variable_list  rbra colon unitary_formula 
                     {      $1                $3                           $6 }

variable_list  :: {[V]}
variable_list  : variable  { [$1] }
                | variable  comma variable_list  { $1 : $3 }

unary_formula  :: {Formula}
unary_formula  : unary_connective  unitary_formula  { $1 $2 }
                | fol_infix_unary  { $1 }
   



-- cnf_formula :: {Formula}
-- cnf_formula : assoc_binary {$1}
--             | lp assoc_binary rp {$2}

cnf_formula  :: {Formula}
cnf_formula  :  lp disjunction  rp  { $2 }
              | disjunction  { $1 }

                
disjunction  :: {Formula}
disjunction  : literal  more_disjunction 
              { foldl (.|.) $1 $2 }
              
more_disjunction  :: {[Formula]}
more_disjunction  :  {[]} | vline  literal more_disjunction 
                   { $2 : $3 }

literal  :: {Formula}
literal  : atomic_formula  {$1} 
          | tilde atomic_formula  { (.~.) $2} 
          | fol_infix_unary  {$1}
          
fol_infix_unary  :: {Formula}
fol_infix_unary  : term  infix_inequality  term  { $2 $1 $3 }

quantifier :: {[V] -> Formula -> Formula}
quantifier  : exclam { for_all } | question { exists }

binary_connective  :: {Formula -> Formula -> Formula}
binary_connective  : iff { (.<=>.) }
                    | implies { (.=>.) }
                    | impliedby { (.<=.) }
                    | xor { (.<~>.) }
                    | nor  { (.~|.) }
                    | nand { (.~&.) }

--- assoc_connective  : vline  
---                    | ampersand
                   
unary_connective  :: {Formula -> Formula}
unary_connective  : tilde { (.~.) }

-- defined_type  :== atomic_defined_word 

-- defined_type  :== $oType | $o | $iType | $i | $tType | $real | $int
-- system_type  :== atomic_system_word 

atomic_formula  :: {Formula} 
atomic_formula  :  plain_atomic_formula    {$1}
                 | defined_atomic_formula  {$1}
                 | system_atomic_formula   {$1}
                 

plain_atomic_formula  :: {Formula}
plain_atomic_formula  : plain_term  { fApp2pApp $1 }

-- plain_atomic_formula  :== proposition  | predicate  lp arguments  rp 
-- proposition  :== predicate 
-- predicate  :== atomic_word 

defined_atomic_formula  :: {Formula}
defined_atomic_formula  :  defined_plain_formula  {$1} 
                         | defined_infix_formula  {$1}
                         
defined_plain_formula  :: {Formula}
defined_plain_formula  : defined_plain_term  {fApp2pApp $1}
                        
--defined_plain_formula  :== defined_prop  | defined_pred  lp arguments  rp 
--defined_prop  :== atomic_defined_word 
--defined_prop  :== $true | $false
--defined_pred  :== atomic_defined_word 
--defined_pred  :== $equal


defined_infix_formula  :: {Formula}
defined_infix_formula  : term  defined_infix_pred  term  { $2 $1 $3 }
                        
defined_infix_pred :: { Term -> Term -> Formula } 
defined_infix_pred  : infix_equality  { $1 }

infix_equality  :: { Term -> Term -> Formula }
infix_equality  : equals { (.=.) }
                
infix_inequality  :: { Term -> Term -> Formula }
infix_inequality  : nequals { (.!=.) }

system_atomic_formula  :: {Formula} 
system_atomic_formula  : system_term  {fApp2pApp $1}

term  :: {Term}                        
term  :  function_term  {$1}
       | variable       {var $1}
       
function_term  :: {Term}                        
function_term  : plain_term {$1} 
                | defined_term  {$1}
                | system_term {$1}

plain_term  :: {Term}                        
plain_term  :  constant                  {fApp $1 []}
             | functor  lp arguments  rp {fApp $1 $3}
              
constant  :: {AtomicWord}
constant  : functor {$1}

functor  :: {AtomicWord}
functor  : atomic_word {$1}

defined_term  :: {Term}                        
defined_term  : defined_atom {$1} 
               | defined_atomic_term {$1}
               

defined_atom  :: {Term}                        
defined_atom  : number {numberLitTerm $1} 
               | distinct_object {distinctObjectTerm (stripQuotes '"' $1)}
                 
defined_atomic_term :: {Term}                
defined_atomic_term  : defined_plain_term {$1}
                      
defined_plain_term  :: {Term}                        
defined_plain_term  : defined_constant {fApp (AtomicWord $1) []} 
                     | defined_functor  lp arguments  rp {fApp (AtomicWord $1) $3} 

defined_constant  :: {String}
defined_constant  : defined_functor {$1}
-- defined_constant  :==

defined_functor  :: {String}
defined_functor  : atomic_defined_word {$1}
-- defined_functor  :==

system_term  :: {Term} 
system_term  :  system_constant  {fApp (AtomicWord $1) []}
              | system_functor  lp arguments  rp {fApp (AtomicWord $1) $3} 

system_constant  :: {String}                
system_constant  : system_functor  {$1}

system_functor  :: {String}                
system_functor  : atomic_system_word {$1}
                 
variable  :: {V}
variable  : upper_word {V $1}

arguments  :: {[Term]}
arguments  : term  {[$1]}
            | term  comma arguments  { $1 : $3 }

source  :: {GTerm} 
source  : general_term  {$1}

-- source  :== dag_source  | internal_source  | external_source  | unknown

-- dag_source  :== name  | inference_record 

-- inference_record  :== inference lp inference_rule  comma useful_info  comma  [parent_list ] rp 
-- inference_rule  :== atomic_word 
-- parent_list  :== parent_info  | parent_info  comma parent_list 
-- parent_info  :== source parent_details 
-- parent_details  :== :general_list  | null 
-- internal_source  :== introduced lp intro_type optional_info  rp 
-- intro_type  :== definition | axiom_of_choice | tautology | assumption
-- external_source  :== file_source  | theory  | creator_source 
-- file_source  :== file lp file_name file_info  rp 
-- file_info  :==  comma name  | null 
-- theory  :== theory lp theory_name optional_info  rp 
-- theory_name  :== equality | ac
-- creator_source  :== creator lp creator_name optional_info  rp 
-- creator_name  :== atomic_word 

optional_info  :: {UsefulInfo} 
optional_info  :  comma useful_info  {$2} |  {NoUsefulInfo}
    
useful_info  :: { UsefulInfo }
useful_info  : general_list  {UsefulInfo $1}

-- useful_info  :== [] | [info_items ]
-- info_items  :== info_item  | info_item  comma info_items 
-- info_item  :== formula_item  | inference_item  | general_function 
-- formula_item  :== description_item  | iquote_item 
-- description_item  :== description lp atomic_word  rp 
-- iquote_item  :== iquote lp atomic_word  rp 
-- inference_item  :== inference_status  | assumptions_record  | refutation 
-- inference_status  :== status lp status_value  rp  | inference_info 
-- status_value  :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac | wec | eth | tau | wtc | wth | cax | sca | tca | wca |cup | csp | ecs | csa | cth | ceq | unc | wcc | ect | fun | uns | wuc | wct | scc | uca | noc

-- inference_info  :== inference_rule  lp atomic_word  comma general_list  rp 
-- assumptions_record  :== assumptions lp [name_list ] rp 
-- refutation  :== refutation lp file_source  rp 

include :: {TPTP_Input}
include  : include_ lp file_name formula_selection  rp dot { Include $3 $4 } 

formula_selection  :: {[AtomicWord]}
formula_selection  :  comma lbra name_list  rbra { $3 } 
                    |   { [] }

name_list  :: {[AtomicWord]}
name_list  : name  {[$1]}
            | name  comma name_list  { $1 : $3 }

              
general_term  :: {GTerm}
general_term  :  general_data  {GTerm $1} 
               | general_data colon general_term  {ColonSep $1 $3} 
               | general_list {GList $1} 

general_data  :: {GData}
general_data  :  atomic_word  { GWord $1 } 
               | atomic_word  lp general_terms  rp { GApp $1 $3 }  
               | variable  { GVar $1 }
               | number  { GNumber $1 }
               | distinct_object { GDistinctObject (stripQuotes '"' $1) }
               | formula_data  { $1 }
               
formula_data :: {GData}
formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 $3 }
              -- too ambiguous | dollar_word lp cnf_formula  rp { GFormulaData $1 $3 }
                
general_list  :: {[GTerm]}
general_list  : lbra rbra {[]}
               | lbra general_terms  rbra {$2}
               
general_terms  :: {[GTerm]}
general_terms  :  general_term  {[$1]} 
                | general_term  comma general_terms  {$1 : $3}

name  :: {AtomicWord}
name  : atomic_word  {$1}
       | unsigned_integer {AtomicWord(show $1)}
         
atomic_word  :: {AtomicWord}       
atomic_word  : lower_word_ {AtomicWord $1}
              | single_quoted{AtomicWord (stripQuotes '\'' $1)}
                
atomic_defined_word  :: {String}              
atomic_defined_word  : dollar_word{$1}
                      
atomic_system_word  :: {String}              
atomic_system_word  : dollar_dollar_word{$1}

number  :: {Double} -- maybe keep track of the number type that was actually parsed
number  : real {$1} | signed_integer {fromIntegral $1} | unsigned_integer {fromIntegral $1}
    
file_name  :: {String}              
file_name  : single_quoted {stripQuotes '\'' $1}
            
lower_word_ :: {String}
lower_word_ : lower_word {$1} | fof {"fof"} | cnf {"cnf"} | include_ {"include"} -- "fof" is a perfectly cromulent lower_word, but it is interpreted as a "fof" token

lp                 :: {Token}
lp                 : tok_lp                  comment_list { $1 }
rp                 :: {Token}
rp                 : tok_rp                  comment_list { $1 }
lbra               :: {Token}
lbra               : tok_lbra                comment_list { $1 }
rbra               :: {Token}
rbra               : tok_rbra                comment_list { $1 }
comma              :: {Token}
comma              : tok_comma               comment_list { $1 }
dot                :: {Token}
dot                : tok_dot                 comment_list { $1 }
star               :: {Token}
star               : tok_star                comment_list { $1 }
plus               :: {Token}
plus               : tok_plus                comment_list { $1 }
rangle             :: {Token}
rangle             : tok_rangle              comment_list { $1 }
colon              :: {Token}
colon              : tok_colon               comment_list { $1 }

iff                :: {Token}
iff                : tok_iff                 comment_list { $1 }
implies            :: {Token}
implies            : tok_implies             comment_list { $1 }
xor                :: {Token}
xor                : tok_xor                 comment_list { $1 }
nor                :: {Token}
nor                : tok_nor                 comment_list { $1 }
nand               :: {Token}
nand               : tok_nand                comment_list { $1 }
impliedby          :: {Token}
impliedby          : tok_impliedby           comment_list { $1 }
equals             :: {Token}
equals             : tok_equals              comment_list { $1 }
nequals            :: {Token}
nequals            : tok_nequals             comment_list { $1 }

exclam             :: {Token}
exclam             : tok_exclam              comment_list { $1 }
question           :: {Token}
question           : tok_question            comment_list { $1 }
ampersand          :: {Token}
ampersand          : tok_ampersand           comment_list { $1 }
vline              :: {Token}
vline              : tok_vline               comment_list { $1 }
tilde              :: {Token}
tilde              : tok_tilde               comment_list { $1 }

fof                :: {Token}
fof                : tok_fof                 comment_list { $1 }
cnf                :: {Token}
cnf                : tok_cnf                 comment_list { $1 }
include_           :: {Token}
include_           : tok_include_            comment_list { $1 }

single_quoted      :: {String}
single_quoted      : tok_single_quoted       comment_list { $1 }
distinct_object    :: {String}
distinct_object    : tok_distinct_object     comment_list { $1 }
dollar_word        :: {String}
dollar_word        : tok_dollar_word         comment_list { $1 }
dollar_dollar_word :: {String}
dollar_dollar_word : tok_dollar_dollar_word  comment_list { $1 }
upper_word         :: {String}
upper_word         : tok_upper_word          comment_list { $1 }
lower_word         :: {String}
lower_word         : tok_lower_word          comment_list { $1 }
signed_integer     :: {Int}
signed_integer     : tok_signed_integer      comment_list { $1 }
unsigned_integer   :: {Int}
unsigned_integer   : tok_unsigned_integer    comment_list { $1 }
real               :: {Double}
real               : tok_real                comment_list { $1 }

comment_list :: {[String]}
comment_list : {[]} | comment comment_list { $1 : $2 }
       
{

stripQuotes which (x:xs) = go xs
                      where
                        go [x] = []
                        go ('\\':'\\':xs) = '\\':go xs
                        go ('\\':which:xs) = which:go xs
                        go (x:xs) = x:go xs
                     
fApp2pApp (T (Identity (FunApp x args))) = (F (Identity (PredApp x args))) 
}