{ {-# OPTIONS -XDeriveDataTypeable -XCPP #-} 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 } %name parseTPTP %tokentype { Token } %error { ((\xs -> case xs of xs -> error ("Parse error, pos: "++show (take 25 xs)))) } %token lp { LP } rp { RP } lbra { Lbrack } rbra { Rbrack } comma { Comma } dot { Dot } star { Star } plus { Plus } rangle { Rangle } colon { Oper ":" } iff { Oper "<=>"} implies { Oper "=>"} xor { Oper "<~>"} nor { Oper "~|"} nand { Oper "~&"} impliedby { Oper "<=" } equals { Oper "=" } nequals { Oper "!=" } exclam { Oper "!" } question { Oper "?" } ampersand { Oper "&" } vline { Oper "|" } tilde { Oper "~" } fof { LowerWord "fof" } cnf { LowerWord "cnf" } include_ { LowerWord "include" } single_quoted { SingleQuoted $$ } distinct_object { DoubleQuoted $$ } dollar_word { DollarWord $$ } dollar_dollar_word { DollarDollarWord $$ } upper_word { UpperWord $$ } lower_word { LowerWord $$ } signed_integer { SignedInt $$ } unsigned_integer { UnsignedInt $$ } 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 (fst $8) (snd $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) (fst $8)(snd $8) } annotations :: { (SourceInfo,UsefulInfo) } annotations : comma source optional_info { ($2,$3) } | { (NoSourceInfo, NoUsefulInfo) } 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 :: {[String]} 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 :: {[String] -> 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 {let TT (FunApp x args) = $1 in pApp x args} -- 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 {let TT (FunApp x args) = $1 in pApp x args} --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 {let TT (FunApp x args) = $1 in pApp x args} 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 :: {String} variable : upper_word {$1} arguments :: {[Term]} arguments : term {[$1]} | term comma arguments { $1 : $3 } source :: {SourceInfo} source : general_term {SourceInfo $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 { 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 }