e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : devGraph rule that calls provers for specific logics
d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederCopyright : (c) J. Gerken, T. Mossakowski, K. Luettich, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
4e2331b387b90a234dc36b12c778914d3e202718Christian MaederStability : provisional
4e2331b387b90a234dc36b12c778914d3e202718Christian MaederPortability : non-portable(Logic)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskidevGraph rule that calls provers for specific logics
57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill MossakowskiProof rule "basic inference" in the development graphs calculus.
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder Follows Sect. IV:4.4 of the CASL Reference Manual.
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder T. Mossakowski, S. Autexier and D. Hutter:
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder Extending Development Graphs With Hiding.
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder Lecture Notes in Computer Science 2029, p. 269-283,
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder Springer-Verlag 2001.
96d23995ee55ff3af632eedbb9e7ffc293a414a2Thiemo Wiedemeyer ( basicInferenceNode
abee46762c1663b85c6f18d934cd11df83828f6eChristian MaederselectProver :: [(G_prover, AnyComorphism)]
abee46762c1663b85c6f18d934cd11df83828f6eChristian Maeder -> ResultT IO (G_prover, AnyComorphism)
594891d02ecf595cd5fdd12e8036e686f1b90ddfChristian MaederselectProver ps = case ps of
594891d02ecf595cd5fdd12e8036e686f1b90ddfChristian Maeder [] -> fail "No prover available"
594891d02ecf595cd5fdd12e8036e686f1b90ddfChristian Maeder [p] -> return p
594891d02ecf595cd5fdd12e8036e686f1b90ddfChristian Maeder sel <- lift $ listBox "Choose a translation to a prover-supported logic"
abee46762c1663b85c6f18d934cd11df83828f6eChristian Maeder $ map (\ (aGN, cm) -> shows cm $ " (" ++ getProverName aGN ++ ")") ps
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder i <- case sel of
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder Just j -> return j
df75389b9266b115f0dc71a97679aec3dc0e48e1Christian Maeder _ -> fail "Proofs.Proofs: selection"
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder return $ ps !! i
4e2331b387b90a234dc36b12c778914d3e202718Christian MaederproveTheory :: Logic lid sublogics
4e2331b387b90a234dc36b12c778914d3e202718Christian Maeder basic_spec sentence symb_items symb_map_items
eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder sign morphism symbol raw_symbol proof_tree
433bb7cb49200f4e6c7341101da25309e423c0e2Christian Maeder => lid -> Prover sign sentence morphism sublogics proof_tree
eac3174ea16c143bfaeb3f2e2103a11a2f162c6cChristian Maeder -> String -> Theory sign sentence proof_tree
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski -> [FreeDefMorphism sentence morphism]
c2b17498cf4334382500475dc0f5556264e52079Christian Maeder -> IO ( [ProofStatus proof_tree]
c2b17498cf4334382500475dc0f5556264e52079Christian Maeder , [(Named sentence, ProofStatus proof_tree)])
1ac36418f204bbe56f4cd951a979180721758999Christian MaederproveTheory _ =
1ac36418f204bbe56f4cd951a979180721758999Christian Maeder fromMaybe (\ _ _ -> fail "proveGUI not implemented") . proveGUI
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder{- | applies basic inference to a given node. The result is a theory which is
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder either a model after a consistency check or a new theory for the node
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo WiedemeyerbasicInferenceNode :: LogicGraph -> LibName -> DGraph -> LNode DGNodeLab
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer -> LibEnv -> IORef IntState
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder -> IO (Result G_theory)
325e8aca700ad30d8ac47a00482c02dea2de3df0Christian MaederbasicInferenceNode lg ln dGraph (node, lbl) libEnv intSt =
95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder runResultT $ do
abee46762c1663b85c6f18d934cd11df83828f6eChristian Maeder -- compute the theory (that may contain proved theorems) and its name
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder thForProof <- liftR $ getGlobalTheory lbl
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder let thName = libToFileName ln ++ "_" ++ getDGNodeName lbl
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder freedefs = getCFreeDefMorphs libEnv ln dGraph node
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ps <- lift $ getUsableProvers ProveGUI (sublogicOfTh thForProof) lg
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer kpMap <- liftR knownProversGUI
42f76486938cb03ba650ee09c68304fd4a86fb87Jonathan von Schroeder {- let kpMap = foldl (\m (G_prover _ p,c) ->
247eefa106a467b872521724ff7bf4af5c27220dJonathan von Schroeder case Map.lookup (proverName p) m of
247eefa106a467b872521724ff7bf4af5c27220dJonathan von Schroeder Just cs -> Map.insert (proverName p) (c:cs) m
42f76486938cb03ba650ee09c68304fd4a86fb87Jonathan von Schroeder Nothing -> Map.insert (proverName p) [c] m) Map.empty ps -}
1caac17e785f1133f7c4d9a97f367f7832823cfcJonathan von Schroeder ResultT $ proverGUI ProofActions
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer { proveF = proveKnownPMap lg intSt freedefs
0cdeccb66730b876f73bddd2705ddc62e180320dThiemo Wiedemeyer , fineGrainedSelectionF = proveFineGrainedSelect lg intSt freedefs
feb4e4217d5621a971077c8399b4b49237f07bacChristian Maeder , recalculateSublogicF = return . recalculateSublogicAndSelectedTheory
1caac17e785f1133f7c4d9a97f367f7832823cfcJonathan von Schroeder } thName (hidingLabelWarning lbl) thForProof kpMap ps
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaederproveKnownPMap :: LogicGraph
ce1c76a52a42788c085b7794a1a5f9758799a0e2Markus Gross -> IORef IntState
42f76486938cb03ba650ee09c68304fd4a86fb87Jonathan von Schroeder -> [GFreeDefMorphism]
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder -> ProofState -> IO (Result ProofState)
c2b17498cf4334382500475dc0f5556264e52079Christian MaederproveKnownPMap lg intSt freedefs st =
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu maybe (proveFineGrainedSelect lg intSt freedefs st)
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu (callProver st intSt False freedefs) $
da955132262baab309a50fdffe228c9efe68251dCui Jian lookupKnownProver st ProveGUI
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaedercallProver :: ProofState
ce1c76a52a42788c085b7794a1a5f9758799a0e2Markus Gross -> IORef IntState
71654489020a03cf6ce9f2947f3da26a996f9c32Razvan Pascanu -> Bool -- indicates if a translation was chosen
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder -> [GFreeDefMorphism]
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder -> (G_prover, AnyComorphism) -> IO (Result ProofState)
c2b17498cf4334382500475dc0f5556264e52079Christian MaedercallProver st intSt trans_chosen freedefs p_cm@(_, acm) =
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich runResultT $ do
62f38a562115f39afdec71801ba3b74d53706db7Thiemo Wiedemeyer (_, exit) <- lift $ pulseBar "prepare for proving" "please wait..."
7c8051ef91610c696bc9fa2e61ad1b153fbe7ce0Klaus Luettich G_theory_with_prover lid th p <- liftR $ prepareForProving st p_cm
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder freedefs1 <- mapM (\ (GFreeDefMorphism fdlid fd) ->
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder coerceFreeDefMorphism fdlid lid "" fd) freedefs
06799f39787bc3facfaebb50bdc87439d2b6f99bChristian Maeder (ps, _) <- lift $ proveTheory lid p (theoryName st) th freedefs1
f9aa644af131a2571514a7e5bbd8901e32ad6273Markus Gross let st' = markProved acm lid ps st
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder lift $ addCommandHistoryToState intSt st'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (if trans_chosen then Just p_cm else Nothing) ps "" (False, 0)
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian MaederproveFineGrainedSelect :: LogicGraph
ce1c76a52a42788c085b7794a1a5f9758799a0e2Markus Gross -> IORef IntState
dba73947b1f8befd8ffb81fbed7deb6e582f3f62Christian Maeder -> [GFreeDefMorphism]
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder -> ProofState -> IO (Result ProofState)
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan PascanuproveFineGrainedSelect lg intSt freedefs st =
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder runResultT $ do
fdf94376fa12e6f685f87741be2f3d02e03c429eChristian Maeder let sl = sublogicOfTheory st
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder cmsToProvers <- lift $ getUsableProvers ProveGUI sl lg
d4cb5f03c55f0aeff72f06dac61e1af24479ddd9Rainer Grabbe pr <- selectProver cmsToProvers
5607bbe40d1b360797381a83a6eae6773ee7cd2cChristian Maeder ResultT $ callProver st { comorphismsToProvers = cmsToProvers }
8f5219469b89a15dc6d4c2c30463775975f5841cRazvan Pascanu intSt True freedefs pr