ParseCLAsLibDefn.hs revision 8247c2f9606497ccfc5b4d10b3fcb07d8c0f6074
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : Eugen Kuksa 2011
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicense : GPLv2 or higher, see LICENSE.txt
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : eugenk@informatik.uni-bremen.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettPortability : non-portable (imports Logic.Logic)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachAnalyses CommonLogic files.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettmodule CommonLogic.ParseCLAsLibDefn (parseCL_CLIF) where
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Id
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.LibName
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.AS_Annotation as Anno
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.AnnoState
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederimport Text.ParserCombinators.Parsec
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport Logic.Grothendieck
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport CommonLogic.AS_CommonLogic as CL
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport CommonLogic.Logic_CommonLogic
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport CommonLogic.Parse_CLIF (basicSpec)
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Syntax.AS_Library
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Syntax.AS_Structured as Struc
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport System.IO
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder-- | call for CommonLogic CLIF-parser
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy GimblettparseCL_CLIF :: FilePath -> IO LIB_DEFN
04ceed96d1528b939f2e592d0656290d81d1c045Andy GimblettparseCL_CLIF filename = do
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett handle <- openFile filename ReadMode
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly contents <- hGetContents handle
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder maybeText <- return $ runParser (many basicSpec) (emptyAnnos ()) "" contents
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett case maybeText of
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder Right bs -> return $ convertToLibDefN filename $ reverse bs
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Left x -> error $ "Error parsing CLIF-File." ++ show x
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- maps imports in basic spec to global definition links (extensions) in
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- development graph
842ae753ab848a8508c4832ab64296b929167a97Christian MaederconvertToLibDefN :: FilePath -> [BASIC_SPEC] -> LIB_DEFN
842ae753ab848a8508c4832ab64296b929167a97Christian MaederconvertToLibDefN filename bs =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let fn = convertFileToLibStr filename
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett knownSpecs = map (\(i,b) -> specName i b fn) $ zip [0..] bs
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly in Lib_defn
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (emptyLibName fn)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (concat $ foldl (
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly \r bn -> (convertBS knownSpecs bn : r)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly ) [] $ zip bs knownSpecs
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett )
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder nullRange
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly []
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- Creates Nodes in the Logic Graph.
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- Also gives each non-named text a unique name in the graph.
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederconvertBS :: [NAME] -> (BASIC_SPEC, NAME) -> [Anno.Annoted LIB_ITEM]
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederconvertBS knownSpecs (b,n) =
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder let imports = getImports b
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly missingTexts = filter (\i -> not $ elem i knownSpecs) imports
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly in map (\m -> emptyAnno $ Download_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (emptyLibName $ tokStr m)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly [Item_name $ m]
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly nullRange
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly ) missingTexts
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder ++ [emptyAnno $ Spec_defn
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder n
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder emptyGenericity
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder (createSpec imports b)
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder nullRange]
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- one importation is an extension
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- many importations are an extension of a union
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettcreateSpec :: [NAME] -> BASIC_SPEC -> Anno.Annoted SPEC
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettcreateSpec imports b =
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett let bs = emptyAnno $ Struc.Basic_spec (G_basic_spec CommonLogic b) nullRange
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett in case imports of
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett [] -> bs
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett _ -> emptyAnno $ Extension [
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (case imports of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett [n] -> cnvimport n
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett _ -> emptyAnno $ Union (map cnvimport imports) nullRange)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett , bs
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett ] nullRange
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- converts an imporation name to a SPEC
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillycnvimport :: NAME -> Annoted SPEC
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillycnvimport n = emptyAnno $ Spec_inst n [] nullRange
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- retrieves all importations from the text
61051521e4d82769a47f23aecb5fb477de47d534Andy GimblettgetImports :: BASIC_SPEC -> [NAME]
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettgetImports (CL.Basic_spec items) =
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett concatMap getImports_textMrs $ map textFromBasicItems items
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillytextFromBasicItems :: Anno.Annoted (BASIC_ITEMS) -> TEXT_MRS
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy GimbletttextFromBasicItems abi = case Anno.item abi of
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Axiom_items annoText -> Anno.item annoText
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettgetImports_textMrs :: TEXT_MRS -> [NAME]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettgetImports_textMrs (Text_mrs (t,_)) = getImports_text t
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaedergetImports_text :: TEXT -> [NAME]
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaedergetImports_text (Text ps _) = map impToName $ filter isImportation ps
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettgetImports_text (Named_text _ t _) = getImports_text t
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettisImportation :: PHRASE -> Bool
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettisImportation (Importation _) = True
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisImportation _ = False
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett
842ae753ab848a8508c4832ab64296b929167a97Christian MaederimpToName :: PHRASE -> NAME
842ae753ab848a8508c4832ab64296b929167a97Christian MaederimpToName (Importation (Imp_name n)) = n
842ae753ab848a8508c4832ab64296b929167a97Christian MaederimpToName _ = undefined -- not necessary because filtered out
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- returns a unique name for a node
842ae753ab848a8508c4832ab64296b929167a97Christian MaederspecName :: Int -> CL.BASIC_SPEC -> String -> NAME
842ae753ab848a8508c4832ab64296b929167a97Christian MaederspecName i (CL.Basic_spec []) def = mkSimpleId $ def ++ "_" ++ show i
842ae753ab848a8508c4832ab64296b929167a97Christian MaederspecName i (CL.Basic_spec [items]) def =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case Anno.item items of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Axiom_items ax ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett case Anno.item ax of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Text_mrs (Text _ _, _) -> mkSimpleId $ def ++ "_" ++ show i
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Text_mrs (Named_text n _ _, _) -> mkSimpleId n
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettspecName i (CL.Basic_spec (_:_)) def = mkSimpleId $ def ++ "_" ++ show i
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly