InferBasic.hs revision 29d0028b733c2c9b909095ed1eb397131c910daf
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerModule : $Header$
6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerDescription : devGraph rule that calls provers for specific logics
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCopyright : (c) J. Gerken, T. Mossakowski, K. Luettich, Uni Bremen 2002-2006
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerMaintainer : till@informatik.uni-bremen.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerPortability : non-portable(Logic)
7520452bb30b5abbd471f82352fc4c1c937e02c5Till MossakowskidevGraph rule that calls provers for specific logics
7520452bb30b5abbd471f82352fc4c1c937e02c5Till MossakowskiProof rule "basic inference" in the development graphs calculus.
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski Follows Sect. IV:4.4 of the CASL Reference Manual.
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer T. Mossakowski, S. Autexier and D. Hutter:
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Extending Development Graphs With Hiding.
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Lecture Notes in Computer Science 2029, p. 269-283,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Springer-Verlag 2001.
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ( basicInferenceNode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , consistencyCheck
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , ConsistencyStatus(..)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Common.Lib.Graph as Tree
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.Graph.Inductive.Basic (elfilter)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.Time.LocalTime (timeToTimeOfDay)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.Time.Clock (secondsToDiffTime)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.Ord (comparing)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetCFreeDefLinks :: DGraph -> Node
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetCFreeDefLinks dg tgt =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let isGlobalOrCFreeEdge = liftOr isGlobalEdge $ liftOr isFreeEdge isCofreeEdge
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer paths = map reverse $ Tree.getAllPathsTo tgt
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer $ elfilter (isGlobalOrCFreeEdge . dgl_type) $ dgBody dg
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer myfilter p = filter ( \ ((_, _, lbl) : _) -> p $ dgl_type lbl)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in (myfilter isFreeEdge paths, myfilter isCofreeEdge paths)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermkFreeDefMor :: [Named sentence] -> morphism -> morphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> FreeDefMorphism sentence morphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermkFreeDefMor sens m1 m2 = FreeDefMorphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer { freeDefMorphism = m1
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer , pathFromFreeDef = m2
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , freeTheory = sens
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer , isCofree = False }
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo WiedemeyergetFreeDefMorphism :: Logic lid sublogics
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer basic_spec sentence symb_items symb_map_items
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer sign morphism symbol raw_symbol proof_tree =>
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer lid -> LibEnv -> LibName -> DGraph -> [LEdge DGLinkLab]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> Maybe (FreeDefMorphism sentence morphism)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetFreeDefMorphism lid libEnv ln dg path = case path of
d5f9a0b274192a496eb8d2fb8ce81c33ac2f1717Thiemo Wiedemeyer [] -> error "getFreeDefMorphism"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (s, t, l) : rp -> do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer gmor@(GMorphism cid _ _ fmor _) <- return $ dgl_morphism l
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer G_theory lidth (ExtSign _sign _) _ axs _ <-
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer resultToMaybe $ computeTheory libEnv ln s
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer if isHomogeneous gmor then do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer cfmor <- coerceMorphism (targetLogic cid) lid "getFreeDefMorphism1" fmor
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer sens <- coerceSens lidth lid "getFreeDefMorphism4" (toNamedList axs)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer G_theory lid2 (ExtSign sig _) _ _ _ <-
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer return $ dgn_theory $ labDG dg t
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer sig2 <- coercePlainSign lid2 lid "getFreeDefMorphism2" sig
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ mkFreeDefMor sens cfmor $ ide sig2
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer pm@(GMorphism cid2 _ _ pmor _) <- calculateMorphismOfPath rp
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer if isHomogeneous pm then do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer cpmor <- coerceMorphism (targetLogic cid2) lid
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer "getFreeDefMorphism3" pmor
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ mkFreeDefMor sens cfmor cpmor
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetCFreeDefMorphs :: Logic lid sublogics
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer basic_spec sentence symb_items symb_map_items
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer sign morphism symbol raw_symbol proof_tree =>
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer lid -> LibEnv -> LibName -> DGraph -> Node
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> [FreeDefMorphism sentence morphism]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyergetCFreeDefMorphs lid libEnv ln dg node = let
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo Wiedemeyer (frees, cofrees) = getCFreeDefLinks dg node
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer myget = mapMaybe (getFreeDefMorphism lid libEnv ln dg)
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer mkCoFree m = m { isCofree = True }
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in myget frees ++ map mkCoFree (myget cofrees)
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo WiedemeyerselectProver :: GetPName a => [(a, AnyComorphism)]
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer -> ResultT IO (a, AnyComorphism)
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo WiedemeyerselectProver ps = case ps of
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer [] -> fail "No prover available"
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer [p] -> return p
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer sel <- lift $ listBox "Choose a translation to a prover-supported logic"
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer $ map (\ (aGN, cm) -> shows cm $ " (" ++ getPName aGN ++ ")") ps
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer i <- case sel of
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer Just j -> return j
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer _ -> fail "Proofs.Proofs: selection"
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer return $ ps !! i
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo WiedemeyerproveTheory :: Logic lid sublogics
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer basic_spec sentence symb_items symb_map_items
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer sign morphism symbol raw_symbol proof_tree
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer => lid -> Prover sign sentence morphism sublogics proof_tree
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer -> String -> Theory sign sentence proof_tree
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer -> [FreeDefMorphism sentence morphism]
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer -> IO([ProofStatus proof_tree])
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo WiedemeyerproveTheory _ =
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer fromMaybe (\ _ _ -> fail "proveGUI not implemented") . proveGUI
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer{- | applies basic inference to a given node. The result is a theory which is
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer either a model after a consistency check or a new theory for the node
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyerbasicInferenceNode :: LogicGraph -> LibName -> DGraph -> LNode DGNodeLab
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -> LibEnv -> IORef IntState
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -> IO (Result G_theory)
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyerbasicInferenceNode lg ln dGraph (node, lbl) libEnv intSt =
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer runResultT $ do
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -- compute the theory of the node, and its name
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer -- may contain proved theorems
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer thForProof@(G_theory lid1 _ _ _ _) <- liftR $ getGlobalTheory lbl
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer let thName = shows (getLibId ln) "_" ++ getDGNodeName lbl
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer sublogic = sublogicOfTh thForProof
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer -- select a suitable translation and prover
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer cms = filter hasModelExpansion $ findComorphismPaths lg sublogic
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer freedefs = getCFreeDefMorphs lid1 libEnv ln dGraph node
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer kpMap <- liftR knownProversGUI
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer ResultT $ proverGUI lid1 ProofActions
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer { proveF = proveKnownPMap lg intSt freedefs
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer , fineGrainedSelectionF = proveFineGrainedSelect lg intSt freedefs
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer , recalculateSublogicF = return . recalculateSublogicAndSelectedTheory
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer } thName (hidingLabelWarning lbl) thForProof kpMap
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (getProvers ProveGUI (Just sublogic) cms)
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyerdata SType = CSUnchecked
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer | CSInconsistent
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer | CSConsistent
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer deriving (Eq, Ord)
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyerdata ConsistencyStatus = ConsistencyStatus { sType :: SType
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer , sMessage :: String }
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyerinstance Show ConsistencyStatus where
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer show cs = case sType cs of
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer CSUnchecked -> "Unchecked"
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer _ -> sMessage cs
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyerinstance Eq ConsistencyStatus where
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (==) cs1 cs2 = compare cs1 cs2 == EQ
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyerinstance Ord ConsistencyStatus where
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer compare = comparing sType
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyerconsistencyCheck :: Bool -> G_cons_checker -> AnyComorphism -> LibName -> LibEnv
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -> DGraph -> LNode DGNodeLab -> Int -> IO ConsistencyStatus
966a6c024c828387023fccb0cd0049f78687e5dcThiemo WiedemeyerconsistencyCheck includeTheorems (G_cons_checker lid4 cc) (Comorphism cid) ln
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer le dg (n', lbl) t'' = do
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let lidS = sourceLogic cid
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer lidT = targetLogic cid
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer thName = shows (getLibId ln) "_" ++ getDGNodeName lbl
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer t = t'' * 1000000
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer t' = timeToTimeOfDay $ secondsToDiffTime $ toInteger t''
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer ts = TacticScript $ if ccNeedsTimer cc then "" else show t''
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer mTimeout = "No results within: " ++ show t'
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (G_theory lid1 (ExtSign sign _) _ axs _) <- getGlobalTheory lbl
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let namedSens = toNamedList axs
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer sens = if includeTheorems then
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer map (\ s -> s { isAxiom = True }) namedSens
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer else namedSens
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens)
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (sig2, sens2) <- wrapMapTheory cid bTh'
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer incl <- subsig_inclusion lidT (empty_signature lidT) sig2
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return (sig1, TheoryMorphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer { tSource = emptyTheory lidT
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , tTarget = Theory sig2 $ toThSens sens2
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer , tMorphism = incl }) of
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer Result ds Nothing ->
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer return $ ConsistencyStatus CSError $ unlines $ map diagString ds
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer Result _ (Just (sig1, mor)) -> do
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer cc' <- coerceConsChecker lid4 lidT "" cc
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ret <- (if ccNeedsTimer cc then timeout t else ((return . Just) =<<))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (ccAutomatic cc' thName ts mor $ getCFreeDefMorphs lidT le ln dg n')
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ case ret of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just ccStatus -> case ccResult ccStatus of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just b -> if b then let
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result ds ms = extractModel cid sig1 $ ccProofTree ccStatus
966a6c024c828387023fccb0cd0049f78687e5dcThiemo Wiedemeyer Nothing -> ConsistencyStatus CSConsistent $ unlines
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer ("consistent, but could not reconstruct a model"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer : map diagString ds ++ lines (show $ ccProofTree ccStatus))
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer Just (sig3, sens3) -> ConsistencyStatus CSConsistent $ showDoc
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer (G_theory lidS (mkExtSign sig3) startSigId (toThSens sens3)
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer else ConsistencyStatus CSInconsistent $ show (ccProofTree ccStatus)
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer Nothing -> if ccUsedTime ccStatus >= t' then
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder ConsistencyStatus CSTimeout mTimeout
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer else ConsistencyStatus CSError $ show (ccProofTree ccStatus)
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer Nothing -> ConsistencyStatus CSTimeout mTimeout
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian MaederproveKnownPMap :: (Logic lid sublogics1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer symb_map_items1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer proof_tree1) =>
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> IORef IntState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> [FreeDefMorphism sentence morphism1]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> ProofState lid sentence -> IO (Result (ProofState lid sentence))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerproveKnownPMap lg intSt freedefs st =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer maybe (proveFineGrainedSelect lg intSt freedefs st)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (callProver st intSt False freedefs) $
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer lookupKnownProver st ProveGUI
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercallProver :: (Logic lid sublogics1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer symb_map_items1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer proof_tree1) =>
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ProofState lid sentence
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> IORef IntState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> Bool -- indicates if a translation was chosen
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> [FreeDefMorphism sentence morphism1]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> (G_prover,AnyComorphism) -> IO (Result (ProofState lid sentence))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercallProver st intSt trans_chosen freedefs p_cm@(_,acm) =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer runResultT $ do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (_, exit) <- lift $ pulseBar "prepare for proving" "please wait..."
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer G_theory_with_prover lid th p <- liftR $ prepareForProving st p_cm
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let freedefs1 = fromMaybe [] $ mapM (coerceFreeDefMorphism (logicId st)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer lid "Logic.InferBasic: callProver")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ps <- lift $ proveTheory lid p (theoryName st) th freedefs1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let st' = markProved acm lid ps st
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer lift $ addCommandHistoryToState intSt st'
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (if trans_chosen then Just p_cm else Nothing) ps
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerproveFineGrainedSelect ::
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (Logic lid sublogics1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer symb_map_items1
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer proof_tree1) =>
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> IORef IntState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> [FreeDefMorphism sentence morphism1]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> ProofState lid sentence -> IO (Result (ProofState lid sentence))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerproveFineGrainedSelect lg intSt freedefs st =
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer runResultT $ do
6c59ae2c44a1fe22ef1712a57afe129e9dbd3368Thiemo Wiedemeyer let sl = sublogicOfTheory st
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer cmsToProvers =
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer if sl == lastSublogic st
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer then comorphismsToProvers st
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer else getProvers ProveGUI (Just sl) $
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer filter hasModelExpansion $ findComorphismPaths lg sl
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer pr <- selectProver cmsToProvers
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer ResultT $ callProver st{lastSublogic = sublogicOfTheory st,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer comorphismsToProvers = cmsToProvers}
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer intSt True freedefs pr