Parse_AS_Basic.hs revision 0095c7efbddd0ffeed6aaf8ec015346be161d819
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Christian Maeder, Uni Bremen 2002-2004
25449dd4a796d3244e754bde21a5e9c401dc135eEwaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : maeder@tzi.de
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzStability : provisional
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzPortability : portable
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzDescription : parse CASL basic specifications (SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC)
1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst Schulz Follows Sect. II:3.1 of the CASL Reference Manual.
c73c3d0df595b7feab36cf441a1a31cd1a2c7c1dEwaryst Schulz from 25 March 2001
c73c3d0df595b7feab36cf441a1a31cd1a2c7c1dEwaryst Schulz C.2.1 Basic Specifications with Subsorts
e77f7260babdf86b287a632f9676c601bd0db077Ewaryst Schulz-- ------------------------------------------------------------------------
348346590dc302381df4daf372d6dc601b860eaeEwaryst Schulz-- ------------------------------------------------------------------------
62ff5e56ab685e81ebde4712eb1bf677322bfba9Ewaryst SchulzsortItems, typeItems, opItems, predItems, sigItems
348346590dc302381df4daf372d6dc601b860eaeEwaryst Schulz :: (AParsable s, AParsable f) => [String] -> AParser st (SIG_ITEMS s f)
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzsortItems ks = itemList ks sortS sortItem Sort_items
c208973c890b8f993297720fd0247bc7481d4304Christian MaedertypeItems ks = itemList ks typeS datatype Datatype_items
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzopItems ks = itemList ks opS opItem Op_items
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzpredItems ks = itemList ks predS predItem Pred_items
5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst SchulzsigItems ks = fmap Ext_SIG_ITEMS aparser <|>
348346590dc302381df4daf372d6dc601b860eaeEwaryst Schulz sortItems ks <|> opItems ks <|> predItems ks <|> typeItems ks
df0d1a7e7dfff3be40c24b25318a6a07c748be20Ewaryst Schulz---- helpers ----------------------------------------------------------------
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzdatatypeToFreetype :: (AParsable b, AParsable s, AParsable f) =>
e77f7260babdf86b287a632f9676c601bd0db077Ewaryst Schulz SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzdatatypeToFreetype d pos =
5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulz Datatype_items ts ps -> Free_datatype ts (pos `appRange` ps)
df0d1a7e7dfff3be40c24b25318a6a07c748be20Ewaryst Schulz _ -> error "datatypeToFreetype"
348346590dc302381df4daf372d6dc601b860eaeEwaryst SchulzaxiomToLocalVarAxioms :: (AParsable b, AParsable s, AParsable f) =>
348346590dc302381df4daf372d6dc601b860eaeEwaryst Schulz BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
49c8d0af1a96cab75795d49b078b9163b666473fEwaryst Schulz -> BASIC_ITEMS b s f
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzaxiomToLocalVarAxioms ai a vs posl =
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz Axiom_items ((Annoted ft qs as rs):fs) ds ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let aft = Annoted ft qs (a++as) rs
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz in Local_var_axioms vs (aft:fs) (posl `appRange` ds)
938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz _ -> error "axiomToLocalVarAxioms"
f887ef77051188d95ceb8c37f39af91fc1195137Ewaryst Schulz-- ------------------------------------------------------------------------
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz-- ------------------------------------------------------------------------
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst SchulzbasicItems :: (AParsable b, AParsable s, AParsable f) =>
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz [String] -> AParser st (BASIC_ITEMS b s f)
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst SchulzbasicItems ks = fmap Ext_BASIC_ITEMS aparser <|> fmap Sig_items (sigItems ks)
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz <|> do f <- asKey freeS
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz ti <- typeItems ks
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz return (datatypeToFreetype ti (tokPos f))
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz <|> do g <- asKey generatedS
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz do t <- typeItems ks
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz return (Sort_gen [Annoted t nullRange [] []] $ tokPos g)
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz do o <- oBraceT
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz is <- annosParser (sigItems ks)
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz a <- lineAnnos
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz return (Sort_gen (init is ++ [appendAnno (last is) a])
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz (toPos g [o] c))
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz <|> do v <- pluralKeyword varS
aae33d0d1a0f8174a7a704e2fdbb29482e0bf587Ewaryst Schulz (vs, ps) <- varItems ks
aae33d0d1a0f8174a7a704e2fdbb29482e0bf587Ewaryst Schulz return (Var_items vs (catPos (v:ps)))
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz <|> do f <- forallT
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz (vs, ps) <- varDecl ks `separatedBy` anSemi
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz ai <- dotFormulae ks
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz return (axiomToLocalVarAxioms ai a vs
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz $ catPos (f:ps))
d1fddc394ac2af87a6210e7a3504bb565d088e7aEwaryst Schulz <|> dotFormulae ks
5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulz <|> itemList ks axiomS formula Axiom_items
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzvarItems :: [String] -> AParser st ([VAR_DECL], [Token])
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz do v <- varDecl ks
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz do s <- try (addAnnos >> Common.Lexer.semiT) << addLineAnnos
d1fddc394ac2af87a6210e7a3504bb565d088e7aEwaryst Schulz do tryItemEnd (ks ++ startKeyword)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return ([v], [s])
5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulz <|> do (vs, ts) <- varItems ks
5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulz return (v:vs, s:ts)
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz <|> return ([v], [])
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzdotFormulae :: (AParsable b, AParsable s, AParsable f) =>
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz [String] -> AParser st (BASIC_ITEMS b s f)
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzdotFormulae ks =
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz (fs, ds) <- aFormula ks `separatedBy` dotT
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz (m, an) <- optSemi
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz let ps = catPos (d:ds)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz ns = init fs ++ [appendAnno (last fs) an]
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz return $ Axiom_items ns (ps `appRange` catPos m)
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst SchulzaFormula :: AParsable f => [String] -> AParser st (Annoted (FORMULA f))
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst SchulzaFormula ks = bind appendAnno (annoParser $ formula ks) lineAnnos
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst Schulz-- ------------------------------------------------------------------------
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz-- ------------------------------------------------------------------------
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst SchulzbasicSpec :: (AParsable f, AParsable s, AParsable b) =>
699f8456142e7c89bd15acf3aa8790fd02f4420dEwaryst Schulz [String] -> AParser st (BASIC_SPEC b s f)
f58e5059e02c7e903059f3ec37bcb3b482afd63fEwaryst SchulzbasicSpec ks = (fmap Basic_spec $ annosParser $ basicItems ks)
aae33d0d1a0f8174a7a704e2fdbb29482e0bf587Ewaryst Schulz <|> (oBraceT >> cBraceT >> return (Basic_spec []))