ApplyChanges.hs revision c208973c890b8f993297720fd0247bc7481d4304
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffModule : $Header$
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffDescription : apply xupdate changes to a development graph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffCopyright : (c) Christian Maeder, DFKI GmbH 2010
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffLicense : GPLv2 or higher, see LICENSE.txt
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffMaintainer : Christian.Maeder@dfki.de
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffStability : provisional
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffPortability : non-portable(Grothendieck)
8cf870d281dc8c242f083d14dfef05f24aa5fceeJnRouvignacadjust development graph according to xupdate information
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffmodule Static.ApplyChanges (dgXUpdate) where
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffimport qualified Common.OrderedMap as OMap
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffimport Common.Utils (readMaybe, atMaybe)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffimport qualified Data.Set as Set
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffimport qualified Data.Map as Map
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcdufftrace :: String -> a -> a
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcdufftrace = const id
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffdgXUpdate :: Monad m => String -> LibEnv -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffdgXUpdate xs le =
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff liftM (computeDGraphTheories le) . applyXUpdates xs
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcdufflookupNodeByNodeName :: NodeName -> DGraph -> [LNode DGNodeLab]
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcdufflookupNodeByNodeName nn = lookupNodeWith (eqNN nn . dgn_name . snd)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffeqNN :: NodeName -> NodeName -> Bool
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffeqNN a b = getName a == getName b
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff && extString a == extString b
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff && extIndex a == extIndex b
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffgetNodeByName :: Monad m => String -> NodeName -> DGraph -> m (LNode DGNodeLab)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffgetNodeByName msg nn dg = let s = showName nn in
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case lookupNodeByNodeName nn dg of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff [] -> fail $ msg ++ "missing node: " ++ s
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff [i] -> return i
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ msg ++ "ambiguous node: " ++ s
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffapplyXUpdates :: Monad m => String -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffapplyXUpdates xs dg = do
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff cs <- anaXUpdates xs
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff let acs = foldr (\ c l -> case changeDG c of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> trace ("skip1: " ++ show c) l
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just s -> s : l) [] cs
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff return $ foldr (\ s g -> case applyChange s g of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Left r -> trace ("skip2: " ++ shows s "\n" ++ r) g
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Right ng -> trace ("succeeded: " ++ show s) ng) dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ sortBy cmpSelChanges acs
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffcmpSelChanges :: SelChangeDG -> SelChangeDG -> Ordering
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffcmpSelChanges (SelChangeDG _ ch1) (SelChangeDG _ ch2) =
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case (ch1, ch2) of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (RemoveChDG, RemoveChDG) -> EQ
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (RemoveChDG, _) -> LT
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (_, RemoveChDG) -> GT
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffapplyChange :: Monad m => SelChangeDG -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffapplyChange (SelChangeDG se ch) dg = case ch of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff RemoveChDG -> remove se dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff UpdateChDG str -> update str se dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff AddChDG _ ls ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff foldM (add se) dg ls
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffadd :: Monad m => SelElem -> DGraph -> AddChangeDG -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffadd se dg ch = case ch of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff SpecEntryDG n _fm ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff trace ("ignore adding spec entry " ++ show n ++ " to:\n" ++ show se)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ return dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ViewEntryDG n _fm s t gm ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff trace ("ignore adding view entry " ++ show n ++ " from " ++ show s
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ " to " ++ show t ++ "\n" ++ gm
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ "via:\n" ++ show se)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ return dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff NodeDG n _refn _consStatus ds ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff trace ("ignore adding node " ++ showName n
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ " (via:\n" ++ show se ++ ") " ++ show ds)
2706915084d41c1829bb186eb242e800e8fd35b2jvergara $ return dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff LinkDG e s t _linkTy gm ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff trace ("ignore adding link " ++ showEdgeId e ++ " from "
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ showName s ++ " to " ++ showName t
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ "\n" ++ gm
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ "\nvia: " ++ show se)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ return dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff StringElem en str -> case en of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff "Symbol" -> addSymbol str se dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ | elem en ["Axiom", "Theorem"] -> addAxOrTh str se dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> trace ("ignore adding: " ++ show en ++ "\nat: " ++ show se)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ return dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffaddSymbol :: Monad m => String -> SelElem -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffaddSymbol str se dg = let err = "Static.ApplyChanges.addSymbol: " in case se of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff NodeElem nn (Just (DeclSymbol Nothing)) -> do
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (v, lbl) <- getNodeByName err nn dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case extendByBasicSpec (globalAnnos dg) str (dgn_theory lbl) of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (Success nGt nSens nSyms _, _) ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff if nSens == 0 && Set.size nSyms == 1 then do
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff diffSig <- resultToMonad "ApplyChanges.addSymbol"
2706915084d41c1829bb186eb242e800e8fd35b2jvergara $ homGsigDiff (signOf nGt) $ dgn_sign lbl
2706915084d41c1829bb186eb242e800e8fd35b2jvergara let newLbl = lbl { dgn_theory = nGt
2706915084d41c1829bb186eb242e800e8fd35b2jvergara , nodeInfo = case nodeInfo lbl of
2706915084d41c1829bb186eb242e800e8fd35b2jvergara DGNode (DGBasicSpec _ _ syms) _ -> newNodeInfo $
2706915084d41c1829bb186eb242e800e8fd35b2jvergara DGBasicSpec Nothing diffSig
2706915084d41c1829bb186eb242e800e8fd35b2jvergara finLbl = newLbl { globalTheory = computeLabelTheory Map.empty dg
2706915084d41c1829bb186eb242e800e8fd35b2jvergara (v, newLbl) }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff return $ changeDGH dg $ SetNodeLab lbl (v, finLbl)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff else fail $ err ++ "just add a single symbol to: " ++ showName nn
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (_, msg) -> fail $ err ++ msg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ "cannot add symbol to: " ++ show se
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffaddAxOrTh :: Monad m => String -> SelElem -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffaddAxOrTh str se dg = let err = "Static.ApplyChanges.addAxOrTh: " in case se of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff NodeElem nn (Just _) -> do
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (v, lbl) <- getNodeByName err nn dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case extendByBasicSpec (globalAnnos dg) str (dgn_theory lbl) of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (Success nGt nSens _ sameSig, msg) -> case nSens of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff 1 | sameSig -> let
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff newLbl = lbl { dgn_theory = nGt }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff finLbl = newLbl { globalTheory = computeLabelTheory Map.empty dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (v, newLbl) }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff in return $ changeDGH dg $ SetNodeLab lbl (v, finLbl)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff 0 -> fail $ err ++ "missing sentence for: " ++ str
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ msg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (_, msg) -> fail $ err ++ msg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ "cannot add sentence to: " ++ show se
2706915084d41c1829bb186eb242e800e8fd35b2jvergararemove :: Monad m => SelElem -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffremove se dg = let err = "Static.ApplyChanges.remove: " in case se of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff NodeElem nn m -> do
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff i <- getNodeByName err nn dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff let s = showName nn
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> return $ changeDGH dg (DeleteNode i)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just (DeclSymbol md) -> case md of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> fail $ err ++ "cannot remove all declarations from: " ++ s
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just (si, b) -> if b then
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff trace ("ignore removing symbol attributes from: " ++ s) $ return dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff else removeNthSymbol si dg i
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just (Axioms si) -> removeNthAxOrTh True si dg i
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just (Theorems si) -> removeNthAxOrTh False si dg i
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff LinkElem eId src tar m -> let e = showEdgeId eId in case m of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case (lookupNodeByNodeName src dg, lookupNodeByNodeName tar dg) of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ([s], [t]) -> case filter (\ (_, o, l) -> o == fst t && eId == dgl_id l)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ outDG dg (fst s) of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff [le] -> return $ changeDGH dg (DeleteEdge le)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff [] -> fail $ err ++ "edge not found: " ++ e
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ "ambiguous edge: " ++ e
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (sl, tl) -> if null sl || null tl
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff then trace ("cannot remove link " ++ showEdgeId eId
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ " from " ++ showName src
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ " to " ++ showName tar)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ return dg -- assume link is gone
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff else fail $ err ++ "non-unique source or target for edge: " ++ e
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ "\n" ++ show (map (\ (v, l) -> (v, getDGNodeName l)) $ sl ++ tl)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just _ -> fail $ err ++ "cannot remove edge morphisms"
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ "unimplemented selection"
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffupdate :: Monad m => String -> SelElem -> DGraph -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffupdate str se dg =
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff let err = "Static.ApplyChanges.update with: " ++ str ++ "\n"
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff in case se of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff NodeElem nn m -> case m of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> let s = showName nn in case lookupNodeByNodeName nn dg of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff [_] -> trace ("update '" ++ str ++ "' is ignored on: " ++ show se)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ return dg -- ignore any attribute changes
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff [] -> fail $ err ++ "node not found: " ++ s
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ "ambiguous node: " ++ s
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just nse -> fail $ err ++ "cannot remove node symbols\n" ++ show nse
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff NextLinkId -> case readMaybe str of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just i -> return dg { getNewEdgeId = EdgeId i }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> fail $ err ++ "could not update nextlinkid using: " ++ str
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ err ++ "unimplemented selection:\n" ++ show se
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffremoveNthSymbol :: Monad m => Int -> DGraph -> LNode DGNodeLab -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffremoveNthSymbol n dg (v, lbl) = let nn = getDGNodeName lbl in
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case nodeInfo lbl of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff DGRef _ _ -> fail $ "cannot remove symbols from ref-node: " ++ nn
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff DGNode orig _ -> case orig of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff DGBasicSpec _ _ syms -> case atMaybe (Set.toList syms) $ n - 1 of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> fail $ "symbol " ++ show n ++ " not found in node: " ++ nn
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ "\n" ++ showDoc syms ""
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just gs@(G_symbol lid sym) -> case dgn_theory lbl of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff G_theory lid2 sig si sens _ ->
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff let Result ds mr = ext_cogenerated_sign lid2
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (Set.singleton $ coerceSymbol lid lid2 sym) sig
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff in case mr of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> fail $ "hiding " ++ showDoc sym " in " ++ nn ++
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff " failed:\n" ++ showRelDiags 1 ds
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just mor -> case makeExtSign lid2 $ dom mor of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff tarSig -> do
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff diffSig <- resultToMonad "ApplyChanges.removeNthSymbol"
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ homGsigDiff (G_sign lid2 sig si)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff $ G_sign lid2 tarSig startSigId
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff let newLbl = lbl
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff { dgn_theory = G_theory lid2 tarSig startSigId
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff sens startThId
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff , nodeInfo = newNodeInfo $ DGBasicSpec Nothing diffSig
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff finLbl = newLbl
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff { globalTheory = computeLabelTheory Map.empty dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (v, newLbl) }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff return $ changeDGH dg $ SetNodeLab lbl (v, finLbl)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff _ -> fail $ "cannot remove symbol from non-basic-spec node: " ++ nn
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffremoveNthAxOrTh :: Monad m => Bool -> Int -> DGraph -> LNode DGNodeLab
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff -> m DGraph
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduffremoveNthAxOrTh b n dg (v, lbl) = let nn = getDGNodeName lbl in
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff case dgn_theory lbl of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff G_theory lid sig si thsens _ -> let
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff sens = toNamedList $ OMap.filter ((if b then id else not) . isAxiom)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff in case atMaybe sens $ n - 1 of
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Nothing -> fail $ "sentence " ++ show n ++ " not found in node: "
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff ++ nn ++ "\n" ++ intercalate ", " (map senAttr sens)
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff Just ns -> let
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff newLbl = lbl { dgn_theory = G_theory lid sig si
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (Map.delete (senAttr ns) thsens) startThId }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff finLbl = newLbl { globalTheory = computeLabelTheory Map.empty dg
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff (v, newLbl) }
d25372dc8e65a9ed019a88fdf659ca61313f1b31jcduff in return $ changeDGH dg $ SetNodeLab lbl (v, finLbl)