content: {- |
  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)
  