-- | Basic stuff for first order logic.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Logic.ATP.FOL
    ( IsFirstOrder
    -- * Semantics
    , Interp
    , holds
    , holdsQuantified
    , holdsAtom
    , termval
    -- * Free Variables
    , var
    , fv, fva, fvt
    , generalize
    -- * Substitution
    , subst, substq, asubst, tsubst, lsubst
    , bool_interp
    , mod_interp
    -- * Concrete instances of formula types for use in unit tests.
    , ApFormula, EqFormula
    -- * Tests
    , testFOL
    ) where

import Data.Logic.ATP.Apply (ApAtom, HasApply(PredOf, TermOf, overterms, onterms), Predicate)
import Data.Logic.ATP.Equate ((.=.), EqAtom, foldEquate, HasEquate)
import Data.Logic.ATP.Formulas (fromBool, IsFormula(..))
import Data.Logic.ATP.Lib (setAny, tryApplyD, undefine, (|->))
import Data.Logic.ATP.Lit ((.~.), foldLiteral, JustLiteral)
import Data.Logic.ATP.Pretty (prettyShow)
import Data.Logic.ATP.Prop (BinOp(..), IsPropositional((.&.), (.|.), (.=>.), (.<=>.)))
import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, IsQuantified(VarOf), Quant((:!:), (:?:)), QFormula)
import Data.Logic.ATP.Term (FName, foldTerm, IsTerm(FunOf, TVarOf, vt, fApp), V, variant)
import Data.Map.Strict as Map (empty, fromList, insert, lookup, Map)
import Data.Maybe (fromMaybe)
import Data.Set as Set (difference, empty, fold, fromList, member, Set, singleton, union, unions)
import Data.String (IsString(fromString))
import Prelude hiding (pred)
import Test.HUnit

-- | Combine IsQuantified, HasApply, IsTerm, and make sure the term is
-- using the same variable type as the formula.
class (IsQuantified formula,
       HasApply (AtomOf formula),
       IsTerm (TermOf (AtomOf formula)),
       VarOf formula ~ TVarOf (TermOf (AtomOf formula)))
    => IsFirstOrder formula

-- | A formula type with no equality predicate
type ApFormula = QFormula V ApAtom
instance IsFirstOrder ApFormula

-- | A formula type with equality predicate
type EqFormula = QFormula V EqAtom
instance IsFirstOrder EqFormula

{-
(* Trivial example of "x + y < z".                                           *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
Atom(R("<",[Fn("+",[Var "x"; Var "y"]); Var "z"]));;
END_INTERACTIVE;;

(* ------------------------------------------------------------------------- *)
(* Parsing of terms.                                                         *)
(* ------------------------------------------------------------------------- *)

let is_const_name s = forall numeric (explode s) or s = "nil";;

let rec parse_atomic_term vs inp =
  match inp with
    [] -> failwith "term expected"
  | "("::rest -> parse_bracketed (parse_term vs) ")" rest
  | "-"::rest -> papply (fun t -> Fn("-",[t])) (parse_atomic_term vs rest)
  | f::"("::")"::rest -> Fn(f,[]),rest
  | f::"("::rest ->
      papply (fun args -> Fn(f,args))
             (parse_bracketed (parse_list "," (parse_term vs)) ")" rest)
  | a::rest ->
      (if is_const_name a & not(mem a vs) then Fn(a,[]) else Var a),rest

and parse_term vs inp =
  parse_right_infix "::" (fun (e1,e2) -> Fn("::",[e1;e2]))
    (parse_right_infix "+" (fun (e1,e2) -> Fn("+",[e1;e2]))
       (parse_left_infix "-" (fun (e1,e2) -> Fn("-",[e1;e2]))
          (parse_right_infix "*" (fun (e1,e2) -> Fn("*",[e1;e2]))
             (parse_left_infix "/" (fun (e1,e2) -> Fn("/",[e1;e2]))
                (parse_left_infix "^" (fun (e1,e2) -> Fn("^",[e1;e2]))
                   (parse_atomic_term vs)))))) inp;;

let parset = make_parser (parse_term []);;

(* ------------------------------------------------------------------------- *)
(* Parsing of formulas.                                                      *)
(* ------------------------------------------------------------------------- *)

let parse_infix_atom vs inp =
  let tm,rest = parse_term vs inp in
  if exists (nextin rest) ["="; "<"; "<="; ">"; ">="] then
        papply (fun tm' -> Atom(R(hd rest,[tm;tm'])))
               (parse_term vs (tl rest))
  else failwith "";;

let parse_atom vs inp =
  try parse_infix_atom vs inp with Failure _ ->
  match inp with
  | p::"("::")"::rest -> Atom(R(p,[])),rest
  | p::"("::rest ->
      papply (fun args -> Atom(R(p,args)))
             (parse_bracketed (parse_list "," (parse_term vs)) ")" rest)
  | p::rest when p <> "(" -> Atom(R(p,[])),rest
  | _ -> failwith "parse_atom";;

let parse = make_parser
  (parse_formula (parse_infix_atom,parse_atom) []);;

(* ------------------------------------------------------------------------- *)
(* Set up parsing of quotations.                                             *)
(* ------------------------------------------------------------------------- *)

let default_parser = parse;;

let secondary_parser = parset;;

{-
(* ------------------------------------------------------------------------- *)
(* Example.                                                                  *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
<<(forall x. x < 2 ==> 2 * x <= 3) \/ false>>;;

<<|2 * x|>>;;
END_INTERACTIVE;;
-}

(* ------------------------------------------------------------------------- *)
(* Printing of terms.                                                        *)
(* ------------------------------------------------------------------------- *)

let rec print_term prec fm =
  match fm with
    Var x -> print_string x
  | Fn("^",[tm1;tm2]) -> print_infix_term true prec 24 "^" tm1 tm2
  | Fn("/",[tm1;tm2]) -> print_infix_term true prec 22 " /" tm1 tm2
  | Fn("*",[tm1;tm2]) -> print_infix_term false prec 20 " *" tm1 tm2
  | Fn("-",[tm1;tm2]) -> print_infix_term true prec 18 " -" tm1 tm2
  | Fn("+",[tm1;tm2]) -> print_infix_term false prec 16 " +" tm1 tm2
  | Fn("::",[tm1;tm2]) -> print_infix_term false prec 14 "::" tm1 tm2
  | Fn(f,args) -> print_fargs f args

and print_fargs f args =
  print_string f;
  if args = [] then () else
   (print_string "(";
    open_box 0;
    print_term 0 (hd args); print_break 0 0;
    do_list (fun t -> print_string ","; print_break 0 0; print_term 0 t)
            (tl args);
    close_box();
    print_string ")")

and print_infix_term isleft oldprec newprec sym p q =
  if oldprec > newprec then (print_string "("; open_box 0) else ();
  print_term (if isleft then newprec else newprec+1) p;
  print_string sym;
  print_break (if String.sub sym 0 1 = " " then 1 else 0) 0;
  print_term (if isleft then newprec+1 else newprec) q;
  if oldprec > newprec then (close_box(); print_string ")") else ();;

let printert tm =
  open_box 0; print_string "<<|";
  open_box 0; print_term 0 tm; close_box();
  print_string "|>>"; close_box();;

#install_printer printert;;

(* ------------------------------------------------------------------------- *)
(* Printing of formulas.                                                     *)
(* ------------------------------------------------------------------------- *)

let print_atom prec (R(p,args)) =
  if mem p ["="; "<"; "<="; ">"; ">="] & length args = 2
  then print_infix_term false 12 12 (" "^p) (el 0 args) (el 1 args)
  else print_fargs p args;;

let print_fol_formula = print_qformula print_atom;;

#install_printer print_fol_formula;;

(* ------------------------------------------------------------------------- *)
(* Examples in the main text.                                                *)
(* ------------------------------------------------------------------------- *)

START_INTERACTIVE;;
<<forall x y. exists z. x < z /\ y < z>>;;

<<~(forall x. P(x)) <=> exists y. ~P(y)>>;;
END_INTERACTIVE;;
-}

-- | Specify the domain of a formula interpretation, and how to
-- interpret its functions and predicates.
data Interp function predicate d
    = Interp { forall function predicate d. Interp function predicate d -> [d]
domain :: [d]
             , forall function predicate d.
Interp function predicate d -> function -> [d] -> d
funcApply :: function -> [d] -> d
             , forall function predicate d.
Interp function predicate d -> predicate -> [d] -> Bool
predApply :: predicate -> [d] -> Bool
             , forall function predicate d.
Interp function predicate d -> d -> d -> Bool
eqApply :: d -> d -> Bool }

-- | The holds function computes the value of a formula for a finite domain.
class FiniteInterpretation a function predicate v dom where
    holds :: Interp function predicate dom -> Map v dom -> a -> Bool

-- | Implementation of holds for IsQuantified formulas.
holdsQuantified :: forall formula function predicate dom.
                   (IsQuantified formula,
                    FiniteInterpretation (AtomOf formula) function predicate (VarOf formula) dom,
                    FiniteInterpretation formula function predicate (VarOf formula) dom) =>
                   Interp function predicate dom -> Map (VarOf formula) dom -> formula -> Bool
holdsQuantified :: forall formula function predicate dom.
(IsQuantified formula,
 FiniteInterpretation
   (AtomOf formula) function predicate (VarOf formula) dom,
 FiniteInterpretation
   formula function predicate (VarOf formula) dom) =>
Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
holdsQuantified Interp function predicate dom
m Map (VarOf formula) dom
v formula
fm =
    (Quant -> VarOf formula -> formula -> Bool)
-> (formula -> BinOp -> formula -> Bool)
-> (formula -> Bool)
-> (Bool -> Bool)
-> (AtomOf formula -> Bool)
-> formula
-> Bool
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> Bool
qu formula -> BinOp -> formula -> Bool
co formula -> Bool
ne Bool -> Bool
forall {p}. p -> p
tf AtomOf formula -> Bool
at formula
fm
    where
      qu :: Quant -> VarOf formula -> formula -> Bool
qu Quant
(:!:) VarOf formula
x formula
p = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((dom -> Bool) -> [dom] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\dom
a -> Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m (VarOf formula
-> dom -> Map (VarOf formula) dom -> Map (VarOf formula) dom
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarOf formula
x dom
a Map (VarOf formula) dom
v) formula
p) (Interp function predicate dom -> [dom]
forall function predicate d. Interp function predicate d -> [d]
domain Interp function predicate dom
m)) -- >>= return . any (== True)
      qu Quant
(:?:) VarOf formula
x formula
p = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ((dom -> Bool) -> [dom] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\dom
a -> Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m (VarOf formula
-> dom -> Map (VarOf formula) dom -> Map (VarOf formula) dom
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarOf formula
x dom
a Map (VarOf formula) dom
v) formula
p) (Interp function predicate dom -> [dom]
forall function predicate d. Interp function predicate d -> [d]
domain Interp function predicate dom
m)) -- return . all (== True)?
      ne :: formula -> Bool
ne formula
p = Bool -> Bool
not (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p)
      co :: formula -> BinOp -> formula -> Bool
co formula
p BinOp
(:&:) formula
q = (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
&& (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
      co formula
p BinOp
(:|:) formula
q = (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
|| (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
      co formula
p BinOp
(:=>:) formula
q = Bool -> Bool
not (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
|| (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
      co formula
p BinOp
(:<=>:) formula
q = (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
p) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v formula
q)
      tf :: p -> p
tf p
x = p
x
      at :: AtomOf formula -> Bool
at = (Interp function predicate dom
-> Map (VarOf formula) dom -> AtomOf formula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp function predicate dom
m Map (VarOf formula) dom
v :: AtomOf formula -> Bool)

-- | Implementation of holds for atoms with equate predicates.
holdsAtom :: (HasEquate atom, IsTerm term, Eq dom,
              term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) =>
             Interp function predicate dom -> Map v dom -> atom -> Bool
holdsAtom :: forall atom term dom v function predicate.
(HasEquate atom, IsTerm term, Eq dom, term ~ TermOf atom,
 v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) =>
Interp function predicate dom -> Map v dom -> atom -> Bool
holdsAtom Interp function predicate dom
m Map v dom
v atom
at = (TermOf atom -> TermOf atom -> Bool)
-> (PredOf atom -> [TermOf atom] -> Bool) -> atom -> Bool
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
t1 TermOf atom
t2 -> Interp function predicate dom -> dom -> dom -> Bool
forall function predicate d.
Interp function predicate d -> d -> d -> Bool
eqApply Interp function predicate dom
m (Interp function predicate dom -> Map v dom -> term -> dom
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate dom
m Map v dom
v term
TermOf atom
t1) (Interp function predicate dom -> Map v dom -> term -> dom
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate dom
m Map v dom
v term
TermOf atom
t2))
                                (\PredOf atom
r [TermOf atom]
args -> Interp function predicate dom -> predicate -> [dom] -> Bool
forall function predicate d.
Interp function predicate d -> predicate -> [d] -> Bool
predApply Interp function predicate dom
m predicate
PredOf atom
r ((term -> dom) -> [term] -> [dom]
forall a b. (a -> b) -> [a] -> [b]
map (Interp function predicate dom -> Map v dom -> term -> dom
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate dom
m Map v dom
v) [term]
[TermOf atom]
args)) atom
at

termval :: (IsTerm term, v ~ TVarOf term, function ~ FunOf term) => Interp function predicate r -> Map v r -> term -> r
termval :: forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate r
m Map v r
v term
tm =
    (TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm (\TVarOf term
x -> r -> Maybe r -> r
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> r
forall a. HasCallStack => [Char] -> a
error ([Char]
"Undefined variable: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ v -> [Char]
forall a. Show a => a -> [Char]
show v
TVarOf term
x)) (v -> Map v r -> Maybe r
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
TVarOf term
x Map v r
v))
             (\FunOf term
f [term]
args -> Interp function predicate r -> function -> [r] -> r
forall function predicate d.
Interp function predicate d -> function -> [d] -> d
funcApply Interp function predicate r
m function
FunOf term
f ((term -> r) -> [term] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map (Interp function predicate r -> Map v r -> term -> r
forall term v function predicate r.
(IsTerm term, v ~ TVarOf term, function ~ FunOf term) =>
Interp function predicate r -> Map v r -> term -> r
termval Interp function predicate r
m Map v r
v) [term]
args)) term
tm

{-
START_INTERACTIVE;;
holds bool_interp undefined <<forall x. (x = 0) \/ (x = 1)>>;;

holds (mod_interp 2) undefined <<forall x. (x = 0) \/ (x = 1)>>;;

holds (mod_interp 3) undefined <<forall x. (x = 0) \/ (x = 1)>>;;

let fm = <<forall x. ~(x = 0) ==> exists y. x * y = 1>>;;

filter (fun n -> holds (mod_interp n) undefined fm) (1--45);;

holds (mod_interp 3) undefined <<(forall x. x = 0) ==> 1 = 0>>;;
holds (mod_interp 3) undefined <<forall x. x = 0 ==> 1 = 0>>;;
END_INTERACTIVE;;
-}

-- | Examples of particular interpretations.
bool_interp :: Interp FName Predicate Bool
bool_interp :: Interp FName Predicate Bool
bool_interp =
    [Bool]
-> (FName -> [Bool] -> Bool)
-> (Predicate -> [Bool] -> Bool)
-> (Bool -> Bool -> Bool)
-> Interp FName Predicate Bool
forall function predicate d.
[d]
-> (function -> [d] -> d)
-> (predicate -> [d] -> Bool)
-> (d -> d -> Bool)
-> Interp function predicate d
Interp [Bool
False, Bool
True] FName -> [Bool] -> Bool
forall {a}. (Eq a, IsString a, Show a) => a -> [Bool] -> Bool
func Predicate -> [Bool] -> Bool
forall {a} {p} {a}. Show a => a -> p -> a
pred Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)
    where
      func :: a -> [Bool] -> Bool
func a
f [] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"False" = Bool
False
      func a
f [] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"True" = Bool
True
      func a
f [Bool
x,Bool
y] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"+" = Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
y
      func a
f [Bool
x,Bool
y] | a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> a
forall a. IsString a => [Char] -> a
fromString [Char]
"*" = Bool
x Bool -> Bool -> Bool
&& Bool
y
      func a
f [Bool]
_ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error ([Char]
"bool_interp - uninterpreted function: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
f)
      pred :: a -> p -> a
pred a
p p
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"bool_interp - uninterpreted predicate: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
p)

mod_interp :: Int -> Interp FName Predicate Int
mod_interp :: Int -> Interp FName Predicate Int
mod_interp Int
n =
    [Int]
-> (FName -> [Int] -> Int)
-> (Predicate -> [Int] -> Bool)
-> (Int -> Int -> Bool)
-> Interp FName Predicate Int
forall function predicate d.
[d]
-> (function -> [d] -> d)
-> (predicate -> [d] -> Bool)
-> (d -> d -> Bool)
-> Interp function predicate d
Interp [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] FName -> [Int] -> Int
func Predicate -> [Int] -> Bool
forall {a} {p} {a}. Show a => a -> p -> a
pred Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==)
    where
      func :: FName -> [Int] -> Int
func FName
f [] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"0" = Int
0
      func FName
f [] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"1" = Int
1 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n
      func FName
f [Int
x,Int
y] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"+" = (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n
      func FName
f [Int
x,Int
y] | FName
f FName -> FName -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> FName
forall a. IsString a => [Char] -> a
fromString [Char]
"*" = (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
y) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n
      func FName
f [Int]
_ = [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char]
"mod_interp - uninterpreted function: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FName -> [Char]
forall a. Show a => a -> [Char]
show FName
f)
      pred :: a -> p -> a
pred a
p p
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"mod_interp - uninterpreted predicate: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
p)

instance Eq dom => FiniteInterpretation EqFormula FName Predicate V dom where holds :: Interp FName Predicate dom -> Map V dom -> EqFormula -> Bool
holds = Interp FName Predicate dom -> Map V dom -> EqFormula -> Bool
Interp FName Predicate dom
-> Map (VarOf EqFormula) dom -> EqFormula -> Bool
forall formula function predicate dom.
(IsQuantified formula,
 FiniteInterpretation
   (AtomOf formula) function predicate (VarOf formula) dom,
 FiniteInterpretation
   formula function predicate (VarOf formula) dom) =>
Interp function predicate dom
-> Map (VarOf formula) dom -> formula -> Bool
holdsQuantified
instance Eq dom => FiniteInterpretation EqAtom FName Predicate V dom where holds :: Interp FName Predicate dom
-> Map V dom -> FOL Predicate FTerm -> Bool
holds = Interp FName Predicate dom
-> Map V dom -> FOL Predicate FTerm -> Bool
forall atom term dom v function predicate.
(HasEquate atom, IsTerm term, Eq dom, term ~ TermOf atom,
 v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) =>
Interp function predicate dom -> Map v dom -> atom -> Bool
holdsAtom

test01 :: Test
test01 :: Test
test01 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds bool test (p. 126)" Bool
expected Bool
input
    where input :: Bool
input = Interp FName Predicate Bool -> Map V Bool -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds Interp FName Predicate Bool
bool_interp (Map V Bool
forall k a. Map k a
Map.empty :: Map V Bool) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" ((TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x") TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"False" []) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x") TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"True" [])) :: EqFormula)
          expected :: Bool
expected = Bool
True
test02 :: Test
test02 :: Test
test02 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 1 (p. 126)" Bool
expected Bool
input
    where input :: Bool
input =  Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
2) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" []) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [])) :: EqFormula)
          expected :: Bool
expected = Bool
True
test03 :: Test
test03 :: Test
test03 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 2 (p. 126)" Bool
expected Bool
input
    where input :: Bool
input =  Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
3) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [] EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" []) :: EqFormula)
          expected :: Bool
expected = Bool
False

test04 :: Test
test04 :: Test
test04 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> [Int] -> [Int] -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 3 (p. 126)" [Int]
expected [Int]
input
    where input :: [Int]
input = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ Int
n -> Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
n) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) EqFormula
fm) [Int
1..Int
45]
                  where fm :: EqFormula
fm = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (EqFormula -> EqFormula
forall formula. IsLiteral formula => formula -> formula
(.~.) (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" []) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf EqFormula
"y" (FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"*" [TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"y"] TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [])) :: EqFormula
          expected :: [Int]
expected = [Int
1,Int
2,Int
3,Int
5,Int
7,Int
11,Int
13,Int
17,Int
19,Int
23,Int
29,Int
31,Int
37,Int
41,Int
43]

test05 :: Test
test05 :: Test
test05 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 4 (p. 129)" Bool
expected Bool
input
    where input :: Bool
input = Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
3) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) ((VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [])) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [] TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [] :: EqFormula)
          expected :: Bool
expected = Bool
True
test06 :: Test
test06 :: Test
test06 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"holds mod test 5 (p. 129)" Bool
expected Bool
input
    where input :: Bool
input = Interp FName Predicate Int -> Map V Int -> EqFormula -> Bool
forall a function predicate v dom.
FiniteInterpretation a function predicate v dom =>
Interp function predicate dom -> Map v dom -> a -> Bool
holds (Int -> Interp FName Predicate Int
mod_interp Int
3) (Map V Int
forall k a. Map k a
Map.empty :: Map V Int) (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
V
"x" TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" [] EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"1" [] TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FunOf FTerm -> [FTerm] -> FTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf FTerm
FName
"0" []) :: EqFormula)
          expected :: Bool
expected = Bool
False

-- Free variables in terms and formulas.

-- | Find the free variables in a formula.
fv :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v
fv :: forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
fm =
    (Quant -> VarOf formula -> formula -> Set v)
-> (formula -> BinOp -> formula -> Set v)
-> (formula -> Set v)
-> (Bool -> Set v)
-> (AtomOf formula -> Set v)
-> formula
-> Set v
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> VarOf formula -> formula -> Set v
Quant -> VarOf formula -> formula -> Set (VarOf formula)
forall {formula} {p}.
IsFirstOrder formula =>
p -> VarOf formula -> formula -> Set (VarOf formula)
qu formula -> BinOp -> formula -> Set v
formula -> BinOp -> formula -> Set (VarOf formula)
forall {formula} {formula} {p}.
(TVarOf (TermOf (AtomOf formula))
 ~ TVarOf (TermOf (AtomOf formula)),
 VarOf formula ~ TVarOf (TermOf (AtomOf formula)),
 IsFirstOrder formula, IsFirstOrder formula) =>
formula -> p -> formula -> Set (VarOf formula)
co formula -> Set v
formula -> Set (VarOf formula)
forall {formula}.
IsFirstOrder formula =>
formula -> Set (VarOf formula)
ne Bool -> Set v
forall {p} {a}. p -> Set a
tf AtomOf formula -> Set v
AtomOf formula -> Set (TVarOf (TermOf (AtomOf formula)))
at formula
fm
    where
      qu :: p -> VarOf formula -> formula -> Set (VarOf formula)
qu p
_ VarOf formula
x formula
p = Set (VarOf formula) -> Set (VarOf formula) -> Set (VarOf formula)
forall a. Ord a => Set a -> Set a -> Set a
difference (formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) (VarOf formula -> Set (VarOf formula)
forall a. a -> Set a
singleton VarOf formula
x)
      ne :: formula -> Set (VarOf formula)
ne formula
p = formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p
      co :: formula -> p -> formula -> Set (VarOf formula)
co formula
p p
_ formula
q = Set (VarOf formula) -> Set (VarOf formula) -> Set (VarOf formula)
forall a. Ord a => Set a -> Set a -> Set a
union (formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) (formula -> Set (VarOf formula)
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
q)
      tf :: p -> Set a
tf p
_ = Set a
forall a. Set a
Set.empty
      at :: AtomOf formula -> Set (TVarOf (TermOf (AtomOf formula)))
at = AtomOf formula -> Set (TVarOf (TermOf (AtomOf formula)))
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
atom -> Set v
fva

-- | Find all the variables in a formula.
-- var :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v
var :: (IsFormula formula, HasApply atom,
        atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>
       formula -> Set v
var :: forall formula atom term v.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula,
 term ~ TermOf atom, v ~ TVarOf term) =>
formula -> Set v
var formula
fm = (AtomOf formula -> Set v -> Set v) -> formula -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r. (AtomOf formula -> r -> r) -> formula -> r -> r
overatoms (\AtomOf formula
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (atom -> Set v
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
atom -> Set v
fva atom
AtomOf formula
a) Set v
s) formula
fm Set v
forall a. Monoid a => a
mempty

-- | Find the variables in an atom
fva :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => atom -> Set v
fva :: forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
atom -> Set v
fva = (TermOf atom -> Set v -> Set v) -> Set v -> atom -> Set v
forall atom r.
HasApply atom =>
(TermOf atom -> r -> r) -> r -> atom -> r
forall r. (TermOf atom -> r -> r) -> r -> atom -> r
overterms (\TermOf atom
t Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (term -> Set v
forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt term
TermOf atom
t) Set v
s) Set v
forall a. Monoid a => a
mempty

-- | Find the variables in a term
fvt :: (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt :: forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt term
tm = (TVarOf term -> Set v)
-> (FunOf term -> [term] -> Set v) -> term -> Set v
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> Set v
TVarOf term -> Set v
forall a. a -> Set a
singleton (\FunOf term
_ [term]
args -> [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
unions ((term -> Set v) -> [term] -> [Set v]
forall a b. (a -> b) -> [a] -> [b]
map term -> Set v
forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt [term]
args)) term
tm

-- | Universal closure of a formula.
generalize :: IsFirstOrder formula => formula -> formula
generalize :: forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm = (TVarOf (TermOf (AtomOf formula)) -> formula -> formula)
-> formula -> Set (TVarOf (TermOf (AtomOf formula))) -> formula
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold TVarOf (TermOf (AtomOf formula)) -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all formula
fm (formula -> Set (TVarOf (TermOf (AtomOf formula)))
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
fm)

test07 :: Test
test07 :: Test
test07 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> V -> V -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"variant 1 (p. 133)" V
expected V
input
    where input :: V
input = V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant V
"x" ([V] -> Set V
forall a. Ord a => [a] -> Set a
Set.fromList [V
"y", V
"z"]) :: V
          expected :: V
expected = V
"x"
test08 :: Test
test08 :: Test
test08 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> V -> V -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"variant 2 (p. 133)" V
expected V
input
    where input :: V
input = V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant V
"x" ([V] -> Set V
forall a. Ord a => [a] -> Set a
Set.fromList [V
"x", V
"y"]) :: V
          expected :: V
expected = V
"x'"
test09 :: Test
test09 :: Test
test09 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> V -> V -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual [Char]
"variant 3 (p. 133)" V
expected V
input
    where input :: V
input = V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant V
"x" ([V] -> Set V
forall a. Ord a => [a] -> Set a
Set.fromList [V
"x", V
"x'"]) :: V
          expected :: V
expected = V
"x''"

-- | Substitution in formulas, with variable renaming.
subst :: (IsFirstOrder formula, term ~ TermOf (AtomOf formula), v ~ VarOf formula) => Map v term -> formula -> formula
subst :: forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
fm =
    (Quant -> VarOf formula -> formula -> formula)
-> (formula -> BinOp -> formula -> formula)
-> (formula -> formula)
-> (Bool -> formula)
-> (AtomOf formula -> formula)
-> formula
-> formula
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> v -> formula -> formula
Quant -> VarOf formula -> formula -> formula
qu formula -> BinOp -> formula -> formula
co formula -> formula
ne Bool -> formula
forall {formula}. IsFormula formula => Bool -> formula
tf AtomOf formula -> formula
at formula
fm
    where
      qu :: Quant -> v -> formula -> formula
qu Quant
(:!:) v
x formula
p = Map v term -> (v -> formula -> formula) -> v -> formula -> formula
forall formula v term.
(IsFirstOrder formula, v ~ VarOf formula,
 term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq Map v term
subfn v -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all v
x formula
p
      qu Quant
(:?:) v
x formula
p = Map v term -> (v -> formula -> formula) -> v -> formula -> formula
forall formula v term.
(IsFirstOrder formula, v ~ VarOf formula,
 term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq Map v term
subfn v -> formula -> formula
VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists v
x formula
p
      ne :: formula -> formula
ne formula
p = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p)
      co :: formula -> BinOp -> formula -> formula
co formula
p BinOp
(:&:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
      co formula
p BinOp
(:|:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
      co formula
p BinOp
(:=>:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
      co formula
p BinOp
(:<=>:) formula
q = (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
p) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst Map v term
subfn formula
q)
      tf :: Bool -> formula
tf Bool
False = formula
forall formula. IsFormula formula => formula
false
      tf Bool
True = formula
forall formula. IsFormula formula => formula
true
      at :: AtomOf formula -> formula
at = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf formula -> formula)
-> (AtomOf formula -> AtomOf formula) -> AtomOf formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> AtomOf formula -> AtomOf formula
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v term
subfn

-- | Substitution within terms.
tsubst :: (IsTerm term, v ~ TVarOf term) => Map v term -> term -> term
tsubst :: forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> term -> term
tsubst Map v term
sfn term
tm =
    (TVarOf term -> term)
-> (FunOf term -> [term] -> term) -> term -> term
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm (\TVarOf term
x -> term -> Maybe term -> term
forall a. a -> Maybe a -> a
fromMaybe term
tm (v -> Map v term -> Maybe term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
TVarOf term
x Map v term
sfn))
             (\FunOf term
f [term]
args -> FunOf term -> [term] -> term
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf term
f ((term -> term) -> [term] -> [term]
forall a b. (a -> b) -> [a] -> [b]
map (Map v term -> term -> term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> term -> term
tsubst Map v term
sfn) [term]
args))
             term
tm

-- | Substitution within a Literal
lsubst :: (JustLiteral lit, HasApply atom, IsTerm term,
           atom ~ AtomOf lit,
           term ~ TermOf atom,
           v ~ TVarOf term) =>
          Map v term -> lit -> lit
lsubst :: 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
subfn lit
fm =
    (lit -> lit) -> (Bool -> lit) -> (AtomOf lit -> lit) -> lit -> lit
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit -> lit
ne Bool -> lit
forall {formula}. IsFormula formula => Bool -> formula
fromBool atom -> lit
AtomOf lit -> lit
at lit
fm
    where
      ne :: lit -> lit
ne lit
p = lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) (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
subfn lit
p)
      at :: atom -> lit
at = atom -> lit
AtomOf lit -> lit
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (atom -> lit) -> (atom -> atom) -> atom -> lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v term -> atom -> atom
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v term
subfn

-- | Substitution within atoms.
asubst :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> atom -> atom
asubst :: forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v term
sfn atom
a = (TermOf atom -> TermOf atom) -> atom -> atom
forall atom.
HasApply atom =>
(TermOf atom -> TermOf atom) -> atom -> atom
onterms (Map v term -> term -> term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> term -> term
tsubst Map v term
sfn) atom
a

-- | Substitution within quantifiers
substq :: (IsFirstOrder formula, v ~ VarOf formula, term ~ TermOf (AtomOf formula)) =>
          Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq :: forall formula v term.
(IsFirstOrder formula, v ~ VarOf formula,
 term ~ TermOf (AtomOf formula)) =>
Map v term -> (v -> formula -> formula) -> v -> formula -> formula
substq Map v term
subfn v -> formula -> formula
qu v
x formula
p =
  let x' :: v
x' = if (v -> Bool) -> Set v -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\v
y -> v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
x (term -> Set v
forall term v. (IsTerm term, v ~ TVarOf term) => term -> Set v
fvt(Map v term -> v -> term -> term
forall k a. Ord k => Map k a -> k -> a -> a
tryApplyD Map v term
subfn v
y (TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt v
TVarOf term
y))))
                     (Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
difference (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv formula
p) (v -> Set v
forall a. a -> Set a
singleton v
x))
           then v -> Set v -> v
forall v. IsVariable v => v -> Set v -> v
variant v
x (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (v -> Map v term -> Map v term
forall k a. Ord k => k -> Map k a -> Map k a
undefine v
x Map v term
subfn) formula
p)) else v
x in
  v -> formula -> formula
qu v
x' (Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst ((v
x v -> term -> Map v term -> Map v term
forall k a. Ord k => k -> a -> Map k a -> Map k a
|-> TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt v
TVarOf term
x') Map v term
subfn) formula
p)

-- Examples.

test10 :: Test
test10 :: Test
test10 =
    let [FTerm
x, FTerm
x', FTerm
y] = [TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x'", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"y"]
        fm :: EqFormula
fm = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" ((FTerm
TermOf (FOL Predicate FTerm)
x TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
y)) :: EqFormula
        expected :: EqFormula
expected = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x'" (FTerm
TermOf (FOL Predicate FTerm)
x' TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x) :: EqFormula in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> EqFormula -> EqFormula -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual ([Char]
"subst (\"y\" |=> Var \"x\") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ EqFormula -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow EqFormula
fm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (p. 134)")
                           EqFormula
expected
                           (Map V FTerm -> EqFormula -> EqFormula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst ([(V, FTerm)] -> Map V FTerm
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(V
"y", FTerm
x)]) EqFormula
fm)

test11 :: Test
test11 :: Test
test11 =
    let [FTerm
x, FTerm
x', FTerm
x'', FTerm
y] = [TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x'", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"x''", TVarOf FTerm -> FTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf FTerm
"y"]
        fm :: EqFormula
fm = (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x" (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x'" ((FTerm
TermOf (FOL Predicate FTerm)
x TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
y) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (FTerm
TermOf (FOL Predicate FTerm)
x TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x')))) :: EqFormula
        expected :: EqFormula
expected = VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x'" (VarOf EqFormula -> EqFormula -> EqFormula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf EqFormula
"x''" ((FTerm
TermOf (FOL Predicate FTerm)
x' TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x) EqFormula -> EqFormula -> EqFormula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. ((FTerm
TermOf (FOL Predicate FTerm)
x' TermOf (FOL Predicate FTerm)
-> TermOf (FOL Predicate FTerm) -> EqFormula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. FTerm
TermOf (FOL Predicate FTerm)
x'')))) :: EqFormula in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> EqFormula -> EqFormula -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
[Char] -> a -> a -> Assertion
assertEqual ([Char]
"subst (\"y\" |=> Var \"x\") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ EqFormula -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow EqFormula
fm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (p. 134)")
                           EqFormula
expected
                           (Map V FTerm -> EqFormula -> EqFormula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst ([(V, FTerm)] -> Map V FTerm
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(V
"y", FTerm
x)]) EqFormula
fm)

testFOL :: Test
testFOL :: Test
testFOL = [Char] -> Test -> Test
TestLabel [Char]
"FOL" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03, Test
test04,
                                     Test
test05, Test
test06, Test
test07, Test
test08, Test
test09,
                                     Test
test10, Test
test11])