WriteFn.hs revision ce900a84ed9d9882c64fccbd6300f6b0d67efa82
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor{-# OPTIONS -cpp #-}
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorModule : $Header$
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorDescription : Writing various formats, according to Hets options
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorCopyright : (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorMaintainer : Christian.Maeder@dfki.de
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorStability : provisional
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorPortability : non-portable(DevGraph)
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenWriting various formats, according to Hets options
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzormodule Driver.WriteFn (writeSpecFiles) where
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport Data.List (partition, (\\))
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport Common.GlobalAnnotations (GlobalAnnos)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport qualified Data.Map as Map
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport Logic.Logic (language_name)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#if HAXML_PACKAGE
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#ifdef PROGRAMATICA
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport Isabelle.IsaPrint (printIsaTheory)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#ifndef NOOWLLOGIC
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport OWL.Print (printOWLBasicTheory)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport OWL.Parse (basicSpec)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport qualified Static.PrintDevGraph as DG
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorimport Proofs.TheoremHideShift (theoremsToAxioms, computeTheory)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#ifdef HXTFILTER
cae0359c9286c8e34cbccd15eee2da90562c1ee2sfwriteVerbFile :: HetcatsOpts -> FilePath -> String -> IO ()
cae0359c9286c8e34cbccd15eee2da90562c1ee2sfwriteVerbFile opts f str = do
cae0359c9286c8e34cbccd15eee2da90562c1ee2sf putIfVerbose opts 2 $ "Writing file: " ++ f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeFile f str
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LIB_NAME -> OutType
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteLibEnv opts filePrefix lenv ln ot =
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor let f = filePrefix ++ "." ++ show ot
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor dg = lookupDGraph ln lenv in case ot of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Prf -> toShATermString (ln, lookupHistory ln lenv)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor >>= writeVerbFile opts f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#ifdef HXTFILTER
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor OmdocOut -> hetsToOMDoc opts (ln, lenv) f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor GraphOut (Dot showInternalNodeLabels) -> writeVerbFile opts f
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh $ dotGraph showInternalNodeLabels dg
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> return ()
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteSoftFOL :: HetcatsOpts -> FilePath -> G_theory -> LIB_NAME -> SIMPLE_ID
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor -> SPFType -> Int -> String -> IO ()
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteSoftFOL opts f gTh ln i c n msg = do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor mDoc <- printTheoryAsSoftFOL ln i n (case c of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ConsistencyCheck -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor OnlyAxioms -> False) $ theoremsToAxioms gTh
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor maybe (putIfVerbose opts 0 $
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor "could not translate to " ++ msg ++ " file: " ++ f)
fed47023e9be04c612b5f6d4a5ee2b8e7c587181rbowen ( \ d -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor let str = shows d "\n"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor forget p = fmap (const ()) p
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor case parse (if n == 0 then forget parseSPASS else forget tptp)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Left err -> putIfVerbose opts 0 $ show err
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeVerbFile opts f str) mDoc
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LIB_NAME -> SIMPLE_ID
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteIsaFile opts fp raw_gTh ln i = case createIsaTheory raw_gTh of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Result ds Nothing -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 0 $ "could not translate to Isabelle theory: " ++ fp
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 2 $ unlines $ map show ds
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Result _ (Just (sign, sens)) -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor let tn = reverse (takeWhile (/= '/') $ reverse $ show $ getLIB_ID ln)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ++ "_" ++ show i
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor sf = shows (printIsaTheory tn sign sens) "\n"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor f = fp ++ ".thy"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor case parse parseTheory f sf of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Left err -> putIfVerbose opts 0 $ show err
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh writeVerbFile opts f sf
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh when (hasPrfOut opts && verbose opts >= 3) $ let
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh (axs, rest) = partition ( \ s -> isAxiom s || isDef s) sens
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh in mapM_ ( \ s -> let
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh tnf = tn ++ "_" ++ senAttr s
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor tf = fp ++ "_" ++ senAttr s ++ ".thy"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor in writeVerbFile opts tf $ shows
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor (printIsaTheory tnf sign $ s : axs) "\n") rest
f039cf01b271a31e317d5b84f24cb135f1c1b6d7ndwriteTheory :: HetcatsOpts -> FilePath -> GlobalAnnos -> G_theory -> LIB_NAME
48c64aeceef385e19025b384bd719b2a9789592dnd -> SIMPLE_ID -> OutType -> IO ()
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteTheory opts filePrefix ga
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor raw_gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) ln i ot =
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor let fp = filePrefix ++ "_" ++ show i
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor f = fp ++ "." ++ show ot
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor th = (sign0, toNamedList sens0)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor in case ot of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ThyFile -> writeIsaFile opts fp raw_gTh ln i
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor DfgFile c -> writeSoftFOL opts f raw_gTh ln i c 0 "DFG"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor TPTPFile c -> writeSoftFOL opts f raw_gTh ln i c 1 "TPTP"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor TheoryFile d -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor if null $ show d then
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeVerbFile opts f $ shows (DG.printTh ga i raw_gTh) "\n"
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh else putIfVerbose opts 0 "printing theory delta is not implemented"
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh when (language_name lid == language_name VSE) $ do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh (sign, sens) <- coerceBasicTheory lid VSE "" th
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh let (sign', sens') = addUniformRestr sign sens
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh lse = map (namedSenToSExpr sign') sens'
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor unless (null lse) $ writeVerbFile opts (fp ++ ".sexpr")
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor $ shows (prettySExpr $ SList lse) "\n"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor SigFile d -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor if null $ show d then
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeVerbFile opts f $ shows (pretty $ signOf raw_gTh) "\n"
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh else putIfVerbose opts 0 "printing signature delta is not implemented"
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh when (language_name lid == language_name VSE) $ do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh (sign, sens) <- coerceBasicTheory lid VSE "" th
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh let (sign', _sens') = addUniformRestr sign sens
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh writeVerbFile opts (f ++ ".sexpr")
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor $ shows (prettySExpr $ vseSignToSExpr sign') "\n"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#ifdef PROGRAMATICA
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor HaskellOut -> case printModule raw_gTh of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 0 $ "could not translate to Haskell file: " ++ f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Just d -> writeVerbFile opts f $ shows d "\n"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor#if HAXML_PACKAGE
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh ComptableXml -> if language_name lid == language_name CASL then do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh th2 <- coerceBasicTheory lid CASL "" th
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor let Result ds res = computeCompTable i th2
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor showDiags opts ds
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor case res of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Just td -> writeVerbFile opts f $ render $ table_document td
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Nothing -> return ()
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor else putIfVerbose opts 0 $ "expected CASL theory for: " ++ f
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh#ifndef NOOWLLOGIC
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor OWLOut -> if language_name lid == language_name OWL then do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh th2 <- coerceBasicTheory lid OWL "" th
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh let owltext = shows (printOWLBasicTheory th2) "\n"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor case parse (basicSpec >> eof) f owltext of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Left err -> putIfVerbose opts 0 $ show err
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeVerbFile opts f owltext
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor else putIfVerbose opts 0 $ "expected OWL theory for: " ++ f
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> return () -- ignore other file types
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzormodelSparQCheck :: HetcatsOpts -> G_theory -> SIMPLE_ID -> IO ()
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzormodelSparQCheck opts gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) i =
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh case coerceBasicTheory lid CASL "" (sign0, toNamedList sens0) of
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh Just th2 -> do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh table <- parseSparQTableFromFile $ modelSparQ opts
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh case table of
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh Left _ -> putIfVerbose opts 0
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor $ "could not parse SparQTable from file: " ++ modelSparQ opts
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Right y -> let Result d _ = modelCheck i th2 y in
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor if length d > 0 then showDiags opts {verbose = 2 } $ take 10 d
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor else putIfVerbose opts 0 "Modelcheck suceeded, no errors found"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 0 $ "could not translate Theory to CASL:\n "
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ++ showDoc gTh ""
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteTheoryFiles :: HetcatsOpts -> [OutType] -> FilePath -> LibEnv
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor -> GlobalAnnos -> LIB_NAME -> SIMPLE_ID -> Int -> IO ()
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteTheoryFiles opts specOutTypes filePrefix lenv ga ln i n =
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor unless (maybe True isDGRef $ lab (dgBody $ lookupDGraph ln lenv) n) $
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor case computeTheory False lenv ln n of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Result ds Nothing -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 0 $ "could not compute theory of spec "
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 2 $ unlines $ map show ds
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Result _ (Just (_lenv', raw_gTh0)) -> do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh -- what do I do with lenv' here?
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh let tr = transNames opts
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh resTh = if null tr then return (raw_gTh0, "") else do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh comor <- lookupCompComorphism (map tokStr tr) logicGraph
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh tTh <- mapG_theory comor raw_gTh0
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh return (tTh, show comor)
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh case resTh of
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh Result es Nothing -> do
ba543b319188dc1887607f6d59feddc00e38eee2humbedooh putIfVerbose opts 0 "could not translate theory"
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 0 $ unlines $ map show es
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Result _ (Just (raw_gTh, tStr)) -> do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor unless (null tStr) $
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 2 $ "Translated using comorphism " ++ tStr
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 4 $ "Sublogic of " ++ show i ++ ": " ++
cae0359c9286c8e34cbccd15eee2da90562c1ee2sf show (sublogicOfTh raw_gTh)
cae0359c9286c8e34cbccd15eee2da90562c1ee2sf unless (modelSparQ opts == "") $
cae0359c9286c8e34cbccd15eee2da90562c1ee2sf modelSparQCheck opts (theoremsToAxioms raw_gTh) i
cae0359c9286c8e34cbccd15eee2da90562c1ee2sf mapM_ (writeTheory opts filePrefix ga raw_gTh ln i) specOutTypes
cae0359c9286c8e34cbccd15eee2da90562c1ee2sfwriteSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LIB_NAME -> DGraph
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzorwriteSpecFiles opts file lenv ln dg = do
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor let gctx = globalEnv dg
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ga = globalAnnos dg
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ns = specNames opts
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor filePrefix = snd $ getFilePrefix opts file
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor outTypes = outtypes opts
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor specOutTypes = filter ( \ ot -> case ot of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ThyFile -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor DfgFile _ -> True
fed47023e9be04c612b5f6d4a5ee2b8e7c587181rbowen TPTPFile _ -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor TheoryFile _ -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor SigFile _ -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor OWLOut -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor HaskellOut -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ComptableXml -> True
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> False) outTypes
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor allSpecs = null ns
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ignore = null specOutTypes && modelSparQ opts == ""
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor mapM_ (writeLibEnv opts filePrefix lenv ln) $
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor if null $ dumpOpts opts then outTypes else EnvOut : outTypes
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor mapM_ ( \ i -> case Map.lookup i gctx of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor Just (SpecEntry (ExtGenSig _ _ _ (NodeSig n _))) ->
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeTheoryFiles opts specOutTypes filePrefix lenv ga ln i n
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> if allSpecs then return () else
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor putIfVerbose opts 0 $ "Unknown spec name: " ++ show i
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor ) $ if ignore then [] else
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor if allSpecs then Map.keys gctx else ns
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor mapM_ ( \ n ->
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeTheoryFiles opts specOutTypes filePrefix lenv ga ln
fed47023e9be04c612b5f6d4a5ee2b8e7c587181rbowen (genToken $ 'n' : show n) n)
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor $ if ignore || not allSpecs then [] else
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor \\ Map.fold ( \ e l -> case e of
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor SpecEntry (ExtGenSig _ _ _ (NodeSig n _)) -> n : l
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor _ -> l) [] gctx
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor doDump opts "GlobalAnnos" $ putStrLn $ showGlobalDoc ga ga ""
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor doDump opts "PrintStat" $ putStrLn $ printStatistics dg
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor doDump opts "DGraph" $ putStrLn $ showDoc dg ""
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor doDump opts "LogicGraph" $ putStrLn $ showDoc logicGraph ""
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor doDump opts "LibEnv" $
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor writeVerbFile opts (filePrefix ++ ".lenv") $
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor shows (DG.prettyLibEnv lenv) "\n"