Changeset 12745

Show
Ignore:
Timestamp:
28.10.2009 20:20:15 (3 weeks ago)
Author:
maeder
Message:

refactored consistency checkers

Location:
trunk
Files:
16 modified

Legend:

Unmodified
Added
Removed

  • trunk/CMDL/DgCommands.hs

    r12730 r12745  
    205205                th 
    206206                (shrinkKnownProvers sl kpMap) 
    207                 (getProvers ProveCMDLautomatic sl $ 
     207                (getProvers ProveCMDLautomatic (Just sl) $ 
    208208                 filter hasModelExpansion $ 
    209                  findComorphismPaths logicGraph $ 
    210                  sublogicOfTh th 
     209                 findComorphismPaths logicGraph sl 
    211210                ) 
    212211         -- all goals and axioms are selected initialy in the proof status 

  • trunk/CMDL/ProveConsistency.hs

    r12731 r12745  
    3838import Static.ComputeTheory 
    3939 
    40 import Logic.Comorphism(AnyComorphism(..), Comorphism(targetLogic)) 
    41 import Logic.Grothendieck(findComorphismPaths) 
    42 import Logic.Logic(Language(language_name), Logic(provers)) 
     40import Logic.Comorphism 
     41import Logic.Grothendieck 
     42import Logic.Logic 
    4343import qualified Logic.Prover as P 
    4444 
    … …  
    5454                               swapMVar, modifyMVar_) 
    5555 
    56 import Control.Monad(when) 
    57  
    58  
    59 getProversAutomatic :: [AnyComorphism] -> [(G_prover, AnyComorphism)] 
    60 getProversAutomatic = foldl addProvers [] 
    61  where addProvers acc cm = 
    62         case cm of 
    63          Comorphism cid -> acc ++ 
    64              foldl (\ l p -> 
    65                           if P.hasProverKind 
    66                              P.ProveCMDLautomatic p 
    67                           then (G_prover (targetLogic cid) 
    68                              p,cm):l 
    69                           else l) []  (provers $ targetLogic cid) 
    70  
     56import Control.Monad 
     57 
     58getProversAutomatic :: G_sublogics -> [(G_prover, AnyComorphism)] 
     59getProversAutomatic sl = 
     60  getProvers P.ProveCMDLautomatic (Just sl) $ findComorphismPaths logicGraph sl 
    7161 
    7262-- | Select a prover 
    73 cProver::String -> CmdlState -> 
    74                     IO CmdlState 
     63cProver::String -> CmdlState -> IO CmdlState 
    7564cProver input state = 
    7665  do 
    … …  
    8675     case elements pS of 
    8776      [] -> return $ genErrorMsg "Nothing selected" state 
    88       (Element z _):_ -> 
     77      Element z _ :_ -> let sl = sublogicOfTh $ theory z in 
    8978        -- see if any comorphism was used 
    9079       case cComorphism pS of 
    9180       -- if none use the theory  of the first selected node 
    9281       -- to find possible comorphisms 
    93        Nothing-> case find (\(y,_)-> getPName y == inp) $ 
    94                       getProversAutomatic $ findComorphismPaths logicGraph $ 
    95                       sublogicOfTh $ theory z of 
     82       Nothing-> case find (\ (y, _)-> getPName y == inp) 
     83                 $ getProversAutomatic sl of 
    9684                   Nothing -> return $ genErrorMsg ("No applicable prover with" 
    9785                                                ++" this name found") state 
    … …  
    10795       -- of provers 
    10896       Just x -> 
    109          case find (\(y,_)-> getPName y == inp) $ getProversAutomatic [x] of 
     97         case find (\ (y, _)-> getPName y == inp) 
     98         $ getProvers P.ProveCMDLautomatic (Just sl) [x] of 
    11099            Nothing -> 
    111              case find (\(y,_) -> getPName y == inp) $ getProversAutomatic $ 
    112                   findComorphismPaths logicGraph $ sublogicOfTh $ theory z of 
     100             case find (\(y,_) -> getPName y == inp) 
     101               $ getProversAutomatic sl of 
    113102               Nothing -> return $ genErrorMsg ("No applicable prover with" 
    114103                                          ++ " this name found") state 
    … …  
    156145        Nothing -> case find (\(y,_)-> 
    157146                                  getPName y == inp) $ 
    158                              getConsCheckersAutomatic $ findComorphismPaths 
     147                             getConsCheckers $ findComorphismPaths 
    159148                                logicGraph $ sublogicOfTh $ theory z of 
    160149                    Nothing -> return $ genErrorMsg ("No applicable "++ 
    … …  
    171160        Just x -> 
    172161          case find(\(y,_) -> getPName y == inp) 
    173                      $ getConsCheckersAutomatic [x] of 
     162                     $ getConsCheckers [x] of 
    174163           Nothing -> 
    175             case find (\(y,_) -> getPName y == inp)$ getConsCheckersAutomatic $ 
     164            case find (\(y,_) -> getPName y == inp) $ getConsCheckers $ 
    176165                          findComorphismPaths logicGraph $ sublogicOfTh $ 
    177166                          theory z of 
    … …  
    209198              -- proofState of the node that needs proving 
    210199              -- all theorems, goals and axioms should have 
    211               -- been selected before,but the theory should have 
    212               -- not beed recomputed 
     200              -- been selected before, but the theory should have 
     201              -- not been recomputed 
    213202              Int_NodeInfo -> 
    214203              -- node name 
    … …  
    226215              -- returns an error message if anything happens 
    227216               IO String 
    228 checkNode useTh save2File sTxt ndpf ndnm mp mcm mThr mSt mlbE libname 
     217checkNode _useTh _save2File sTxt ndpf ndnm mp mcm _mThr mSt _mlbE _libname 
    229218 = case ndpf of 
    230219    Element pf_st nd -> 
    … …  
    235224     -- compute a prover,comorphism pair to be used in preparing 
    236225     -- the theory 
    237      p_cm@(_,acm) 
    238         <-case mcm of 
    239            Nothing -> lookupKnownConsChecker st P.ProveCMDLautomatic 
     226     p_cm@(_, acm)<- case mcm of 
     227           Nothing -> lookupKnownConsChecker st 
    240228           Just cm' -> 
    241229            case mp of 
    242              Nothing-> lookupKnownConsChecker st P.ProveCMDLautomatic 
    243              Just p' -> return (p',cm') 
     230             Nothing -> lookupKnownConsChecker st 
     231             Just p' -> return (p', cm') 
    244232 
    245233     -- try to prepare the theory 
    … …  
    248236               do 
    249237                p_cm'@(prv',acm'@(Comorphism cid)) <- 
    250                           lookupKnownConsChecker st P.ProveCMDLautomatic 
     238                          lookupKnownConsChecker st 
    251239                putStrLn ("Analyzing node " ++ ndnm) 
    252240                putStrLn ("Using the comorphism " ++ language_name cid) 
    … …  
    254242                return $ case prepareForConsChecking st p_cm' of 
    255243                          Result _ Nothing -> Nothing 
    256                           Result _ (Just sm)-> Just (sm,acm') 
    257              Result _ (Just sm) -> return $ Just (sm,acm) 
     244                          Result _ (Just sm)-> Just (sm, acm') 
     245             Result _ (Just sm) -> return $ Just (sm, acm) 
    258246     case prep of 
    259247     -- theory could not be computed 
    260248      Nothing -> return "No suitable prover and comorphism found" 
    261       Just (G_theory_with_cons_checker lid1 th p, cmp)-> 
    262         case P.proveCMDLautomaticBatch p of 
    263          Nothing -> return "Error obtaining the prover" 
    264          Just fn -> 
     249      Just (G_theory_with_cons_checker _ th p, _)-> 
     250        case P.ccAutomatic p of 
     251         fn -> 
    265252          do 
    266           -- mVar to poll the prover for results 
    267           answ <- newMVar (return []) 
    268           let st' = st { proverRunning= True} 
     253          let st' = st { proverRunning = True} 
    269254          -- store initial input of the prover 
    270255          swapMVar mSt $ Just $ Element st' nd 
    271           {- putStrLn ((theoryName st)++"\n"++ 
    272                     (showDoc sign "") ++ 
    273                     show (vsep (map (print_named lid1) 
    274                                         $ P.toNamedList sens))) -} 
    275           case selectedGoals st' of 
    276            [] -> return "No goals selected. Nothing to prove" 
    277            _ -> 
    278             do 
    279              tmp <-fn useTh 
    280                       save2File 
    281                       answ 
    282                       (theoryName st) 
     256          fn (theoryName st) 
    283257                      (P.TacticScript $ show sTxt) 
    284258                      th [] 
    285              swapMVar mThr $ Just $ fst tmp 
    286              getResults lid1 cmp (snd tmp) answ mSt 
    287              swapMVar mThr Nothing 
    288              lbEnv  <- readMVar mlbE 
    289              state <- readMVar mSt 
    290              case state of 
    291               Nothing -> return [] 
    292               Just state' -> 
    293                do 
    294                 lbEnv' <- addResults lbEnv libname state' 
    295                 swapMVar mSt  Nothing 
    296                 swapMVar mlbE lbEnv' 
    297                 return [] 
    298  
     259          swapMVar mSt $ Just $ Element st nd 
     260          return "" 
    299261 
    300262-- | Given a proofstatus the function does the actual call of the 
    … …  
    377339           _ -> 
    378340            do 
    379              tmp <-fn useTh 
     341             tmp <- fn useTh 
    380342                      save2File 
    381343                      answ 
    … …  
    419381 
    420382-- | inserts the results of the proof in the development graph 
    421 addResults ::    LibEnv 
    422               -> LibName 
    423               -> Int_NodeInfo 
    424               -> IO LibEnv 
     383addResults :: LibEnv -> LibName -> Int_NodeInfo -> IO LibEnv 
    425384addResults lbEnv libname ndps = 
    426385  case ndps of 
    427    Element ps' node -> 
    428     do 
    429     -- inspired from Proofs/InferBasic.hs 
    430     -- and GUI/ProofManagement.hs 
    431     let ps'' = ps' { 
    432                     proverRunning = False } 
    433     case theory ps'' of 
     386   Element ps'' node -> case theory ps'' of 
    434387     G_theory lidT sigT indT sensT _ -> 
    435388      do 
    436        gMap <-coerceThSens (logicId ps'') lidT 
     389       gMap <- coerceThSens (logicId ps'') lidT 
    437390                  "ProveCommands last coerce" 
    438391                  (goalMap ps'') 
    … …  
    531484                                    mlbE 
    532485                                    (i_ln pS)) 
    533            when (not $ null err) (putStrLn err) 
     486           unless (null err) (putStrLn err) 
    534487           doLoop mlbE mThr mSt mOut pS l prvr 

  • trunk/CMDL/Shell.hs

    r12730 r12745  
    3636import Interfaces.GenericATPState 
    3737 
    38 import Logic.Comorphism(AnyComorphism(..), Comorphism(sourceLogic, targetLogic)) 
     38import Logic.Comorphism 
    3939import Logic.Grothendieck(findComorphismPaths) 
    40 import Logic.Prover(ProverKind(ProveCMDLautomatic), 
    41                     ProverTemplate(proverName), hasProverKind) 
    42 import Logic.Logic(Language(language_name), Logic(cons_checkers, provers)) 
    43  
    44 import Proofs.AbstractState(ProofState(logicId, theory), G_prover(..), 
    45                             G_cons_checker(..)) 
     40import Logic.Prover 
     41import Logic.Logic 
     42 
     43import Proofs.AbstractState 
    4644 
    4745import Static.DevGraph(DGNodeLab(dgn_name), isProvenSenStatus, showName) 
    … …  
    334332                 then trimRight input 
    335333                 else unwords $ init $ words input 
    336            addConsCheckers acc cm = 
    337             case cm of 
    338              Comorphism cid -> acc ++ 
    339                  foldl (\ l p -> if hasProverKind ProveCMDLautomatic p 
    340                                    then G_cons_checker (targetLogic cid) p : l 
    341                                    else l) 
    342                  [] 
    343                  (cons_checkers $ targetLogic cid) 
    344            getPName' x = case x of 
    345                           (G_cons_checker _ p) -> proverName p 
    346            getConsCheckersAutomatic' = foldl addConsCheckers [] 
    347            createConsCheckersList = map getPName' . getConsCheckersAutomatic' 
    348        case  i_state $ intState allState of 
     334           getCCName (G_cons_checker _ p) = ccName p 
     335           createConsCheckersList = map (getCCName . fst) . getConsCheckers 
     336       case i_state $ intState allState of 
    349337        Nothing -> 
    350338         -- not in proving mode !? you can not choose a consistency 
    … …  
    354342         case cComorphism proofState of 
    355343          -- some comorphism was used 
    356           Just c-> return $ map (app bC) $ filter (isPrefixOf tC) 
     344          Just c -> return $ map (app bC) $ filter (isPrefixOf tC) 
    357345                   $ createConsCheckersList [c] 
    358346          Nothing -> 
    … …  
    360348            -- no elements selected 
    361349            [] -> return [] 
    362             c:_ -> 
    363               case c of 
     350            c : _ -> case c of 
    364351               Element z _ -> return $ map (app bC) 
    365352                               $ filter (isPrefixOf tC) 
    … …  
    368355                                   (sublogicOfTh $ theory z) 
    369356   ReqProvers -> do 
    370        let tC = unwords $ tail $ words input 
    371            bC =  head $ words input 
    372            addProvers acc cm = 
    373             case cm of 
    374             Comorphism cid -> acc ++ 
    375                 foldl (\ l p -> if hasProverKind ProveCMDLautomatic p 
    376                                   then G_prover (targetLogic cid) p : l 
    377                                   else l) 
    378                 [] 
    379                 (provers $ targetLogic cid) 
    380            -- this function is identical to the one defined 
    381            -- in Proofs.InferBasic, but it is redone here 
    382            -- because InferBasic does not compile without 
    383            -- UNI_PACKAGE (so it should be moved) 
    384            getPName' (G_prover _ p) = proverName p 
    385       -- from the given comorphism generate a list of 
    386       -- provers that can be applied to theories in that 
    387       -- comorphism 
    388            getProversCMDLautomatic = foldl addProvers [] 
    389            createProverList = map getPName' . getProversCMDLautomatic 
     357       let bC : tl = words input 
     358           tC = unwords tl 
     359           createProverList = map (getProverName . fst) 
     360             . getProvers ProveCMDLautomatic Nothing 
    390361      -- find the last comorphism used if none use the 
    391362      -- the comorphism of the first selected node 
    … …  
    406377             [] -> return [] 
    407378             -- use the first element to get a comorphism 
    408              c:_ -> 
    409                case c of 
    410                 Element z _->do 
     379             c : _ -> case c of 
     380                Element z _ -> do 
    411381                              lst <- checkPresenceProvers 
    412382                                         $ createProverList 

  • trunk/Comorphisms/HetLogicGraph.hs

    r12661 r12745  
    6969                        top_gsl = toGSLPair $ top_sublogic lid 
    7070                        getPrvSL = map proverSublogic 
    71                         prv_sls = getPrvSL (provers lid) ++ 
    72                                   getPrvSL (cons_checkers lid) 
     71                        prv_sls = getPrvSL (provers lid) 
    7372                    in Map.union mp $ 
    7473                       Map.fromList (top_gsl : 

  • trunk/GUI/GtkConsistencyChecker.hs

    r12743 r12745  
    264264  forkIOWithPostProcessing 
    265265    (return $ Map.elems $ foldr 
    266                 (\ (cc,c) m -> 
     266                (\ (cc, c) m -> 
    267267                  let n = getPName cc 
    268268                      f = Map.findWithDefault (Finder n cc [] 0) n m in 
    269269                  Map.insert n (f { comorphs = c : comorphs f}) m 
    270270                ) Map.empty 
    271                 $ getConsCheckersAutomatic $ findComorphismPaths logicGraph sl) 
     271                $ getConsCheckers $ findComorphismPaths logicGraph sl) 
    272272    $ \ res -> do 
    273273      mapM_ (listStoreAppend list) res 

  • trunk/GUI/ShowLogicGraph.hs

    r12661 r12745  
    223223 
    224224             showConsChecker lid = if null (cons_checkers lid) then "None" 
    225                         else unlines $ map proverName (cons_checkers lid) 
     225                        else unlines $ map ccName (cons_checkers lid) 
    226226             showParse lid = 
    227227                   let s1 =  case parse_basic_spec lid of 
    … …  
    415415             showConsChecker li = case cons_checkers li of 
    416416                 [] -> "None" 
    417                  ls -> unlines $ map proverName ls 
     417                 ls -> unlines $ map ccName ls 
    418418             showParse li = 
    419419                   let s1 =  case parse_basic_spec li of 

  • trunk/Isabelle/IsaProve.hs

    r12661 r12745  
    4242import Data.List (isSuffixOf) 
    4343import Control.Monad 
     44import Data.Time (midnight) 
    4445 
    4546import System.Directory 
    … …  
    5758 
    5859isabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) () 
    59 isabelleConsChecker = mkProverTemplate "Isabelle-refute" () consCheck 
     60isabelleConsChecker = ConsChecker "Isabelle-refute" () consCheck 
    6061 
    6162-- | the name of the inconsistent lemma for consistency checks 
    … …  
    7071    _ -> binImpl (foldr1 binConj ts) t 
    7172 
    72 consCheck :: String -> TheoryMorphism Sign Sentence (DefaultMorphism Sign) () 
    73           -> a -> IO([ProofStatus ()]) 
    74 consCheck thName tm freedefs = case tTarget tm of 
    75     Theory sig nSens -> let (axs, _) = getAxioms $ toNamedList nSens in 
    76        isaProve (thName ++ "_c") 
     73consCheck :: String -> b 
     74  -> TheoryMorphism Sign Sentence (DefaultMorphism Sign) () -> a 
     75  -> IO (CCStatus ()) 
     76consCheck thName _tac tm freedefs = case tTarget tm of 
     77    Theory sig nSens -> do 
     78      let (axs, _) = getAxioms $ toNamedList nSens 
     79      l <- isaProve (thName ++ "_c") 
    7780           (Theory sig 
    7881               $ markAsGoal $ toThSens $ if null axs then [] else 
    … …  
    8184                     $ map (metaToTerm . metaTerm . sentence) axs ]) 
    8285           freedefs 
     86      return $ CCStatus () midnight $ case l of 
     87        [_] -> Just False -- inconsistency was proven 
     88        _ -> Nothing -- consistency cannot be recorded automatically 
    8389 
    8490prepareTheory :: Theory Sign Sentence () 
    … …  
    117123getAllProofDeps :: Map.Map String String -> String -> [String] 
    118124                -> IO([ProofStatus ()]) 
    119 getAllProofDeps m thName = mapM $ getProofDeps m thName 
     125getAllProofDeps m = mapM . getProofDeps m 
    120126 
    121127checkFinalThyFile :: (TheoryHead, Body) -> String -> IO Bool 
    … …  
    130136                  return False 
    131137              else return $ null ds 
    132     Left err -> putStrLn (show err) >> return False 
     138    Left err -> print err >> return False 
    133139 
    134140mkProved :: String -> [String] -> ProofStatus () 
    … …  
    144150    exOrig <- doesFileExist origFile 
    145151    exThyFile <- doesFileExist thyFile 
    146     if exOrig then return () else writeFile origFile thy 
    147     if exThyFile then return () else writeFile thyFile thy 
     152    unless exOrig $ writeFile origFile thy 
     153    unless exThyFile $ writeFile thyFile thy 
    148154    thy_time <- getModificationTime thyFile 
    149155    orig_time <- getModificationTime origFile 
    … …  
    174180            unless (h && null ds) $ revertThyFile thyFile thy 
    175181    Left err -> do 
    176       putStrLn $ show err 
     182      print err 
    177183      revertThyFile thyFile thy 
    178184 
    … …  
    213219          else return [] 
    214220    Left err -> do 
    215       putStrLn $ show err 
     221      print err 
    216222      putStrLn $ "Sorry, generated theory cannot be parsed, see: " ++ thyFile 
    217223      writeFile thyFile thy 

  • trunk/Logic/Prover.hs

    r12661 r12745  
    2323import Data.List 
    2424import Data.Maybe (isJust) 
    25 import Data.Time (TimeOfDay,midnight) 
     25import Data.Time (TimeOfDay, midnight) 
    2626import Data.Typeable 
    2727 
    … …  
    166166  Theory sig (mapThSensStatus (mapProofStatus f) thSens) 
    167167 
    168 -- | theory morphisms between two theories 
    169 data TheoryMorphism sign sen mor proof_tree = TheoryMorphism 
    170     { tSource :: Theory sign sen proof_tree 
    171     , tTarget :: Theory sign sen proof_tree 
    172     , tMorphism :: mor } 
    173  
    174168-- e.g. the file name, or the script itself, or a configuration string 
    175169data TacticScript = TacticScript String deriving (Eq, Ord, Show) 
    … …  
    208202openGoalStatus = Open $ Reason [] 
    209203 
    210 -- | data type representing the proof status for a goal or 
     204-- | data type representing the proof status for a goal 
    211205data ProofStatus proof_tree = ProofStatus 
    212206    { goalName :: String 
    … …  
    217211    , usedTime :: TimeOfDay 
    218212    , tacticScript :: TacticScript } 
    219     | Consistent TacticScript 
    220213    deriving (Show, Eq, Ord) 
    221214 
    … …  
    223216     make sure to set proofTree to a useful value before you access it. -} 
    224217openProofStatus :: Ord pt => String -- ^ name of the goal 
    225                  -> String -- ^ name of the prover 
    226                  -> pt -> ProofStatus pt 
     218                -> String -- ^ name of the prover 
     219                -> pt -> ProofStatus pt 
    227220openProofStatus goalname provername proof_tree = ProofStatus 
    228221   { goalName = goalname 
    … …  
    238231 
    239232isProvedStat :: ProofStatus proof_tree -> Bool 
    240 isProvedStat pst = case pst of 
    241     Consistent _ -> False 
    242     _ -> isProvedGStat . goalStatus $ pst 
     233isProvedStat = isProvedGStat . goalStatus 
    243234 
    244235isProvedGStat :: GoalStatus -> Bool 
    … …  
    290281                 -> theory  -- 6. 
    291282                 -> [FreeDefMorphism sentence morphism] 
    292                  -> IO (Concurrent.ThreadId,Concurrent.MVar ())) -- output 
     283                 -> IO (Concurrent.ThreadId, Concurrent.MVar ())) -- output 
    293284      -- input: 1. True means include proven theorems in subsequent 
    294285      --           proof attempts; 
    … …  
    321312    , proveCMDLautomaticBatch = Nothing } 
    322313 
    323 type ConsChecker sign sentence sublogics morphism proof_tree = 
    324     ProverTemplate (TheoryMorphism sign sentence morphism proof_tree) 
    325         sentence morphism sublogics proof_tree 
     314-- | theory morphisms between two theories 
     315data TheoryMorphism sign sen mor proof_tree = TheoryMorphism 
     316    { tSource :: Theory sign sen proof_tree 
     317    , tTarget :: Theory sign sen proof_tree 
     318    , tMorphism :: mor } 
     319 
     320data CCStatus proof_tree = CCStatus 
     321  { ccProofTree :: proof_tree 
     322  , ccUsedTime :: TimeOfDay 
     323  , ccResult :: Maybe Bool } 
     324 
     325data ConsChecker sign sentence sublogics morphism proof_tree = ConsChecker 
     326  { ccName :: String 
     327  , ccSublogic :: sublogics 
     328  , ccAutomatic :: String -- 1. 
     329                 -> TacticScript  -- 2. 
     330                 -> TheoryMorphism sign sentence morphism proof_tree  -- 3. 
     331                 -> [FreeDefMorphism sentence morphism]  -- 4. 
     332                 -> IO (CCStatus proof_tree) -- output 
     333      -- input: 1. theory name 
     334      --        2. default TacticScript 
     335      --        3. theory morphism 
     336      --        5. ingoing free definition morphisms 
     337      -- output: consistency result status 
     338  } deriving Typeable 
     339 

  • trunk/Makefile

    r12733 r12745  
    250250ATC/Prover.der.hs: Logic/Prover.hs $(GENRULES) 
    251251        $(GENRULECALL) -x Logic.Prover.ProverTemplate \ 
     252            -x  Logic.Prover.ConsChecker \ 
    252253            -i ATC.AS_Annotation -i ATC.OrderedMap -o $@ $< 
    253254 

  • trunk/OWL/ProvePellet.hs

    r12730 r12745  
    2727import GUI.GenericATP 
    2828import Interfaces.GenericATPState 
    29 import GUI.Utils (createTextSaveDisplay, infoDialog) 
     29import GUI.Utils (infoDialog) 
    3030 
    3131import Proofs.BatchProcessing 
    … …  
    7777pelletProverState sig oSens _ = PelletProverState 
    7878         { ontologySign = sig 
    79           ,initialState = filter isAxiom oSens } 
     79         , initialState = filter isAxiom oSens } 
    8080 
    8181{- | 
    … …  
    8787    , proveCMDLautomaticBatch = Just pelletCMDLautomaticBatch } 
    8888 
    89 pelletConsChecker :: ConsChecker Sign Axiom OWLSub 
    90                      OWLMorphism ProofTree 
    91 pelletConsChecker = (mkProverTemplate "Pellet Consistency Checker" sl_top 
    92   (\ s -> consCheck True s $ TacticScript "800")) 
    93   { proveCMDLautomatic = Just 
    94       $ \ s ts t -> fmap return . consCheck False s ts t } 
     89pelletConsChecker :: ConsChecker Sign Axiom OWLSub OWLMorphism ProofTree 
     90pelletConsChecker = ConsChecker "Pellet" sl_top consCheck 
    9591 
    9692{- | 
    … …  
    120116                  -> Named Axiom -- ^ goal to add 
    121117                  -> PelletProverState 
    122 insertOWLAxiom pps s = 
    123     pps{initialState = (initialState pps) ++ [s]} 
     118insertOWLAxiom pps s = pps { initialState = initialState pps ++ [s] } 
    124119 
    125120-- ** GUI 
    … …  
    183178-} 
    184179 
    185 spamOutput :: ProofStatus ProofTree -> IO () 
    186 spamOutput ps = 
    187     let 
    188         dName = goalName ps 
    189         dStat = goalStatus ps 
    190         dTree = proofTree ps 
    191     in 
    192       case dStat of 
    193         Open (Reason l) -> 
    194             createTextSaveDisplay "Pellet prover" ("./"++ dName ++".pellet.log") 
    195               $ unlines 
    196                 (show dTree :l) 
    197         Disproved -> createTextSaveDisplay "Pellet prover" (dName ++".pellet.owl") 
    198                 ( 
    199                  show dTree 
    200                 ) 
    201         Proved (Just True) ->     -- consistent 
    202              do --createInfoWindow "Pellet consistency check" 
    203                 --                     "This ontology is consistent." 
    204                 createTextSaveDisplay "Pellet prover" ("./"++ dName ++".pellet.log") 
    205                  ( 
    206                  -- "I found a model for the theory " ++ 
    207                  -- dName ++". :) \n" ++ 
    208                  show dTree 
    209                  ) 
    210  
    211         Proved (Just False) ->   -- not consistent 
    212              do --createInfoWindow "Pellet consistency check" 
    213                 --                     "This ontology is not consistent." 
    214                 createTextSaveDisplay "Pellet prover" ("./"++ dName ++".pellet.log") 
    215                  ( 
    216                  -- "I found a model for the theory " ++ 
    217                  -- dName ++". :) \n" ++ 
    218                  show dTree 
    219                  ) 
    220  
    221         Proved Nothing -> return ()  -- todo: another errors 
    222  
    223180getEnvSec :: String -> IO String 
    224181getEnvSec s = getEnvDef s "" 
    225182 
    226 consCheck :: Bool -> String 
     183consCheck :: String 
    227184          -> TacticScript 
    228185          -> TheoryMorphism Sign Axiom OWLMorphism ProofTree 
    229186          -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints 
    230           -> IO([ProofStatus ProofTree]) 
    231 consCheck doSpamOutput thName tac@(TacticScript tl) tm freedefs = 
     187          -> IO (CCStatus ProofTree) 
     188consCheck thName (TacticScript tl) tm freedefs = 
    232189    case tTarget tm of 
    233190      Theory sig nSens -> 
    … …  
    237194          proverStateI = pelletProverState sig 
    238195                                       (toNamedList nSens) freedefs 
    239           -- problem     = showOWLProblemA thName proverStateI [] 
    240196          problemS     = showOWLProblemS thName proverStateI [] 
    241197          simpleOptions = "consistency " 
    … …  
    243199          saveFileName  = reverse $ fst $ span (/='/') $ reverse thName 
    244200          tmpFileName   = saveFileName 
    245           pStatus out tUsed = ProofStatus 
    246             { goalName = thName 
    247             , goalStatus = Disproved 
    248             , usedAxioms = getAxioms 
    249             , usedProver = proverName pelletProver 
    250             , proofTree = ProofTree $ unlines out ++ "\n\n" ++ problemS 
    251             , usedTime = timeToTimeOfDay 
    252                 $ secondsToDiffTime $ toInteger tUsed 
    253             , tacticScript  = tac } 
     201          pStatus out tUsed = CCStatus 
     202            { ccResult = Nothing 
     203            , ccProofTree = ProofTree $ unlines out ++ "\n\n" ++ problemS 
     204            , ccUsedTime = timeToTimeOfDay 
     205                $ secondsToDiffTime $ toInteger tUsed } 
    254206          proofStatM :: ExitCode -> String ->  [String] 
    255                       -> Int -> ProofStatus ProofTree 
     207                     -> Int -> CCStatus ProofTree 
    256208          proofStatM exitCode _ out tUsed = 
    257209              case exitCode of 
    258210                ExitSuccess ->   -- consistent 
    259211                    (pStatus out tUsed) 
    260                     { goalStatus = Proved (Just True) } 
     212                    { ccResult = Just True } 
    261213                ExitFailure 1 ->   -- not consistent 
    262214                    (pStatus out tUsed) 
    263                     { goalStatus = Proved (Just False) } 
     215                    { ccResult = Just False } 
    264216                ExitFailure 2 ->   -- error by runing pellet 
    265217                    (pStatus out tUsed) 
    266                     { proofTree = ProofTree "Cannot run pellet." } 
     218                    { ccProofTree = ProofTree "Cannot run pellet." } 
    267219                ExitFailure 3 ->  -- timeout 
    268220                    (pStatus out tUsed) 
    269                     { goalStatus = openGoalStatus 
    270                     , proofTree = ProofTree $ unlines out ++ "\n\n" ++ "timeout" 
    271                         ++ unlines out 
    272                     , usedTime = timeToTimeOfDay $ secondsToDiffTime 0 } 
     221                    { ccProofTree = ProofTree $ unlines out ++ "\n\n" 
     222                                    ++ "timeout" } 
    273223                ExitFailure 4 ->   -- error by runing pellet 
    274224                    (pStatus out tUsed) 
    275                     { proofTree = ProofTree $ "Pellet returned an error.\n" 
     225                    { ccProofTree = ProofTree $ "Pellet returned an error.\n" 
    276226                        ++ unlines out } 
    277227                ExitFailure _ ->    -- another errors 
    278228                    pStatus out tUsed 
    279           getAxioms = 
    280                map senAttr $ initialState proverStateI 
    281  
    282           timeWatch :: Int 
    283                     -> IO (ProofStatus ProofTree) 
    284                     -> IO (ProofStatus ProofTree) 
     229 
     230          timeWatch :: Int -> IO (CCStatus ProofTree) -> IO (CCStatus ProofTree) 
    285231          timeWatch time process = 
    286232              do 
    … …  
    297243                  Nothing -> do 
    298244                           killThread tid1 `catch` print 
    299                            return (ProofStatus{ 
    300                                goalName = thName 
    301                              , goalStatus = openGoalStatus 
    302                              , usedAxioms = getAxioms 
    303                              , usedProver = proverName pelletProver 
    304                              , proofTree  = ProofTree ("\n\n" ++ "timeout") 
    305                              , usedTime = timeToTimeOfDay $ secondsToDiffTime 0 
    306                              , tacticScript = tac 
    307                              }) 
     245                           return $ pStatus ["timeout"] time 
    308246        in 
    309247          do 
    … …  
    336274                       return outState 
    337275                     ) 
    338                    when doSpamOutput $ spamOutput outState 
    339276                   removeFile timeTmpFile 
    340                    return [outState] 
     277                   return outState 
    341278                (b, _) -> do 
    342279                   let mess = "Pellet not " ++ 
    343280                         if b then "executable" else "found" 
    344281                   infoDialog "Pellet prover" mess 
    345                    return [(openProofStatus thName (proverName pelletProver) 
    346                            $ ProofTree mess) 
    347                            { usedAxioms = getAxioms 
    348                            , tacticScript = tac 
    349                            }] 
     282                   return $ pStatus [mess] (0 :: Int) 
    350283 
    351284check4Pellet :: IO (Bool, Bool) 

  • trunk/Proofs/AbstractState.hs

    r12661 r12745  
    2121    , coerceConsChecker 
    2222    , ProofActions (..) 
    23     , ProofState 
    24     , theoryName, theory, logicId, sublogicOfTheory, lastSublogic 
    25     , goalMap, proversMap, comorphismsToProvers, selectedGoals 
    26     , includedAxioms, includedTheorems, proverRunning, accDiags 
    27     , selectedProver, selectedConsChecker, selectedTheory 
     23    , ProofState (..) 
    2824    , initialState 
    29     , selectedGoalMap, axiomMap 
     25    , selectedGoalMap 
     26    , axiomMap 
    3027    , recalculateSublogicAndSelectedTheory 
    3128    , GetPName (..) 
    … …  
    3532    , prepareForProving 
    3633    , prepareForConsChecking 
    37     , getProvers, getConsCheckers 
     34    , getProvers 
     35    , getConsCheckers 
    3836    , lookupKnownProver 
    3937    , lookupKnownConsChecker 
    40     , getConsCheckersAutomatic 
    4138    ) where 
    4239 
    … …  
    6158import Static.GTheory 
    6259import Static.DevGraph 
    63  
    6460 
    6561-- * Provers 
    … …  
    358354 
    359355instance GetPName G_prover where 
    360     getPName (G_prover _ p) = proverName p 
     356    getPName = getProverName 
    361357 
    362358instance GetPName G_cons_checker where 
    363     getPName (G_cons_checker _ p) = proverName p 
    364  
    365  
    366 getConsCheckersAutomatic :: [AnyComorphism] -> 
    367                                 [(G_cons_checker, AnyComorphism)] 
    368 getConsCheckersAutomatic = foldl addConsCheckers [] 
    369  where addConsCheckers acc cm = 
    370         case cm of 
    371          Comorphism cid -> acc ++ 
    372             foldl (\ l p -> 
    373                          if hasProverKind 
    374                             ProveCMDLautomatic p 
    375                          then (G_cons_checker (targetLogic cid) p,cm):l 
    376                          else l) [] (cons_checkers $ targetLogic cid) 
    377  
     359    getPName (G_cons_checker _ p) = ccName p 
     360 
     361 
     362getConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)] 
     363getConsCheckers = concatMap (\ cm@(Comorphism cid) -> 
     364    map (\ cc -> (G_cons_checker (targetLogic cid) cc, cm)) 
     365      $ cons_checkers $ targetLogic cid) 
    378366 
    379367lookupKnownConsChecker :: (Logic lid sublogics1 
    … …  
    387375                            raw_symbol1 
    388376                            proof_tree1 
    389                          ,Monad m) => 
    390                          ProofState lid sentence -> ProverKind 
    391                          -> m (G_cons_checker,AnyComorphism) 
    392 lookupKnownConsChecker st _ = 
     377                         , Monad m) => 
     378                         ProofState lid sentence 
     379                         -> m (G_cons_checker, AnyComorphism) 
     380lookupKnownConsChecker st = 
    393381       let sl = sublogicOfTheory st 
    394382           mt = do 
    … …  
    397385                 return (pr_s, ps) 
    398386           matchingCC s (gp,_) = case gp of 
    399                                   G_cons_checker _ p -> proverName p == s 
     387                                  G_cons_checker _ p -> ccName p == s 
    400388           findCC (pr_n,cms) = 
    401389               case filter (matchingCC pr_n) $ getConsCheckers 
    … …  
    427415           ps <- Map.lookup pr_s (proversMap st) 
    428416           return (pr_s, ps) 
    429         matchingPr s (gp,_) = case gp of 
    430                                G_prover _ p -> proverName p == s 
     417        matchingPr s (gp, _) = case gp of 
     418          G_prover _ p -> proverName p == s 
    431419        findProver (pr_n, cms) = 
    432             case filter (matchingPr pr_n) $ getProvers pk sl 
     420            case filter (matchingPr pr_n) $ getProvers pk (Just sl) 
    433421                 $ filter (lessSublogicComor sl) cms of 
    434422               [] -> fail "Proofs.InferBasic: no prover found" 
    … …  
    438426 
    439427-- | Pairs each target prover of these comorphisms with its comorphism 
    440 getProvers :: ProverKind -> G_sublogics 
     428getProvers :: ProverKind -> Maybe G_sublogics 
    441429           -> [AnyComorphism] -> [(G_prover, AnyComorphism)] 
    442 getProvers pk (G_sublogics lid sl) = foldl addProvers [] 
    443     where addProvers acc cm = 
    444               case cm of 
    445               Comorphism cid -> let slid = sourceLogic cid in acc ++ 
    446                   foldl (\ l p -> if hasProverKind pk p 
    447                                     && language_name lid == language_name slid 
    448                                     && maybe False 
    449                                      (flip isSubElem $ proverSublogic p) 
    450                                      (mapSublogic cid 
    451                                      $ forceCoerceSublogic lid slid sl) 
    452                                      then (G_prover (targetLogic cid) p,cm):l 
    453                                      else l) 
    454                         [] 
    455                         (provers $ targetLogic cid) 
    456  
    457 getConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)] 
    458 getConsCheckers = foldl addCCs [] 
    459     where addCCs acc cm = 
    460               case cm of 
    461               Comorphism cid -> acc ++ 
    462                   map (\p -> (G_cons_checker (targetLogic cid) p,cm)) 
    463                       (cons_checkers $ targetLogic cid) 
     430getProvers pk msl = foldl addProvers [] 
     431    where addProvers acc cm = case cm of 
     432              Comorphism cid -> let 
     433                slid = sourceLogic cid 
     434                tlid = targetLogic cid 
     435                in acc ++ foldl (\ l p -> 
     436                  if hasProverKind pk p 
     437                    && case msl of 
     438                      Just (G_sublogics lid sl) -> 
     439                        language_name lid == language_name slid 
     440                         && maybe False (flip isSubElem $ proverSublogic p) 
     441                           (mapSublogic cid $ forceCoerceSublogic lid slid sl) 
     442                      Nothing -> True 
     443                  then (G_prover tlid p, cm) : l else l) 
     444                [] (provers tlid) 
    464445 
    465446-- | the list of proof statuses is integrated into the goalMap of the state 
    … …  
    484465         sign morphism symbol raw_symbol proof_tree) => 
    485466       AnyComorphism -> lid -> [ProofStatus proof_tree] 
    486     -> ThSens a (AnyComorphism,BasicProof) 
    487     -> ThSens a (AnyComorphism,BasicProof) 
     467    -> ThSens a (AnyComorphism, BasicProof) 
     468    -> ThSens a (AnyComorphism, BasicProof) 
    488469markProvedGoalMap c lid status thSens = foldl upd thSens status 
    489470    where upd m pStat = OMap.update (updStat pStat) (goalName pStat) m 

  • trunk/Proofs/InferBasic.hs

    r12661 r12745  
    143143           -> TheoryMorphism sign sentence morphism proof_tree 
    144144           -> [FreeDefMorphism sentence morphism] 
    145            -> IO (Result [ProofStatus proof_tree]) 
    146 consCheck _ = 
    147   fromMaybe (\ _ _ -> fail "proveCMDLautomatic not implemented") 
    148             . proveCMDLautomatic 
     145           -> IO (CCStatus proof_tree) 
     146consCheck _ = ccAutomatic 
    149147 
    150148proveTheory :: Logic lid sublogics 
    … …  
    195193            pts <- lift $ consCheck lidT cc' thName (TacticScript "20") mor 
    196194                $ getCFreeDefMorphs lidT libEnv ln dGraph node 
    197             liftR $ case pts of 
    198                   Result _ (Just [pt]) -> case goalStatus pt of 
    199                     Proved (Just True) -> let 
    200                       Result ds ms = extractModel cid sig1 $ proofTree pt 
    201                       in case ms of 
    202                       Nothing -> fail $ "consistent but could not reconstruct model\n" 
    203                         ++ show (proofTree pt) 
    204                       Just (sig3, sens3) -> Result ds $ Just $ 
     195            liftR $ case ccResult pts of 
     196              Just True -> let 
     197                Result ds ms = extractModel cid sig1 $ ccProofTree pts 
     198                in case ms of 
     199                Nothing -> fail $ "consistent but could not reconstruct model\n" 
     200                Just (sig3, sens3) -> Result ds $ Just $ 
    205201                         G_theory lidS (mkExtSign sig3) startSigId 
    206202                              (toThSens sens3) startThId 
    207                     st -> fail $ "prover status is: " ++ show st 
    208                   Result ds _ -> Result ds Nothing 
     203              Just False -> fail "theory is inconsistent." 
     204              Nothing -> fail "could not determine consistency." 
    209205          else do 
    210206            let freedefs = getCFreeDefMorphs lid1 libEnv ln dGraph node 
    … …  
    218214                                     recalculateSublogicAndSelectedTheory 
    219215                     } thName (hidingLabelWarning lbl) thForProof 
    220                        kpMap (getProvers ProveGUI sublogic cms) 
     216                       kpMap (getProvers ProveGUI (Just sublogic) cms) 
    221217 
    222218data ConsistencyStatus = CSUnchecked 
    … …  
    229225                 -> DGraph -> LNode DGNodeLab -> Int 
    230226                 -> IO ConsistencyStatus 
    231 consistencyCheck (G_cons_checker lid4 cc) (Comorphism cid) ln le dg (n',lbl) 
     227consistencyCheck (G_cons_checker lid4 cc) (Comorphism cid) ln le dg (n', lbl) 
    232228                 timeout = do 
    233229  let lidS = sourceLogic cid 
     230      lidT = targetLogic cid 
     231      thName = shows (getLibId ln) "_" ++ getDGNodeName lbl 
    234232      t' = timeToTimeOfDay $ secondsToDiffTime $ toInteger timeout 
    235233      ts = TacticScript $ show timeout 
    236   res <- runResultT $ do 
    237     (G_theory lid1 (ExtSign sign _) _ axs _) <- 
    238       liftR $ getGlobalTheory lbl 
    239     let thName = shows (getLibId ln) "_" ++ getDGNodeName lbl 
    240         sens = toNamedList axs 
    241         lidT = targetLogic cid 
    242     bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens) 
    243     (sig2, sens2) <- liftR $ wrapMapTheory cid bTh' 
    244     incl <- liftR $ subsig_inclusion lidT (empty_signature lidT) sig2 
    245     let mor = TheoryMorphism { tSource = emptyTheory lidT 
    246                              , tTarget = Theory sig2 $ toThSens sens2 
    247                              , tMorphism = incl } 
    248     cc' <- coerceConsChecker lid4 lidT "" cc 
    249     Result ds pts <- lift $ consCheck lidT cc' thName ts mor 
     234  case do 
     235        (G_theory lid1 (ExtSign sign _) _ axs _) <- getGlobalTheory lbl 
     236        let sens = toNamedList axs 
     237        bTh'@(sig1, _) <- coerceBasicTheory lid1 lidS "" (sign, sens) 
     238        (sig2, sens2) <- wrapMapTheory cid bTh' 
     239        incl <- subsig_inclusion lidT (empty_signature lidT) sig2 
     240        return (sig1, TheoryMorphism 
     241          { tSource = emptyTheory lidT 
     242          , tTarget = Theory sig2 $ toThSens sens2 
     243          , tMorphism = incl }) of 
     244    Result ds Nothing -> return $ CSError $ unlines $ map diagString ds 
     245    Result _ (Just (sig1, mor)) -> do 
     246      cc' <- coerceConsChecker lid4 lidT "" cc 
     247      pt <- consCheck lidT cc' thName ts mor 
    250248                $ getCFreeDefMorphs lidT le ln dg n' 
    251     case pts of 
    252       Just pts' -> return (pts', sig1) 
    253       _ -> liftR $ Result ds Nothing 
    254   case res of 
    255     Result ds Nothing -> return $ CSError $ unlines $ map diagString ds 
    256     Result _ (Just ([pt], sig1)) -> if usedTime pt >= t' then 
    257         return $ CSTimeout $ "No results within: " ++ show (usedTime pt) 
    258       else case goalStatus pt of 
    259         Proved (Just True) -> let 
    260           Result ds ms = extractModel cid sig1 $ proofTree pt 
     249      return $ case ccResult pt of 
     250        Just b -> if b then let 
     251          Result ds ms = extractModel cid sig1 $ ccProofTree pt 
    261252          in case ms of 
    262           Nothing ->  return $ CSConsistent $ unlines $ 
    263             "consistent, but could not (re-)construct a model" 
    264             : map diagString ds 
    265           Just (sig3, sens3) ->  return $ CSConsistent $ showDoc 
     253          Nothing -> CSConsistent $ unlines $ 
     254            "consistent, but could not reconstruct a model" 
     255            : map diagString ds ++ lines (show $ ccProofTree pt) 
     256          Just (sig3, sens3) -> CSConsistent $ showDoc 
    266257            (G_theory lidS (mkExtSign sig3) startSigId (toThSens sens3) 
    267258                       startThId) "" 
    268         st -> return $ CSInconsistent $ "prover status is:\n\n" ++ show st 
    269     _ -> return $ CSError "no unique cons checkers found!" 
     259          else CSInconsistent $ "prover status is:\n\n" ++ show (ccProofTree pt) 
     260        Nothing -> if ccUsedTime pt >= t' then 
     261          CSTimeout $ "No results within: " ++ show (ccUsedTime pt) 
     262          else CSError $ show (ccProofTree pt) 
    270263 
    271264proveKnownPMap :: (Logic lid sublogics1 
    … …  
    338331             if sl == lastSublogic st 
    339332               then comorphismsToProvers st 
    340                else getProvers ProveGUI sl $ 
     333               else getProvers ProveGUI (Just sl) $ 
    341334                      filter hasModelExpansion $ findComorphismPaths lg sl 
    342335       pr <- selectProver cmsToProvers 

  • trunk/Propositional/Prove.hs

    r12730 r12745  
    3434import Interfaces.GenericATPState 
    3535import GUI.GenericATP 
    36 import GUI.Utils (infoDialog) 
    3736 
    3837import Common.UniUtils as CP 
    … …  
    5049import Data.List 
    5150import Data.Maybe 
    52 import Data.Time (TimeOfDay,timeToTimeOfDay) 
     51import Data.Time (TimeOfDay, timeToTimeOfDay, midnight) 
    5352import System.Directory 
    5453import System.Cmd 
    … …  
    8382propConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL 
    8483                                  PMorphism.Morphism ProofTree 
    85 propConsChecker = LP.mkProverTemplate zchaffS top consCheck 
    86  
    87 consCheck :: String -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA 
    88              PMorphism.Morphism ProofTree 
    89           -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] 
    90           -- ^ free definitions 
    91           -> IO([LP.ProofStatus ProofTree]) 
    92 consCheck thName tm _ = 
     84propConsChecker = LP.ConsChecker zchaffS top consCheck 
     85 
     86consCheck :: String -> LP.TacticScript 
     87   -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree 
     88   -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] 
     89    -- ^ free definitions 
     90   -> IO (LP.CCStatus ProofTree) 
     91consCheck thName _ tm _ = 
    9392    case LP.tTarget tm of 
    9493      LP.Theory sig nSens -> do 
    … …  
    120119            exitCode <- system ("zchaff " ++ tmpFile ++ " >> " ++ resultFile) 
    121120            removeFile tmpFile 
    122             if exitCode /= ExitSuccess then 
    123                 infoDialog "consistency checker" 
    124                           ("error by call zchaff " ++ thName) 
     121            if exitCode /= ExitSuccess then return $ LP.CCStatus 
     122                   (ProofTree $ "error by call zchaff " ++ thName) 
     123                   midnight Nothing 
    125124               else do 
    126                    resultHf <- openFile resultFile ReadMode 
    127                    isSAT <- searchResult resultHf 
    128                    hClose resultHf 
    129                    removeFile resultFile 
    130                    if isSAT then 
    131                        infoDialog "consistency checker" 
    132                           ("consistent.") 
    133                      else 
    134                          infoDialog "consistency checker" 
    135                           ("inconsistent.") 
    136             return [] 
     125                   resultHf <- readFile resultFile 
     126                   let isSAT = searchResult resultHf 
     127                   when (length resultHf > 0) $ removeFile resultFile 
     128                   return $ LP.CCStatus (ProofTree resultHf) midnight isSAT 
    137129 
    138130    where 
    … …  
    141133        getAxioms f = map (AS_Anno.makeNamed "consistency" . AS_Anno.sentence) 
    142134          $ filter AS_Anno.isAxiom f 
    143  
    144         searchResult :: Handle -> IO Bool 
    145         searchResult hf = do 
    146             eof <- hIsEOF hf 
    147             if eof then 
    148                 return False 
    149               else 
    150                do 
    151                 line <- hGetLine hf 
    152                 putStrLn line 
    153                 if line == "RESULT:\tUNSAT" then 
    154                       return True 
    155                   else if line == "RESULT:\tSAT" then 
    156                           return False 
    157                          else searchResult hf 
     135        searchResult :: String -> Maybe Bool 
     136        searchResult hf = let ls = lines hf in 
     137          if any (== "RESULT:\tUNSAT") ls then Just True else 
     138          if any (== "RESULT:\tSAT") ls then Just False else Nothing 
    158139 
    159140-- ** GUI 

  • trunk/Propositional/ProveMinisat.hs

    r12730 r12745  
    3333import Interfaces.GenericATPState 
    3434import GUI.GenericATP 
    35 import GUI.Utils (infoDialog) 
    3635 
    3736import Common.ProofTree 
    … …  
    4342import Control.Monad (when) 
    4443import qualified Control.Concurrent as Concurrent 
    45 import Data.Time (timeToTimeOfDay) 
     44import Data.Time (timeToTimeOfDay, midnight) 
    4645import System.Directory 
    4746import System.Exit 
    … …  
    7978-} 
    8079minisatConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL 
    81                                   PMorphism.Morphism ProofTree 
    82 minisatConsChecker = LP.mkProverTemplate minisatS top consCheck 
    83  
    84 consCheck :: String -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA 
    85             PMorphism.Morphism ProofTree 
    86           -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] 
    87           -- ^ free definitions 
    88           -> IO([LP.ProofStatus ProofTree]) 
    89 consCheck thName tm _ = 
     80  PMorphism.Morphism ProofTree 
     81minisatConsChecker = LP.ConsChecker minisatS top consCheck 
     82 
     83consCheck :: String -> LP.TacticScript 
     84  -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree 
     85  -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism] 
     86  -- ^ free definitions 
     87  -> IO (LP.CCStatus ProofTree) 
     88consCheck thName _ tm _ = 
    9089    case LP.tTarget tm of 
    9190      LP.Theory sig nSens -> do 
    … …  
    118117            exitCode <- waitForProcess pid 
    119118            removeFile tmpFile 
    120             infoDialog "consistency checker" $ case exitCode of 
    121               ExitFailure 20 -> "consistent." 
    122               ExitFailure 10 -> "inconsistent." 
    123               _ -> "error by calling minisat " ++ thName 
    124             return [] 
    125  
     119            let (res, out) = case exitCode of 
     120                  ExitFailure 20 -> (Just True, "consistent.") 
     121                  ExitFailure 10 -> (Just False, "inconsistent.") 
     122                  _ -> (Nothing, "error by calling minisat " ++ thName) 
     123            return LP.CCStatus 
     124              { LP.ccResult = res 
     125              , LP.ccUsedTime = midnight 
     126              , LP.ccProofTree = ProofTree out } 
    126127    where 
    127128        getAxioms :: [LP.SenStatus AS_BASIC.FORMULA (LP.ProofStatus ProofTree)] 

  • trunk/Propositional/ProveWithTruthTable.hs

    r12730 r12745  
    3232import qualified Propositional.ProverState as PState 
    3333import qualified Propositional.Sign as Sig 
    34 import Propositional.Sublogic(PropSL,top) 
     34import Propositional.Sublogic (PropSL, top) 
    3535 
    3636import qualified Logic.Prover as LP 
    … …  
    5151import qualified Common.Result as Result 
    5252 
    53  
     53import Data.Time (midnight) 
    5454 
    5555-- * Prover implementation 
    … …  
    6464 
    6565-- display error message when signature is too large 
    66 sigTooLarge :: Int -> IO() 
    67 sigTooLarge sigSize = 
    68    infoDialog "Signature is too large" 
    69               ("Signature is too large. "++ 
    70                "It should contain < "++show maxSigSize++" symbols, "++ 
    71                "but it contains "++show sigSize++" symbols.") 
     66sigTooLarge :: Int -> String 
     67sigTooLarge sigSize = unlines 
     68  [ "Signature is too large." 
     69  , "It should contain < " ++ show maxSigSize ++ " symbols," 
     70  , "but it contains " ++ show sigSize ++ " symbols." ] 
    7271 
    7372ttHelpText :: String 
    … …  
    223222    in case map makeExtRow (rextrows r) of 
    224223       [] -> [common] 
    225        (e:extrows) -> (common++e):map (emptyPrefix ++) extrows 
     224       e : extrows -> (common ++ e) : map (emptyPrefix ++) extrows 
    226225  table = concatMap makeRow rowsTT 
    227226 
    … …  
    242241ttConsistencyChecker :: LP.ConsChecker Sig.Sign FORMULA PropSL 
    243242                                  PMorphism.Morphism ProofTree 
    244 ttConsistencyChecker = LP.mkProverTemplate ttS top consCheck 
    245  
    246 consCheck :: String -> LP.TheoryMorphism Sig.Sign FORMULA 
    247             PMorphism.Morphism ProofTree 
    248           -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism] 
    249           -- ^ free definitions 
    250           -> IO([LP.ProofStatus ProofTree]) 
    251 consCheck thName tm _freedefs = 
     243ttConsistencyChecker = LP.ConsChecker ttS top consCheck 
     244 
     245consCheck :: String -> LP.TacticScript 
     246  -> LP.TheoryMorphism Sig.Sign FORMULA PMorphism.Morphism ProofTree 
     247  -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism] 
     248    -- ^ free definitions 
     249  -> IO (LP.CCStatus ProofTree) 
     250consCheck _ _ tm _freedefs = 
    252251  case LP.tTarget tm of 
    253252    LP.Theory sig nSens -> 
    254253      let sigSize = Set.size (items sig) in 
    255       if sigSize >= maxSigSize then do 
    256         sigTooLarge sigSize 
    257         return [] 
     254      if sigSize >= maxSigSize then 
     255        return $ LP.CCStatus (ProofTree $ sigTooLarge sigSize) midnight Nothing 
    258256      else do 
    259257        let axs = filter (AS_Anno.isAxiom . snd) $ OMap.toList nSens 
    … …  
    281279                                 trows = rows 
    282280                               } 
    283             title = if isOK then "Theory is consistent" 
    284                             else "Theory is inconsistent" 
    285             legend = "Legend:\nM+ = model of the axioms\n"++ 
    286                      " - = not a model of the axioms\n" 
    287             body = legend++"\n"++render id (renderTT table) 
    288         createTextSaveDisplay title (thName++".tt") body 
    289         return [] 
    290  
     281            legend = "Legend:\nM+ = model of the axioms\n" 
     282              ++ " - = not a model of the axioms\n" 
     283            body = legend ++ "\n" ++ render id (renderTT table) 
     284        return $ LP.CCStatus (ProofTree body) midnight $ Just isOK 
    291285 
    292286-- ** prover GUI 
    … …  
    359353      sigSize = Set.size $ items sig 
    360354   in if sigSize >= maxSigSize then do 
    361         sigTooLarge sigSize 
     355        infoDialog "Signature too large" $ sigTooLarge sigSize 
    362356        return (ATPState.ATPTLimitExceeded, 
    363357                cfg{ATPState.proofStatus = defaultProofStatus nGoal}) 
    … …  
    449443  in 
    450444    if sigSize >= maxSigSize then do 
    451        return (seq (unsafePerformIO $ sigTooLarge sigSize) Nothing) 
     445       return Nothing 
    452446    else do 
    453447      let imageAxs = map (AS_Anno.mapNamed (PMorphism.mapSentenceH mor)) srcAxs 

  • trunk/SoftFOL/ProveDarwin.hs

    r12661 r12745  
    5959    , proveCMDLautomaticBatch = Just darwinCMDLautomaticBatch } 
    6060 
    61 darwinConsChecker 
    62     :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree 
    63 darwinConsChecker = (mkProverTemplate "darwin" () 
    64     (\ s -> consCheck s $ TacticScript "20")) 
    65     { proveCMDLautomatic = Just (\ s ts t -> fmap return . consCheck s ts t) } 
     61darwinConsChecker :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree 
     62darwinConsChecker = ConsChecker "darwin" () consCheck 
    6663 
    6764{- | 
    … …  
    154151          -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree 
    155152          -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints 
    156           -> IO([ProofStatus ProofTree]) 
    157 consCheck thName tac@(TacticScript tl) tm freedefs = case tTarget tm of 
     153          -> IO(CCStatus ProofTree) 
     154consCheck thName (TacticScript tl) tm freedefs = case tTarget tm of 
    158155    Theory sig nSens -> let 
    159156        saveTPTP = False 
    160157        proverStateI = spassProverState sig (toNamedList nSens) freedefs 
    161158        problem     = showTPTPProblemM thName proverStateI [] 
    162         simpleOptions = "" 
    163159        extraOptions  = "-pc true -pmtptp true -fd true -to " 
    164160                        ++ tl 
    165161        saveFileName  = reverse $ fst $ span (/= '/') $ reverse thName 
    166         runDarwinRealM :: IO([ProofStatus ProofTree]) 
     162        runDarwinRealM :: IO(CCStatus ProofTree) 
    167163        runDarwinRealM = do 
    168164            probl <- problem 
    … …  
    171167              ExitFailure _ -> do 
    172168                  infoDialog "Darwin prover" "Darwin not found" 
    173                   return [ProofStatus 
    174                     { goalName = thName 
    175                     , goalStatus = openGoalStatus 
    176                     , usedAxioms = getAxioms 
    177                     , usedProver = proverName darwinProver 
    178                     , proofTree  = ProofTree "Darwin not found" 
    179                     , usedTime = timeToTimeOfDay $ secondsToDiffTime 0 
    180                     , tacticScript  = tac }] 
     169                  return CCStatus 
     170                    { ccResult = Nothing 
     171                    , ccProofTree  = ProofTree "Darwin not found" 
     172                    , ccUsedTime = timeToTimeOfDay $ secondsToDiffTime 0 } 
    181173              ExitSuccess -> do 
    182174                  when saveTPTP $ writeFile (saveFileName ++ ".tptp") probl 
    … …  
    188180                  (_, outh, errh, proch) <- runInteractiveCommand command 
    189181                  (exCode, output, tUsed) <- parseDarwinOut outh errh proch 
    190                   let outState = proofStatM exCode simpleOptions output tUsed 
    191                   return [outState] 
    192         proofStatM :: ExitCode -> String ->  [String] -> Int 
    193                     -> ProofStatus ProofTree 
    194         proofStatM exitCode _ out tUsed = let 
    195              outState = ProofStatus 
    196                { goalName = thName 
    197                , goalStatus = Proved (Just True) 
    198                , usedAxioms = getAxioms 
    199                , usedProver = proverName darwinProver 
    200                , proofTree = ProofTree (unlines out) 
    201                , usedTime = timeToTimeOfDay $ secondsToDiffTime 
    202                             $ toInteger tUsed 
    203                , tacticScript  = tac } 
     182                  let outState = proofStatM exCode output tUsed 
     183                  return outState 
     184        proofStatM :: ExitCode -> [String] -> Int -> CCStatus ProofTree 
     185        proofStatM exitCode out tUsed = let 
     186             outState = CCStatus 
     187               { ccResult = Just True 
     188               , ccProofTree = ProofTree $ unlines $ show exitCode : out 
     189               , ccUsedTime = timeToTimeOfDay $ secondsToDiffTime 
     190                            $ toInteger tUsed } 
    204191             in case exitCode of 
    205192                  ExitSuccess -> outState 
    206193                  ExitFailure i -> outState 
    207                     { goalStatus = if elem i [2, 105, 112] 
    208                         then Open $ Reason [show exitCode] 
    209                         else Disproved } 
    210         getAxioms = let 
    211               fl = formulaLists $ initialLogicalPart proverStateI 
    212               fs = concatMap formulae $ filter isAxiomFormula fl 
    213               in map AS_Anno.senAttr fs 
     194                    { ccResult = if elem i [2, 105, 112] 
     195                        then Nothing else Just False } 
    214196        in runDarwinRealM 
    215197