isa.hs revision e1f395fef7ea8b00a675a330e5461fad35158ca5
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederDescription : a standalone Isabelle parser
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) C. Maeder and Uni Bremen 2005
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : Christian.Maeder@dfki.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederparse Isabelle theory files
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedermodule Main where
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport qualified Data.Map as Map
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedermain = getArgs >>= mapM_ process
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederprocess :: String -> IO ()
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederprocess f = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder s <- readFile f
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder putStrLn $ case parse parseTheory f s of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Right (_, b) -> show $ printBody b
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Left err -> show err
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprintBody :: Body -> Doc
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprintBody f = let
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder axs = axiomsF f
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder gls = goalsF f
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder cns = constsF f
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder dts = datatypesF f
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder col a b = a <+> colon <+> b
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder dcol a b = a <+> text "::" <+> b
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder in (if Map.null axs then empty else keyword axiomsS)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder printMap id vcat col axs
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder (if Map.null gls then empty else keyword lemmaS)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder ppMap pretty (sep . prepPunctuate (text andS <> Doc.space)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder . map pretty . simpValue)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder id vcat col gls
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (if Map.null cns then empty else keyword constsS)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder printMap id vcat dcol cns
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (if Map.null dts then empty else keyword datatypeS)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder printMap id vcat dcol dts