logic-classes-1.1: Data/Logic/Harrison/FOL.hs
{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeSynonymInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Logic.Harrison.FOL
( eval
, list_disj
, list_conj
, var
, fv
, subst
, generalize
) where
import Data.Logic.Classes.Apply (Apply(..), apply)
import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..), binop)
import Data.Logic.Classes.Constants (Constants (fromBool, true, false))
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), quant)
import Data.Logic.Classes.Formula (Formula(allVariables, substitute))
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Term (Term(vt), fvt)
import Data.Logic.Classes.Variable (Variable(..))
import Data.Logic.Harrison.Formulas.FirstOrder (on_atoms)
import Data.Logic.Harrison.Lib ((|->), setAny)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import qualified Data.Set as Set
import Prelude hiding (pred)
-- =========================================================================
-- Basic stuff for first order logic.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
-- =========================================================================
-- -------------------------------------------------------------------------
-- Interpretation of formulas.
-- -------------------------------------------------------------------------
eval :: FirstOrderFormula formula atom v => formula -> (atom -> Bool) -> Bool
eval fm v =
foldFirstOrder qu co id at fm
where
qu _ _ p = eval p v
co ((:~:) p) = not (eval p v)
co (BinOp p (:&:) q) = eval p v && eval q v
co (BinOp p (:|:) q) = eval p v || eval q v
co (BinOp p (:=>:) q) = not (eval p v) || eval q v
co (BinOp p (:<=>:) q) = eval p v == eval q v
at = v
list_conj :: (Constants formula, Combinable formula) => Set.Set formula -> formula
list_conj l = maybe true (\ (x, xs) -> Set.fold (.&.) x xs) (Set.minView l)
list_disj :: (Constants formula, Combinable formula) => Set.Set formula -> formula
list_disj l = maybe false (\ (x, xs) -> Set.fold (.|.) x xs) (Set.minView l)
mkLits :: (FirstOrderFormula formula atom v, Ord formula) =>
Set.Set formula -> (atom -> Bool) -> formula
mkLits pvs v = list_conj (Set.map (\ p -> if eval p v then p else (.~.) p) pvs)
-- -------------------------------------------------------------------------
-- Special case of applying a subfunction to the top *terms*.
-- -------------------------------------------------------------------------
on_formula :: (FirstOrderFormula fol atom v, Apply atom p term) => (term -> term) -> fol -> fol
on_formula f = on_atoms (foldApply (\ p ts -> atomic (apply p (map f ts))) fromBool)
-- -------------------------------------------------------------------------
-- 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;;
-}
-- -------------------------------------------------------------------------
-- 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;;
-}
-- -------------------------------------------------------------------------
-- Free variables in terms and formulas.
-- -------------------------------------------------------------------------
-- | Return all variables occurring in a formula.
var :: forall formula atom term v. (FirstOrderFormula formula atom v, Formula atom term v) => formula -> Set.Set v
var fm =
foldFirstOrder qu co tf allVariables fm
where
qu _ x p = Set.insert x (var p)
co ((:~:) p) = var p
co (BinOp p _ q) = Set.union (var p) (var q)
tf _ = Set.empty
-- | Return the variables that occur free in a formula.
fv :: forall formula atom term v. (FirstOrderFormula formula atom v, Formula atom term v) => formula -> Set.Set v
fv fm =
foldFirstOrder qu co tf allVariables fm
where
qu _ x p = Set.delete x (fv p)
co ((:~:) p) = fv p
co (BinOp p _ q) = Set.union (fv p) (fv q)
tf _ = Set.empty
-- -------------------------------------------------------------------------
-- Universal closure of a formula.
-- -------------------------------------------------------------------------
generalize :: (FirstOrderFormula formula atom v, Formula atom term v) => formula -> formula
generalize fm = Set.fold for_all fm (fv fm)
-- -------------------------------------------------------------------------
-- Substitution in formulas, with variable renaming.
-- -------------------------------------------------------------------------
subst :: (FirstOrderFormula formula atom v, Formula atom term v, Term term v f) =>
Map.Map v term -> formula -> formula
subst env fm =
foldFirstOrder qu co tf at fm
where
qu op x p = quant op x' (subst ((x |-> vt x') env) p)
where
x' = if setAny (\ y -> Set.member x (fvt (fromMaybe (vt y) (Map.lookup y env)))) (Set.delete x (fv p))
then variant x (fv (subst (Map.delete x env) p))
else x
co ((:~:) p) = ((.~.) (subst env p))
co (BinOp p op q) = binop (subst env p) op (subst env q)
tf = fromBool
at = atomic . substitute env
{-
-- |Replace each free occurrence of variable old with term new.
substitute :: forall formula atom term v f. (FirstOrderFormula formula atom v, Term term v f) => v -> term -> (atom -> formula) -> formula -> formula
substitute old new atom formula =
foldTerm (\ new' -> if old == new' then formula else substitute' formula)
(\ _ _ -> substitute' formula)
new
where
substitute' =
foldFirstOrder -- If the old variable appears in a quantifier
-- we can stop doing the substitution.
(\ q v f' -> quant q v (if old == v then f' else substitute' f'))
(\ cm -> case cm of
((:~:) f') -> combine ((:~:) (substitute' f'))
(BinOp f1 op f2) -> combine (BinOp (substitute' f1) op (substitute' f2)))
fromBool
atom
-}
{-
substitute old new atom formula
where
atom = foldAtomEq (\ p ts -> pApp p (map st ts)) fromBool (\ t1 t2 -> st t1 .=. st t2)
st :: term -> term
st t = foldTerm sv (\ func ts -> fApp func (map st ts)) t
sv v = if v == old then new else vt v
-}