Parse_AS_Basic.hs revision 2c47bb55d963ff37dbae4a0a7701274fddb95fc8
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule : $Header$
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyDescription : Parsing CASL's SIG-ITEMS, BASIC-ITEMS and BASIC-SPEC
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : (c) Christian Maeder, Uni Bremen 2002-2004
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyMaintainer : Christian.Maeder@dfki.de
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : provisional
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : portable
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyParser for CASL basic specifications (SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Follows Sect. II:3.1 of the CASL Reference Manual.
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder from 25 March 2001
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly C.2.1 Basic Specifications with Subsorts
fa373bc327620e08861294716b4454be8d25669fChristian Maeder-- * signature items
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillysortItems, typeItems, opItems, predItems, sigItems
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly :: (AParsable s, AParsable f) => [String] -> AParser st (SIG_ITEMS s f)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillysortItems ks = itemList ks esortS sortItem (Sort_items PossiblyEmptySorts)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly <|> itemList ks sortS sortItem (Sort_items NonEmptySorts)
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillytypeItems ks = itemList ks typeS datatype (Datatype_items NonEmptySorts)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly <|> itemList ks etypeS datatype (Datatype_items PossiblyEmptySorts)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederopItems ks = itemList ks opS opItem Op_items
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederpredItems ks = itemList ks predS predItem Pred_items
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedersigItems ks = fmap Ext_SIG_ITEMS aparser <|>
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sortItems ks <|> opItems ks <|> predItems ks <|> typeItems ks
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederdatatypeToFreetype :: (AParsable b, AParsable s, AParsable f) =>
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederdatatypeToFreetype d pos =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Datatype_items sk ts ps -> Free_datatype sk ts (pos `appRange` ps)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder _ -> error "datatypeToFreetype"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyaxiomToLocalVarAxioms :: (AParsable b, AParsable s, AParsable f) =>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -> BASIC_ITEMS b s f
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaxiomToLocalVarAxioms ai a vs posl =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Axiom_items ((Annoted ft qs as rs):fs) ds ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder let aft = Annoted ft qs (a++as) rs
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder in Local_var_axioms vs (aft:fs) (posl `appRange` ds)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder _ -> error "axiomToLocalVarAxioms"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- * basic items
fa373bc327620e08861294716b4454be8d25669fChristian MaederbasicItems :: (AParsable b, AParsable s, AParsable f) =>
fa373bc327620e08861294716b4454be8d25669fChristian Maeder [String] -> AParser st (BASIC_ITEMS b s f)
fa373bc327620e08861294716b4454be8d25669fChristian MaederbasicItems ks = fmap Ext_BASIC_ITEMS aparser <|> fmap Sig_items (sigItems ks)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder <|> do f <- asKey freeS
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ti <- typeItems ks
fa373bc327620e08861294716b4454be8d25669fChristian Maeder return (datatypeToFreetype ti (tokPos f))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder <|> do g <- asKey generatedS
fa373bc327620e08861294716b4454be8d25669fChristian Maeder do t <- typeItems ks
fa373bc327620e08861294716b4454be8d25669fChristian Maeder return (Sort_gen [Annoted t nullRange [] []] $ tokPos g)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder do o <- oBraceT
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is <- annosParser (sigItems ks)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder a <- lineAnnos
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder return (Sort_gen (init is ++ [appendAnno (last is) a])
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (toRange g [o] c))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|> do v <- pluralKeyword varS
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (vs, ps) <- varItems ks
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder return (Var_items vs (catRange (v:ps)))
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder <|> do f <- forallT
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (vs, ps) <- varDecl ks `separatedBy` anSemi
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ai <- dotFormulae ks
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder return (axiomToLocalVarAxioms ai a vs
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder $ catRange (f:ps))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder <|> dotFormulae ks
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder <|> itemList ks axiomS formula Axiom_items
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedervarItems :: [String] -> AParser st ([VAR_DECL], [Token])
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder do v <- varDecl ks
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder do s <- try (addAnnos >> Common.Lexer.semiT) << addLineAnnos
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder do tryItemEnd (ks ++ startKeyword)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder return ([v], [s])
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder <|> do (vs, ts) <- varItems ks
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder return (v:vs, s:ts)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder <|> return ([v], [])
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederdotFormulae :: (AParsable b, AParsable s, AParsable f) =>
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder [String] -> AParser st (BASIC_ITEMS b s f)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederdotFormulae ks =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (fs, ds) <- aFormula ks `separatedBy` dotT
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (m, an) <- optSemi
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder let ps = catRange (d:ds)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ns = init fs ++ [appendAnno (last fs) an]
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder return $ Axiom_items ns (ps `appRange` catRange m)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaFormula :: AParsable f => [String] -> AParser st (Annoted (FORMULA f))
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederaFormula = allAnnoParser . formula
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- * basic spec
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederbasicSpec :: (AParsable f, AParsable s, AParsable b) =>
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder [String] -> AParser st (BASIC_SPEC b s f)
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederbasicSpec = fmap Basic_spec . annosParser . basicItems