VSE.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews{-# LANGUAGE CPP #-}
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsModule : $Header$
3398334b3acda24b086957286288ca9852662b12Automatic UpdaterDescription : Interface to send structured theories to the VSE prover
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsCopyright : (c) C. Maeder, DFKI 2009
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsLicense : GPLv2 or higher
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsMaintainer : Christian.Maeder@dfki.de
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsStability : provisional
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsPortability : needs POSIX
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewscall an adaption of VSE II to hets
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsthe prover should be attached to a node's menu (if applicable) but take the
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewswhole library environment as in- and output like development graph rules.
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsimport qualified Common.OrderedMap as OMap
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsimport qualified Data.Map as Map
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsimport qualified Data.Set as Set
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsimport Data.Graph.Inductive.Basic (elfilter, gfold)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsimport Data.Graph.Inductive.Graph hiding (out)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsthName :: LibName -> LNode DGNodeLab -> String
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsthName ln (n, lbl) = map (\ c -> if elem c "/,[]: " then '-' else c)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews $ shows (getLibId ln) "_" ++ getDGNodeName lbl ++ "_" ++ show n
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsgetSubGraph :: Node -> DGraph -> DGraph
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsgetSubGraph n dg =
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let g = dgBody dg
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ns = nodes g
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews sns = gfold pre' (\ c s -> Set.insert (node' c) s)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (\ m s -> Set.union s $ fromMaybe Set.empty m, Set.empty) [n] g
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews in delNodesDG (Set.toList $ Set.difference (Set.fromList ns) sns) dg
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews-- | applies basic inference to a given node and whole import tree above
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsprove :: (LibName, Node) -> LibEnv -> IO (Result LibEnv)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrewsprove (ln, node) libEnv =
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews runResultT $ do
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews qLibEnv <- liftR $ qualifyLibEnv libEnv
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let dg1 = lookupDGraph ln qLibEnv
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews dg2 = dg1 { dgBody = elfilter (isGlobalEdge . dgl_type) $ dgBody dg1 }
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews dg3 = getSubGraph node dg2
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews oLbl = labDG dg3 node
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ostr = thName ln (node, oLbl)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews G_theory olid _ _ _ _ <- return $ dgn_theory oLbl
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let mcm = if Logic CASL == Logic olid then Just (Comorphism CASL2VSE) else
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews dGraph <- liftR $ maybe return (flip $ dg_translation qLibEnv) mcm dg3
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let nls = topsortedNodes dGraph
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ns = map snd nls
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ts <- liftR $ mapM
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (\ lbl -> do
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let lbln = getDGNodeName lbl
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews G_theory lid (ExtSign sign0 _) _ sens0 _ <- return $ dgn_theory lbl
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (sign1, sens1) <-
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews addErrorDiag "failure when proving VSE nodes of" (getLibId ln)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews $ coerceBasicTheory lid VSE
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ("cannot cast untranslated node '" ++ lbln ++ "'")
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (sign0, toNamedList sens0)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let (sign2, sens2) = addUniformRestr sign1 sens1
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ( show $ prettySExpr
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews $ qualVseSignToSExpr (mkSimpleId lbln)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (getLibId ln) sign2
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews , show $ prettySExpr
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews $ SList $ map (namedSenToSExpr sign2) sens2)) ns
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews#ifdef TAR_PACKAGE
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews moveVSEFiles ostr
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (inp, out, cp) <- prepareAndCallVSE
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews sendMyMsg inp $ "(" ++ unlines (map (thName ln) nls) ++ ")"
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews mapM_ (\ nl -> do
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews readMyMsg cp out linksP
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews str <- getLinksTo ln dGraph nl
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews sendMyMsg inp str) nls
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews mapM_ (\ (fsig, _) -> do
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews readMyMsg cp out sigP
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews sendMyMsg inp fsig) ts
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews mapM_ (\ (_, sens) -> do
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews readMyMsg cp out lemsP
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews sendMyMsg inp sens) ts
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ms <- readFinalVSEOutput cp out
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews#ifdef TAR_PACKAGE
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews createVSETarFile ostr
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews Nothing -> return libEnv
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews Just lemMap -> return $ foldr (\ (n, lbl) le ->
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews let str = map toUpper $ thName ln (n, lbl)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews lems = Set.fromList $ Map.findWithDefault [] str lemMap
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews in if Set.null lems then le else let
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews dg = lookupDGraph ln le
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews in case lab (dgBody dg) n of
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews Nothing -> le -- node missing in original graph
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews Just olbl -> case dgn_theory olbl of
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews G_theory lid sig sigId sens _ -> let
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews nsens = OMap.mapWithKey (\ name sen ->
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews if not (isAxiom sen) && Set.member
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (map toUpper $ transString name) lems
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews senAttr = ThmStatus $
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews (Comorphism CASL2VSE,
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews BasicProof VSE $
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews mkVseProofStatus name axs)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews : thmStatus sen }
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews else sen) sens
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews nlbl = olbl { dgn_theory
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews = G_theory lid sig sigId nsens startThId }
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt flbl = nlbl { globalTheory
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews = computeLabelTheory le dg (n, nlbl) }
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ndg = changeDGH dg $ SetNodeLab olbl (n, flbl)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews in Map.insert ln ndg le) libEnv nls
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewsgetLinksTo :: LibName -> DGraph -> LNode DGNodeLab -> IO String
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan HuntgetLinksTo ln dg (n, lbl) = do
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt let (ls, rs) = partition (\ (s, _, el) -> s /= n
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt && isGlobalDef (dgl_type el)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews && isInc (getRealDGLinkType el)) $ innDG dg n
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews mapM_ (\ e -> putStrLn
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews $ "ignored unsupported link (non-inclusion or theorem link):\n "
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt ++ show (prettyLEdge e)) rs
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt return $ show $ prettySExpr $ SList
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt $ map (\ (s, _, el) -> let
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ltype = dgl_type el
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews defl = isGlobalDef ltype
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt [ SSymbol $ (if defl then "definition" else "theorem") ++ "-link"
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews , SSymbol $ "edge" ++ showEdgeId (dgl_id el)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews , SSymbol $ thName ln (s, labDG dg s)
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews , SSymbol $ thName ln (n, lbl)
3398334b3acda24b086957286288ca9852662b12Automatic Updater , SSymbol "global"
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews , SList $ SSymbol "morphism" : hetMorToSSexpr (dgl_morphism el)]
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews ++ if defl then [] else
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews [SSymbol $ if isProven ltype then "proven" else "open"]) ls
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewshetMorToSSexpr :: GMorphism -> [SExpr]
6098d364b690cb9dabf96e9664c4689c8559bd2eMark AndrewshetMorToSSexpr (GMorphism cid _ _ mor _) =
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt let tlid = targetLogic cid
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt in case coerceMorphism tlid VSE "" mor of
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt Just vsemor -> morToSExprs vsemor
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt Nothing -> case coerceMorphism tlid CASL "" mor of
9a859983d7059a6eb9c877c1d2ac6a3a5b7170f7Evan Hunt Just cmor -> morToSExprs cmor
6098d364b690cb9dabf96e9664c4689c8559bd2eMark Andrews Nothing -> []