4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$

e47d29b522739fbf08aac80c6faa447dde113fbcChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2002-2004

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian MaederMaintainer : hets@tzi.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder parse terms and formulae

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder{-

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder http://www.cofi.info/Documents/CASL/Summary/

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder from 25 March 2001

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder C.2.1 Basic Specifications with Subsorts

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder remarks:

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder when-else-TERMs are non-mixfix,

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder because when-else has lowest precedence.

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder C.3.1 Precedence

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder Sorted (or casted) terms are not directly recognized,

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder because "u v : s" may be "u (v:s)" or "(u v):s"

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder No term or formula may start with a parenthesized argument list that

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder includes commas.

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder The arguments of qualified ops or preds can only be given by a following

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder parenthesized argument list.

62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Braced or bracketed term-lists including commas stem from a possible

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder %list-annotation or (for brackets) from compound lists.

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder C.6.3 Literal syntax for lists

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder `%list b1__b2, c, f'.

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder b1 must contain at least one open brace or bracket ("{" or [")

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder and all brackets must be balanced in "b1 b2" (the empty list).

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder all parsers are paramterized with a String list containing additional

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder keywords

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-}

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian Maedermodule CASL.Formula (term, formula, restrictedTerm, restrictedFormula, anColon

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , varDecl, opSort, opFunSort, opType, predType, predUnitType)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder where

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maederimport Common.AnnoState

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.Id

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.Keywords

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.Lexer

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.Token

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport CASL.AS_Basic_CASL

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Text.ParserCombinators.Parsec

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersimpleTerm :: [String] -> AParser st (TERM f)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaedersimpleTerm k = fmap Mixfix_token (pToken(scanFloat <|> scanString

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder <|> scanQuotedChar <|> scanDotWords

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder <|> reserved (k ++ casl_reserved_fwords) scanAnyWords

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder <|> reserved (k ++ casl_reserved_fops) scanAnySigns

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder <|> placeS <?> "id/literal" ))

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederrestTerms :: (AParsable f) => [String] -> AParser st [TERM f]

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederrestTerms k = (tryItemEnd startKeyword >> return []) <|>

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder bind (:) (restTerm k) (restTerms k)

fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder <|> return []

25612a7b3ce708909298d5426406592473880a20Christian Maeder

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederstartTerm, restTerm, mixTerm, whenTerm :: AParsable f => [String]

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder -> AParser st (TERM f)

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian MaederstartTerm k =

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder parenTerm <|> braceTerm <|> bracketTerm <|> try (addAnnos >> simpleTerm k)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederrestTerm k = startTerm k <|> typedTerm k <|> castedTerm k

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaedermixTerm k =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do l <- startTerm k <:> restTerms k

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder return (if isSingle l then head l else Mixfix_term l)

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaederwhenTerm k =

18b709ce961d68328da768318dcc70067f066d86Christian Maeder do t <- mixTerm k

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder do w <- asKey whenS

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder f <- impFormula k

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder e <- asKey elseS

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder r <- whenTerm k

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (Conditional t f r $ toPos w [] e)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|> return t

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maederterm :: AParsable f => [String] -> AParser st (TERM f)

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maederterm = whenTerm

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederrestrictedTerm :: AParsable f => [String] -> AParser st (TERM f)

797f811e57952d59e73b8cd03b667eef276db972Christian MaederrestrictedTerm = whenTerm

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian MaederanColon :: AParser st Token

797f811e57952d59e73b8cd03b667eef276db972Christian MaederanColon = wrapAnnos colonST

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian MaedertypedTerm, castedTerm :: [String] -> AParser st (TERM f)

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskitypedTerm k =

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder do c <- colonT

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder t <- sortId k

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder return $ Mixfix_sorted_term t $ tokPos c

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaedercastedTerm k =

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder do c <- asT

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder t <- sortId k

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder return $ Mixfix_cast t $ tokPos c

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maederterms :: AParsable f => [String] -> AParser st ([TERM f], [Token])

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maederterms k =

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder do (ts, ps) <- whenTerm k `separatedBy` anComma

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder return (ts, ps)

d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder

22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian MaederqualVarName, qualOpName :: Token -> AParser st (TERM f)

22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian MaederqualVarName o =

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder do v <- asKey varS

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder i <- varId []

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder c <- colonT

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder s <- sortId [] << addAnnos

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder p <- cParenT

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder return $ Qual_var i s $ toPos o [v, c] p

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederqualOpName o =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do v <- asKey opS

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder i <- parseId []

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder c <- anColon

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder t <- opType [] << addAnnos

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder p <- cParenT

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder return $ Application (Qual_op_name i t $ toPos o [v, c] p) [] []

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederopSort :: [String] -> GenParser Char st (Bool, Id, [Pos])

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederopSort k = fmap (\s -> (False, s, [])) (sortId k) <|>

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder do q <- quMarkT

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder s <- sortId k

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder return (True, s, tokPos q)

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederopFunSort :: [String] -> [Id] -> [Token] -> GenParser Char st OP_TYPE

9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederopFunSort k ts ps =

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder do a <- pToken (string funS)

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder (b, s, qs) <- opSort k

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return $ Op_type (if b then Partial else Total) ts s

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder (catPos (ps ++ [a]) ++ qs)

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian MaederopType :: [String] -> AParser st OP_TYPE

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaederopType k =

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder do (b, s, p) <- opSort k

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder if b then return (Op_type Partial [] s p)

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder else do c <- crossT

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder (ts, ps) <- sortId k `separatedBy` crossT

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder opFunSort k (s:ts) (c:ps)

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder <|> opFunSort k [s] []

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder <|> return (Op_type Total [] s [])

65835942d66905c377fa503e0d577df5aade58feChristian Maeder

65835942d66905c377fa503e0d577df5aade58feChristian MaederparenTerm, braceTerm, bracketTerm :: AParsable f => AParser st (TERM f)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederparenTerm =

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder do o <- wrapAnnos oParenT

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder qualVarName o <|> qualOpName o <|> qualPredName o <|>

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do (ts, ps) <- terms []

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder c <- addAnnos >> cParenT

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder return (Mixfix_parenthesized ts $ toPos o ps c)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederbraceTerm =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do o <- wrapAnnos oBraceT

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder (ts, ps) <- option ([], []) $ terms []

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder c <- addAnnos >> cBraceT

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder return $ Mixfix_braced ts $ toPos o ps c

bracketTerm =

do o <- wrapAnnos oBracketT

(ts, ps) <- option ([], []) $ terms []

c <- addAnnos >> cBracketT

return $ Mixfix_bracketed ts $ toPos o ps c

quant :: AParser st (QUANTIFIER, Token)

quant = do q <- asKey (existsS++exMark)

return (Unique_existential, q)

<|>

do q <- asKey existsS

return (Existential, q)

<|>

do q <- forallT

return (Universal, q)

<?> "quantifier"

quantFormula :: AParsable f => [String] -> AParser st (FORMULA f)

quantFormula k =

do (q, p) <- quant

(vs, ps) <- varDecl k `separatedBy` anSemi

d <- dotT

f <- impFormula k

return $ Quantification q vs f

$ toPos 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 (catPos ps ++ tokPos c)

predType :: [String] -> AParser st PRED_TYPE

predType k =

do (ts, ps) <- sortId k `separatedBy` crossT

return (Pred_type ts (catPos ps))

<|> predUnitType

predUnitType :: GenParser Char st PRED_TYPE

predUnitType = do o <- oParenT

c <- cParenT

return $ Pred_type [] (tokPos o ++ tokPos c)

qualPredName :: Token -> AParser st (TERM f)

qualPredName o =

do v <- asKey predS

i <- parseId []

c <- colonT

s <- predType [] << addAnnos

p <- cParenT

return $ Mixfix_qual_pred $ Qual_pred_name i s $ toPos o [v, c] p

parenFormula :: AParsable f => [String] -> AParser st (FORMULA f)

parenFormula k =

do o <- oParenT << addAnnos

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 <- impFormula [] << addAnnos

case f of Mixfix_formula t ->

do c <- cParenT

l <- restTerms k

let tt = Mixfix_parenthesized [t]

(toPos o [] c)

ft = if null l then tt

else Mixfix_term (tt:l)

in termFormula k ft

-- commas are not allowed

_ -> cParenT >> return f

termFormula :: AParsable f => [String] -> (TERM f) -> AParser st (FORMULA f)

termFormula k t = do e <- try (asKey exEqual)

r <- whenTerm k

return (Existl_equation t r $ tokPos e)

<|>

do try (string exEqual)

unexpected ("sign following " ++ exEqual)

<|>

do e <- try equalT

r <- whenTerm k

return (Strong_equation t r $ tokPos e)

<|>

do e <- try (asKey inS)

s <- sortId k

return (Membership t s $ tokPos e)

<|> return (Mixfix_formula t)

primFormula :: AParsable f => [String] -> AParser st (FORMULA f)

primFormula k = do f <- aparser

return (ExtFORMULA f)

<|>

do c <- asKey trueS

return (True_atom $ tokPos c)

<|>

do c <- asKey falseS

return (False_atom $ tokPos c)

<|>

do c <- asKey defS

t <- whenTerm k

return (Definedness t $ tokPos c)

<|>

do c <- try(asKey notS <|> asKey negS) <?> "\"not\""

f <- primFormula k

return (Negation f $ tokPos c)

<|> parenFormula k <|> quantFormula k

<|> (whenTerm k >>= termFormula k)

andKey, orKey :: AParser st Token

andKey = asKey lAnd

orKey = asKey lOr

andOrFormula :: AParsable f => [String] -> AParser st (FORMULA f)

andOrFormula k =

do f <- primFormula k

do c <- andKey

(fs, ps) <- primFormula k `separatedBy` andKey

return (Conjunction (f:fs) (catPos (c:ps)))

<|>

do c <- orKey

(fs, ps) <- primFormula k `separatedBy` orKey

return (Disjunction (f:fs) (catPos (c:ps)))

<|> return f

implKey, ifKey :: AParser st Token

implKey = asKey implS

ifKey = asKey ifS

impFormula :: AParsable f => [String] -> AParser st (FORMULA f)

impFormula k =

do f <- andOrFormula k

do c <- implKey

(fs, ps) <- andOrFormula k `separatedBy` implKey

return (makeImpl True (f:fs) (catPos (c:ps)))

<|>

do c <- ifKey

(fs, ps) <- andOrFormula k `separatedBy` ifKey

return (makeIf (f:fs) (catPos (c:ps)))

<|>

do c <- asKey equivS

g <- andOrFormula k

return (Equivalence f g $ tokPos c)

<|> return f

where makeImpl b [f,g] p = Implication f g b p

makeImpl b (f:r) (c:p) =

Implication f (makeImpl b r p) b [c]

makeImpl _ _ _ =

error "makeImpl got illegal argument"

makeIf l p = makeImpl False (reverse l) (reverse p)

formula :: AParsable f => [String] -> AParser st (FORMULA f)

formula = impFormula

restrictedFormula :: AParsable f => [String] -> AParser st (FORMULA f)

restrictedFormula = impFormula