2b873214c9ab511bbca437c036371ab664aedaceChristian Maedermodule BasicItem where

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maederimport Id

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederimport Lexer

54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian Maederimport LocalEnv

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskiimport Maybe

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maederimport Parsec

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskiimport ParseTerm

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowskiimport ParseType

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Token

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederimport Term

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederimport Type

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

da955132262baab309a50fdffe228c9efe68251dCui Jian{-

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian MaederisSigStartKeyword s = s `elem` (words "sort sorts op ops pred preds type types var vars axiom axioms forall free generated .")

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder-}

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermapf :: (Functor f) => f a -> (a -> b) -> f b

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maedermapf = flip fmap

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder

52d922076b89f12234f721974e82531bc69a6f69Christian MaederpluralKeyword s = makeToken (string s <++> option "" (string "s"))

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder

43b4c41fbb07705c9df321221ab9cb9832460407Christian MaedersortId = parseId

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian MaederopId = parseId

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian MaederoptSemi = bind (\ x y -> (x, y)) (option Nothing (fmap Just semi)) ann

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian MaedertopVarDecls t = do { l <- varDecl t

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ; (m, an) <- optSemi

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder ; let h:t = reverse l

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder h2 = h {declAn = an}

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder l2 = reverse (h2:t)

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder in

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder case m of Nothing -> return l2

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Just key -> do { r <- option [] (try (topVarDecls key))

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning ; return (l2 ++ r)

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder }

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu }

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederdata ParsedSortItems = AllLess [(Token, Id)] (Maybe (Token, Id))

a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder | AllEqual [(Token, Id)]

0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder | SubType (Token, Id) Type Term

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder deriving (Show)

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaedercommaSortDecl :: [(Token, Id)] -> Parser ParsedSortItems

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaedercommaSortDecl l = do { c <- comma

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder ; s <- sortId

6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maeder ; let l2 = (c, s) : l in

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl commaSortDecl l2

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova <|> subSortDecl l2

63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz <|> return (AllLess l2 Nothing)

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder }

14c89b2d830777bf4db2850f038c9f60acaca486Christian MaederequalSortDecl :: Token -> [(Token, Id)] -> Parser [(Token, Id)]

57026bc09337d158b89775048a9bcc9c17d825caChristian MaederequalSortDecl e l = do { s2 <- sortId

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder ; let l2 = (e, s2):l in

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder option l2 (do { e2 <- equal

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder ; equalSortDecl e2 l2

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder })

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl }

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

2b873214c9ab511bbca437c036371ab664aedaceChristian Maederequal = skipChar '='

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederisoDecl :: Token -> Id -> Parser ParsedSortItems

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederisoDecl key s1 = do { e <- equal

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder ; subSortDefn key s1

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder <|>

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross (do { l <- equalSortDecl e [(key, s1)]

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross ; return (AllEqual l)

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder })

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder }

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maederbar = skipChar '|'

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder

a31430de8b0632d29f42634d6395e982bf31b14dChristian MaedersubSortDefn :: Token -> Id -> Parser ParsedSortItems

a31430de8b0632d29f42634d6395e982bf31b14dChristian MaedersubSortDefn key s = do { o <- oBrace

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; v <- varId

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; c <- colon

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; t <- funType c

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; bar

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; e <- mixTerm

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; cBrace

a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ; let f = Binding SupersortVar [Decl (Symb v t) o []] e

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder in return (SubType (key, s) t f)

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder }

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder

9175e29c044318498a40f323f189f9dfd50378efChristian MaedersubSortDecl :: [(Token, Id)] -> Parser ParsedSortItems

9175e29c044318498a40f323f189f9dfd50378efChristian MaedersubSortDecl l = do { t <- skipChar '<'

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder ; s <- sortId

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl ; return (AllLess l (Just (t, s)))

f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian Maeder }

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedersortItem :: Token -> Parser ParsedSortItems

f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian MaedersortItem key = do { s1 <- sortId

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ; subSortDecl [(key, s1)]

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder <|>

bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas commaSortDecl [(key, s1)]

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder <|>

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder isoDecl key s1

e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder <|>

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder return (AllLess [(key, s1)] Nothing)

57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder }

22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder

7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von SchroedertoSymb s = Symb s Sort

fa388aea9cef5f9734fec346159899a74432ce26Christian MaedermkItem :: [Type] -> [Type] -> (Token, Id) -> SortItem

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedermkItem subs supers (key, id) =

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder SortItem (Decl (toSymb id) key []) (SortRels subs supers) Nothing []

0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder

52d922076b89f12234f721974e82531bc69a6f69Christian MaederasSortItems :: ParsedSortItems -> [SortItem]

52d922076b89f12234f721974e82531bc69a6f69Christian MaederasSortItems (AllLess l m) =

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl let p = maybeToList m

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova f = map (asType . snd)

72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz super = f p

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder sis = map (mkItem [] super) l

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder subs = reverse (f l)

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder supers = map (mkItem subs []) p

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder in supers ++ sis

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder

bb63f684c4f5f33ffcd1dcc02c58d6a703900fafJonathan von SchroederasSortItems (AllEqual l) =

b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder let types = reverse (map (asType . snd) l)

b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder sorts = map (mkItem types types) l

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross in sorts -- maybe delete self

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross

d56ece59c372cb887355825901222b9f3377f7e6Thiemo WiedemeyerasSortItems (SubType p t e) =

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer [(mkItem [] [t] p) {sortDef = Just (SubsortDefn e)}]

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder

9175e29c044318498a40f323f189f9dfd50378efChristian MaedersortItemsAux sig key = do { si <- sortItem key;

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder (m, an) <- optSemi;

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich let (l:li) = asSortItems si

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder li2 = (l {sortAn = an}) : li

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder sig2 = sig {sorts = li2 ++ sorts sig}

in

case m of Nothing -> return sig2

Just key -> option sig2

(try (sortItemsAux sig2 key))

}

sortItems sig = do { key <- pluralKeyword "sort"

; sortItemsAux sig key

}

opItem = do { o1 <- opId;

opDecl o1

<|>

opDefn o1

}

opDecl = return

opDefn = return

opItems = do { pluralKeyword "op";

s <- sepBy1 opItem semi;

optSemi;

return s;

}

sigItems = sortItems -- <|> opItems

basicItem = sigItems

basicItem :: Env -> Parser Env

basicItems sig = do { sig2 <- basicItem sig;

option (sig2) (basicItems sig2)

}

basicSpec sig = do { ann;

basicItems sig

}