import
Data.List (isPrefixOf, stripPrefix, nubBy)
-- | Returns the list of all nodes, if it is not up to date
-- the function recomputes the list
getAllNodes :: IntIState -> [LNode DGNodeLab]
= labNodesDG $ lookupDGraph (i_ln st) (i_libEnv st)
-- | Returns the list of all edges, if it is not up to date
-- the funcrion recomputes the list
getAllEdges :: IntIState -> [LEdge DGLinkLab]
getAllEdges st = labEdgesDG $ lookupDGraph (i_ln st) (i_libEnv st)
-- | Constructor for CMDLProofGUIState datatype
initNodeInfo:: (Logic lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>
ProofState lid1 sentence1 -> Int
emptyIntIState :: LibEnv -> LibName -> IntIState
script = ATPTacticScript {
emptyIntState :: IntState
IntState { i_state = Just $ emptyIntIState emptyLibEnv $ emptyLibName ""
, i_hist = IntHistory { undoList = []
-- If an absolute path is given,
-- it tries to remove the current working directory as prefix of it.
tryRemoveAbsolutePathComponent :: String -> IO String
tryRemoveAbsolutePathComponent f
| "/" `isPrefixOf` f = do
dir <- getCurrentDirectory
return $ fromMaybe f (stripPrefix (dir ++ "/") f)
-- Converts a list of proof-trees to a prove
proofTreeToProve :: FilePath
-> ProofState lid sentence -- current proofstate
-> Maybe (G_prover, AnyComorphism) -- possible used translation
-> [ProofStatus proof_tree] -- goals included in prove
proofTreeToProve fn st pcm pt =
drop 1 $ splitOn ';' $ language_name cid) trans
++ concatMap goalToCommands goals
prvr = maybe (selectedProver st) (Just . getProverName . fst) pcm
trans = maybe Nothing (Just . snd) pcm
-- 1. filter out the not proven goals
-- 2. reverse the list, because the last proven goals are on top
-- 3. convert all proof-trees to goals
-- 4. merge goals with same used axioms
-- axioms to include in prove
allax = case theory st of G_theory _ _ _ axs _ ->
OMap.keys axs
nodeName = dropName fn $ theoryName st
-- A goal is a pair of a name as String and time limit as Int
-- Merge goals with the same time-limit
mergeGoals :: [(String, Int)] -> [(String, Int)]
mergeGoals ((n,l):t) | l == l' = mergeGoals $ (n ++ ' ':n', l):
Prelude.tail t
| otherwise = (n,l):mergeGoals t
dropName :: String -> String -> String
-- This checks wether a goal was proved or not
wasProved :: ProofStatus proof_Tree -> Bool
wasProved g = case goalStatus g of
-- Converts a proof-tree into a goal.
parseTimeLimit :: ProofStatus proof_tree -> Int
(TacticScript scrpt) = tacticScript pt
addCommandHistoryToState :: IORef IntState
-> ProofState lid sentence -- current proofstate
-> Maybe (G_prover, AnyComorphism) -- possible used translation
-> [ProofStatus proof_tree] -- goals included in prove
addCommandHistoryToState intSt st pcm pt
| null $ filter wasProved pt = return $ Result [] $ Just ()
fn <- tryRemoveAbsolutePathComponent $ filename ost
writeIORef intSt $ add2history
(
IC.GroupCmd $ proofTreeToProve (rmSuffix fn) st pcm pt)
ost [ IStateChange $ i_state ost ]
return $ Result [] $ Just ()
conservativityRule :: DGRule
conservativityRule = DGRule "ConservativityCheck"
conservativityChoser :: Bool ->[ConservativityChecker sign sentence morphism]
-> IO (Result (ConservativityChecker sign sentence morphism))
conservativityChoser useGUI checkers = case checkers of
[] -> return $ fail "No conservativity checker available"
if useGUI && not (null tl) then do
chosenOne <- listBox "Pic a conservativity checker"
Nothing -> return $ fail "No conservativity checker chosen"
Just i -> return $ return $ checkers !! i
conservativityChoser _ checkers = case checkers of
[] -> return $ fail "No conservativity checker available"
checkConservativityNode :: Bool -> (LNode DGNodeLab) -> LibEnv -> LibName
-> IO (String, LibEnv, ProofHistory)
checkConservativityNode useGUI (nodeId, nodeLab) libEnv ln = do
let dg = lookupDGraph ln libEnv
emptyTh = case dgn_sign nodeLab of
noSensGTheory lid (mkExtSign $ empty_signature lid) startSigId
newL = (newNodeLab emptyNodeName DGProof emptyTh)
{ globalTheory = Just emptyTh }
morphism = case resultToMaybe $ ginclusion logicGraph (dgn_sign newL) $
lnk = (newN, nodeId, defDGLink
morphism (ScopedLink Global DefLink $ getNodeConsStatus nodeLab)
tempChanges = [ InsertNode (newN, newL), InsertEdge lnk ]
tempDG = changesDGH dg tempChanges
tempLibEnv = insert ln (groupHistory dg conservativityRule tempDG) libEnv
(str, tempLibEnv', _) <- checkConservativityEdge useGUI lnk tempLibEnv ln
if isPrefixOf "No conservativity" str
let tempDG' = lookupDGraph ln tempLibEnv'
(_,_,lnkLab) = head $ outDG tempDG' newN
nodeLab' = nodeLab { nodeInfo = nInfo { node_cons_status =
getLinkConsStatus $ dgl_type lnkLab } }
changes = [ SetNodeLab nodeLab (nodeId, nodeLab') ]
dg' = changesDGH dg changes
history = snd $ splitHistory dg dg'
libEnv' = insert ln (groupHistory dg conservativityRule dg') libEnv
return (str, libEnv', history)
checkConservativityEdge :: Bool -> (LEdge DGLinkLab) -> LibEnv -> LibName
-> IO (String, LibEnv, ProofHistory)
checkConservativityEdge useGUI (source,target,linklab) libEnv ln
case computeTheory libEnv ln target of
Result _ (Just th1) -> th1
_ -> error "checkconservativityOfEdge: computeTheory"
G_theory lid _sign _ sensTar _ <- return thTar
GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
morphism2' <- coerceMorphism (targetLogic cid) lid
"checkconservativityOfEdge" morphism2
let compMor = case dgn_sigma $ labDG (lookupDGraph ln libEnv) target of
Just (GMorphism cid' _ _ morphism3 _) -> case
coerceMorphism (targetLogic cid') lid
"checkconservativityOfEdge" morphism3
Result _ (Just phi) -> phi
_ -> error "checkconservativityOfEdge: comp"
case computeTheory libEnv ln source of
Result _ (Just th1) -> th1
_ -> error "checkconservativityOfEdge: computeTheory"
G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
let transSensSrc = propagateErrors
$ mapThSensValueM (map_sen lid compMor) sensSrc2
if length (conservativityCheck lid) < 1
then return ( "No conservativity checkers available"
checkerR <- conservativityChoser useGUI $ conservativityCheck lid
if hasErrors $ diags checkerR
then return ( "No conservativity checker chosen"
let chCons = checkConservativity $
fromMaybe (error "checkconservativityOfEdge")
inputThSens = nubBy (\ a b -> sentence a == sentence b) $
(plainSign sign2, toNamedList sensSrc2)
Just (Just (cst, _)) -> cst
consNew csv = if cs' >= csv
then Proven conservativityRule emptyProofBasis
(newDglType, edgeChange) = case dgl_type linklab of
ScopedLink sc dl (ConsStatus consv cs op) ->
let np = consNew consv in
ConsStatus consv (max cs $ max consv cs') np, np /= op)
, linklab { dgl_type = newDglType }
dg = lookupDGraph ln libEnv
nodelab = labDG dg target
obligations = case res of
Just (Just (_, os)) -> os
namedNewSens = toThSens [ (makeNamed "" o) {isAxiom = False} |
G_theory glid gsign gsigid gsens gid <- return $ dgn_theory nodelab
namedNewSens' <- coerceThSens lid glid "" namedNewSens
-- Sort out the named sentences which have a different name,
mergedSens = nubBy (\(_,a) (_,b) -> sentence a == sentence b) $
(newTheory, nodeChange) =
length oldSens /= length mergedSens)
,nodelab { dgn_theory = newTheory })
nodeChanges = [ SetNodeLab nodelab newTargetNode | nodeChange ]
edgeChanges = if edgeChange then
[ DeleteEdge (source,target,linklab)
, InsertEdge provenEdge ] else []
nextGr = changesDGH dg $ nodeChanges ++ edgeChanges
(groupHistory dg conservativityRule nextGr) libEnv
history = snd $ splitHistory dg nextGr
showObls lst = ", provided that the following proof "
++ "obligations can be discharged:\n"
mapNamed (simplify_sen glid sig1)) lst)
Just (Just (cst,_)) -> "The link is "
++ showConsistencyStatus cst
++ showObls (toNamedList namedNewSens')
_ -> "Could not determine whether link is "
myDiags = showRelDiags 2 ds
return ( showRes ++ "\n" ++ myDiags