{- |
module: $Header$
description: Higher order logic conversions
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.Conv
where

import HOL.Data
import qualified HOL.Rule as Rule
import qualified HOL.Term as Term
import qualified HOL.TermAlpha as TermAlpha
import HOL.Thm (Thm)
import qualified HOL.Thm as Thm

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

data Result =
    Unchanged
  | Changed Thm
  deriving (Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c== :: Result -> Result -> Bool
Eq,Eq Result
Eq Result
-> (Result -> Result -> Ordering)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Result)
-> (Result -> Result -> Result)
-> Ord Result
Result -> Result -> Bool
Result -> Result -> Ordering
Result -> Result -> Result
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Result -> Result -> Result
$cmin :: Result -> Result -> Result
max :: Result -> Result -> Result
$cmax :: Result -> Result -> Result
>= :: Result -> Result -> Bool
$c>= :: Result -> Result -> Bool
> :: Result -> Result -> Bool
$c> :: Result -> Result -> Bool
<= :: Result -> Result -> Bool
$c<= :: Result -> Result -> Bool
< :: Result -> Result -> Bool
$c< :: Result -> Result -> Bool
compare :: Result -> Result -> Ordering
$ccompare :: Result -> Result -> Ordering
$cp1Ord :: Eq Result
Ord,Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> Result -> ShowS
Show)

newtype Conv = Conv (Term -> Maybe Result)

-------------------------------------------------------------------------------
-- Applying conversions to terms
-------------------------------------------------------------------------------

apply :: Conv -> Term -> Maybe Result
apply :: Conv -> Term -> Maybe Result
apply (Conv Term -> Maybe Result
f) Term
tm = Term -> Maybe Result
f Term
tm

applyData :: Conv -> Conv -> Conv -> TermData -> Maybe Result
applyData :: Conv -> Conv -> Conv -> TermData -> Maybe Result
applyData Conv
cf Conv
cx Conv
_ (AppTerm Term
f Term
x) = do
    Result
f' <- Conv -> Term -> Maybe Result
apply Conv
cf Term
f
    Result
x' <- Conv -> Term -> Maybe Result
apply Conv
cx Term
x
    case (Result
f',Result
x') of
      (Result
Unchanged,Result
Unchanged) -> Result -> Maybe Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Unchanged
      (Result
Unchanged, Changed Thm
x'') -> Result -> Maybe Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> Maybe Result) -> Result -> Maybe Result
forall a b. (a -> b) -> a -> b
$ Thm -> Result
Changed (Thm -> Result) -> Thm -> Result
forall a b. (a -> b) -> a -> b
$ Term -> Thm -> Thm
Rule.randUnsafe Term
f Thm
x''
      (Changed Thm
f'', Result
Unchanged) -> Result -> Maybe Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> Maybe Result) -> Result -> Maybe Result
forall a b. (a -> b) -> a -> b
$ Thm -> Result
Changed (Thm -> Result) -> Thm -> Result
forall a b. (a -> b) -> a -> b
$ Thm -> Term -> Thm
Rule.ratorUnsafe Thm
f'' Term
x
      (Changed Thm
f'', Changed Thm
x'') -> Result -> Maybe Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> Maybe Result) -> Result -> Maybe Result
forall a b. (a -> b) -> a -> b
$ Thm -> Result
Changed (Thm -> Result) -> Thm -> Result
forall a b. (a -> b) -> a -> b
$ Thm -> Thm -> Thm
Thm.mkAppUnsafe Thm
f'' Thm
x''
applyData Conv
_ Conv
_ Conv
cb (AbsTerm Var
v Term
b) = do
    Result
b' <- Conv -> Term -> Maybe Result
apply Conv
cb Term
b
    case Result
b' of
      Result
Unchanged -> Result -> Maybe Result
forall (m :: * -> *) a. Monad m => a -> m a
return Result
Unchanged
      Changed Thm
b'' -> Result -> Maybe Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> Maybe Result) -> Result -> Maybe Result
forall a b. (a -> b) -> a -> b
$ Thm -> Result
Changed (Thm -> Result) -> Thm -> Result
forall a b. (a -> b) -> a -> b
$ Var -> Thm -> Thm
Thm.mkAbsUnsafe Var
v Thm
b''
applyData Conv
_ Conv
_ Conv
_ TermData
_ = Result -> Maybe Result
forall a. a -> Maybe a
Just Result
Unchanged

applyTerm :: Conv -> Term -> Term
applyTerm :: Conv -> Term -> Term
applyTerm Conv
c Term
tm =
    case Conv -> Term -> Maybe Result
apply Conv
c Term
tm of
      Just (Changed Thm
th) -> Term -> Term
Term.rhsUnsafe (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest (TermAlpha -> Term) -> TermAlpha -> Term
forall a b. (a -> b) -> a -> b
$ Thm -> TermAlpha
Thm.concl (Thm -> TermAlpha) -> Thm -> TermAlpha
forall a b. (a -> b) -> a -> b
$ Thm
th
      Maybe Result
_ -> Term
tm

-------------------------------------------------------------------------------
-- Basic conversions
-------------------------------------------------------------------------------

fail :: Conv
fail :: Conv
fail = (Term -> Maybe Result) -> Conv
Conv (Maybe Result -> Term -> Maybe Result
forall a b. a -> b -> a
const Maybe Result
forall a. Maybe a
Nothing)

id :: Conv
id :: Conv
id = (Term -> Maybe Result) -> Conv
Conv (Maybe Result -> Term -> Maybe Result
forall a b. a -> b -> a
const (Maybe Result -> Term -> Maybe Result)
-> Maybe Result -> Term -> Maybe Result
forall a b. (a -> b) -> a -> b
$ Result -> Maybe Result
forall a. a -> Maybe a
Just Result
Unchanged)

beta :: Conv
beta :: Conv
beta = (Term -> Maybe Result) -> Conv
Conv ((Thm -> Result) -> Maybe Thm -> Maybe Result
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Thm -> Result
Changed (Maybe Thm -> Maybe Result)
-> (Term -> Maybe Thm) -> Term -> Maybe Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Thm
Thm.betaConv)

betaSimp :: Conv
betaSimp :: Conv
betaSimp = (Term -> Bool) -> Conv -> Conv -> Conv
cond Term -> Bool
p Conv
beta Conv
HOL.Conv.fail
  where
    p :: Term -> Bool
p Term
tm =
        case Term -> Maybe (Term, Term)
Term.destApp Term
tm of
          Maybe (Term, Term)
Nothing -> Bool
False
          Just (Term
f,Term
x) ->
              Term -> Bool
Term.isVar Term
x Bool -> Bool -> Bool
||
              case Term -> Maybe (Var, Term)
Term.destAbs Term
f of
                Maybe (Var, Term)
Nothing -> Bool
False
                Just (Var
v,Term
b) -> Bool -> Bool
not (Var -> Term -> Bool
Term.freeInMultiple Var
v Term
b)

-------------------------------------------------------------------------------
-- Conversionals
-------------------------------------------------------------------------------

orelse :: Conv -> Conv -> Conv
orelse :: Conv -> Conv -> Conv
orelse Conv
c1 Conv
c2 = (Term -> Maybe Result) -> Conv
Conv Term -> Maybe Result
f
  where
    f :: Term -> Maybe Result
f Term
tm = case Conv -> Term -> Maybe Result
apply Conv
c1 Term
tm of
             Maybe Result
Nothing -> Conv -> Term -> Maybe Result
apply Conv
c2 Term
tm
             Maybe Result
x -> Maybe Result
x

thenc :: Conv -> Conv -> Conv
thenc :: Conv -> Conv -> Conv
thenc Conv
c1 Conv
c2 = (Term -> Maybe Result) -> Conv
Conv Term -> Maybe Result
f
  where
    f :: Term -> Maybe Result
f Term
tm = let r1 :: Maybe Result
r1 = Conv -> Term -> Maybe Result
apply Conv
c1 Term
tm in
           case Maybe Result
r1 of
             Maybe Result
Nothing -> Maybe Result
forall a. Maybe a
Nothing
             Just Result
Unchanged -> Conv -> Term -> Maybe Result
apply Conv
c2 Term
tm
             Just (Changed Thm
th1) ->
                 let tm' :: Term
tm' = Term -> Term
Term.rhsUnsafe (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest (TermAlpha -> Term) -> TermAlpha -> Term
forall a b. (a -> b) -> a -> b
$ Thm -> TermAlpha
Thm.concl Thm
th1 in
                 case Conv -> Term -> Maybe Result
apply Conv
c2 Term
tm' of
                   Maybe Result
Nothing -> Maybe Result
forall a. Maybe a
Nothing
                   Just Result
Unchanged -> Maybe Result
r1
                   Just (Changed Thm
th2) ->
                       Result -> Maybe Result
forall a. a -> Maybe a
Just (Result -> Maybe Result) -> Result -> Maybe Result
forall a b. (a -> b) -> a -> b
$ Thm -> Result
Changed (Thm -> Result) -> Thm -> Result
forall a b. (a -> b) -> a -> b
$ Thm -> Thm -> Thm
Rule.transUnsafe Thm
th1 Thm
th2

try :: Conv -> Conv
try :: Conv -> Conv
try Conv
c = Conv
c Conv -> Conv -> Conv
`orelse` Conv
HOL.Conv.id

repeat :: Conv -> Conv
repeat :: Conv -> Conv
repeat Conv
c = Conv -> Conv
try (Conv
c Conv -> Conv -> Conv
`thenc` Conv -> Conv
HOL.Conv.repeat Conv
c)

sub :: Conv -> Conv
sub :: Conv -> Conv
sub Conv
c = (Term -> Maybe Result) -> Conv
Conv (Conv -> Conv -> Conv -> TermData -> Maybe Result
applyData Conv
c Conv
c Conv
c (TermData -> Maybe Result)
-> (Term -> TermData) -> Term -> Maybe Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TermData
Term.dest)

rator :: Conv -> Conv
rator :: Conv -> Conv
rator Conv
c = (Term -> Maybe Result) -> Conv
Conv (Conv -> Conv -> Conv -> TermData -> Maybe Result
applyData Conv
c Conv
HOL.Conv.id Conv
HOL.Conv.id (TermData -> Maybe Result)
-> (Term -> TermData) -> Term -> Maybe Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TermData
Term.dest)

rand :: Conv -> Conv
rand :: Conv -> Conv
rand Conv
c = (Term -> Maybe Result) -> Conv
Conv (Conv -> Conv -> Conv -> TermData -> Maybe Result
applyData Conv
HOL.Conv.id Conv
c Conv
HOL.Conv.id (TermData -> Maybe Result)
-> (Term -> TermData) -> Term -> Maybe Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TermData
Term.dest)

abs :: Conv -> Conv
abs :: Conv -> Conv
abs Conv
c = (Term -> Maybe Result) -> Conv
Conv (Conv -> Conv -> Conv -> TermData -> Maybe Result
applyData Conv
HOL.Conv.id Conv
HOL.Conv.id Conv
c (TermData -> Maybe Result)
-> (Term -> TermData) -> Term -> Maybe Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TermData
Term.dest)

cond :: (Term -> Bool) -> Conv -> Conv -> Conv
cond :: (Term -> Bool) -> Conv -> Conv -> Conv
cond Term -> Bool
p Conv
c1 Conv
c2 = (Term -> Maybe Result) -> Conv
Conv Term -> Maybe Result
f
  where
    f :: Term -> Maybe Result
f Term
tm = Conv -> Term -> Maybe Result
apply (if Term -> Bool
p Term
tm then Conv
c1 else Conv
c2) Term
tm

-------------------------------------------------------------------------------
-- Traversal strategies
-------------------------------------------------------------------------------

bottomUp :: Conv -> Conv
bottomUp :: Conv -> Conv
bottomUp Conv
c = Conv -> Conv
sub (Conv -> Conv
bottomUp Conv
c) Conv -> Conv -> Conv
`thenc` Conv -> Conv
try Conv
c

-------------------------------------------------------------------------------
-- Evaluating terms to weak head normal form
-------------------------------------------------------------------------------

eval :: Conv -> Conv
eval :: Conv -> Conv
eval Conv
c = Conv
whnf
  where
    whnf :: Conv
whnf = Conv -> Conv
rator Conv
whnf Conv -> Conv -> Conv
`thenc` Conv -> Conv
try ((Conv
c Conv -> Conv -> Conv
`orelse` Conv
beta) Conv -> Conv -> Conv
`thenc` Conv
whnf)