Parse_AS_Basic.hs revision e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannModule : $Header$
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannCopyright : (c) Christian Maeder, Uni Bremen 2002-2004
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannMaintainer : maeder@tzi.de
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannStability : provisional
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannPortability : portable
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmannparse SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Follows Sect. II:3.1 of the CASL Reference Manual.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann http://www.cofi.info/Documents/CASL/Summary/
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann from 25 March 2001
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann C.2.1 Basic Specifications with Subsorts
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- ------------------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- ------------------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsortItems, typeItems, opItems, predItems, sigItems
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann :: (AParsable s, AParsable f) => [String] -> AParser st (SIG_ITEMS s f)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsortItems ks = itemList ks sortS sortItem Sort_items
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanntypeItems ks = itemList ks typeS datatype Datatype_items
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannopItems ks = itemList ks opS opItem Op_items
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannpredItems ks = itemList ks predS predItem Pred_items
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannsigItems ks = fmap Ext_SIG_ITEMS aparser <|>
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann sortItems ks <|> opItems ks <|> predItems ks <|> typeItems ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann---- helpers ----------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanndatatypeToFreetype :: (AParsable b, AParsable s, AParsable f) =>
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanndatatypeToFreetype d pos =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Datatype_items ts ps -> Free_datatype ts (pos `appRange` ps)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann _ -> error "datatypeToFreetype"
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannaxiomToLocalVarAxioms :: (AParsable b, AParsable s, AParsable f) =>
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann -> BASIC_ITEMS b s f
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannaxiomToLocalVarAxioms ai a vs posl =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann Axiom_items ((Annoted ft qs as rs):fs) ds ->
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann let aft = Annoted ft qs (a++as) rs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann in Local_var_axioms vs (aft:fs) (posl `appRange` ds)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann _ -> error "axiomToLocalVarAxioms"
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- ------------------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- ------------------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbasicItems :: (AParsable b, AParsable s, AParsable f) =>
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann [String] -> AParser st (BASIC_ITEMS b s f)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbasicItems ks = fmap Ext_BASIC_ITEMS aparser <|> fmap Sig_items (sigItems ks)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> do f <- asKey freeS
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ti <- typeItems ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (datatypeToFreetype ti (tokPos f))
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> do g <- asKey generatedS
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do t <- typeItems ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (Sort_gen [Annoted t nullRange [] []] $ tokPos g)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do o <- oBraceT
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann is <- annosParser (sigItems ks)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann a <- lineAnnos
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (Sort_gen (init is ++ [appendAnno (last is) a])
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (toPos g [o] c))
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> do v <- pluralKeyword varS
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (vs, ps) <- varItems ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (Var_items vs (catPos (v:ps)))
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> do f <- forallT
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (vs, ps) <- varDecl ks `separatedBy` anSemi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ai <- dotFormulae ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (axiomToLocalVarAxioms ai a vs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann $ catPos (f:ps))
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> dotFormulae ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> itemList ks axiomS formula Axiom_items
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannvarItems :: [String] -> AParser st ([VAR_DECL], [Token])
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do v <- varDecl ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do s <- try (addAnnos >> Common.Lexer.semiT) << addLineAnnos
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann do tryItemEnd (ks ++ startKeyword)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return ([v], [s])
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> do (vs, ts) <- varItems ks
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return (v:vs, s:ts)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> return ([v], [])
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanndotFormulae :: (AParsable b, AParsable s, AParsable f) =>
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann [String] -> AParser st (BASIC_ITEMS b s f)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmanndotFormulae ks =
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (fs, ds) <- aFormula ks `separatedBy` dotT
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann (m, an) <- optSemi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann let ps = catPos (d:ds)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann ns = init fs ++ [appendAnno (last fs) an]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann return $ Axiom_items ns (ps `appRange` catPos m)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannaFormula :: AParsable f => [String] -> AParser st (Annoted (FORMULA f))
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannaFormula ks = bind appendAnno (annoParser $ formula ks) lineAnnos
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- ------------------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann-- ------------------------------------------------------------------------
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbasicSpec :: (AParsable f, AParsable s, AParsable b) =>
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann [String] -> AParser st (BASIC_SPEC b s f)
2450a4210dee64b064499a3a1154129bdfc74981Daniel HausmannbasicSpec ks = (fmap Basic_spec $ annosParser $ basicItems ks)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann <|> (oBraceT >> cBraceT >> return (Basic_spec []))