{-# LANGUAGE FlexibleInstances #-}
{- |
Module      :  ./CASL/QuickCheck.hs
Description :  QuickCheck model checker for CASL.CFOL
Copyright   :  (c) Till Mossakowski, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via GUI imports, FlexibleInstances)

QuickCheck model checker for CASL.CFOL.
Initially, only finite enumeration domains are supported
-}

module CASL.QuickCheck (quickCheckProver) where

import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Result as Result

import CASL.AS_Basic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.Morphism
import CASL.Quantification
import CASL.ToDoc
import CASL.SimplifySen

import Logic.Prover

import Common.DocUtils
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Utils (timeoutSecs)

import qualified Data.Map as Map
import Data.Maybe
import Data.List

import Control.Monad
import Control.Concurrent
import qualified Control.Monad.Fail as Fail

import GUI.GenericATP

import Interfaces.GenericATPState

import Proofs.BatchProcessing

-- a qmodel is a certain term model used by QuickCheck
data QModel = QModel
        { QModel -> CASLSign
sign :: CASLSign
        -- sentences determining the set of terms for a sort
        , QModel -> Map SORT [CASLFORMULA]
carrierSens :: Map.Map SORT [CASLFORMULA]
        -- definitions of predicates and operations
        , QModel -> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
predDefs :: Map.Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
        , QModel -> Map OP_SYMB [([CASLTERM], CASLTERM)]
opDefs :: Map.Map OP_SYMB [([CASLTERM], CASLTERM)]
        -- currently evaluated items, for avoiding infinite recursion
        , QModel -> [(PRED_SYMB, [CASLTERM])]
evaluatedPreds :: [(PRED_SYMB, [CASLTERM])]
        , QModel -> [(OP_SYMB, [CASLTERM])]
evaluatedOps :: [(OP_SYMB, [CASLTERM])]
        } deriving Int -> QModel -> ShowS
[QModel] -> ShowS
QModel -> String
(Int -> QModel -> ShowS)
-> (QModel -> String) -> ([QModel] -> ShowS) -> Show QModel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QModel] -> ShowS
$cshowList :: [QModel] -> ShowS
show :: QModel -> String
$cshow :: QModel -> String
showsPrec :: Int -> QModel -> ShowS
$cshowsPrec :: Int -> QModel -> ShowS
Show

{- |
  Run the QuickCheck service.
-}
runQuickCheck :: QModel
           {- ^ logical part containing the input Sign and axioms and possibly
           goals that have been proved earlier as additional axioms -}
           -> GenericConfig ProofTree -- ^ configuration to use
           -> Bool -- ^ True means save theory file
           -> String -- ^ name of the theory in the DevGraph
           -> AS_Anno.Named CASLFORMULA -- ^ goal to prove
           -> IO (ATPRetval, GenericConfig ProofTree)
           -- ^ (retval, configuration with proof status and complete output)
runQuickCheck :: QModel
-> GenericConfig ProofTree
-> Bool
-> String
-> Named CASLFORMULA
-> IO (ATPRetval, GenericConfig ProofTree)
runQuickCheck qm :: QModel
qm cfg :: GenericConfig ProofTree
cfg _saveFile :: Bool
_saveFile _thName :: String
_thName nGoal :: Named CASLFORMULA
nGoal = do
  (stat :: ATPRetval
stat, Result d :: [Diagnosis]
d res :: Maybe Bool
res) <- case GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig ProofTree
cfg of
    Nothing -> (ATPRetval, Result Bool) -> IO (ATPRetval, Result Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPSuccess, QModel -> Named CASLFORMULA -> Result Bool
quickCheck QModel
qm Named CASLFORMULA
nGoal)
    Just t :: Int
t -> do
      Maybe (Result Bool)
mRes <- Int -> IO (Result Bool) -> IO (Maybe (Result Bool))
forall a. Int -> IO a -> IO (Maybe a)
timeoutSecs Int
t (IO (Result Bool) -> IO (Maybe (Result Bool)))
-> IO (Result Bool) -> IO (Maybe (Result Bool))
forall a b. (a -> b) -> a -> b
$ Result Bool -> IO (Result Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Bool -> IO (Result Bool))
-> Result Bool -> IO (Result Bool)
forall a b. (a -> b) -> a -> b
$ QModel -> Named CASLFORMULA -> Result Bool
quickCheck QModel
qm Named CASLFORMULA
nGoal
      (ATPRetval, Result Bool) -> IO (ATPRetval, Result Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATPRetval, Result Bool) -> IO (ATPRetval, Result Bool))
-> (ATPRetval, Result Bool) -> IO (ATPRetval, Result Bool)
forall a b. (a -> b) -> a -> b
$ (ATPRetval, Result Bool)
-> (Result Bool -> (ATPRetval, Result Bool))
-> Maybe (Result Bool)
-> (ATPRetval, Result Bool)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ATPRetval
ATPTLimitExceeded, String -> Result Bool
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "time limit exceeded")
                     (\ x :: Result Bool
x -> (ATPRetval
ATPSuccess, Result Bool
x)) Maybe (Result Bool)
mRes
  let fstr :: String
fstr = Doc -> String
forall a. Show a => a -> String
show (Named CASLFORMULA -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula (Named CASLFORMULA -> Doc) -> Named CASLFORMULA -> Doc
forall a b. (a -> b) -> a -> b
$ (CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed
                       (CASLSign -> CASLFORMULA -> CASLFORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen (CASLSign -> CASLFORMULA -> CASLFORMULA)
-> CASLSign -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ QModel -> CASLSign
sign QModel
qm) Named CASLFORMULA
nGoal)
      showDiagStrings :: [Diagnosis] -> String
showDiagStrings = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String)
-> ([Diagnosis] -> [String]) -> [Diagnosis] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Diagnosis -> String) -> [Diagnosis] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> String
diagString -- no final newline
      diagstr :: String
diagstr = case (Maybe Bool
res, [Diagnosis]
d) of
        (Just True, _) -> [Diagnosis] -> String
showDiagStrings (Int -> [Diagnosis] -> [Diagnosis]
forall a. Int -> [a] -> [a]
take 10 [Diagnosis]
d)
        (_, []) -> ""
        _ -> [String] -> String
unlines ["Formula failed: ", String
fstr, " some Counterexamples: "]
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Diagnosis] -> String
showDiagStrings (Int -> [Diagnosis] -> [Diagnosis]
forall a. Int -> [a] -> [a]
take 10 [Diagnosis]
d)
      gstat :: GoalStatus
gstat = case Maybe Bool
res of
        Just True -> Bool -> GoalStatus
Proved Bool
True
        Just False -> GoalStatus
Disproved
        Nothing -> GoalStatus
openGoalStatus
      setStatus :: ProofStatus proof_tree -> ProofStatus ProofTree
setStatus pstat :: ProofStatus proof_tree
pstat = ProofStatus proof_tree
pstat { goalStatus :: GoalStatus
goalStatus = GoalStatus
gstat
                              , usedProver :: String
usedProver = "QuickCheck"
                              , proofTree :: ProofTree
proofTree = String -> ProofTree
ProofTree String
diagstr }
      cfg' :: GenericConfig ProofTree
cfg' = GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree -> ProofStatus ProofTree
forall proof_tree. ProofStatus proof_tree -> ProofStatus ProofTree
setStatus (GenericConfig ProofTree -> ProofStatus ProofTree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig ProofTree
cfg)
                 , resultOutput :: [String]
resultOutput = [String
diagstr] }
  (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
stat, GenericConfig ProofTree
cfg')
  -- return ATPError if time is up???

-- * QModels

-- | initial QModel
makeQm :: CASLSign -> QModel
makeQm :: CASLSign -> QModel
makeQm sig :: CASLSign
sig = QModel :: CASLSign
-> Map SORT [CASLFORMULA]
-> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
-> Map OP_SYMB [([CASLTERM], CASLTERM)]
-> [(PRED_SYMB, [CASLTERM])]
-> [(OP_SYMB, [CASLTERM])]
-> QModel
QModel { sign :: CASLSign
sign = CASLSign
sig
                    , carrierSens :: Map SORT [CASLFORMULA]
carrierSens = Map SORT [CASLFORMULA]
forall k a. Map k a
Map.empty
                    , predDefs :: Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
predDefs = Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
forall k a. Map k a
Map.empty
                    , opDefs :: Map OP_SYMB [([CASLTERM], CASLTERM)]
opDefs = Map OP_SYMB [([CASLTERM], CASLTERM)]
forall k a. Map k a
Map.empty
                    , evaluatedPreds :: [(PRED_SYMB, [CASLTERM])]
evaluatedPreds = []
                    , evaluatedOps :: [(OP_SYMB, [CASLTERM])]
evaluatedOps = []
                    }

insertSens :: QModel -> [AS_Anno.Named CASLFORMULA] -> QModel
insertSens :: QModel -> [Named CASLFORMULA] -> QModel
insertSens = (QModel -> Named CASLFORMULA -> QModel)
-> QModel -> [Named CASLFORMULA] -> QModel
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl QModel -> Named CASLFORMULA -> QModel
insertSen

-- | insert sentences into a QModel
insertSen :: QModel -> AS_Anno.Named CASLFORMULA -> QModel
insertSen :: QModel -> Named CASLFORMULA -> QModel
insertSen qm :: QModel
qm sen :: Named CASLFORMULA
sen = if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom Named CASLFORMULA
sen then QModel
qm else
  let f :: CASLFORMULA
f = Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence Named CASLFORMULA
sen
      qm1 :: QModel
qm1 = case CASLFORMULA
f of
               -- sort generation constraint?
               Sort_gen_ax cs :: [Constraint]
cs _ ->
                 let s :: [(SORT, [CASLFORMULA])]
s = (Constraint -> (SORT, [CASLFORMULA]))
-> [Constraint] -> [(SORT, [CASLFORMULA])]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Constraint
c -> (Constraint -> SORT
newSort Constraint
c, [CASLFORMULA
f])) [Constraint]
cs
                     ins :: Map SORT [a] -> [(SORT, [a])] -> Map SORT [a]
ins = ((SORT, [a]) -> Map SORT [a] -> Map SORT [a])
-> Map SORT [a] -> [(SORT, [a])] -> Map SORT [a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((SORT, [a]) -> Map SORT [a] -> Map SORT [a])
 -> Map SORT [a] -> [(SORT, [a])] -> Map SORT [a])
-> ((SORT, [a]) -> Map SORT [a] -> Map SORT [a])
-> Map SORT [a]
-> [(SORT, [a])]
-> Map SORT [a]
forall a b. (a -> b) -> a -> b
$ (SORT -> [a] -> Map SORT [a] -> Map SORT [a])
-> (SORT, [a]) -> Map SORT [a] -> Map SORT [a]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((SORT -> [a] -> Map SORT [a] -> Map SORT [a])
 -> (SORT, [a]) -> Map SORT [a] -> Map SORT [a])
-> (SORT -> [a] -> Map SORT [a] -> Map SORT [a])
-> (SORT, [a])
-> Map SORT [a]
-> Map SORT [a]
forall a b. (a -> b) -> a -> b
$ ([a] -> [a] -> [a]) -> SORT -> [a] -> Map SORT [a] -> Map SORT [a]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)
                  in QModel
qm { carrierSens :: Map SORT [CASLFORMULA]
carrierSens = Map SORT [CASLFORMULA]
-> [(SORT, [CASLFORMULA])] -> Map SORT [CASLFORMULA]
forall a. Map SORT [a] -> [(SORT, [a])] -> Map SORT [a]
ins (QModel -> Map SORT [CASLFORMULA]
carrierSens QModel
qm) [(SORT, [CASLFORMULA])]
s }
               -- axiom forcing empty carrier?
               Quantification Universal [Var_decl [_] s :: SORT
s _] (Atom False _) _ ->
                 QModel
qm { carrierSens :: Map SORT [CASLFORMULA]
carrierSens = ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA])
-> SORT
-> [CASLFORMULA]
-> Map SORT [CASLFORMULA]
-> Map SORT [CASLFORMULA]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) SORT
s [CASLFORMULA
f] (QModel -> Map SORT [CASLFORMULA]
carrierSens QModel
qm) }
               _ -> QModel
qm
      insertPred :: PRED_SYMB -> [CASLTERM] -> CASLFORMULA -> QModel -> QModel
insertPred p :: PRED_SYMB
p args :: [CASLTERM]
args body :: CASLFORMULA
body q :: QModel
q =
        QModel
q { predDefs :: Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
predDefs = ([([CASLTERM], CASLFORMULA)]
 -> [([CASLTERM], CASLFORMULA)] -> [([CASLTERM], CASLFORMULA)])
-> PRED_SYMB
-> [([CASLTERM], CASLFORMULA)]
-> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
-> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [([CASLTERM], CASLFORMULA)]
-> [([CASLTERM], CASLFORMULA)] -> [([CASLTERM], CASLFORMULA)]
forall a. [a] -> [a] -> [a]
(++) PRED_SYMB
p [([CASLTERM]
args, CASLFORMULA
body)] (QModel -> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
predDefs QModel
q)}
      insertOp :: OP_SYMB -> [CASLTERM] -> CASLTERM -> QModel -> QModel
insertOp op :: OP_SYMB
op args :: [CASLTERM]
args body :: CASLTERM
body q :: QModel
q =
        QModel
q { opDefs :: Map OP_SYMB [([CASLTERM], CASLTERM)]
opDefs = ([([CASLTERM], CASLTERM)]
 -> [([CASLTERM], CASLTERM)] -> [([CASLTERM], CASLTERM)])
-> OP_SYMB
-> [([CASLTERM], CASLTERM)]
-> Map OP_SYMB [([CASLTERM], CASLTERM)]
-> Map OP_SYMB [([CASLTERM], CASLTERM)]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [([CASLTERM], CASLTERM)]
-> [([CASLTERM], CASLTERM)] -> [([CASLTERM], CASLTERM)]
forall a. [a] -> [a] -> [a]
(++) OP_SYMB
op [([CASLTERM]
args, CASLTERM
body)] (QModel -> Map OP_SYMB [([CASLTERM], CASLTERM)]
opDefs QModel
q) }
  in case CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
stripAllQuant CASLFORMULA
f of
  -- insert a predicate or operation definition into a QModel
   Predication predsymb :: PRED_SYMB
predsymb args :: [CASLTERM]
args _ ->
     PRED_SYMB -> [CASLTERM] -> CASLFORMULA -> QModel -> QModel
insertPred PRED_SYMB
predsymb [CASLTERM]
args CASLFORMULA
forall f. FORMULA f
trueForm QModel
qm1
   Negation (Predication predsymb :: PRED_SYMB
predsymb args :: [CASLTERM]
args _) _ ->
     PRED_SYMB -> [CASLTERM] -> CASLFORMULA -> QModel -> QModel
insertPred PRED_SYMB
predsymb [CASLTERM]
args CASLFORMULA
forall f. FORMULA f
falseForm QModel
qm1
   Relation (Predication predsymb :: PRED_SYMB
predsymb args :: [CASLTERM]
args _) Equivalence body :: CASLFORMULA
body _ ->
     PRED_SYMB -> [CASLTERM] -> CASLFORMULA -> QModel -> QModel
insertPred PRED_SYMB
predsymb [CASLTERM]
args CASLFORMULA
body QModel
qm1
   Equation (Application opsymb :: OP_SYMB
opsymb args :: [CASLTERM]
args _) _ body :: CASLTERM
body _ ->
     OP_SYMB -> [CASLTERM] -> CASLTERM -> QModel -> QModel
insertOp OP_SYMB
opsymb [CASLTERM]
args CASLTERM
body QModel
qm1
   {- treat equality as special predicate symbol, for detecting inequalities
   also exploit that inequality is symmetric -}
   Negation (Equation t1 :: CASLTERM
t1 _ t2 :: CASLTERM
t2 _) _ ->
     PRED_SYMB -> [CASLTERM] -> CASLFORMULA -> QModel -> QModel
insertPred PRED_SYMB
eqSymb [CASLTERM
t1, CASLTERM
t2] CASLFORMULA
forall f. FORMULA f
falseForm (QModel -> QModel) -> QModel -> QModel
forall a b. (a -> b) -> a -> b
$
       PRED_SYMB -> [CASLTERM] -> CASLFORMULA -> QModel -> QModel
insertPred PRED_SYMB
eqSymb [CASLTERM
t2, CASLTERM
t1] CASLFORMULA
forall f. FORMULA f
falseForm QModel
qm1
   _ -> QModel
qm1

-- | predicate symbol for equality (with dummy type)
eqSymb :: PRED_SYMB
eqSymb :: PRED_SYMB
eqSymb = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
eqId ([SORT] -> Range -> PRED_TYPE
Pred_type [] Range
nullRange)

-- * Variable assignments

data VariableAssignment = VariableAssignment QModel [(VAR, CASLTERM)]

instance Show VariableAssignment where
  show :: VariableAssignment -> String
show (VariableAssignment qm :: QModel
qm assignList :: [(VAR, CASLTERM)]
assignList) = QModel -> [(VAR, CASLTERM)] -> String
showAssignments QModel
qm [(VAR, CASLTERM)]
assignList

showAssignments :: QModel -> [(VAR, CASLTERM)] -> String
showAssignments :: QModel -> [(VAR, CASLTERM)] -> String
showAssignments qm :: QModel
qm xs :: [(VAR, CASLTERM)]
xs =
  '[' Char -> ShowS
forall a. a -> [a] -> [a]
: String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " (((VAR, CASLTERM) -> String) -> [(VAR, CASLTERM)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (QModel -> (VAR, CASLTERM) -> String
showSingleAssignment QModel
qm) [(VAR, CASLTERM)]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"

showSingleAssignment :: QModel -> (VAR, CASLTERM) -> String
showSingleAssignment :: QModel -> (VAR, CASLTERM) -> String
showSingleAssignment qm :: QModel
qm (v :: VAR
v, t :: CASLTERM
t) =
  VAR -> String
forall a. Show a => a -> String
show VAR
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ "->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLTERM -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (Min () ()
-> (CASLSign -> () -> ()) -> CASLSign -> CASLTERM -> CASLTERM
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT ((() -> Result ()) -> Min () ()
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return) ((() -> ()) -> CASLSign -> () -> ()
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) (QModel -> CASLSign
sign QModel
qm) CASLTERM
t) ""

emptyAssignment :: QModel -> VariableAssignment
emptyAssignment :: QModel -> VariableAssignment
emptyAssignment qm :: QModel
qm = QModel -> [(VAR, CASLTERM)] -> VariableAssignment
VariableAssignment QModel
qm []

insertAssignment :: VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment
insertAssignment :: VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment
insertAssignment (VariableAssignment qm :: QModel
qm ass :: [(VAR, CASLTERM)]
ass) (v :: VAR
v, t :: CASLTERM
t) =
  QModel -> [(VAR, CASLTERM)] -> VariableAssignment
VariableAssignment QModel
qm ((VAR
v, CASLTERM
t) (VAR, CASLTERM) -> [(VAR, CASLTERM)] -> [(VAR, CASLTERM)]
forall a. a -> [a] -> [a]
: [(VAR, CASLTERM)]
ass)

concatAssignment :: VariableAssignment -> VariableAssignment
                 -> VariableAssignment
concatAssignment :: VariableAssignment -> VariableAssignment -> VariableAssignment
concatAssignment (VariableAssignment qm :: QModel
qm l1 :: [(VAR, CASLTERM)]
l1) (VariableAssignment _ l2 :: [(VAR, CASLTERM)]
l2) =
  QModel -> [(VAR, CASLTERM)] -> VariableAssignment
VariableAssignment QModel
qm ([(VAR, CASLTERM)] -> VariableAssignment)
-> [(VAR, CASLTERM)] -> VariableAssignment
forall a b. (a -> b) -> a -> b
$ [(VAR, CASLTERM)]
l1 [(VAR, CASLTERM)] -> [(VAR, CASLTERM)] -> [(VAR, CASLTERM)]
forall a. [a] -> [a] -> [a]
++ [(VAR, CASLTERM)]
l2

-- * The quickcheck model checker

quickCheck :: QModel -> AS_Anno.Named CASLFORMULA -> Result Bool
quickCheck :: QModel -> Named CASLFORMULA -> Result Bool
quickCheck qm :: QModel
qm =
  Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
True QModel
qm (QModel -> VariableAssignment
emptyAssignment QModel
qm) (CASLFORMULA -> Result Bool)
-> (Named CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA
-> Result Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence

calculateTerm :: QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm :: QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm qm :: QModel
qm ass :: VariableAssignment
ass trm :: CASLTERM
trm = case CASLTERM
trm of
    Qual_var var :: VAR
var _ _ -> VAR -> VariableAssignment -> Result CASLTERM
lookupVar VAR
var VariableAssignment
ass
    Application opSymb :: OP_SYMB
opSymb terms :: [CASLTERM]
terms _ ->
              QModel
-> VariableAssignment -> OP_SYMB -> [CASLTERM] -> Result CASLTERM
applyOperation QModel
qm VariableAssignment
ass OP_SYMB
opSymb [CASLTERM]
terms
    Sorted_term term :: CASLTERM
term _ _ -> QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm VariableAssignment
ass CASLTERM
term
    Conditional t1 :: CASLTERM
t1 fo :: CASLFORMULA
fo t2 :: CASLTERM
t2 _ -> do
              Bool
res <- Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
ass CASLFORMULA
fo
              QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm VariableAssignment
ass (CASLTERM -> Result CASLTERM) -> CASLTERM -> Result CASLTERM
forall a b. (a -> b) -> a -> b
$ if Bool
res then CASLTERM
t1 else CASLTERM
t2
    _ -> String -> Result CASLTERM
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result CASLTERM) -> String -> Result CASLTERM
forall a b. (a -> b) -> a -> b
$ "QuickCheck.calculateTerm: unsupported: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLTERM -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CASLTERM
trm ""

lookupVar :: VAR -> VariableAssignment -> Result CASLTERM
lookupVar :: VAR -> VariableAssignment -> Result CASLTERM
lookupVar v :: VAR
v (VariableAssignment _ ass :: [(VAR, CASLTERM)]
ass) = case VAR -> [(VAR, CASLTERM)] -> Maybe CASLTERM
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VAR
v [(VAR, CASLTERM)]
ass of
  Nothing -> String -> Result CASLTERM
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("no value for variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VAR -> String
forall a. Show a => a -> String
show VAR
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ " found")
  Just val :: CASLTERM
val -> CASLTERM -> Result CASLTERM
forall (m :: * -> *) a. Monad m => a -> m a
return CASLTERM
val

applyOperation :: QModel -> VariableAssignment -> OP_SYMB -> [CASLTERM]
               -> Result CASLTERM
applyOperation :: QModel
-> VariableAssignment -> OP_SYMB -> [CASLTERM] -> Result CASLTERM
applyOperation qm :: QModel
qm ass :: VariableAssignment
ass opsymb :: OP_SYMB
opsymb terms :: [CASLTERM]
terms = do
  -- block infinite recursion
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((OP_SYMB
opsymb, [CASLTERM]
terms) (OP_SYMB, [CASLTERM]) -> [(OP_SYMB, [CASLTERM])] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` QModel -> [(OP_SYMB, [CASLTERM])]
evaluatedOps QModel
qm)
       (String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("infinite recursion when calculating"
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLTERM -> String
forall a. Show a => a -> String
show (OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
opsymb [CASLTERM]
terms)))
  let qm' :: QModel
qm' = QModel
qm { evaluatedOps :: [(OP_SYMB, [CASLTERM])]
evaluatedOps = (OP_SYMB
opsymb, [CASLTERM]
terms) (OP_SYMB, [CASLTERM])
-> [(OP_SYMB, [CASLTERM])] -> [(OP_SYMB, [CASLTERM])]
forall a. a -> [a] -> [a]
: QModel -> [(OP_SYMB, [CASLTERM])]
evaluatedOps QModel
qm }
  -- evaluate argument terms
  [CASLTERM]
args <- (CASLTERM -> Result CASLTERM) -> [CASLTERM] -> Result [CASLTERM]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm' VariableAssignment
ass) [CASLTERM]
terms
  -- find appropriate operation definition
  case OP_SYMB
-> Map OP_SYMB [([CASLTERM], CASLTERM)]
-> Maybe [([CASLTERM], CASLTERM)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OP_SYMB
opsymb (QModel -> Map OP_SYMB [([CASLTERM], CASLTERM)]
opDefs QModel
qm) of
    Nothing ->
      -- no operation definition? Then return unevaluated term
      CASLTERM -> Result CASLTERM
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
opsymb [CASLTERM]
terms)
    Just bodies :: [([CASLTERM], CASLTERM)]
bodies -> do
      -- bind formal to actual arguments
      (body :: CASLTERM
body, m :: [(VAR, CASLTERM)]
m) <- [([CASLTERM], CASLTERM)]
-> [CASLTERM] -> String -> Result (CASLTERM, [(VAR, CASLTERM)])
forall a.
[([CASLTERM], a)]
-> [CASLTERM] -> String -> Result (a, [(VAR, CASLTERM)])
match [([CASLTERM], CASLTERM)]
bodies [CASLTERM]
args (String -> Result (CASLTERM, [(VAR, CASLTERM)]))
-> String -> Result (CASLTERM, [(VAR, CASLTERM)])
forall a b. (a -> b) -> a -> b
$
                   CASLTERM -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
opsymb [CASLTERM]
args) ""
      let ass' :: VariableAssignment
ass' = (VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment)
-> VariableAssignment -> [(VAR, CASLTERM)] -> VariableAssignment
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment
insertAssignment VariableAssignment
ass [(VAR, CASLTERM)]
m
      -- evaluate body of operation definition
      QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm' VariableAssignment
ass' CASLTERM
body

{- | match a list of arguments (second parameter) against a
a a list of bodies (first argument), each coming with a
list of formal parameters and a body term or formula -}
match :: [([CASLTERM], a)] -> [CASLTERM] -> String
      -> Result (a, [(VAR, CASLTERM)])
match :: [([CASLTERM], a)]
-> [CASLTERM] -> String -> Result (a, [(VAR, CASLTERM)])
match bodies :: [([CASLTERM], a)]
bodies args :: [CASLTERM]
args msg :: String
msg =
  case (([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)]))
-> [([CASLTERM], a)] -> [(a, [(VAR, CASLTERM)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([CASLTERM] -> ([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)])
forall a.
[CASLTERM] -> ([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)])
match1 [CASLTERM]
args) [([CASLTERM], a)]
bodies of
    [] -> String -> Result (a, [(VAR, CASLTERM)])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("no matching found for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg)
    subst :: (a, [(VAR, CASLTERM)])
subst : _ -> (a, [(VAR, CASLTERM)]) -> Result (a, [(VAR, CASLTERM)])
forall (m :: * -> *) a. Monad m => a -> m a
return (a, [(VAR, CASLTERM)])
subst

-- match against a single body
match1 :: [CASLTERM] -> ([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)])
match1 :: [CASLTERM] -> ([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)])
match1 args :: [CASLTERM]
args (vars :: [CASLTERM]
vars, body :: a
body) = do
  [(VAR, CASLTERM)]
subst <- ([[(VAR, CASLTERM)]] -> [(VAR, CASLTERM)])
-> Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(VAR, CASLTERM)]] -> [(VAR, CASLTERM)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)])
-> Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)]
forall a b. (a -> b) -> a -> b
$ (CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)])
-> [CASLTERM] -> [CASLTERM] -> Maybe [[(VAR, CASLTERM)]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 [CASLTERM]
vars [CASLTERM]
args
  if [(VAR, CASLTERM)] -> Bool
consistent [(VAR, CASLTERM)]
subst then (a, [(VAR, CASLTERM)]) -> Maybe (a, [(VAR, CASLTERM)])
forall (m :: * -> *) a. Monad m => a -> m a
return (a
body, [(VAR, CASLTERM)]
subst) else Maybe (a, [(VAR, CASLTERM)])
forall a. Maybe a
Nothing

match2 :: CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 :: CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 (Qual_var v :: VAR
v _ _) t :: CASLTERM
t = [(VAR, CASLTERM)] -> Maybe [(VAR, CASLTERM)]
forall a. a -> Maybe a
Just [(VAR
v, CASLTERM
t)]
match2 (Application opsymb1 :: OP_SYMB
opsymb1 terms1 :: [CASLTERM]
terms1 _) (Application opsymb2 :: OP_SYMB
opsymb2 terms2 :: [CASLTERM]
terms2 _) =
   -- direct match of operation symbols?
   if OP_SYMB
opsymb1 OP_SYMB -> OP_SYMB -> Bool
forall a. Eq a => a -> a -> Bool
== OP_SYMB
opsymb2 then
     ([[(VAR, CASLTERM)]] -> [(VAR, CASLTERM)])
-> Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(VAR, CASLTERM)]] -> [(VAR, CASLTERM)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)])
-> Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)]
forall a b. (a -> b) -> a -> b
$ (CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)])
-> [CASLTERM] -> [CASLTERM] -> Maybe [[(VAR, CASLTERM)]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 [CASLTERM]
terms1 [CASLTERM]
terms2
   -- if not, try to exploit overloading relation
    else do
      let (opsymb1' :: OP_SYMB
opsymb1', terms1' :: [CASLTERM]
terms1', w1 :: [SORT]
w1) = OP_SYMB -> [CASLTERM] -> (OP_SYMB, [CASLTERM], [SORT])
stripInj OP_SYMB
opsymb1 [CASLTERM]
terms1
          (opsymb2' :: OP_SYMB
opsymb2', terms2' :: [CASLTERM]
terms2', w2 :: [SORT]
w2) = OP_SYMB -> [CASLTERM] -> (OP_SYMB, [CASLTERM], [SORT])
stripInj OP_SYMB
opsymb2 [CASLTERM]
terms2
      Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OP_SYMB -> SORT
opSymbName OP_SYMB
opsymb1' SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
/= OP_SYMB -> SORT
opSymbName OP_SYMB
opsymb2' Bool -> Bool -> Bool
|| [SORT]
w1 [SORT] -> [SORT] -> Bool
forall a. Eq a => a -> a -> Bool
/= [SORT]
w2) Maybe ()
forall a. Maybe a
Nothing
      ([[(VAR, CASLTERM)]] -> [(VAR, CASLTERM)])
-> Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(VAR, CASLTERM)]] -> [(VAR, CASLTERM)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)])
-> Maybe [[(VAR, CASLTERM)]] -> Maybe [(VAR, CASLTERM)]
forall a b. (a -> b) -> a -> b
$ (CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)])
-> [CASLTERM] -> [CASLTERM] -> Maybe [[(VAR, CASLTERM)]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 [CASLTERM]
terms1' [CASLTERM]
terms2'
match2 (Sorted_term t1 :: CASLTERM
t1 _ _) t2 :: CASLTERM
t2 = CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 CASLTERM
t1 CASLTERM
t2
match2 t1 :: CASLTERM
t1 (Sorted_term t2 :: CASLTERM
t2 _ _) = CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
match2 CASLTERM
t1 CASLTERM
t2
match2 _ _ = Maybe [(VAR, CASLTERM)]
forall a. Maybe a
Nothing

-- | strip off the injections of an application
stripInj :: OP_SYMB -> [CASLTERM] -> (OP_SYMB, [CASLTERM], [SORT])
stripInj :: OP_SYMB -> [CASLTERM] -> (OP_SYMB, [CASLTERM], [SORT])
stripInj opsymb :: OP_SYMB
opsymb terms :: [CASLTERM]
terms =
  let (opsymb' :: OP_SYMB
opsymb', terms' :: [CASLTERM]
terms') =
        case (SORT -> Bool
isInjName (SORT -> Bool) -> SORT -> Bool
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> SORT
opSymbName OP_SYMB
opsymb, [CASLTERM]
terms) of
          (True, [Application o :: OP_SYMB
o ts :: [CASLTERM]
ts _]) -> (OP_SYMB
o, [CASLTERM]
ts)
          _ -> (OP_SYMB
opsymb, [CASLTERM]
terms)
      strip1 :: TERM f -> TERM f
strip1 t1 :: TERM f
t1@(Application o :: OP_SYMB
o [t2 :: TERM f
t2] _) =
        if SORT -> Bool
isInjName (SORT -> Bool) -> SORT -> Bool
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> SORT
opSymbName OP_SYMB
o then TERM f
t2 else TERM f
t1
      strip1 t1 :: TERM f
t1 = TERM f
t1
      terms'' :: [CASLTERM]
terms'' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
forall f. TERM f -> TERM f
strip1 [CASLTERM]
terms'
  in (OP_SYMB
opsymb', [CASLTERM]
terms'', (CASLTERM -> SORT) -> [CASLTERM] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm [CASLTERM]
terms'')

-- | is a substitution consistent with itself?
consistent :: [(VAR, CASLTERM)] -> Bool
consistent :: [(VAR, CASLTERM)] -> Bool
consistent ass :: [(VAR, CASLTERM)]
ass =
  Maybe (Map VAR CASLTERM) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Map VAR CASLTERM) -> Bool)
-> Maybe (Map VAR CASLTERM) -> Bool
forall a b. (a -> b) -> a -> b
$ (Map VAR CASLTERM -> (VAR, CASLTERM) -> Maybe (Map VAR CASLTERM))
-> Map VAR CASLTERM
-> [(VAR, CASLTERM)]
-> Maybe (Map VAR CASLTERM)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map VAR CASLTERM -> (VAR, CASLTERM) -> Maybe (Map VAR CASLTERM)
forall k a. (Ord k, Eq a) => Map k a -> (k, a) -> Maybe (Map k a)
insertAss Map VAR CASLTERM
forall k a. Map k a
Map.empty [(VAR, CASLTERM)]
ass
  where
  insertAss :: Map k a -> (k, a) -> Maybe (Map k a)
insertAss m :: Map k a
m (v :: k
v, t :: a
t) =
    case k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
v Map k a
m of
      Just t1 :: a
t1 -> if a
t a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
t1 then Map k a -> Maybe (Map k a)
forall (m :: * -> *) a. Monad m => a -> m a
return Map k a
m else Maybe (Map k a)
forall a. Maybe a
Nothing
      Nothing -> Map k a -> Maybe (Map k a)
forall a. a -> Maybe a
Just (Map k a -> Maybe (Map k a)) -> Map k a -> Maybe (Map k a)
forall a b. (a -> b) -> a -> b
$ k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
v a
t Map k a
m

ternaryAnd :: (Result Bool, a) -> (Result Bool, a) -> (Result Bool, a)
ternaryAnd :: (Result Bool, a) -> (Result Bool, a) -> (Result Bool, a)
ternaryAnd b1 :: (Result Bool, a)
b1@(Result _ (Just False), _) _ = (Result Bool, a)
b1
ternaryAnd (Result d1 :: [Diagnosis]
d1 (Just True), _) (b2 :: Result Bool
b2, x2 :: a
x2) =
  ([Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Result () -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result Bool
b2, a
x2)
ternaryAnd (Result d1 :: [Diagnosis]
d1 Nothing, _) (b2 :: Result Bool
b2@(Result _ (Just False)), x2 :: a
x2) =
  ([Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Result () -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result Bool
b2, a
x2)
ternaryAnd (Result d1 :: [Diagnosis]
d1 Nothing, _) (b2 :: Result Bool
b2, x2 :: a
x2) =
  ([Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Result () -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result Bool
b2 Result Bool -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Diagnosis] -> Maybe Bool -> Result Bool
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe Bool
forall a. Maybe a
Nothing, a
x2)

ternaryOr :: Result Bool -> Result Bool -> Result Bool
ternaryOr :: Result Bool -> Result Bool -> Result Bool
ternaryOr b1 :: Result Bool
b1@(Result _ (Just True)) _ = Result Bool
b1
ternaryOr (Result d1 :: [Diagnosis]
d1 (Just False)) b2 :: Result Bool
b2 = [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Result () -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result Bool
b2
ternaryOr (Result d1 :: [Diagnosis]
d1 Nothing) b2 :: Result Bool
b2@(Result _ (Just True)) =
  [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Result () -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result Bool
b2
ternaryOr (Result d1 :: [Diagnosis]
d1 Nothing) b2 :: Result Bool
b2 =
  [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
d1 (() -> Maybe ()
forall a. a -> Maybe a
Just ()) Result () -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result Bool
b2 Result Bool -> Result Bool -> Result Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Diagnosis] -> Maybe Bool -> Result Bool
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe Bool
forall a. Maybe a
Nothing

calculateFormula :: Bool -> QModel -> VariableAssignment -> CASLFORMULA
    -> Result Bool
calculateFormula :: Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula isOuter :: Bool
isOuter qm :: QModel
qm varass :: VariableAssignment
varass f :: CASLFORMULA
f = case CASLFORMULA
f of
    Quantification {} ->
       Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateQuantification Bool
isOuter QModel
qm VariableAssignment
varass CASLFORMULA
f
    Junction j :: Junctor
j formulas :: [CASLFORMULA]
formulas _ ->
       let newFs :: [Result Bool]
newFs = (CASLFORMULA -> Result Bool) -> [CASLFORMULA] -> [Result Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
varass) [CASLFORMULA]
formulas
       in if Junctor
j Junctor -> Junctor -> Bool
forall a. Eq a => a -> a -> Bool
== Junctor
Dis then (Result Bool -> Result Bool -> Result Bool)
-> Result Bool -> [Result Bool] -> Result Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Result Bool -> Result Bool -> Result Bool
ternaryOr (Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) [Result Bool]
newFs else do
       let (res :: Result Bool
res, f1 :: CASLFORMULA
f1) =
             ((Result Bool, CASLFORMULA)
 -> (Result Bool, CASLFORMULA) -> (Result Bool, CASLFORMULA))
-> (Result Bool, CASLFORMULA)
-> [(Result Bool, CASLFORMULA)]
-> (Result Bool, CASLFORMULA)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Result Bool, CASLFORMULA)
-> (Result Bool, CASLFORMULA) -> (Result Bool, CASLFORMULA)
forall a. (Result Bool, a) -> (Result Bool, a) -> (Result Bool, a)
ternaryAnd (Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True, CASLFORMULA
f)
               ([Result Bool] -> [CASLFORMULA] -> [(Result Bool, CASLFORMULA)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((CASLFORMULA -> Result Bool) -> [CASLFORMULA] -> [Result Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
varass) [CASLFORMULA]
formulas) [CASLFORMULA]
formulas)
       Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isOuter (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ case Result Bool -> Maybe Bool
forall a. Result a -> Maybe a
maybeResult Result Bool
res of
         Just False ->
             () -> String -> Result ()
forall a. a -> String -> Result a
justWarn () (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "Conjunction not fulfilled\n"
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ "Formula that failed: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLFORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CASLFORMULA
f1 ""
         _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       Result Bool
res
    Relation f1 :: CASLFORMULA
f1 c :: Relation
c f2 :: CASLFORMULA
f2 _ ->
        let res1 :: Result Bool
res1 = Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
varass CASLFORMULA
f1
            res2 :: Result Bool
res2 = Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
varass CASLFORMULA
f2
        in if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence then (Bool -> Bool -> Bool) -> Result Bool -> Result Bool -> Result Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) Result Bool
res1 Result Bool
res2 else
               Result Bool -> Result Bool -> Result Bool
ternaryOr ((Bool -> Bool) -> Result Bool -> Result Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not Result Bool
res1) Result Bool
res2
    Negation f1 :: CASLFORMULA
f1 _ ->
        (Bool -> Bool) -> Result Bool -> Result Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (Result Bool -> Result Bool) -> Result Bool -> Result Bool
forall a b. (a -> b) -> a -> b
$ Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
varass CASLFORMULA
f1
    Atom b :: Bool
b _ -> Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
    Equation term1 :: CASLTERM
term1 _ term2 :: CASLTERM
term2 _ -> do
        CASLTERM
t1 <- QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm VariableAssignment
varass CASLTERM
term1
        CASLTERM
t2 <- QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm VariableAssignment
varass CASLTERM
term2
        QModel -> CASLTERM -> CASLTERM -> Result Bool
equalElements QModel
qm CASLTERM
t1 CASLTERM
t2
    Predication predsymb :: PRED_SYMB
predsymb terms :: [CASLTERM]
terms _ ->
        QModel
-> VariableAssignment -> PRED_SYMB -> [CASLTERM] -> Result Bool
applyPredicate QModel
qm VariableAssignment
varass PRED_SYMB
predsymb [CASLTERM]
terms
    _ -> String -> Result Bool
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Bool) -> String -> Result Bool
forall a b. (a -> b) -> a -> b
$ "formula evaluation not implemented for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLFORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CASLFORMULA
f ""

calculateQuantification :: Bool -> QModel -> VariableAssignment -> CASLFORMULA
                        -> Result Bool
calculateQuantification :: Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateQuantification isOuter :: Bool
isOuter qm :: QModel
qm varass :: VariableAssignment
varass qf :: CASLFORMULA
qf = case CASLFORMULA
qf of
  Quantification quant :: QUANTIFIER
quant vardecls :: [VAR_DECL]
vardecls f :: CASLFORMULA
f _ -> do
    [VariableAssignment]
assments <- QModel -> [VAR_DECL] -> Result [VariableAssignment]
generateVariableAssignments QModel
qm [VAR_DECL]
vardecls
    let assments' :: [VariableAssignment]
assments' = (VariableAssignment -> VariableAssignment)
-> [VariableAssignment] -> [VariableAssignment]
forall a b. (a -> b) -> [a] -> [b]
map (VariableAssignment -> VariableAssignment -> VariableAssignment
`concatAssignment` VariableAssignment
varass) [VariableAssignment]
assments
    case QUANTIFIER
quant of
      Universal -> do
        let resList :: [Result Bool]
resList = (VariableAssignment -> Result Bool)
-> [VariableAssignment] -> [Result Bool]
forall a b. (a -> b) -> [a] -> [b]
map ((VariableAssignment -> CASLFORMULA -> Result Bool)
-> CASLFORMULA -> VariableAssignment -> Result Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm) CASLFORMULA
f) [VariableAssignment]
assments'
            (res :: Result Bool
res, fass :: VariableAssignment
fass) = ((Result Bool, VariableAssignment)
 -> (Result Bool, VariableAssignment)
 -> (Result Bool, VariableAssignment))
-> (Result Bool, VariableAssignment)
-> [(Result Bool, VariableAssignment)]
-> (Result Bool, VariableAssignment)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Result Bool, VariableAssignment)
-> (Result Bool, VariableAssignment)
-> (Result Bool, VariableAssignment)
forall a. (Result Bool, a) -> (Result Bool, a) -> (Result Bool, a)
ternaryAnd (Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True, QModel -> VariableAssignment
emptyAssignment QModel
qm)
                                          ([Result Bool]
-> [VariableAssignment] -> [(Result Bool, VariableAssignment)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Result Bool]
resList [VariableAssignment]
assments')
        Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isOuter (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ case Result Bool -> Maybe Bool
forall a. Result a -> Maybe a
maybeResult Result Bool
res of
          Just False ->
              () -> String -> Result ()
forall a. a -> String -> Result a
justWarn () ("Universal quantification not fulfilled\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ "Counterexample: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VariableAssignment -> String
forall a. Show a => a -> String
show VariableAssignment
fass)
          _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Result Bool
res
      Existential ->
        (Result Bool -> Result Bool -> Result Bool)
-> Result Bool -> [Result Bool] -> Result Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Result Bool -> Result Bool -> Result Bool
ternaryOr (Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
                        ((VariableAssignment -> Result Bool)
-> [VariableAssignment] -> [Result Bool]
forall a b. (a -> b) -> [a] -> [b]
map ((VariableAssignment -> CASLFORMULA -> Result Bool)
-> CASLFORMULA -> VariableAssignment -> Result Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm) CASLFORMULA
f) [VariableAssignment]
assments')
      Unique_existential ->
        {- scan the assingments, stop scanning once the result is clear,
        using the Left constructor of the Either monad -}
        let combineEx1 :: Either
  ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
  ([Diagnosis], Maybe VariableAssignment)
-> VariableAssignment
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
combineEx1 state :: Either
  ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
  ([Diagnosis], Maybe VariableAssignment)
state ass2 :: VariableAssignment
ass2 = case Either
  ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
  ([Diagnosis], Maybe VariableAssignment)
state of
              Right (msgsSoFar :: [Diagnosis]
msgsSoFar, ass1 :: Maybe VariableAssignment
ass1) ->
                let Result msgs :: [Diagnosis]
msgs res :: Maybe Bool
res = Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm VariableAssignment
ass2 CASLFORMULA
f
                in case (Maybe Bool
res, Maybe VariableAssignment
ass1) of
                -- the first fulfilment
                (Just True, Nothing) -> ([Diagnosis], Maybe VariableAssignment)
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
forall a b. b -> Either a b
Right ([Diagnosis]
msgsSoFar [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
msgs, VariableAssignment -> Maybe VariableAssignment
forall a. a -> Maybe a
Just VariableAssignment
ass2)
                -- the second fulfilment
                (Just True, Just ass1' :: VariableAssignment
ass1') ->
                    ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
forall a b. a -> Either a b
Left ([Diagnosis]
msgsSoFar [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
msgs, (VariableAssignment, VariableAssignment)
-> Maybe (VariableAssignment, VariableAssignment)
forall a. a -> Maybe a
Just (VariableAssignment
ass1', VariableAssignment
ass2))
                -- not fulfilled? Then nothing changes
                (Just False, _) -> ([Diagnosis], Maybe VariableAssignment)
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
forall a b. b -> Either a b
Right ([Diagnosis]
msgsSoFar [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
msgs, Maybe VariableAssignment
ass1)
                -- don't know? Then we don't know either
                (Nothing, _) -> ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
forall a b. a -> Either a b
Left ([Diagnosis]
msgsSoFar [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
msgs, Maybe (VariableAssignment, VariableAssignment)
forall a. Maybe a
Nothing)
              Left _ -> Either
  ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
  ([Diagnosis], Maybe VariableAssignment)
state
        in case (Either
   ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
   ([Diagnosis], Maybe VariableAssignment)
 -> VariableAssignment
 -> Either
      ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
      ([Diagnosis], Maybe VariableAssignment))
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
-> [VariableAssignment]
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Either
  ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
  ([Diagnosis], Maybe VariableAssignment)
-> VariableAssignment
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
combineEx1 (([Diagnosis], Maybe VariableAssignment)
-> Either
     ([Diagnosis], Maybe (VariableAssignment, VariableAssignment))
     ([Diagnosis], Maybe VariableAssignment)
forall a b. b -> Either a b
Right ([], Maybe VariableAssignment
forall a. Maybe a
Nothing)) [VariableAssignment]
assments' of
          Right (msgs :: [Diagnosis]
msgs, Just _) -> [Diagnosis] -> Maybe Bool -> Result Bool
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
msgs (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
          Right (msgs :: [Diagnosis]
msgs, Nothing) -> do
            [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
msgs (() -> Maybe ()
forall a. a -> Maybe a
Just ())
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isOuter
              (() -> String -> Result ()
forall a. a -> String -> Result a
justWarn () ("Unique Existential quantification"
                           String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not fulfilled: no assignment found"))
            Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Left (msgs :: [Diagnosis]
msgs, Just (ass1 :: VariableAssignment
ass1, ass2 :: VariableAssignment
ass2)) -> do
            [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
msgs (() -> Maybe ()
forall a. a -> Maybe a
Just ())
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isOuter
              (() -> String -> Result ()
forall a. a -> String -> Result a
justWarn () ("Unique Existential quantification"
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not fulfilled: at least two assignments found:\n"
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ VariableAssignment -> String
forall a. Show a => a -> String
show VariableAssignment
ass1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ VariableAssignment -> String
forall a. Show a => a -> String
show VariableAssignment
ass2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n"))
            Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Left (msgs :: [Diagnosis]
msgs, Nothing) ->
            [Diagnosis] -> Maybe Bool -> Result Bool
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
msgs Maybe Bool
forall a. Maybe a
Nothing
  _ -> String -> Result Bool
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "calculateQuantification wrongly applied"

applyPredicate :: QModel -> VariableAssignment -> PRED_SYMB -> [CASLTERM]
               -> Result Bool
applyPredicate :: QModel
-> VariableAssignment -> PRED_SYMB -> [CASLTERM] -> Result Bool
applyPredicate qm :: QModel
qm ass :: VariableAssignment
ass predsymb :: PRED_SYMB
predsymb terms :: [CASLTERM]
terms = do
  -- block infinite recursion
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((PRED_SYMB, [CASLTERM]) -> [(PRED_SYMB, [CASLTERM])] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (PRED_SYMB
predsymb, [CASLTERM]
terms) ([(PRED_SYMB, [CASLTERM])] -> Bool)
-> [(PRED_SYMB, [CASLTERM])] -> Bool
forall a b. (a -> b) -> a -> b
$ QModel -> [(PRED_SYMB, [CASLTERM])]
evaluatedPreds QModel
qm)
       (String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("infinite recursion when calculating"
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLFORMULA -> String
forall a. Show a => a -> String
show (PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
predsymb [CASLTERM]
terms)))
  let qm' :: QModel
qm' = QModel
qm { evaluatedPreds :: [(PRED_SYMB, [CASLTERM])]
evaluatedPreds = (PRED_SYMB
predsymb, [CASLTERM]
terms) (PRED_SYMB, [CASLTERM])
-> [(PRED_SYMB, [CASLTERM])] -> [(PRED_SYMB, [CASLTERM])]
forall a. a -> [a] -> [a]
: QModel -> [(PRED_SYMB, [CASLTERM])]
evaluatedPreds QModel
qm }
  -- evaluate argument terms
  [CASLTERM]
args <- (CASLTERM -> Result CASLTERM) -> [CASLTERM] -> Result [CASLTERM]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
calculateTerm QModel
qm' VariableAssignment
ass) [CASLTERM]
terms
  -- find appropriate predicate definition
  case PRED_SYMB
-> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
-> Maybe [([CASLTERM], CASLFORMULA)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PRED_SYMB
predsymb (QModel -> Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
predDefs QModel
qm) of
    Nothing -> String -> Result Bool
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("no predicate definition for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PRED_SYMB -> ShowS
forall a. Pretty a => a -> ShowS
showDoc PRED_SYMB
predsymb "")
    Just bodies :: [([CASLTERM], CASLFORMULA)]
bodies -> do
      -- bind formal to actual arguments
      (body :: CASLFORMULA
body, m :: [(VAR, CASLTERM)]
m) <- [([CASLTERM], CASLFORMULA)]
-> [CASLTERM] -> String -> Result (CASLFORMULA, [(VAR, CASLTERM)])
forall a.
[([CASLTERM], a)]
-> [CASLTERM] -> String -> Result (a, [(VAR, CASLTERM)])
match [([CASLTERM], CASLFORMULA)]
bodies [CASLTERM]
args (String -> Result (CASLFORMULA, [(VAR, CASLTERM)]))
-> String -> Result (CASLFORMULA, [(VAR, CASLTERM)])
forall a b. (a -> b) -> a -> b
$
                   CASLFORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
predsymb [CASLTERM]
args) ""
      let ass' :: VariableAssignment
ass' = (VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment)
-> VariableAssignment -> [(VAR, CASLTERM)] -> VariableAssignment
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment
insertAssignment VariableAssignment
ass [(VAR, CASLTERM)]
m
      -- evaluate body of predicate definition
      Bool -> QModel -> VariableAssignment -> CASLFORMULA -> Result Bool
calculateFormula Bool
False QModel
qm' VariableAssignment
ass' CASLFORMULA
body

equalElements :: QModel -> CASLTERM -> CASLTERM -> Result Bool
equalElements :: QModel -> CASLTERM -> CASLTERM -> Result Bool
equalElements qm :: QModel
qm t1 :: CASLTERM
t1 t2 :: CASLTERM
t2 =
  if CASLTERM
t1 CASLTERM -> CASLTERM -> Bool
forall a. Eq a => a -> a -> Bool
== CASLTERM
t2 then Bool -> Result Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
   else QModel
-> VariableAssignment -> PRED_SYMB -> [CASLTERM] -> Result Bool
applyPredicate QModel
qm (QModel -> VariableAssignment
emptyAssignment QModel
qm) PRED_SYMB
eqSymb [CASLTERM
t1, CASLTERM
t2]

generateVariableAssignments :: QModel -> [VAR_DECL]
                            -> Result [VariableAssignment]
generateVariableAssignments :: QModel -> [VAR_DECL] -> Result [VariableAssignment]
generateVariableAssignments qm :: QModel
qm vardecls :: [VAR_DECL]
vardecls = do
   let vars :: [(VAR, SORT)]
vars = [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs [VAR_DECL]
vardecls
   [[CASLTERM]]
carriers <- ((VAR, SORT) -> Result [CASLTERM])
-> [(VAR, SORT)] -> Result [[CASLTERM]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QModel -> SORT -> Result [CASLTERM]
getCarrier QModel
qm (SORT -> Result [CASLTERM])
-> ((VAR, SORT) -> SORT) -> (VAR, SORT) -> Result [CASLTERM]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd) [(VAR, SORT)]
vars
   let varsCarriers :: [(VAR, [CASLTERM])]
varsCarriers = [VAR] -> [[CASLTERM]] -> [(VAR, [CASLTERM])]
forall a b. [a] -> [b] -> [(a, b)]
zip (((VAR, SORT) -> VAR) -> [(VAR, SORT)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> VAR
forall a b. (a, b) -> a
fst [(VAR, SORT)]
vars) [[CASLTERM]]
carriers
   [VariableAssignment] -> Result [VariableAssignment]
forall (m :: * -> *) a. Monad m => a -> m a
return ([VariableAssignment] -> Result [VariableAssignment])
-> [VariableAssignment] -> Result [VariableAssignment]
forall a b. (a -> b) -> a -> b
$ ([(VAR, CASLTERM)] -> VariableAssignment)
-> [[(VAR, CASLTERM)]] -> [VariableAssignment]
forall a b. (a -> b) -> [a] -> [b]
map (QModel -> [(VAR, CASLTERM)] -> VariableAssignment
VariableAssignment QModel
qm) ([(VAR, [CASLTERM])] -> [[(VAR, CASLTERM)]]
gVAs [(VAR, [CASLTERM])]
varsCarriers)

gVAs :: [(VAR, [CASLTERM])] -> [[(VAR, CASLTERM)]]
gVAs :: [(VAR, [CASLTERM])] -> [[(VAR, CASLTERM)]]
gVAs [] = [[]]
gVAs ((v :: VAR
v, carrier :: [CASLTERM]
carrier) : vs :: [(VAR, [CASLTERM])]
vs) = let
    rs :: [[(VAR, CASLTERM)]]
rs = [(VAR, [CASLTERM])] -> [[(VAR, CASLTERM)]]
gVAs [(VAR, [CASLTERM])]
vs
    fs :: [(VAR, CASLTERM)]
fs = (CASLTERM -> (VAR, CASLTERM)) -> [CASLTERM] -> [(VAR, CASLTERM)]
forall a b. (a -> b) -> [a] -> [b]
map (\ b :: CASLTERM
b -> (VAR
v, CASLTERM
b)) [CASLTERM]
carrier
    in [(VAR, CASLTERM)
f (VAR, CASLTERM) -> [(VAR, CASLTERM)] -> [(VAR, CASLTERM)]
forall a. a -> [a] -> [a]
: [(VAR, CASLTERM)]
r | (VAR, CASLTERM)
f <- [(VAR, CASLTERM)]
fs, [(VAR, CASLTERM)]
r <- [[(VAR, CASLTERM)]]
rs]


-- | check whether some formula leads to term generation of a sort
termSort :: CASLFORMULA -> Maybe (SORT, [CASLTERM])
-- sort generation constraint
termSort :: CASLFORMULA -> Maybe (SORT, [CASLTERM])
termSort (Sort_gen_ax constr :: [Constraint]
constr _) =
  case [SORT]
sorts of
     -- at the moment, we only treat one-sort constraints with constants
     [s :: SORT
s] -> if (OP_SYMB -> Bool) -> [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all OP_SYMB -> Bool
constant [OP_SYMB]
ops
             then (SORT, [CASLTERM]) -> Maybe (SORT, [CASLTERM])
forall a. a -> Maybe a
Just (SORT
s, (OP_SYMB -> CASLTERM) -> [OP_SYMB] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> CASLTERM
forall f. OP_SYMB -> TERM f
mkTerm [OP_SYMB]
ops)
             else Maybe (SORT, [CASLTERM])
forall a. Maybe a
Nothing
     _ -> Maybe (SORT, [CASLTERM])
forall a. Maybe a
Nothing
    where (sorts :: [SORT]
sorts, ops :: [OP_SYMB]
ops, _) = [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
recover_Sort_gen_ax [Constraint]
constr
          constant :: OP_SYMB -> Bool
constant (Qual_op_name _ (Op_type _ [] _ _) _) = Bool
True
          constant _ = Bool
False
          mkTerm :: OP_SYMB -> TERM f
mkTerm op :: OP_SYMB
op = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
op []
-- axiom forcing empty carrier
termSort (Quantification Universal [Var_decl [_] s :: SORT
s _] (Atom False _) _) =
  (SORT, [CASLTERM]) -> Maybe (SORT, [CASLTERM])
forall a. a -> Maybe a
Just (SORT
s, [])
termSort _ = Maybe (SORT, [CASLTERM])
forall a. Maybe a
Nothing

-- | get the carrier set for a specific sort
getCarrier :: QModel -> SORT -> Result [CASLTERM]
getCarrier :: QModel -> SORT -> Result [CASLTERM]
getCarrier qm :: QModel
qm s :: SORT
s =
  case SORT -> Map SORT [CASLFORMULA] -> Maybe [CASLFORMULA]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
s (QModel -> Map SORT [CASLFORMULA]
carrierSens QModel
qm) of
    Nothing -> String -> Result [CASLTERM]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is not generated")
    Just sens :: [CASLFORMULA]
sens -> case (CASLFORMULA -> Maybe (SORT, [CASLTERM]))
-> [CASLFORMULA] -> [(SORT, [CASLTERM])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe CASLFORMULA -> Maybe (SORT, [CASLTERM])
termSort [CASLFORMULA]
sens of
      [] -> String -> Result [CASLTERM]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is not generated by constants")
      (_, terms :: [CASLTERM]
terms) : _ -> [CASLTERM] -> Result [CASLTERM]
forall (m :: * -> *) a. Monad m => a -> m a
return [CASLTERM]
terms
  -- todo: generalise this

-- * Interfacing to Hets prover interface

{- | The Prover implementation. First runs the batch prover (with
  graphical feedback), then starts the GUI prover. -}
quickCheckProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
quickCheckProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
quickCheckProver = (String
-> CASL_Sublogics
-> (String
    -> Theory CASLSign CASLFORMULA ProofTree
    -> [FreeDefMorphism CASLFORMULA CASLMor]
    -> IO [ProofStatus ProofTree])
-> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate "QuickCheck"
  (CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.top { has_part :: Bool
has_part = Bool
False, which_logic :: CASL_Formulas
which_logic = CASL_Formulas
SL.FOL }) String
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO [ProofStatus ProofTree]
quickCheckGUI)
  { proveCMDLautomaticBatch :: Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus ProofTree])
   -> String
   -> TacticScript
   -> Theory CASLSign CASLFORMULA ProofTree
   -> [FreeDefMorphism CASLFORMULA CASLMor]
   -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch = (Bool
 -> Bool
 -> MVar (Result [ProofStatus ProofTree])
 -> String
 -> TacticScript
 -> Theory CASLSign CASLFORMULA ProofTree
 -> [FreeDefMorphism CASLFORMULA CASLMor]
 -> IO (ThreadId, MVar ()))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus ProofTree])
      -> String
      -> TacticScript
      -> Theory CASLSign CASLFORMULA ProofTree
      -> [FreeDefMorphism CASLFORMULA CASLMor]
      -> IO (ThreadId, MVar ()))
forall a. a -> Maybe a
Just Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO (ThreadId, MVar ())
quickCheckCMDLautomaticBatch }

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}

atpFun :: String -- ^ theory name
       -> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
atpFun :: String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
atpFun _thName :: String
_thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> ShowS
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPFunctions
    { initialProverState :: InitialProverState CASLSign CASLFORMULA CASLMor QModel
initialProverState = \ sig :: CASLSign
sig sens :: [Named CASLFORMULA]
sens _ -> QModel -> [Named CASLFORMULA] -> QModel
insertSens (CASLSign -> QModel
makeQm CASLSign
sig) [Named CASLFORMULA]
sens,
      atpTransSenName :: ShowS
atpTransSenName = ShowS
forall a. a -> a
id,
      atpInsertSentence :: QModel -> Named CASLFORMULA -> QModel
atpInsertSentence = QModel -> Named CASLFORMULA -> QModel
insertSen,
      goalOutput :: QModel -> Named CASLFORMULA -> [String] -> IO String
goalOutput = \ _ _ _ -> do
            String -> IO ()
putStrLn "No display of output yet"
            String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "",
      proverHelpText :: String
proverHelpText =
        "QuickCheck tries to evaluate sentences in term generated models. " String -> ShowS
forall a. [a] -> [a] -> [a]
++
        "This only works if your theory contains enough generated or " String -> ShowS
forall a. [a] -> [a] -> [a]
++
        "freely generated datatypes.",
      batchTimeEnv :: String
batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
      fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions {problemOutput :: String
problemOutput = ".none1",
                                      proverOutput :: String
proverOutput = ".none2",
                                      theoryConfiguration :: String
theoryConfiguration = ".none3"},
      runProver :: QModel
-> GenericConfig ProofTree
-> Bool
-> String
-> Named CASLFORMULA
-> IO (ATPRetval, GenericConfig ProofTree)
runProver = QModel
-> GenericConfig ProofTree
-> Bool
-> String
-> Named CASLFORMULA
-> IO (ATPRetval, GenericConfig ProofTree)
runQuickCheck,
      createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = [String] -> GenericConfig ProofTree -> [String]
forall a b. a -> b -> a
const [] }

-- ** GUI

{- |
  Invokes the generic prover GUI. SPASS specific functions are omitted by
  data type ATPFunctions.
-}
quickCheckGUI :: String -- ^ theory name
           -> Theory CASLSign CASLFORMULA ProofTree
           {- ^ theory consisting of a signature
           and a list of named sentences -}
           -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
           -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
quickCheckGUI :: String
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO [ProofStatus ProofTree]
quickCheckGUI thName :: String
thName th :: Theory CASLSign CASLFORMULA ProofTree
th freedefs :: [FreeDefMorphism CASLFORMULA CASLMor]
freedefs = ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
-> Bool
-> String
-> String
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui (String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
atpFun String
thName) Bool
True
    (Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
-> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
quickCheckProver) String
thName Theory CASLSign CASLFORMULA ProofTree
th [FreeDefMorphism CASLFORMULA CASLMor]
freedefs ProofTree
emptyProofTree

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the QuickCheck prover via MathServe.
  QuickCheck specific functions are omitted by data type ATPFunctions.
-}
quickCheckCMDLautomaticBatch ::
           Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> MVar (Result.Result [ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> TacticScript -- ^ default tactic script
        -> Theory CASLSign CASLFORMULA ProofTree {- ^ theory consisting of a
           signature and a list of named sentences -}
        -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
        -> IO (ThreadId, MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
quickCheckCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO (ThreadId, MVar ())
quickCheckCMDLautomaticBatch inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                        thName :: String
thName defTS :: TacticScript
defTS th :: Theory CASLSign CASLFORMULA ProofTree
th freedefs :: [FreeDefMorphism CASLFORMULA CASLMor]
freedefs =
    ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> ProofTree
-> IO (ThreadId, MVar ())
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> String
-> ATPTacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO (ThreadId, MVar ())
genericCMDLautomaticBatch (String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar (Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
-> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
quickCheckProver) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory CASLSign CASLFORMULA ProofTree
th [FreeDefMorphism CASLFORMULA CASLMor]
freedefs ProofTree
emptyProofTree