Changeset 11229 for trunk/Proofs/InferBasic.hs

Timestamp:

07.01.2009 14:11:49 (14 months ago)

Author:

rpascanu

Message:

Changes to GUI to use common datatypes in Interfaces

Files:

• trunk/Proofs/InferBasic.hs (modified) (10 diffs)

trunk/Proofs/InferBasic.hs

@@ -51 +51 @@
 import GUI.Utils
 import GUI.ProofManagement
-import GUI.History(CommandHistory, addProveToHist)
+-- import GUI.History(CommandHistory, addProveToHist)
 
 import qualified Common.Lib.Graph as Tree
@@ -153 +153 @@
 basicInferenceNode :: Bool -- ^ True = CheckConsistency; False = Prove
                    -> LogicGraph -> (LIB_NAME,Node) -> LIB_NAME
-                   -> GUIMVar -> LibEnv -> CommandHistory
+                   -> GUIMVar -> LibEnv 
+                   -- -> CommandHistory
                    -> IO (Result (LibEnv, Result G_theory))
-basicInferenceNode checkCons lg (ln, node) libname guiMVar libEnv ch = do
+basicInferenceNode checkCons lg (ln, node) libname guiMVar libEnv 
+ -- ch 
+ = do
       let dGraph = lookupDGraph libname libEnv
       runResultT $ do
@@ -211 +214 @@
             newTh <- ResultT $
                    proofManagementGUI lid1 ProofActions {
-                       proveF = (proveKnownPMap lg ch freedefs),
-                       fineGrainedSelectionF = (proveFineGrainedSelect lg ch freedefs),
+                       proveF = (proveKnownPMap lg freedefs),
+                       fineGrainedSelectionF = (proveFineGrainedSelect lg  freedefs),
                        recalculateSublogicF  =
                                      recalculateSublogicAndSelectedTheory }
@@ -238 +241 @@
                    -> (LIB_NAME,Node)
                    -> GUIMVar
-                   -> CommandHistory
+                   -- -> CommandHistory
                    -> LibEnv
                    -> IO (Result (LibEnv, Result G_theory))
-basicInferenceSubTree checkCons lg (ln, node) guiMVar ch libEnv = do
+basicInferenceSubTree checkCons lg (ln, node) guiMVar libEnv = do
       let dGraph = lookupDGraph ln libEnv
       runResultT $ do
@@ -308 +311 @@
             newTh <- ResultT $
                    proofManagementGUI lid1 ProofActions {
-                       proveF = (proveKnownPMap lg ch freedefs),
-                       fineGrainedSelectionF = (proveFineGrainedSelect lg ch freedefs),
+                       proveF = (proveKnownPMap lg freedefs),
+                       fineGrainedSelectionF = (proveFineGrainedSelect lg freedefs),
                        recalculateSublogicF  =
                                      recalculateSublogicAndSelectedTheory }
@@ -340 +343 @@
                raw_symbol1
                proof_tree1) =>
-       LogicGraph -> CommandHistory
+       LogicGraph 
+       -- -> CommandHistory
     -> [FreeDefMorphism sentence morphism1]
     -> ProofState lid sentence -> IO (Result (ProofState lid sentence))
-proveKnownPMap lg ch freedefs st =
-    maybe (proveFineGrainedSelect lg ch freedefs st)
-          (callProver st ch False freedefs) $
+proveKnownPMap lg  freedefs st =
+    maybe (proveFineGrainedSelect lg freedefs st)
+          (callProver st False freedefs) $
           lookupKnownProver st ProveGUI
 
@@ -359 +363 @@
                proof_tree1) =>
        ProofState lid sentence
-    -> CommandHistory -> Bool -- indicates if a translation was chosen
+    -- -> CommandHistory 
+    -> Bool -- indicates if a translation was chosen
     -> [FreeDefMorphism sentence morphism1]
     -> (G_prover,AnyComorphism) -> IO (Result (ProofState lid sentence))
-callProver st ch trans_chosen freedefs p_cm@(_,acm) =
+callProver st trans_chosen freedefs p_cm@(_,acm) =
        runResultT $ do
         G_theory_with_prover lid th p <- liftR $ prepareForProving st p_cm
@@ -372 +377 @@
         -- lift $ putStrLn $ show ps
         let st' = markProved acm lid ps st
-        lift $ addProveToHist ch st'
-            (if trans_chosen then Just p_cm else Nothing) ps
+--        lift $ addProveToHist ch st'
+--            (if trans_chosen then Just p_cm else Nothing) ps
         return st'
 
@@ -387 +392 @@
                raw_symbol1
                proof_tree1) =>
-       LogicGraph -> CommandHistory
+       LogicGraph -- -> CommandHistory
     -> [FreeDefMorphism sentence morphism1]
     -> ProofState lid sentence -> IO (Result (ProofState lid sentence))
-proveFineGrainedSelect lg ch freedefs st =
+proveFineGrainedSelect lg freedefs st =
     runResultT $ do
        let sl = sublogicOfTheory st
@@ -400 +405 @@
        pr <- selectProver cmsToProvers
        ResultT $ callProver st{lastSublogic = sublogicOfTheory st,
-                               comorphismsToProvers = cmsToProvers} ch True freedefs pr
+                               comorphismsToProvers = cmsToProvers} True freedefs pr