{- |
Module      :  ./DFOL/Parse_AS_DFOL.hs
Description :  A parser for first-order logic with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Parse_AS_DFOL
       (
           basicSpec           -- parser for DFOL specifications
       , symbItems           -- parser for symbol lists
       , symbMapItems        -- parser for symbol map lists
       )
       where

import qualified Common.Lexer as Lexer
import Common.Parsec
import Common.Token (criticalKeywords)
import qualified Common.Keywords as Keywords
import qualified Common.AnnoState as AnnoState
import Common.GlobalAnnotations (PrefixMap)
import DFOL.AS_DFOL
import Text.ParserCombinators.Parsec

-- keywords which cannot appear as identifiers in a signature
dfolKeys :: [String]
dfolKeys = [Keywords.trueS,
            Keywords.falseS,
            Keywords.notS,
            Keywords.forallS,
            Keywords.existsS,
            "Univ",
            "Sort",
            "Form",
            "Pi"] ++ criticalKeywords

-- parser for basic spec
basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
basicSpec _ = fmap Basic_spec (AnnoState.trailingAnnosParser basicItemP)
            <|>
            (Lexer.oBraceT >> Lexer.cBraceT >> return (Basic_spec []))

-- parser for basic items
basicItemP :: AnnoState.AParser st BASIC_ITEM
basicItemP = do AnnoState.dotT
                f <- formulaP
                return $ Axiom_item f
             <|>
             do ns <- namesP
                AnnoState.asKey "::"
                t <- typeP
                return $ Decl_item (ns, t)

-- parser for all types
typeP :: AnnoState.AParser st TYPE
typeP = do AnnoState.asKey "Pi"
           vs <- varsP
           t <- typeP
           return $ Pi vs t
        <|>
        do t <- type1P
           (do AnnoState.asKey Keywords.funS
               (ts, _) <- type1P `Lexer.separatedBy`
                            AnnoState.asKey Keywords.funS
               let xs = t : ts
               return $ Func (init xs) (last xs))
            <|>
            return t

-- parser for basic types and types enclosed in parentheses
type1P :: AnnoState.AParser st TYPE
type1P = do AnnoState.asKey "Sort"
            return Sort
         <|>
         do AnnoState.asKey "Form"
            return Form
         <|>
         do AnnoState.asKey "Univ"
            Lexer.oParenT
            t <- termP
            Lexer.cParenT
            return $ Univ t
         <|>
         do t <- termP
            return $ Univ t
         <|>
         do Lexer.oParenT
            t <- typeP
            Lexer.cParenT
            return t

-- parser for terms
termP :: AnnoState.AParser st TERM
termP = do f <- nameP
           do Lexer.oParenT
              (as, _) <- termP `Lexer.separatedBy` AnnoState.anComma
              Lexer.cParenT
              return $ Appl (Identifier f) as
             <|> return (Identifier f)

-- parsers for names
nameP :: AnnoState.AParser st NAME
nameP = Lexer.pToken $ reserved dfolKeys Lexer.scanAnyWords

namesP :: AnnoState.AParser st [NAME]
namesP = fmap fst $ nameP `Lexer.separatedBy` AnnoState.anComma

-- parser for variable declarations
varP :: AnnoState.AParser st ([NAME], TYPE)
varP = do ns <- namesP
          AnnoState.asKey Keywords.colonS
          t <- typeP
          return (ns, t)

varsP :: AnnoState.AParser st [([NAME], TYPE)]
varsP = do (vs, _) <- varP `Lexer.separatedBy` AnnoState.asKey ";"
           AnnoState.dotT
           return vs

-- parser for all formulas
formulaP :: AnnoState.AParser st FORMULA
formulaP = forallP
           <|>
           existsP
           <|>
           formula1P

{- parser for equivalences, implications, conjunctions, disjunctions,
   negations, equalities, atomic formulas, and formulas in parentheses -}
formula1P :: AnnoState.AParser st FORMULA
formula1P = do f <- formula2P
                -- equivalences
               (do AnnoState.asKey Keywords.equivS
                   g <- formula2P
                   return $ Equivalence f g)
                <|>
                -- implications
                do AnnoState.asKey Keywords.implS
                   g <- formula2P
                   return $ Implication f g
                <|> return f -- all other cases

{- parser for conjunctions, disjunctions, negations, equalities,
   atomic formulas, and formulas in parentheses -}
formula2P :: AnnoState.AParser st FORMULA
formula2P = do f <- formula3P
                -- conjunctions
               (do AnnoState.asKey Keywords.lAnd
                   (fs, _) <- formula3P `Lexer.separatedBy`
                                AnnoState.asKey Keywords.lAnd
                   return $ Conjunction (f : fs))
                <|>
                -- disjunctions
                do AnnoState.asKey Keywords.lOr
                   (fs, _) <- formula3P `Lexer.separatedBy`
                                AnnoState.asKey Keywords.lOr
                   return $ Disjunction (f : fs)
                <|> return f -- all other cases

{- parser for negations, equalities, atomic formulas,
   and formulas in parentheses -}
formula3P :: AnnoState.AParser st FORMULA
formula3P = parenFormulaP
            <|>
            negP
            <|>
            formula4P
            <|>
            trueP
            <|>
            falseP

-- parser for equalities and predicate formulas
formula4P :: AnnoState.AParser st FORMULA
formula4P = do x <- termP
                -- equalities
               (do AnnoState.asKey "=="
                   y <- termP
                   return $ Equality x y)
                <|>
                -- predicates
                return (Pred x)

-- parser for formulas enclosed in parentheses
parenFormulaP :: AnnoState.AParser st FORMULA
parenFormulaP = do Lexer.oParenT
                   f <- formulaP
                   Lexer.cParenT
                   return f

-- parser for forall formulas
forallP :: AnnoState.AParser st FORMULA
forallP = do AnnoState.asKey Keywords.forallS
             vs <- varsP
             f <- formulaP
             return $ Forall vs f

-- parser for exists formulas
existsP :: AnnoState.AParser st FORMULA
existsP = do AnnoState.asKey Keywords.existsS
             vs <- varsP
             f <- formulaP
             return $ Exists vs f

-- parser for negations
negP :: AnnoState.AParser st FORMULA
negP = do AnnoState.asKey Keywords.negS <|> AnnoState.asKey Keywords.notS
          f <- formula3P
          return $ Negation f

-- parser for true
trueP :: AnnoState.AParser st FORMULA
trueP = do AnnoState.asKey Keywords.trueS
           return T

-- parser for false
falseP :: AnnoState.AParser st FORMULA
falseP = do AnnoState.asKey Keywords.falseS
            return F

-- parser for symbol items
symbItems :: AnnoState.AParser st SYMB_ITEMS
symbItems = fmap Symb_items namesP

-- parser for symbol map items
symbMapItems :: AnnoState.AParser st SYMB_MAP_ITEMS
symbMapItems = do (xs, _) <- symbOrMap `Lexer.separatedBy` AnnoState.anComma
                  return $ Symb_map_items xs

-- parser for symbols or symbol maps
symbOrMap :: AnnoState.AParser st SYMB_OR_MAP
symbOrMap = do s <- nameP
               (do AnnoState.asKey Keywords.mapsTo
                   t <- nameP
                   return $ Symb_map s t)
                <|>
                return (Symb s)