InferBasic.hs revision 0f2be8b95750f4ac578e8a92ac6ef73b48526580
1965c5d21403c3d66eb1efa29c670378311b1077Paul BryanModule : $Header$
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosDescription : devGraph rule that calls provers for specific logics
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosCopyright : (c) J. Gerken, T. Mossakowski, K. L�ttich, Uni Bremen 2002-2006
23bd88d6bfcb5a6d1140e68c159d14264cb5d41bJason VincentLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosMaintainer : till@tzi.de
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosStability : provisional
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosPortability : non-portable(Logic)
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosdevGraph rule that calls provers for specific logics
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosProof rule "basic inference" in the development graphs calculus.
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordos Follows Sect. IV:4.4 of the CASL Reference Manual.
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordos T. Mossakowski, S. Autexier and D. Hutter:
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordos Extending Development Graphs With Hiding.
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordos H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordos Lecture Notes in Computer Science 2029, p. 269-283,
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordos Springer-Verlag 2001.
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordosmodule Proofs.InferBasic (basicInferenceNode, getGoals, GetPName()) where
e9aaa1f1adc6f718befc047fe7177bdf52198c3aLaszlo Hordosimport qualified Data.Map as Map
e9aaa1f1adc6f718befc047fe7177bdf52198c3aLaszlo Hordosimport qualified Data.Set as Set
e9aaa1f1adc6f718befc047fe7177bdf52198c3aLaszlo Hordosimport qualified Common.OrderedMap as OMap
fd25b99368235181964a13861fbd7bb0a210ddc8Bruno Lavit-- ---------------
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan-- basic inference
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan-- ---------------
bdf1b2b1491da535d3c50421c77fc8b1255e5f0aAndi EgloffgetGoals :: LibEnv -> LIB_NAME -> LEdge DGLinkLab
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit -> Result G_theory
0fdda69ce3627d501e4bb3103765f676bb1ab061Laszlo HordosgetGoals libEnv ln (n,_,edge) = do
43689602ee8a67deb29ea8412c48410dcaa6b30aLaszlo Hordos th <- computeLocalTheory libEnv ln n
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan translateG_theory (dgl_morphism edge) th
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavitclass GetPName a where
fa9b7593e9e156060babbf3a9b06de8d6b5da5a3Laszlo Hordos getPName :: a -> String
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryaninstance GetPName G_prover where
bf3adaa7953ef4d249670fa82f2a0f7f17ee4b7bLaszlo Hordos getPName (G_prover _ p) = prover_name p
376d1bf8f8ca562eecccbf0a0d34aa7c7352e152Laszlo Hordosinstance GetPName G_cons_checker where
4a3638f833b6a5b87f5979857fb774ca53385cefChad Kienle getPName (G_cons_checker _ p) = prover_name p
43689602ee8a67deb29ea8412c48410dcaa6b30aLaszlo Hordos-- | Pairs each target prover of these comorphisms with its comorphism
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno LavitgetProvers :: [AnyComorphism] -> [(G_prover, AnyComorphism)]
4a3638f833b6a5b87f5979857fb774ca53385cefChad KienlegetProvers = foldl addProvers []
4b93fff6cbed4e2ae34e954b9b9bd4f318d34cd4Andi Egloff where addProvers acc cm =
5fc4ae486aef7fabd30ff1d12e8324ca9077b394Andi Egloff Comorphism cid -> acc ++
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit foldl (\ l p -> if hasProverKind ProveGUI p
5fc4ae486aef7fabd30ff1d12e8324ca9077b394Andi Egloff then (G_prover (targetLogic cid) p,cm):l
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan (provers $ targetLogic cid)
11584e05cc53d957ed964dfba41dd3d716f28480Gael Allioux{- [(G_prover (targetLogic cid) p, cm) |
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan cm@(Comorphism cid) <- cms,
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan p <- provers (targetLogic cid)]
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno LavitgetConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
dedea1c74ef770604ee181088cedc7bd891486baAndi EgloffgetConsCheckers = foldl addCCs []
fa9b7593e9e156060babbf3a9b06de8d6b5da5a3Laszlo Hordos where addCCs acc cm =
7e5743eba4787b2af8f31fbbb1f7d529d36196b5Chad Kienle Comorphism cid -> acc ++
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit map (\p -> (G_cons_checker (targetLogic cid) p,cm))
3032add8d51a0dcb46e076c4dc6105e78a7c9150Jake Feasel (cons_checkers $ targetLogic cid)
1965c5d21403c3d66eb1efa29c670378311b1077Paul BryanselectProver :: GetPName a =>
0fdda69ce3627d501e4bb3103765f676bb1ab061Laszlo Hordos [(a,AnyComorphism)] -> ResultT IO (a,AnyComorphism)
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno LavitselectProver [p] = return p
f2f8138695e157f9ce4a11fa2f93d7d44a36d243Laszlo HordosselectProver [] = liftR $ fatal_error "No prover available" nullRange
1965c5d21403c3d66eb1efa29c670378311b1077Paul BryanselectProver ps = do
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan sel <- lift $ listBox
87723f2895f37176408ecb9037bb77388cc5a008Andi Egloff "Choose a translation to a prover-supported logic"
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit $ map (\ (aGN,cm) -> show cm ++" ("++getPName aGN++")") ps
7586bb16914a8a62557e2e56c74a637a451fdd4eAndi Egloff i <- case sel of
5ca0e3ebbca3f4e6e71a985eaaef02346d81df44Laszlo Hordos Just j -> return j
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan _ -> liftR $ fail "Proofs.Proofs: selection"
f17bd17365d88d445f029b5859bf524ede9a92f0Andi Egloff return $ ps !! i
5ca0e3ebbca3f4e6e71a985eaaef02346d81df44Laszlo Hordoscons_check :: Logic lid sublogics
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan basic_spec sentence symb_items symb_map_items
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan sign morphism symbol raw_symbol proof_tree
44e29ab1a81842519755c5d3b9a3403efad35354Laszlo Hordos => lid -> ConsChecker sign sentence morphism proof_tree
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit -> String -> TheoryMorphism sign sentence morphism proof_tree
44e29ab1a81842519755c5d3b9a3403efad35354Laszlo Hordos -> IO([Proof_status proof_tree])
43ac19f28eaa5f298d5534a1f4ac21076399f435Phill Cunningtoncons_check _ c =
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan maybe (\ _ _ -> fail "proveGUI not implemented") id (proveGUI c)
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno LavitproveTheory :: Logic lid sublogics
43ac19f28eaa5f298d5534a1f4ac21076399f435Phill Cunnington basic_spec sentence symb_items symb_map_items
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan sign morphism symbol raw_symbol proof_tree
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan => lid -> Prover sign sentence proof_tree
8d50d56a56b1ad306c415e4fc0578a22a62ec9a0Laszlo Hordos -> String -> Theory sign sentence proof_tree
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit -> IO([Proof_status proof_tree])
ae79bf818de74e667aa5484483357212e418a68cJamie NelsonproveTheory _ p =
24c6182bad770a4a353900e875b7275789087747Jon Branch maybe (\ _ _ -> fail "proveGUI not implemented") id (proveGUI p)
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit-- | applies basic inference to a given node
37d3ea05cca877010506f556b35795e9c60ce848Andi EgloffbasicInferenceNode :: Bool -> LogicGraph -> (LIB_NAME,Node) -> LIB_NAME
24c6182bad770a4a353900e875b7275789087747Jon Branch -> GUIMVar -> LibEnv -> IO (Result LibEnv)
1965c5d21403c3d66eb1efa29c670378311b1077Paul BryanbasicInferenceNode checkCons lg (ln, node) libname guiMVar libEnv = do
4a240685d844397ddead5eff4677efe0b7e94c6cAlin Brici let dGraph = lookupDGraph libname libEnv
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit runResultT $ do
bdf1b2b1491da535d3c50421c77fc8b1255e5f0aAndi Egloff -- compute the theory of the node, and its name
61dd61caaf4be79c641be16977e53b131cd87de3Laszlo Hordos -- may contain proved theorems
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan thForProof@(G_theory lid1 sign _ axs _) <-
7586bb16914a8a62557e2e56c74a637a451fdd4eAndi Egloff liftR $ computeTheory libEnv ln node
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit ctx <- liftR
61dd61caaf4be79c641be16977e53b131cd87de3Laszlo Hordos $ maybeToMonad ("Could not find node "++show node)
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan $ fst $ match node dGraph
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan let nodeName = dgn_name $ lab' ctx
2c51c578e0f48b6ebdca554dbb46b8a6e1379fb1Andi Egloff thName = shows (getLIB_ID ln) "_"
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit ++ {-maybe (show node)-} showName nodeName
44e29ab1a81842519755c5d3b9a3403efad35354Laszlo Hordos sublogic = sublogicOfTh thForProof
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan -- select a suitable translation and prover
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan cms = findComorphismPaths lg sublogic
1db703f79695d1646222740e7229bcd35ff1e63fAndi Egloff if checkCons then do
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit (G_cons_checker lid4 cc, Comorphism cid) <-
1db703f79695d1646222740e7229bcd35ff1e63fAndi Egloff selectProver $ getConsCheckers cms
b7e0eb2a569767e809950d95f945ebf4bdcd9bf6Laszlo Hordos bTh' <- coerceBasicTheory lid1 (sourceLogic cid) ""
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan (sign, toNamedList axs)
1e74f7af8c740d5ac7ea678c3f0f53457629449dAndi Egloff -- Borrowing: translate theory
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit (sign'', sens'') <- liftR $ wrapMapTheory cid bTh'
1e74f7af8c740d5ac7ea678c3f0f53457629449dAndi Egloff let lidT = targetLogic cid
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan incl <- liftR $ inclusion lidT (empty_signature lidT) sign''
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan let mor = TheoryMorphism
c435eacb0cab04714ce858484e971fd820ea8823Chad Kienle { t_source = empty_theory lidT,
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit t_target = Theory sign'' (toThSens sens''),
c435eacb0cab04714ce858484e971fd820ea8823Chad Kienle t_morphism = incl }
d0840514601c4eea1672996b07b27ca61bd4197dLaszlo Hordos cc' <- coerceConsChecker lid4 lidT "" cc
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan lift $ cons_check lidT cc' thName mor
a441ca41891fb1107d649f936b9d6f585b581b0dBrendan Mmiller let nextHistoryElem = ([LocalInference],[])
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit -- ??? to be implemented
d0840514601c4eea1672996b07b27ca61bd4197dLaszlo Hordos newProofStatus = mkResultProofStatus libname
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan libEnv dGraph nextHistoryElem
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan return newProofStatus
48ddd46e9e22ee57a7fb400c6296f977c11173b3Elizabeth Browne else do -- proving
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit -- get known Provers
fb27c098f332a202cf0d952b5d6b14753f72d1feJake Feasel kpMap <- liftR $ knownProversGUI
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan let kpMap' = shrinkKnownProvers sublogic kpMap
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan newTh <- ResultT $
adf530d70e0ee974cd0bace4db9967617819cec1Andi Egloff proofManagementGUI lid1 proveKnownPMap
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit proveFineGrainedSelect
f9823ca3a77d02abd1efc634417380dbb820fc58Brendan Miller (getProvers cms)
0fdda69ce3627d501e4bb3103765f676bb1ab061Laszlo Hordos -- update the development graph
4cb6ef8da83ed001d8087b68aaccb6f6b6b2bc09omebold -- todo: throw out the stuff about edges
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan -- instead, mark proven things as proven in the node
71c8e2e38828e54044dbd846b73003955177072fomebold -- TODO: Reimplement stuff
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit let (_,oldContents) =
71c8e2e38828e54044dbd846b73003955177072fomebold labNode' (safeContext
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan dGraph node)
1d8e3a5de439e48eccaca022d2211f1c540f3437Chad Kienle newNodeLab = oldContents{dgn_theory = newTh}
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit (nextDGraph,changes) =
0fdda69ce3627d501e4bb3103765f676bb1ab061Laszlo Hordos updateWithOneChange (SetNodeLab (node, newNodeLab)) dGraph []
4cb6ef8da83ed001d8087b68aaccb6f6b6b2bc09omebold --adjustNode dGraph (node, newNodeLab)
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan rules = [] -- map (\s -> BasicInference (Comorphism cid)
97bef07e72834d0d06b4490ade414f0dfccd5432omebold -- (BasicProof lidT s))
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit -- FIXME: [Proof_status] not longer available
97bef07e72834d0d06b4490ade414f0dfccd5432omebold nextHistoryElem = (rules,changes)
adf530d70e0ee974cd0bace4db9967617819cec1Andi Egloff return $ mkResultProofStatus libname libEnv
1965c5d21403c3d66eb1efa29c670378311b1077Paul Bryan nextDGraph nextHistoryElem
71c8e2e38828e54044dbd846b73003955177072fomeboldproveKnownPMap :: (Logic lid sublogics1
61dd61caaf4be79c641be16977e53b131cd87de3Laszlo Hordos symb_map_items1
355e5661379644c081271b23fa8b966a098a42d2Jon Branch proof_tree1) =>
355e5661379644c081271b23fa8b966a098a42d2Jon Branch ProofGUIState lid sentence -> IO (Result (ProofGUIState lid sentence))
355e5661379644c081271b23fa8b966a098a42d2Jon BranchproveKnownPMap st =