Ast.hs revision 03b3c9dc9de5716538a9b04ae9bd8f36e22660e3
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedermodule Ast where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport ParseType
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederimport ParseTerm
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedertype SortId = Id
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedertype OpId = Id
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedertype VarId = Id
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersortStr = "sort"
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maedertype Axiom = Term
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata BasicItems = SigItems SigItems
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | FreeDatatypeItems [DatatypeDecl]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | SortGen [SigItems]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | VarItems [VarDecl]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | LocalVarDecl [VarDecl] [Axiom]
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder | Axioms [Axiom]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata SigItems = SortItems Keyword [SortItem]
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder | OpItems Keyword [OpItem]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder | DatatypeItems [DatatypeDecl]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder deriving (Show)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata SortItem = SubsortDecl [SortId] (Maybe Type)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | IsoDecl [SortId]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | SubsortDefn SortId VarId Type Term
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder | AnnotatedSortItem SortItem [Anno]
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedershowSortItem (SubsortDecl l Nothing) = showCommaList l
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedershowSortItem (SubsortDecl l (Just t)) =
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder showCommaList l . showSignStr lessStr . showSign t
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedershowSortItem (IsoDecl l) =
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder showSepList (showSignStr equalStr) showSign l
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedershowSortItem (AnnotatedSortItem s _) = shows s
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedershowSortItem (SubsortDefn s _ _ e) =
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder shows s. showSignStr equalStr . shows e
b99a317dc5c91e28bd294248a0491c374783169aChristian Maederinstance Show SortItem where
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder showsPrec _ = showSortItem
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederassocStr = "assoc"
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedercommStr = "comm"
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederidemStr = "idem"
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederunitStr = "unit"
b99a317dc5c91e28bd294248a0491c374783169aChristian Maederdata OpAttr = AssocOpAttr | CommOpAttr | IdemOpAttr | UnitOpAttr Term
b99a317dc5c91e28bd294248a0491c374783169aChristian Maederinstance Show OpAttr where
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder showsPrec _ AssocOpAttr = showString assocStr
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder showsPrec _ CommOpAttr = showString commStr
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder showsPrec _ IdemOpAttr = showString idemStr
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder showsPrec _ (UnitOpAttr t) = showSignStr unitStr . shows t
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder showList = showString . concat . map (\a -> ',' : show a)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata OpItem = OpItem [OpId] Type [OpAttr] (Maybe Term) [Anno]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder deriving (Show)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdata Component = Component Decl deriving (Show)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-- full function type (in Decl) of constructor
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maederdata Alternative = Construct Decl [Component]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder | Subsorts [SortId]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder deriving (Show)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederdata DatatypeDecl = DatatypeDecl SortId [Alternative] deriving (Show)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederclass Annotatable a where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder annotate :: a -> [Anno] -> a
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Annotatable OpItem where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder annotate (OpItem os t as def _) l = OpItem os t as def l
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederinstance Annotatable SortItem where
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder annotate (AnnotatedSortItem s _) l = AnnotatedSortItem s l
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder annotate s l = AnnotatedSortItem s l
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaedercommaSortDecl :: SortId -> Parser SortItem
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian MaedercommaSortDecl s = do { l <- comma >> (sortId `sepBy1` comma)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; let l' = s : l in
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder subSortDecl l'
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder <|> return (SubsortDecl l' Nothing)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederisoDecl :: SortId -> Parser SortItem
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederisoDecl s = do { e <- equal
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; subSortDefn s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (do { l <- sortId `sepBy1` equal
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; return (IsoDecl (s:l))
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersubSortDefn :: SortId -> Parser SortItem
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersubSortDefn s = do { o <- oBrace
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; t <- colon >>= funType
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; dot <|> bar
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; e <- parseTerm
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; let f = Binding SupersortVar [Decl (Symb [v] t) o []] e
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder in return (SubsortDefn s v t f)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersubSortDecl :: [SortId] -> Parser SortItem
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersubSortDecl l = do { s <- lessSign >>= funType
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; return (SubsortDecl l (Just s))
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedersortItem :: Parser SortItem
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersortItem = do { s <- sortId
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; subSortDecl [s]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder commaSortDecl s
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return (SubsortDecl [s] Nothing)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersortItems = do { key <- pluralKeyword sortStr
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; l <- itemAux sortItem
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; return (SortItems key l)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederpluralKeyword s = makeToken (string s <++> option "" (string "s"))
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederoptSemi = bind (\ x y -> (x, y)) (option Nothing (fmap Just semi)) ann
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederdot = toKey [dotChar] <|> toKey middleDotStr <?> "dot"
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maederbar = toKey [barChar]
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maederequal = toKey equalStr
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederisStartKeyword s = s `elem` [dotChar]:middleDotStr:casl_reserved_words
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederlookAheadItemKeyword :: a -> Parser a
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederlookAheadItemKeyword a =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder do { c <- lookAhead (many (oneOf (['0'..'9'] ++ "'" ++ caslLetters))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder <|> many (oneOf signChars))
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder ; if isStartKeyword c then return a else unexpected c
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederitemAux :: Annotatable a => (Parser a) -> Parser [a]
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederitemAux itemParser =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder do { i <- itemParser
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder ; (m, an) <- optSemi
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ; let i' = if null an then i else annotate i an
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder in case m of Nothing -> return [i']
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Just _ -> try (lookAheadItemKeyword [i'])
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder do { l <- itemAux itemParser
c2d9fa54f8da9197cb390788901d8e16d4f8d210Christian Maeder ; return (i':l)