-- | Relation between FOL and propositonal logic; Herbrand theorem.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Data.Logic.ATP.Herbrand where

import Data.Logic.ATP.Apply (functions, HasApply(TermOf))
import Data.Logic.ATP.DP (dpll)
import Data.Logic.ATP.FOL (IsFirstOrder, lsubst, fv, generalize)
import Data.Logic.ATP.Formulas (IsFormula(AtomOf), overatoms, atomic)
import Data.Logic.ATP.Lib (allpairs, distrib)
import Data.Logic.ATP.Lit ((.~.), JustLiteral, LFormula)
import Data.Logic.ATP.Parser(fof)
import Data.Logic.ATP.Pretty (prettyShow)
import Data.Logic.ATP.Prop (eval, JustPropositional, PFormula, simpcnf, simpdnf, trivial)
import Data.Logic.ATP.Skolem (Formula, HasSkolem(SVarOf), runSkolem, skolemize)
import Data.Logic.ATP.Term (Arity, IsTerm(TVarOf, FunOf), fApp)
import qualified Data.Map.Strict as Map
import Data.Set as Set
import Data.String (IsString(..))
import Debug.Trace
import Test.HUnit hiding (tried)

-- | Propositional valuation.
pholds :: (JustPropositional pf) => (AtomOf pf -> Bool) -> pf -> Bool
pholds :: forall pf.
JustPropositional pf =>
(AtomOf pf -> Bool) -> pf -> Bool
pholds AtomOf pf -> Bool
d pf
fm = pf -> (AtomOf pf -> Bool) -> Bool
forall pf.
JustPropositional pf =>
pf -> (AtomOf pf -> Bool) -> Bool
eval pf
fm AtomOf pf -> Bool
d

-- | Get the constants for Herbrand base, adding nullary one if necessary.
herbfuns :: (atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, IsFormula fof, HasApply atom, Ord function) => fof -> (Set (function, Arity), Set (function, Arity))
herbfuns :: forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns fof
fm =
  let (Set (function, Int)
cns,Set (function, Int)
fns) = ((function, Int) -> Bool)
-> Set (function, Int)
-> (Set (function, Int), Set (function, Int))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (\ (function
_,Int
ar) -> Int
ar Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (fof -> Set (function, Int)
forall formula atom function term.
(IsFormula formula, HasApply atom, Ord function,
 atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term) =>
formula -> Set (function, Int)
functions fof
fm) in
  if Set (function, Int) -> Bool
forall a. Set a -> Bool
Set.null Set (function, Int)
cns then ((function, Int) -> Set (function, Int)
forall a. a -> Set a
Set.singleton (String -> function
forall a. IsString a => String -> a
fromString String
"c",Int
0),Set (function, Int)
fns) else (Set (function, Int)
cns,Set (function, Int)
fns)

-- | Enumeration of ground terms and m-tuples, ordered by total fns.
groundterms :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Arity) -> Int -> Set term
groundterms :: forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Set term
groundterms Set term
cntms Set (f, Int)
_ Int
0 = Set term
cntms
groundterms Set term
cntms Set (f, Int)
fns Int
n =
    ((f, Int) -> Set term -> Set term)
-> Set term -> Set (f, Int) -> Set term
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (f, Int) -> Set term -> Set term
terms Set term
forall a. Set a
Set.empty Set (f, Int)
fns
    where
      terms :: (f, Int) -> Set term -> Set term
terms (f
f,Int
m) Set term
l = Set term -> Set term -> Set term
forall a. Ord a => Set a -> Set a -> Set a
Set.union (([term] -> term) -> Set [term] -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp f
FunOf term
f) (Set term -> Set (f, Int) -> Int -> Int -> Set [term]
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
cntms Set (f, Int)
fns (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
m)) Set term
l

groundtuples :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples :: forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
_ Set (f, Int)
_ Int
0 Int
0 = [term] -> Set [term]
forall a. a -> Set a
Set.singleton []
groundtuples Set term
_ Set (f, Int)
_ Int
_ Int
0 = Set [term]
forall a. Set a
Set.empty
groundtuples Set term
cntms Set (f, Int)
fns Int
n Int
m =
    (Int -> Set [term] -> Set [term])
-> Set [term] -> Set Int -> Set [term]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Int -> Set [term] -> Set [term]
tuples Set [term]
forall a. Set a
Set.empty ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
0 .. Int
n])
    where
      tuples :: Int -> Set [term] -> Set [term]
tuples Int
k Set [term]
l = Set [term] -> Set [term] -> Set [term]
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((term -> [term] -> [term]) -> Set term -> Set [term] -> Set [term]
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (:) (Set term -> Set (f, Int) -> Int -> Set term
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Set term
groundterms Set term
cntms Set (f, Int)
fns Int
k) (Set term -> Set (f, Int) -> Int -> Int -> Set [term]
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
cntms Set (f, Int)
fns (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))) Set [term]
l

-- | Iterate modifier "mfn" over ground terms till "tfn" fails.
herbloop :: forall lit atom function v term.
            (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function,
             JustLiteral lit,
             HasApply atom,
             IsTerm term) =>
            (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
         -> (Set (Set lit) -> Bool)
         -> Set (Set lit)
         -> Set term
         -> Set (function, Int)
         -> [TVarOf term]
         -> Int
         -> Set (Set lit)
         -> Set [term]
         -> Set [term]
         -> Set [term]
herbloop :: forall lit atom function v term.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit,
 HasApply atom, IsTerm term) =>
(Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit) -> Bool
tfn Set (Set lit)
fl0 Set term
cntms Set (function, Int)
fns [TVarOf term]
fvs Int
n Set (Set lit)
fl Set [term]
tried Set [term]
tuples =
  let debug :: Set [term] -> Set [term]
debug Set [term]
x = String -> Set [term] -> Set [term]
forall a. String -> a -> a
trace (Int -> String
forall a. Show a => a -> String
show (Set [term] -> Int
forall a. Set a -> Int
size Set [term]
tried) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ground instances tried; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Set (Set lit) -> Int
forall a. Set a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Set (Set lit)
fl) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" items in list") Set [term]
x in
  case Set [term] -> Maybe ([term], Set [term])
forall a. Set a -> Maybe (a, Set a)
Set.minView (Set [term] -> Set [term]
debug Set [term]
tuples) of
    Maybe ([term], Set [term])
Nothing ->
          let newtups :: Set [term]
newtups = Set term -> Set (function, Int) -> Int -> Int -> Set [term]
forall v term f.
(v ~ TVarOf term, f ~ FunOf term, IsTerm term) =>
Set term -> Set (f, Int) -> Int -> Int -> Set [term]
groundtuples Set term
cntms Set (function, Int)
fns Int
n ([v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
[TVarOf term]
fvs) in
          (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
forall lit atom function v term.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit,
 HasApply atom, IsTerm term) =>
(Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit) -> Bool
tfn Set (Set lit)
fl0 Set term
cntms Set (function, Int)
fns [TVarOf term]
fvs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Set (Set lit)
fl Set [term]
tried Set [term]
newtups
    Just ([term]
tup, Set [term]
tups) ->
        let fpf' :: Map v term
fpf' = [(v, term)] -> Map v term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([v] -> [term] -> [(v, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
[TVarOf term]
fvs [term]
tup) in
        let fl' :: Set (Set lit)
fl' = Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit)
fl0 (Map v term -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
 term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst Map v term
fpf') Set (Set lit)
fl in
        if Bool -> Bool
not (Set (Set lit) -> Bool
tfn Set (Set lit)
fl') then [term] -> Set [term] -> Set [term]
forall a. Ord a => a -> Set a -> Set a
Set.insert [term]
tup Set [term]
tried
        else (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
forall lit atom function v term.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit,
 HasApply atom, IsTerm term) =>
(Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit) -> Bool
tfn Set (Set lit)
fl0 Set term
cntms Set (function, Int)
fns [TVarOf term]
fvs Int
n Set (Set lit)
fl' ([term] -> Set [term] -> Set [term]
forall a. Ord a => a -> Set a -> Set a
Set.insert [term]
tup Set [term]
tried) Set [term]
tups

-- | Hence a simple Gilmore-type procedure.
gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function,
                 JustLiteral lit, Ord lit,
                 HasApply atom,
                 IsTerm term) =>
                Set (Set lit)
             -> Set term
             -> Set (function, Int)
             -> [TVarOf term]
             -> Int
             -> Set (Set lit)
             -> Set [term]
             -> Set [term]
             -> Set [term]
gilmore_loop :: forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 HasApply atom, IsTerm term) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
gilmore_loop =
    (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
forall lit atom function v term.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit,
 HasApply atom, IsTerm term) =>
(Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
forall {lit} {a}.
(IsLiteral lit, Ord lit) =>
Set (Set a) -> (a -> lit) -> Set (Set lit) -> Set (Set lit)
mfn (Bool -> Bool
not (Bool -> Bool) -> (Set (Set lit) -> Bool) -> Set (Set lit) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set lit) -> Bool
forall a. Set a -> Bool
Set.null)
    where
      mfn :: Set (Set a) -> (a -> lit) -> Set (Set lit) -> Set (Set lit)
mfn Set (Set a)
djs0 a -> lit
ifn Set (Set lit)
djs = (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set lit -> Bool) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) (Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib ((Set a -> Set lit) -> Set (Set a) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> lit) -> Set a -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> lit
ifn) Set (Set a)
djs0) Set (Set lit)
djs)

gilmore :: forall fof atom term v function.
           (IsFirstOrder fof, Ord fof, HasSkolem function,
            atom ~ AtomOf fof,
            term ~ TermOf atom,
            function ~ FunOf term,
            v ~ TVarOf term,
            v ~ SVarOf function) =>
           fof -> Int
gilmore :: forall fof atom term v function.
(IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
 v ~ SVarOf function) =>
fof -> Int
gilmore fof
fm =
  let (PFormula atom
sfm :: PFormula atom) = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf fof -> AtomOf (PFormula atom))
-> fof -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm))) in
  let fvs :: [v]
fvs = Set v -> [v]
forall a. Set a -> [a]
Set.toList ((AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ AtomOf (PFormula atom)
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set v
s (fof -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf fof -> fof
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf fof
AtomOf (PFormula atom)
a :: fof))) PFormula atom
sfm (Set v
forall a. Set a
Set.empty))
      (Set (function, Int)
consts,Set (function, Int)
fns) = PFormula atom -> (Set (function, Int), Set (function, Int))
forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns PFormula atom
sfm in
  let cntms :: Set term
cntms = ((function, Int) -> term) -> Set (function, Int) -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ (function
c,Int
_) -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
c []) Set (function, Int)
consts in
  Set [term] -> Int
forall a. Set a -> Int
Set.size (Set (Set (LFormula atom))
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set (LFormula atom))
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 HasApply atom, IsTerm term) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
gilmore_loop ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
sfm :: Set (Set (LFormula atom))) Set term
cntms Set (function, Int)
fns ([v]
[TVarOf term]
fvs) Int
0 (Set (LFormula atom) -> Set (Set (LFormula atom))
forall a. a -> Set a
Set.singleton Set (LFormula atom)
forall a. Set a
Set.empty) Set [term]
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty)

-- | First example and a little tracing.
test01 :: Test
test01 :: Test
test01 =
    let fm :: Formula
fm = [fof| exists x. (forall y. p(x) ==> p(y)) |]
        expected :: Int
expected = Int
2
    in
    Assertion -> Test
TestCase (HasCallStack => String -> Assertion
String -> Assertion
assertString (case Formula -> Int
forall fof atom term v function.
(IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
 v ~ SVarOf function) =>
fof -> Int
gilmore Formula
fm of
                              Int
r | Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
expected -> String
""
                              Int
r -> String
"gilmore(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
fm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
expected))

-- -------------------------------------------------------------------------
-- Quick example.
-- -------------------------------------------------------------------------

p24 :: Test
p24 :: Test
p24 =
     let label :: String
label = String
"gilmore p24 (p. 160): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
fm
         fm :: Formula
fm = [fof|~(exists x. (U(x) & Q(x))) &
                    (forall x. (P(x) ==> Q(x) | R(x))) &
                   ~(exists x. (P(x) ==> (exists x. Q(x)))) &
                    (forall x. (Q(x) & R(x) ==> U(x)))
                       ==> (exists x. (P(x) & R(x)))|] in
    String -> Test -> Test
TestLabel String
label (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Int -> Int -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
label Int
1 (Formula -> Int
forall fof atom term v function.
(IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
 v ~ SVarOf function) =>
fof -> Int
gilmore Formula
fm)

-- | Slightly less easy example.  Expected output:
-- 
-- 0 ground instances tried; 1 items in list
-- 0 ground instances tried; 1 items in list
-- 1 ground instances tried; 13 items in list
-- 1 ground instances tried; 13 items in list
-- 2 ground instances tried; 57 items in list
-- 3 ground instances tried; 84 items in list
-- 4 ground instances tried; 405 items in list
p45fm :: Formula
p45fm :: Formula
p45fm =      [fof| (((forall x.
                      ((P(x) & (forall y. ((G(y) & H(x,y)) ==> J(x,y)))) ==>
                       (forall y. ((G(y) & H(x,y)) ==> R(y))))) &
                     ((~(exists y. (L(y) & R(y)))) &
                      (exists x.
                       (P(x) &
                        ((forall y. (H(x,y) ==> L(y))) &
                         (forall y. ((G(y) & H(x,y)) ==> J(x,y)))))))) ==>
                    (exists x. (P(x) & (~(exists y. (G(y) & H(x,y))))))) |]
p45 :: Test
p45 :: Test
p45 = String -> Test -> Test
TestLabel String
"gilmore p45" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Int -> Int -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"gilmore p45" Int
5 (Formula -> Int
forall fof atom term v function.
(IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
 v ~ SVarOf function) =>
fof -> Int
gilmore Formula
p45fm)
{-
let p24 = gilmore
 <<~(exists x. U(x) /\ Q(x)) /\
   (forall x. P(x) ==> Q(x) \/ R(x)) /\
   ~(exists x. P(x) ==> (exists x. Q(x))) /\
   (forall x. Q(x) /\ R(x) ==> U(x))
   ==> (exists x. P(x) /\ R(x))>>;;
-}
{-
-- -------------------------------------------------------------------------
-- Slightly less easy example.
-- -------------------------------------------------------------------------

let p45 = gilmore
 <<(forall x. P(x) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y))
              ==> (forall y. G(y) /\ H(x,y) ==> R(y))) /\
   ~(exists y. L(y) /\ R(y)) /\
   (exists x. P(x) /\ (forall y. H(x,y) ==> L(y)) /\
                      (forall y. G(y) /\ H(x,y) ==> J(x,y)))
   ==> (exists x. P(x) /\ ~(exists y. G(y) /\ H(x,y)))>>;;
END_INTERACTIVE;;
-}
-- -------------------------------------------------------------------------
-- Apparently intractable example.
-- -------------------------------------------------------------------------

{-

let p20 = gilmore
 <<(forall x y. exists z. forall w. P(x) /\ Q(y) ==> R(z) /\ U(w))
   ==> (exists x y. P(x) /\ Q(y)) ==> (exists z. R(z))>>;;

-}

-- | The Davis-Putnam procedure for first order logic.
dp_mfn :: Ord b => Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn :: forall b a.
Ord b =>
Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn Set (Set a)
cjs0 a -> b
ifn Set (Set b)
cjs = Set (Set b) -> Set (Set b) -> Set (Set b)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((Set a -> Set b) -> Set (Set a) -> Set (Set b)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> b) -> Set a -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> b
ifn) Set (Set a)
cjs0) Set (Set b)
cjs

dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function,
            JustLiteral lit, Ord lit,
            HasApply atom,
            IsTerm term) =>
           Set (Set lit)
        -> Set term
        -> Set (function, Int)
        -> [v]
        -> Int
        -> Set (Set lit)
        -> Set [term]
        -> Set [term]
        -> Set [term]
dp_loop :: forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 HasApply atom, IsTerm term) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
dp_loop = (Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
forall lit atom function v term.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit,
 HasApply atom, IsTerm term) =>
(Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> (Set (Set lit) -> Bool)
-> Set (Set lit)
-> Set term
-> Set (function, Int)
-> [TVarOf term]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
herbloop Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
forall b a.
Ord b =>
Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll

davisputnam :: forall formula atom term v function.
               (IsFirstOrder formula, Ord formula, HasSkolem function,
                atom ~ AtomOf formula,
                term ~ TermOf atom,
                function ~ FunOf term,
                v ~ TVarOf term,
                v ~ SVarOf function) =>
               formula -> Int
davisputnam :: forall fof atom term v function.
(IsFirstOrder fof, Ord fof, HasSkolem function, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term,
 v ~ SVarOf function) =>
fof -> Int
davisputnam formula
fm =
  let (PFormula atom
sfm :: PFormula atom) = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf formula -> AtomOf (PFormula atom))
-> formula -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf formula -> AtomOf (PFormula atom)
forall a. a -> a
id (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) in
  let fvs :: [v]
fvs = Set v -> [v]
forall a. Set a -> [a]
Set.toList ((AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ AtomOf (PFormula atom)
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
AtomOf (PFormula atom)
a :: formula)) Set v
s) PFormula atom
sfm Set v
forall a. Set a
Set.empty)
      (Set (function, Int)
consts,Set (function, Int)
fns) = PFormula atom -> (Set (function, Int), Set (function, Int))
forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns PFormula atom
sfm in
  let cntms :: Set term
cntms = ((function, Int) -> term) -> Set (function, Int) -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ (function
c,Int
_) -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
c []) Set (function, Int)
consts in
  Set [term] -> Int
forall a. Set a -> Int
Set.size (Set (Set (LFormula atom))
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set (LFormula atom))
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 HasApply atom, IsTerm term) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
dp_loop ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
sfm :: Set (Set (LFormula atom))) Set term
cntms Set (function, Int)
fns [v]
fvs Int
0 Set (Set (LFormula atom))
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty)

{-
-- | Show how much better than the Gilmore procedure this can be.
START_INTERACTIVE;;
let p20 = davisputnam
 <<(forall x y. exists z. forall w. P(x) /\ Q(y) ==> R(z) /\ U(w))
   ==> (exists x y. P(x) /\ Q(y)) ==> (exists z. R(z))>>;;
END_INTERACTIVE;;
-}

-- | Show how few of the instances we really need. Hence unification!
davisputnam' :: forall formula atom term v function.
                (IsFirstOrder formula, Ord formula, HasSkolem function,
                 atom ~ AtomOf formula,
                 term ~ TermOf atom,
                 function ~ FunOf term,
                 v ~ TVarOf term,
                 v ~ SVarOf function) =>
                formula -> formula -> formula -> Int
davisputnam' :: forall formula atom term v function.
(IsFirstOrder formula, Ord formula, HasSkolem function,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> formula -> formula -> Int
davisputnam' formula
_ formula
_ formula
fm =
    let (PFormula atom
sfm :: PFormula atom) = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf formula -> AtomOf (PFormula atom))
-> formula -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf formula -> AtomOf (PFormula atom)
forall a. a -> a
id (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) in
    let fvs :: [v]
fvs = Set v -> [v]
forall a. Set a -> [a]
Set.toList ((AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ (AtomOf formula
a :: AtomOf formula) Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
a :: formula)) Set v
s) PFormula atom
sfm Set v
forall a. Set a
Set.empty)
        consts :: Set (function, Arity)
        fns :: Set (function, Arity)
        (Set (function, Int)
consts,Set (function, Int)
fns) = PFormula atom -> (Set (function, Int), Set (function, Int))
forall atom fof term function.
(atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 IsFormula fof, HasApply atom, Ord function) =>
fof -> (Set (function, Int), Set (function, Int))
herbfuns PFormula atom
sfm in
    let cntms :: Set (TermOf (AtomOf formula))
        cntms :: Set (TermOf (AtomOf formula))
cntms = ((function, Int) -> term) -> Set (function, Int) -> Set term
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ (function
c,Int
_) -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp function
FunOf term
c []) Set (function, Int)
consts in
    Set [term] -> Int
forall a. Set a -> Int
Set.size (Set (Set (LFormula atom))
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set (LFormula atom))
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 IsTerm term, HasApply atom) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
dp_refine_loop ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
sfm :: Set (Set (LFormula atom))) Set term
Set (TermOf (AtomOf formula))
cntms Set (function, Int)
fns [v]
fvs Int
0 Set (Set (LFormula atom))
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty Set [term]
forall a. Set a
Set.empty)

-- | Try to cut out useless instantiations in final result.
dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function,
                   JustLiteral lit, Ord lit,
                   IsTerm term,
                   HasApply atom) =>
                  Set (Set lit)
               -> Set term
               -> Set (function, Int)
               -> [v]
               -> Int
               -> Set (Set lit)
               -> Set [term]
               -> Set [term]
               -> Set [term]
dp_refine_loop :: forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 IsTerm term, HasApply atom) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
dp_refine_loop Set (Set lit)
cjs0 Set term
cntms Set (function, Int)
fns [v]
fvs Int
n Set (Set lit)
cjs Set [term]
tried Set [term]
tuples =
    let tups :: Set [term]
tups = Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
forall atom lit term function v.
(atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function, JustLiteral lit, Ord lit,
 HasApply atom, IsTerm term) =>
Set (Set lit)
-> Set term
-> Set (function, Int)
-> [v]
-> Int
-> Set (Set lit)
-> Set [term]
-> Set [term]
-> Set [term]
dp_loop Set (Set lit)
cjs0 Set term
cntms Set (function, Int)
fns [v]
fvs Int
n Set (Set lit)
cjs Set [term]
tried Set [term]
tuples in
    Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
 HasApply atom, JustLiteral lit, Ord lit, IsTerm term) =>
Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
dp_refine Set (Set lit)
cjs0 [v]
[TVarOf term]
fvs Set [term]
tups Set [term]
forall a. Set a
Set.empty

dp_refine :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
              HasApply atom,
              JustLiteral lit, Ord lit,
              IsTerm term
             ) => Set (Set lit) -> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
dp_refine :: forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
 HasApply atom, JustLiteral lit, Ord lit, IsTerm term) =>
Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
dp_refine Set (Set lit)
cjs0 [TVarOf term]
fvs Set [term]
dknow Set [term]
need =
    case Set [term] -> Maybe ([term], Set [term])
forall a. Set a -> Maybe (a, Set a)
Set.minView Set [term]
dknow of
      Maybe ([term], Set [term])
Nothing -> Set [term]
need
      Just ([term]
cl, Set [term]
dknow') ->
          let mfn :: [term] -> Set (Set lit) -> Set (Set lit)
mfn = Set (Set lit) -> (lit -> lit) -> Set (Set lit) -> Set (Set lit)
forall b a.
Ord b =>
Set (Set a) -> (a -> b) -> Set (Set b) -> Set (Set b)
dp_mfn Set (Set lit)
cjs0 ((lit -> lit) -> Set (Set lit) -> Set (Set lit))
-> ([term] -> lit -> lit)
-> [term]
-> Set (Set lit)
-> Set (Set lit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
 term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst (Map v term -> lit -> lit)
-> ([term] -> Map v term) -> [term] -> lit -> lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(v, term)] -> Map v term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(v, term)] -> Map v term)
-> ([term] -> [(v, term)]) -> [term] -> Map v term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [v] -> [term] -> [(v, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
[TVarOf term]
fvs in
          let flag :: Bool
flag = Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (([term] -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set [term] -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold [term] -> Set (Set lit) -> Set (Set lit)
mfn Set (Set lit)
forall a. Set a
Set.empty (Set [term] -> Set [term] -> Set [term]
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set [term]
need Set [term]
dknow')) in
          Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
forall atom lit term v.
(atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term,
 HasApply atom, JustLiteral lit, Ord lit, IsTerm term) =>
Set (Set lit)
-> [TVarOf term] -> Set [term] -> Set [term] -> Set [term]
dp_refine Set (Set lit)
cjs0 [TVarOf term]
fvs Set [term]
dknow' (if Bool
flag then [term] -> Set [term] -> Set [term]
forall a. Ord a => a -> Set a -> Set a
Set.insert [term]
cl Set [term]
need else Set [term]
need)

{-
START_INTERACTIVE;;
let p36 = davisputnam'
 <<(forall x. exists y. P(x,y)) /\
   (forall x. exists y. G(x,y)) /\
   (forall x y. P(x,y) \/ G(x,y)
                ==> (forall z. P(y,z) \/ G(y,z) ==> H(x,z)))
   ==> (forall x. exists y. H(x,y))>>;;

let p29 = davisputnam'
 <<(exists x. P(x)) /\ (exists x. G(x)) ==>
   ((forall x. P(x) ==> H(x)) /\ (forall x. G(x) ==> J(x)) <=>
    (forall x y. P(x) /\ G(y) ==> H(x) /\ J(y)))>>;;
END_INTERACTIVE;;
-}

testHerbrand :: Test
testHerbrand :: Test
testHerbrand = String -> Test -> Test
TestLabel String
"Herbrand" ([Test] -> Test
TestList [Test
test01, Test
p24, Test
p45])