OpItem.hs revision b8a232442cc858a3ad0f948d643b7d974f678553
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Authors: Christian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder parse OP-ITEM and "op/ops OP-ITEM ; ... ; OP-ITEM"
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder parse PRED-ITEM and "op/ops PRED-ITEM ; ... ; PRED-ITEM"
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder http://www.cofi.info/Documents/CASL/Summary/
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder from 25 March 2001
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder C.2.1 Basic Specifications with Subsorts
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule OpItem where
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maederimport AnnoState
64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Keywords
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport AS_Basic_CASL
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport AS_Annotation
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Formula
67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport ItemList
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- stupid cast
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederargDecl :: AParser ARG_DECL
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederargDecl = fmap (\(Var_decl vs s ps) -> Arg_decl vs s ps) varDecl
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzpredHead :: AParser PRED_HEAD
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederpredHead = do o <- oParenT
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder (vs, ps) <- argDecl `separatedBy` semiT
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder return (Pred_head vs (map tokPos (o:ps++[p])))
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopHead :: AParser OP_HEAD
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopHead = do Pred_head vs ps <- predHead
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder (b, s, _) <- opSort
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder let qs = ps ++ [tokPos c] in
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (if b then Partial_op_head vs s qs
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder else Total_op_head vs s qs)
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederopAttr :: AParser (OP_ATTR, Token)
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederopAttr = do p <- asKey assocS
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return (Assoc_op_attr, p)
65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder do p <- asKey commS
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (Comm_op_attr, p)
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do p <- asKey idemS
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Idem_op_attr, p)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do p <- asKey unitS
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Unit_op_attr t, p)
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederisConstant :: OP_TYPE -> Bool
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederisConstant(Total_op_type [] _ _) = True
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian MaederisConstant(Partial_op_type [] _ _) = True
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederisConstant _ = False
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoHead :: Pos -> OP_TYPE -> OP_HEAD
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoHead c (Total_op_type [] s _) = Total_op_head [] s [c]
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoHead c (Partial_op_type [] s _) = Partial_op_head [] s [c]
67869d63d1725c79e4c07b51acd466a31932b275Christian MaedertoHead _ _ = error "toHead got non-empty argument type"
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopItem :: AParser OP_ITEM
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopItem = do (os, cs) <- parseId `separatedBy` commaT
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder if length os == 1 then
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do c <- colonST
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder if isConstant t then
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder opBody (head os) (toHead (tokPos c) t)
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder <|> opAttrs os t [c] -- this always succeeds
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder else opAttrs os t [c]
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder do h <- opHead
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder opBody (head os) h
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do c <- colonST
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder opAttrs os t (cs++[c])
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopBody :: OP_NAME -> OP_HEAD -> AParser OP_ITEM
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopBody o h = do e <- equalT
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Op_defn o h (Annoted t [] a []) [tokPos e])
67869d63d1725c79e4c07b51acd466a31932b275Christian MaederopAttrs :: [OP_NAME] -> OP_TYPE -> [Token] -> AParser OP_ITEM
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopAttrs os t c = do q <- commaT
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (as, cs) <- opAttr `separatedBy` commaT
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let ps = sort (map tokPos (c ++ map snd as ++ (q:cs)))
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in return (Op_decl os t (map fst as) ps)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder <|> return (Op_decl os t [] (map tokPos c))
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder-- overlap "o:t" DEF-or DECL "o:t=e" or "o:t, assoc"
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopItems :: AParser SIG_ITEMS
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederopItems = itemList opS opItem Op_items
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- ----------------------------------------------------------------------
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- ----------------------------------------------------------------------
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederpredItem :: AParser PRED_ITEM
ecf557c0b4f953106755a239da2c0b168064d3f4Christian MaederpredItem = do (ps, cs) <- parseId `separatedBy` commaT
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder if length ps == 1 then
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder predBody (head ps) (Pred_head [] [])
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder do h <- predHead
6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder predBody (head ps) h
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder predTypeCont ps cs
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder else predTypeCont ps cs
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederpredBody :: PRED_NAME -> PRED_HEAD -> AParser PRED_ITEM
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzpredBody p h = do e <- asKey equivS
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder return (Pred_defn p h (Annoted f [] a []) [tokPos e])
083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederpredTypeCont :: [PRED_NAME] -> [Token] -> AParser PRED_ITEM
083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederpredTypeCont ps cs = do c <- colonT
083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder t <- predType
0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder return (Pred_decl ps t (map tokPos (cs++[c])))
083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederpredItems :: AParser SIG_ITEMS
392b67dbb9414475750ac2a977348de77354c600Christian MaederpredItems = itemList predS predItem Pred_items