Parse_AS_Basic.hs revision f6a16d60a0d5c672e5525ec04b82373e754b2fac
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederModule : $Header$
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederDescription : Parsing CASL's SIG-ITEMS, BASIC-ITEMS and BASIC-SPEC
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2002-2004
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederMaintainer : Christian.Maeder@dfki.de
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederStability : provisional
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederPortability : portable
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederParser for CASL basic specifications (SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Follows Sect. II:3.1 of the CASL Reference Manual.
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder http://www.cofi.info/Documents/CASL/Summary/
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder from 25 March 2001
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder C.2.1 Basic Specifications with Subsorts
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-- * signature items
23b1275b6136c9dbec63d3ea87c697f2aa89a061Liam O'ReillysortItems, typeItems, opItems, predItems, sigItems
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder :: (AParsable s, TermParser f) => [String] -> AParser st (SIG_ITEMS s f)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedersortItems ks = itemList ks esortS sortItem (Sort_items PossiblyEmptySorts)
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder <|> itemList ks sortS sortItem (Sort_items NonEmptySorts)
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedertypeItems ks = itemList ks typeS datatype (Datatype_items NonEmptySorts)
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder <|> itemList ks etypeS datatype (Datatype_items PossiblyEmptySorts)
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederopItems ks = itemList ks opS opItem Op_items
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederpredItems ks = itemList ks predS predItem Pred_items
b99a317dc5c91e28bd294248a0491c374783169aChristian MaedersigItems ks = fmap Ext_SIG_ITEMS aparser <|>
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder sortItems ks <|> opItems ks <|> predItems ks <|> typeItems ks
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederdatatypeToFreetype :: (AParsable b, AParsable s, TermParser f) =>
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederdatatypeToFreetype d pos =
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder Datatype_items sk ts ps -> Free_datatype sk ts (pos `appRange` ps)
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder _ -> error "datatypeToFreetype"
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederaxiomToLocalVarAxioms :: (AParsable b, AParsable s, TermParser f) =>
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
b99a317dc5c91e28bd294248a0491c374783169aChristian Maeder -> BASIC_ITEMS b s f
b99a317dc5c91e28bd294248a0491c374783169aChristian MaederaxiomToLocalVarAxioms ai a vs posl =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder Axiom_items (Annoted ft qs as rs : fs) ds ->
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let aft = Annoted ft qs (a ++ as) rs
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder in Local_var_axioms vs (aft : fs) (posl `appRange` ds)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder _ -> error "axiomToLocalVarAxioms"
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-- * basic items
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederbasicItems :: (AParsable b, AParsable s, TermParser f) =>
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder [String] -> AParser st (BASIC_ITEMS b s f)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederbasicItems ks = fmap Ext_BASIC_ITEMS aparser <|> fmap Sig_items (sigItems ks)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder f <- asKey freeS
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ti <- typeItems ks
42bccfa650b681c2602b412fec3863872c3d057bChristian Maeder return (datatypeToFreetype ti (tokPos f))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder g <- asKey generatedS
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder do t <- typeItems ks
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return (Sort_gen [Annoted t nullRange [] []] $ tokPos g)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder is <- annosParser (sigItems ks)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder a <- lineAnnos
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return (Sort_gen (init is ++ [appendAnno (last is) a])
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder (toRange g [o] c))
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder v <- pluralKeyword varS
de16f2cd7bef567000c39b40e6f7b0b263e49d12Christian Maeder (vs, ps) <- varItems ks
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return (Var_items vs (catRange (v : ps)))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (vs, ps) <- varDecls ks
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ai <- dotFormulae ks
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return (axiomToLocalVarAxioms ai a vs $ catRange (f : ps))
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder <|> dotFormulae ks
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder <|> itemList ks axiomS formula Axiom_items
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaedervarItems :: [String] -> AParser st ([VAR_DECL], [Token])
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder do v <- varDecl ks
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder do s <- trySemiOrComma
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder do tryItemEnd (ks ++ startKeyword)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return ([v], [s])
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (vs, ts) <- varItems ks
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return (v : vs, s : ts)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder <|> return ([v], [])
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederdotFormulae :: (AParsable b, AParsable s, TermParser f) =>
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder [String] -> AParser st (BASIC_ITEMS b s f)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederdotFormulae ks =
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (fs, ds) <- aFormula ks `separatedBy` dotT
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder (m, an) <- optSemi
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder let ps = catRange (d : ds)
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ns = init fs ++ [appendAnno (last fs) an]
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder return $ Axiom_items ns (ps `appRange` catRange m)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederaFormula :: TermParser f => [String] -> AParser st (Annoted (FORMULA f))
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederaFormula = allAnnoParser . formula
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder-- * basic spec
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederbasicSpec :: (TermParser f, AParsable s, AParsable b) =>
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder [String] -> AParser st (BASIC_SPEC b s f)
e90dc723887d541f809007ae81c9bb73ced9592eChristian MaederbasicSpec = fmap Basic_spec . annosParser . basicItems