Parse_AS_Basic.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
2509N/A{- |
0N/AModule : $Header$
0N/ADescription : Parsing CASL's SIG-ITEMS, BASIC-ITEMS and BASIC-SPEC
0N/ACopyright : (c) Christian Maeder, Uni Bremen 2002-2004
0N/ALicense : GPLv2 or higher
0N/A
0N/AMaintainer : Christian.Maeder@dfki.de
0N/AStability : provisional
0N/APortability : portable
0N/A
0N/AParser for CASL basic specifications (SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC)
0N/A Follows Sect. II:3.1 of the CASL Reference Manual.
0N/A-}
0N/A
0N/A{-
0N/A http://www.cofi.info/Documents/CASL/Summary/
0N/A from 25 March 2001
2362N/A
2362N/A C.2.1 Basic Specifications with Subsorts
2362N/A-}
1178N/A
2509N/Amodule CASL.Parse_AS_Basic where
0N/A
0N/Aimport Common.AS_Annotation
1178N/Aimport Common.AnnoState
0N/Aimport Common.Id
0N/Aimport Common.Keywords
0N/Aimport Common.Lexer
0N/Aimport Common.Parsec
0N/A
0N/Aimport CASL.AS_Basic_CASL
0N/Aimport CASL.Formula
0N/Aimport CASL.SortItem
0N/Aimport CASL.OpItem
0N/A
0N/Aimport Text.ParserCombinators.Parsec
0N/A
0N/A-- * signature items
0N/A
0N/AsortItems, typeItems, opItems, predItems, sigItems
0N/A :: (AParsable s, AParsable f) => [String] -> AParser st (SIG_ITEMS s f)
0N/AsortItems ks = itemList ks esortS sortItem (Sort_items PossiblyEmptySorts)
0N/A <|> itemList ks sortS sortItem (Sort_items NonEmptySorts)
0N/AtypeItems ks = itemList ks typeS datatype (Datatype_items NonEmptySorts)
0N/A <|> itemList ks etypeS datatype (Datatype_items PossiblyEmptySorts)
0N/A
0N/AopItems ks = itemList ks opS opItem Op_items
0N/ApredItems ks = itemList ks predS predItem Pred_items
0N/AsigItems ks = fmap Ext_SIG_ITEMS aparser <|>
0N/A sortItems ks <|> opItems ks <|> predItems ks <|> typeItems ks
0N/A
0N/A-- * helpers
0N/A
1178N/AdatatypeToFreetype :: (AParsable b, AParsable s, AParsable f) =>
0N/A SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
0N/AdatatypeToFreetype d pos =
0N/A case d of
0N/A Datatype_items sk ts ps -> Free_datatype sk ts (pos `appRange` ps)
0N/A _ -> error "datatypeToFreetype"
1178N/A
1178N/AaxiomToLocalVarAxioms :: (AParsable b, AParsable s, AParsable f) =>
0N/A BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
0N/A -> BASIC_ITEMS b s f
0N/AaxiomToLocalVarAxioms ai a vs posl =
0N/A case ai of
0N/A Axiom_items ((Annoted ft qs as rs):fs) ds ->
0N/A let aft = Annoted ft qs (a++as) rs
0N/A in Local_var_axioms vs (aft:fs) (posl `appRange` ds)
0N/A _ -> error "axiomToLocalVarAxioms"
0N/A
0N/A-- * basic items
0N/A
0N/AbasicItems :: (AParsable b, AParsable s, AParsable f) =>
0N/A [String] -> AParser st (BASIC_ITEMS b s f)
0N/AbasicItems ks = fmap Ext_BASIC_ITEMS aparser <|> fmap Sig_items (sigItems ks)
0N/A <|> do f <- asKey freeS
0N/A ti <- typeItems ks
0N/A return (datatypeToFreetype ti (tokPos f))
0N/A <|> do g <- asKey generatedS
0N/A do t <- typeItems ks
0N/A return (Sort_gen [Annoted t nullRange [] []] $ tokPos g)
0N/A <|>
0N/A do o <- oBraceT
0N/A is <- annosParser (sigItems ks)
0N/A c <- cBraceT
0N/A a <- lineAnnos
0N/A return (Sort_gen (init is ++ [appendAnno (last is) a])
1178N/A (toRange g [o] c))
1178N/A <|> do v <- pluralKeyword varS
1178N/A (vs, ps) <- varItems ks
0N/A return (Var_items vs (catRange (v:ps)))
<|> do f <- forallT
(vs, ps) <- varDecl ks `separatedBy` anSemi
a <- annos
ai <- dotFormulae ks
return (axiomToLocalVarAxioms ai a vs
$ catRange (f:ps))
<|> dotFormulae ks
<|> itemList ks axiomS formula Axiom_items
varItems :: [String] -> AParser st ([VAR_DECL], [Token])
varItems ks =
do v <- varDecl ks
do s <- try (addAnnos >> Common.Lexer.semiT) << addLineAnnos
do tryItemEnd (ks ++ startKeyword)
return ([v], [s])
<|> do (vs, ts) <- varItems ks
return (v:vs, s:ts)
<|> return ([v], [])
dotFormulae :: (AParsable b, AParsable s, AParsable f) =>
[String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae ks =
do d <- dotT
(fs, ds) <- aFormula ks `separatedBy` dotT
(m, an) <- optSemi
let ps = catRange (d:ds)
ns = init fs ++ [appendAnno (last fs) an]
return $ Axiom_items ns (ps `appRange` catRange m)
aFormula :: AParsable f => [String] -> AParser st (Annoted (FORMULA f))
aFormula = allAnnoParser . formula
-- * basic spec
basicSpec :: (AParsable f, AParsable s, AParsable b) =>
[String] -> AParser st (BASIC_SPEC b s f)
basicSpec = fmap Basic_spec . annosParser . basicItems