hets/CASL/Formula.hs

	Formula.hs revision 4ac9fad8454f66963e8985a41e061653147d4d60
{- |
Module      :  $Header$
Description :  Parser for CASL terms and formulae
Copyright   :  (c) Christian Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

parse terms and formulae
-}

{-
   http://www.cofi.info/Documents/CASL/Summary/
   from 25 March 2001
   C.2.1 Basic Specifications with Subsorts

   remarks:

   when-else-TERMs are non-mixfix,
   because when-else has lowest precedence.
   C.3.1 Precedence

   Sorted (or casted) terms are not directly recognized,
   because "u v : s" may be "u (v:s)" or "(u v):s"

   No term or formula may start with a parenthesized argument list that
   includes commas.

   The arguments of qualified ops or preds can only be given by a following
   parenthesized argument list.

   Braced or bracketed term-lists including commas stem from a possible
   %list-annotation or (for brackets) from compound lists.

   C.6.3 Literal syntax for lists

   `%list b1__b2, c, f'.
   b1 must contain at least one open brace or bracket ("{" or [")
   and all brackets must be balanced in "b1 b2" (the empty list).

   all parsers are paramterized with a String list containing additional
   keywords
-}

module CASL.Formula
    ( term
    , primFormula
    , formula
    , anColon
    , varDecl
    , opSort
    , opFunSort
    , opType
    , predType
    , predUnitType
    , qualPredName
    ) where

import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token

import CASL.AS_Basic_CASL

import Text.ParserCombinators.Parsec

simpleTerm :: [String] -> AParser st (TERM f)
simpleTerm k = fmap Mixfix_token $ pToken
    ( scanFloat
  <|> scanString
  <|> scanQuotedChar
  <|> scanDotWords
  <|> reserved (k ++ casl_reserved_fwords) scanAnyWords
  <|> reserved (k ++ casl_reserved_fops) scanAnySigns
  <|> placeS
  <?> "id/literal" )

restTerms :: TermParser f => [String] -> AParser st [TERM f]
restTerms k = (tryItemEnd startKeyword >> return [])
  <|> restTerm k <:> restTerms k
  <|> return []

startTerm :: TermParser f => [String] -> AParser st (TERM f)
startTerm k = fmap ExtTERM (termParser True) <|>
    parenTerm <|> braceTerm <|> bracketTerm <|> try (addAnnos >> simpleTerm k)

restTerm :: TermParser f => [String] -> AParser st (TERM f)
restTerm k = startTerm k <|> typedTerm k <|> castedTerm k

mixTerm :: TermParser f => [String] -> AParser st (TERM f)
mixTerm k = do
  l <- startTerm k <:> restTerms k
  return $ if isSingle l then head l else Mixfix_term l

-- | when-else terms
term :: TermParser f => [String] -> AParser st (TERM f)
term k = do
  t <- mixTerm k
  option t $ do
    w <- asKey whenS
    f <- formula k
    e <- asKey elseS
    r <- term k
    return $ Conditional t f r $ toRange w [] e

anColon :: AParser st Token
anColon = wrapAnnos colonST

typedTerm :: [String] -> AParser st (TERM f)
typedTerm k = do
  c <- colonT
  t <- sortId k
  return $ Mixfix_sorted_term t $ tokPos c

castedTerm :: [String] -> AParser st (TERM f)
castedTerm k = do
  c <- asT
  t <- sortId k
  return $ Mixfix_cast t $ tokPos c

terms :: TermParser f => [String] -> AParser st ([TERM f], [Token])
terms k = term k `separatedBy` anComma

qualVarName :: Token -> AParser st (TERM f)
qualVarName o = do
  v <- asKey varS
  i <- varId []
  c <- colonT
  s <- sortId [] << addAnnos
  p <- cParenT
  return $ Qual_var i s $ toRange o [v, c] p

qualOpName :: Token -> AParser st (TERM f)
qualOpName o = do
  v <- asKey opS
  i <- parseId []
  c <- anColon
  t <- opType [] << addAnnos
  p <- cParenT
  return $ Application (Qual_op_name i t $ toRange o [v, c] p) [] nullRange

opSort :: [String] -> GenParser Char st (Bool, Id, Range)
opSort k = fmap (\ s -> (False, s, nullRange)) (sortId k) <|> do
  q <- quMarkT
  s <- sortId k
  return (True, s, tokPos q)

opFunSort :: [String] -> [Id] -> [Token] -> GenParser Char st OP_TYPE
opFunSort k ts ps = do
  a <- pToken (string funS)
  (b, s, qs) <- opSort k
  return $ Op_type (if b then Partial else Total) ts s
             $ appRange (catRange $ ps ++ [a]) qs

opType :: [String] -> AParser st OP_TYPE
opType k = do
  (b, s, p) <- opSort k
  if b then return $ Op_type Partial [] s p else do
      c <- crossT
      (ts, ps) <- sortId k `separatedBy` crossT
      opFunSort k (s : ts) (c : ps)
    <|> opFunSort k [s] []
    <|> return (Op_type Total [] s nullRange)

parenTerm :: TermParser f => AParser st (TERM f)
parenTerm = do
  o <- wrapAnnos oParenT
  qualVarName o <|> qualOpName o <|> qualPredName [] o <|> do
    (ts, ps) <- terms []
    c <- addAnnos >> cParenT
    return (Mixfix_parenthesized ts $ toRange o ps c)

braceTerm :: TermParser f => AParser st (TERM f)
braceTerm = do
  o <- wrapAnnos oBraceT
  (ts, ps) <- option ([], []) $ terms []
  c <- addAnnos >> cBraceT
  return $ Mixfix_braced ts $ toRange o ps c

bracketTerm :: TermParser f => AParser st (TERM f)
bracketTerm = do
  o <- wrapAnnos oBracketT
  (ts, ps) <- option ([], []) $ terms []
  c <- addAnnos >> cBracketT
  return $ Mixfix_bracketed ts $ toRange o ps c

quant :: AParser st (QUANTIFIER, Token)
quant = choice (map (\ (q, s) -> do
    t <- asKey s
    return (q, t))
  [ (Unique_existential, existsS ++ exMark)
  , (Existential, existsS)
  , (Universal, forallS) ])
  <?> "quantifier"

quantFormula :: TermParser f => [String] -> AParser st (FORMULA f)
quantFormula k = do
  (q, p) <- quant
  (vs, ps) <- varDecl k `separatedBy` anSemi
  d <- dotT
  f <- formula k
  return $ Quantification q vs f $ toRange p ps d

varDecl :: [String] -> AParser st VAR_DECL
varDecl k = do
  (vs, ps) <- varId k `separatedBy` anComma
  c <- colonT
  s <- sortId k
  return $ Var_decl vs s (catRange ps `appRange` tokPos c)

predType :: [String] -> AParser st PRED_TYPE
predType k = do
    (ts, ps) <- sortId k `separatedBy` crossT
    return (Pred_type ts (catRange ps))
  <|> predUnitType

predUnitType :: GenParser Char st PRED_TYPE
predUnitType = do
  o <- oParenT
  c <- cParenT
  return $ Pred_type [] (tokPos o `appRange` tokPos c)

qualPredName :: [String] -> Token -> AParser st (TERM f)
qualPredName k o = do
  v <- asKey predS
  i <- parseId k
  c <- colonT
  s <- predType k << addAnnos
  p <- cParenT
  return $ Mixfix_qual_pred $ Qual_pred_name i s $ toRange o [v, c] p

parenFormula :: TermParser f => [String] -> AParser st (FORMULA f)
parenFormula k = oParenT << addAnnos >>= clParenFormula k

clParenFormula :: TermParser f => [String] -> Token -> AParser st (FORMULA f)
clParenFormula k o = do
      q <- qualPredName [] o <|> qualVarName o <|> qualOpName o
      l <- restTerms []  -- optional arguments
      termFormula k $ if null l then q else Mixfix_term $ q : l
    <|> do
      f <- formula [] << addAnnos
      case f of
        Mixfix_formula t -> do
          c <- cParenT
          l <- restTerms k
          let tt = Mixfix_parenthesized [t] $ toRange o [] c
              ft = if null l then tt else Mixfix_term $ tt : l
          termFormula k ft -- commas are not allowed
        _ -> cParenT >> return f

termFormula :: TermParser f => [String] -> TERM f -> AParser st (FORMULA f)
termFormula k t = do
    e <- asKey exEqual
    r <- term k
    return $ Existl_equation t r $ tokPos e
  <|> do
    tryString exEqual
    unexpected $ "sign following " ++ exEqual
  <|> do
    e <- equalT
    r <- term k
    return $ Strong_equation t r $ tokPos e
  <|> do
    e <- asKey inS
    s <- sortId k
    return $ Membership t s $ tokPos e
  <|> return (Mixfix_formula t)

primFormula :: TermParser f => [String] -> AParser st (FORMULA f)
primFormula k = do
    f <- termParser False
    return $ ExtFORMULA f
  <|> do
    c <- asKey trueS
    return . True_atom . Range $ tokenRange c
  <|> do
    c <- asKey falseS
    return . False_atom . Range $ tokenRange c
  <|> do
    c <- asKey defS
    t <- term k
    return . Definedness t $ tokPos c
  <|> do
    c <- asKey notS <|> asKey negS <?> "\"not\""
    f <- primFormula k
    return $ Negation f $ tokPos c
  <|> parenFormula k
  <|> quantFormula k
  <|> (term k >>= termFormula k)

andKey :: AParser st Token
andKey = asKey lAnd

orKey :: AParser st Token
orKey = asKey lOr

andOrFormula :: TermParser f => [String] -> AParser st (FORMULA f)
andOrFormula k = primFormula k >>= optAndOr k

optAndOr :: TermParser f => [String] -> FORMULA f -> AParser st (FORMULA f)
optAndOr k f = do
      c <- andKey
      (fs, ps) <- primFormula k `separatedBy` andKey
      return $ Conjunction (f : fs) $ catRange $ c : ps
    <|> do
      c <- orKey
      (fs, ps) <- primFormula k `separatedBy` orKey
      return $ Disjunction (f : fs) $ catRange $ c : ps
    <|> return f

implKey :: AParser st Token
implKey = asKey implS

ifKey :: AParser st Token
ifKey = asKey ifS

formula :: TermParser f => [String] -> AParser st (FORMULA f)
formula k = andOrFormula k >>= optImplForm k

optImplForm :: TermParser f => [String] -> FORMULA f -> AParser st (FORMULA f)
optImplForm k f = do
      c <- implKey
      (fs, ps) <- andOrFormula k `separatedBy` implKey
      return $ makeImpl True (f : fs) $ catPosAux $ c : ps
    <|> do
      c <- ifKey
      (fs, ps) <- andOrFormula k `separatedBy` ifKey
      return $ makeIf (f : fs) $ catPosAux $ c : ps
    <|> do
      c <- asKey equivS
      g <- andOrFormula k
      return $ Equivalence f g $ tokPos c
    <|> return f

makeImpl :: Bool -> [FORMULA f] -> [Pos] -> FORMULA f
makeImpl b l p = case (l, p) of
  ([f, g], _) -> Implication f g b (Range p)
  (f : r, c : q) -> Implication f (makeImpl b r q) b (Range [c])
  _ -> error "makeImpl got illegal argument"

makeIf :: [FORMULA f] -> [Pos] -> FORMULA f
makeIf l p = makeImpl False (reverse l) $ reverse p