type ProofStatus = (GlobalContext, [([DGRule], [DGChange])], DGraph) |
|
|
|
|
|
data BasicProof | = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree . Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => BasicProof lid (Proof_status sentence proof_tree) | | Guessed | | Conjectured | | Handwritten |
|
|
|
data BasicConsProof = BasicConsProof |
|
applyRule :: DGRule -> DGraph -> Maybe ([DGChange], DGraph) |
|
globDecomp :: ProofStatus -> ProofStatus |
|
globDecompAux :: DGraph -> [LEdge DGLinkLab] -> ([DGRule], [DGChange]) -> (DGraph, ([DGRule], [DGChange])) |
|
globDecompForOneEdge :: DGraph -> LEdge DGLinkLab -> (DGraph, [DGChange]) |
|
globDecompForOneEdgeAux :: DGraph -> LEdge DGLinkLab -> [DGChange] -> [(Node, [LEdge DGLinkLab])] -> (DGraph, [DGChange]) |
|
globSubsume :: ProofStatus -> ProofStatus |
|
globSubsumeAux :: DGraph -> ([DGRule], [DGChange]) -> [LEdge DGLinkLab] -> (DGraph, ([DGRule], [DGChange])) |
|
getLabelOfEdge :: LEdge b -> b |
|
locDecomp :: ProofStatus -> ProofStatus |
|
locDecompAux :: DGraph -> ([DGRule], [DGChange]) -> [LEdge DGLinkLab] -> (DGraph, ([DGRule], [DGChange])) |
|
getAllGlobPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node -> [[LEdge DGLinkLab]] |
|
filterPathsByMorphism :: GMorphism -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]] |
|
getAllLocGlobDefPathsTo :: DGraph -> Node -> [LEdge DGLinkLab] -> [(Node, [LEdge DGLinkLab])] |
|
getAllGlobPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]] |
|
getAllThmDefPathsOfMorphismBetween :: DGraph -> GMorphism -> Node -> Node -> [[LEdge DGLinkLab]] |
|
getAllGlobDefPathsBetween :: DGraph -> Node -> Node -> [[LEdge DGLinkLab]] |
|
getAllPathsOfTypeBetween :: DGraph -> (LEdge DGLinkLab -> Bool) -> Node -> Node -> [[LEdge DGLinkLab]] |
|
getAllPathsOfTypesBetween :: DGraph -> [LEdge DGLinkLab -> Bool] -> Node -> Node -> [LEdge DGLinkLab] -> [[LEdge DGLinkLab]] |
|
filterByTypes :: [LEdge DGLinkLab -> Bool] -> [LEdge DGLinkLab] -> [LEdge DGLinkLab] |
|
calculateMorphismOfPath :: [LEdge DGLinkLab] -> Maybe GMorphism |
|
getSourceNode :: LEdge DGLinkLab -> Node |
|
isProven :: LEdge DGLinkLab -> Bool |
|
isGlobalThm :: LEdge DGLinkLab -> Bool |
|
isProvenGlobalThm :: LEdge DGLinkLab -> Bool |
|
isUnprovenGlobalThm :: LEdge DGLinkLab -> Bool |
|
isProvenLocalThm :: LEdge DGLinkLab -> Bool |
|
isUnprovenLocalThm :: LEdge DGLinkLab -> Bool |
|
isGlobalDef :: LEdge DGLinkLab -> Bool |
|
isLocalDef :: LEdge DGLinkLab -> Bool |
|
getLabelOfAnyInsertedEdge :: [DGChange] -> Maybe DGLinkLab |
|
getInsertedEdges :: [DGChange] -> [LEdge DGLinkLab] |
|
selectProofBasis :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab] |
|
selectProofBasisAux :: DGLinkLab -> [[LEdge DGLinkLab]] -> [DGLinkLab] |
|
calculateProofBasis :: [LEdge DGLinkLab] -> [DGLinkLab] |
|
getProofBasis :: DGLinkLab -> [DGLinkLab] |
|
filterProvenPaths :: [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]] |
|
notProofCycle :: DGLinkLab -> [LEdge DGLinkLab] -> Bool |
|
isProofCycle :: DGLinkLab -> [LEdge DGLinkLab] -> Bool |
|
elemOfProofBasis :: DGLinkLab -> LEdge DGLinkLab -> Bool |