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
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)
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
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)
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
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
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)