ProveCommands.hs revision 56f49c2883b1da5b18c57ca94457b2c4757a28d3
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantz{-# LANGUAGE CPP #-}
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzModule : $Header$
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzDescription : CMDL interface commands
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzCopyright : uni-bremen and DFKI
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndMaintainer : r.pascanu@jacobs-university.de
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndStability : provisional
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndPortability : portable
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenCMDL.ProveCommands contains all commands (except prove\/consistency check)
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenrelated to prove mode
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd ( cTranslate
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cDropTranslations
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen , cGoalsAxmGeneral
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cProveAll
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cSetUseThms
3f08db06526d6901aa08c110b5bc7dde6bc39905nd , cSetSave2File
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cEndScript
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cStartScript
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd , cTimeLimit
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd , cNotACommand
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport CMDL.DataTypes(CmdlState(intState), CmdlGoalAxiom(..),
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd CmdlListAction(..))
864d6d55a72bdb982ebabbc95cf8f051c43fa6ddrbowenimport CMDL.DataTypesUtils(add2hist, genErrorMsg, genMessage, getIdComorphism)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport CMDL.DgCommands(selectANode)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport CMDL.ProveConsistency(doLoop, sigIntHandler)
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjungimport CMDL.Utils(checkIntString)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Static.GTheory(G_theory(G_theory))
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzimport Common.Result(Result(Result))
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzimport qualified Common.OrderedMap as OMap
e4ca72aa494fed7b6948012734b9c9c098fbba07ndimport Data.List (find, nub)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Comorphisms.LogicGraph(lookupComorphism_in_LG)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Proofs.AbstractState(ProofState(..))
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinimport Logic.Comorphism(compComorphism)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Control.Concurrent.MVar(newEmptyMVar, newMVar, takeMVar)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd#ifdef UNIX
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15ndimport System.Posix.Signals(Handler(Catch), installHandler, sigINT)
b12f74e1aaac71d21e4b9a376b31d7307a8d87d8ndimport Interfaces.GenericATPState(ATPTacticScript(tsTimeLimit, tsExtraOpts))
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohimport Interfaces.DataTypes(ListChange(..), IntIState(..), Int_NodeInfo(..),
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd UndoRedoElem(..), IntState(i_state))
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd-- | Drops any seleceted comorphism
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcDropTranslations :: CmdlState -> IO CmdlState
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcDropTranslations state =
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd case i_state $ intState state of
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Nothing -> return $ genErrorMsg "Nothing selected" state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Just pS ->
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd case cComorphism pS of
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Nothing -> return state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Just _ -> return $
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd add2hist [CComorphismChange $ cComorphism pS] $
e4ca72aa494fed7b6948012734b9c9c098fbba07nd intState = (intState state ) {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd i_state = Just $ pS {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd cComorphism = getIdComorphism $ elements pS } }
e4ca72aa494fed7b6948012734b9c9c098fbba07nd-- | select comorphisms
e4ca72aa494fed7b6948012734b9c9c098fbba07ndcTranslate::String -> CmdlState -> IO CmdlState
e4ca72aa494fed7b6948012734b9c9c098fbba07ndcTranslate input state =
e4ca72aa494fed7b6948012734b9c9c098fbba07nd case i_state $ intState state of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd -- nothing selected !
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Nothing -> return $ genErrorMsg "Nothing selected" state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Just pS ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -- parse the comorphism name
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case lookupComorphism_in_LG $ trim input of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ Nothing -> return $ genErrorMsg "Wrong comorphism name" state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ (Just cm) ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case cComorphism pS of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -- when selecting some theory the Id comorphism is automatically
7e9d90004f580231e0376880710dc25408950ab9rbowen -- generated
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Nothing -> return $ genErrorMsg "No theory selected" state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Just ocm ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case compComorphism ocm cm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ Nothing ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin return $ genErrorMsg "Can not add comorphism" state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ (Just smth) ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin return $ genMessage [] "Adding comorphism"
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin $ add2hist [CComorphismChange $ cComorphism pS] $
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin intState = (intState state) {
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin i_state = Just pS {
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin cComorphism = Just smth } }
7e9d90004f580231e0376880710dc25408950ab9rbowenparseElements :: CmdlListAction -> [String] -> CmdlGoalAxiom
7e9d90004f580231e0376880710dc25408950ab9rbowen -> [Int_NodeInfo]
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -> ([Int_NodeInfo],[ListChange])
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -> ([Int_NodeInfo],[ListChange])
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinparseElements action gls gls_axm elems (acc1,acc2)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin = case elems of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin [] -> (acc1,acc2)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin (Element st nb):ll ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin let allgls = case gls_axm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeGoals -> OMap.keys $ goalMap st
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeAxioms-> case theory st of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin G_theory _ _ _ aMap _ ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin selgls = case gls_axm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeGoals -> selectedGoals st
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeAxioms-> includedAxioms st
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin fn' x y = x==y
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin fn ks x = case find (fn' x) ks of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case action of
7e9d90004f580231e0376880710dc25408950ab9rbowen ActionDel -> False
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case action of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDel -> True
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin gls' = case action of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDelAll -> []
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDel -> filter (fn selgls) gls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionSetAll -> allgls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionSet -> filter (fn allgls) gls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionAdd -> nub $ selgls ++ filter (fn allgls) gls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin nwelm = case gls_axm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeGoals -> Element (st {selectedGoals = gls'}) nb
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeAxioms -> Element (st {includedAxioms= gls'}) nb
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin hchg = case gls_axm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeGoals -> GoalsChange (selectedGoals st) nb
7e9d90004f580231e0376880710dc25408950ab9rbowen ChangeAxioms -> AxiomsChange(includedAxioms st) nb
7e9d90004f580231e0376880710dc25408950ab9rbowen in parseElements action gls gls_axm ll (nwelm:acc1,hchg:acc2)
7e9d90004f580231e0376880710dc25408950ab9rbowen-- | A general function that implements the actions of setting,
7e9d90004f580231e0376880710dc25408950ab9rbowen-- adding or deleting goals or axioms from the selection list
7e9d90004f580231e0376880710dc25408950ab9rbowencGoalsAxmGeneral :: CmdlListAction -> CmdlGoalAxiom ->
7e9d90004f580231e0376880710dc25408950ab9rbowen String ->CmdlState
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -> IO CmdlState
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcGoalsAxmGeneral action gls_axm input state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd = case i_state $ intState state of
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Nothing -> return $ genErrorMsg "Nothing selected" state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Just pS ->
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd case elements pS of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd [] -> return $ genErrorMsg "Nothing selected" state
5bc7abb0ed18f8dbc491d0be0a09bc02e6ee9d85nd let gls = words input
5bc7abb0ed18f8dbc491d0be0a09bc02e6ee9d85nd let (ls',hst) = parseElements action gls
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd ls ([],[])
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd return $ add2hist [ListChange hst] $
aa0b2780958e9b1467c9d0153a05738e399811a5nd intState = (intState state) {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd i_state = Just pS {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd elements = ls'
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igaliccDoLoop :: Bool
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic -> CmdlState
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic -> IO CmdlState
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igaliccDoLoop checkCons state
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic = case i_state $ intState state of
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic Nothing -> return $ genErrorMsg "Nothing selected" state
e487d6c09669296f94a5190cc34586a98e624a00nd case elements pS of
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovener [] -> return $ genErrorMsg "Nothing selected" state
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovener --create initial mVars to comunicate
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovener miSt <- newMVar $ intState state
e4ca72aa494fed7b6948012734b9c9c098fbba07nd mSt <- newMVar Nothing
e4ca72aa494fed7b6948012734b9c9c098fbba07nd mThr <- newMVar Nothing
a29610af88e278144045bfa1bc63b4a1a4b5ff14trawick mW <- newEmptyMVar
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd thrID <- forkIO(doLoop miSt mThr mSt mW ls checkCons)
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd -- install the handler that waits for SIG_INT
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd oldHandler <- installHandler sigINT (Catch $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd sigIntHandler mThr miSt mSt thrID mW (i_ln pS)
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd -- block and wait for answers
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd answ <- takeMVar mW
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd installHandler sigINT oldHandler Nothing
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd let nwpS = case i_state answ of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Nothing -> pS
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Just pS' -> pS'
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd nwls = concatMap(\(Element _ x) -> selectANode x nwpS) ls
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd hst = concatMap(\(Element stt x) ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd [(AxiomsChange (includedAxioms stt) x),
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd (GoalsChange (selectedGoals stt) x)]) ls
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd return $ add2hist [(ListChange hst)] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd state { intState = answ {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd i_state = Just $ nwpS { elements = nwls }
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd-- | Proves only selected goals from all nodes using selected
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProve :: CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProve = cDoLoop False
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd-- | Proves all goals in the nodes selected using all axioms and
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProveAll::CmdlState ->IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProveAll state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd = case i_state $ intState state of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Nothing -> return$ genErrorMsg "Nothing selected" state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd case elements pS of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd [] -> return $ genErrorMsg "Nothing selected" state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd let ls' = map (\(Element st nb) ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd case theory st of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd G_theory _ _ _ aMap _ ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd selectedGoals = OMap.keys $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd goalMap st,
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd includedAxioms = OMap.keys aMap,
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd includedTheorems = OMap.keys $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd let nwSt = add2hist [ListChange [NodesChange $ elements pS]] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd intState = (intState state) {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd i_state = Just $ pS {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd elements = ls' } } }
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd cProve nwSt
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd-- | Sets the use theorems flag of the interface
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcSetUseThms :: Bool -> CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcSetUseThms val state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd = case i_state $ intState state of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Nothing -> return $ genErrorMsg "Norhing selected" state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd return $ add2hist [UseThmChange $ useTheorems pS] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd intState = (intState state) {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd i_state= Just pS {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd useTheorems = val } } }
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd-- | Sets the save2File value to either true or false
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcSetSave2File :: Bool -> CmdlState -> IO CmdlState
3b3b7fc78d1f5bfc2769903375050048ff41ff26ndcSetSave2File val state
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd = case i_state $ intState state of
0066eddda7203f6345b56f77d146a759298dc635gryzor Nothing -> return $ genErrorMsg "Nothing selected" state
7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0nd Just ps ->
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung return $ add2hist [Save2FileChange $ save2file ps] $
0d0ba3a410038e179b695446bb149cce6264e0abnd intState = (intState state) {
727872d18412fc021f03969b8641810d8896820bhumbedooh i_state = Just ps { save2file = val } } }
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh-- | The function is called everytime when the input could
727872d18412fc021f03969b8641810d8896820bhumbedooh-- not be parsed as a command
0d0ba3a410038e179b695446bb149cce6264e0abndcNotACommand :: String -> CmdlState -> IO CmdlState
0d0ba3a410038e179b695446bb149cce6264e0abndcNotACommand input state
0d0ba3a410038e179b695446bb149cce6264e0abnd = case input of
ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh -- if input line is empty do nothing
0d0ba3a410038e179b695446bb149cce6264e0abnd [] -> return state
0d0ba3a410038e179b695446bb149cce6264e0abnd -- anything else see if it is in a blocl of command
727872d18412fc021f03969b8641810d8896820bhumbedooh case i_state $ intState state of
0d0ba3a410038e179b695446bb149cce6264e0abnd Nothing -> return $ genErrorMsg ("Error on input line :"++s) state
0d0ba3a410038e179b695446bb149cce6264e0abnd Just pS ->
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh if loadScript pS
0d0ba3a410038e179b695446bb149cce6264e0abnd let olds = script pS
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd oldextOpts = tsExtraOpts olds
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd let nwSt = state {
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd intState = (intState state) {
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd i_state = Just pS {