{-# LANGUAGE PatternGuards #-}
module Idris.ErrReverse(errReverse) where
import Idris.AbsSyntax
import Idris.Core.Evaluate (unfold)
import Idris.Core.TT
import Data.List
errReverse :: IState -> Term -> Term
errReverse :: IState -> Term -> Term
errReverse IState
ist Term
t = Integer -> Term -> Term
forall {t}. (Eq t, Num t) => t -> Term -> Term
rewrite Integer
5 (Term -> Term
do_unfold Term
t)
where
do_unfold :: Term -> Term
do_unfold :: Term -> Term
do_unfold Term
t = let ns :: [Name]
ns = IState -> [Name]
idris_errReduce IState
ist in
if [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
ns then Term
t
else Context -> Env -> [(Name, Int)] -> Term -> Term
unfold (IState -> Context
tt_ctxt IState
ist) []
((Name -> (Name, Int)) -> [Name] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
x -> (Name
x, Int
1000)) (IState -> [Name]
idris_errReduce IState
ist))
Term
t
rewrite :: t -> Term -> Term
rewrite t
0 Term
t = Term
t
rewrite t
n Term
t = let t' :: Term
t' = (Term -> (Term, Term) -> Term) -> Term -> [(Term, Term)] -> Term
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> (Term, Term) -> Term
applyRule Term
t ([(Term, Term)] -> [(Term, Term)]
forall a. [a] -> [a]
reverse (IState -> [(Term, Term)]
idris_errRev IState
ist)) in
if Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
t' then Term
t
else t -> Term -> Term
rewrite (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) Term
t'
applyRule :: Term -> (Term, Term) -> Term
applyRule :: Term -> (Term, Term) -> Term
applyRule Term
t (Term
l, Term
r) = [Name] -> Term -> Term -> Term -> Term
forall {n}. Eq n => [n] -> TT n -> TT n -> TT n -> TT n
applyNames [] Term
t Term
l Term
r
applyNames :: [n] -> TT n -> TT n -> TT n -> TT n
applyNames [n]
ns TT n
t (Bind n
n (PVar RigCount
_ TT n
ty) TT n
scl) (Bind n
n' (PVar RigCount
_ TT n
ty') TT n
scr)
| n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
n' = [n] -> TT n -> TT n -> TT n -> TT n
applyNames (n
n n -> [n] -> [n]
forall a. a -> [a] -> [a]
: [n]
ns) TT n
t (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref n
n TT n
ty) TT n
scl)
(TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref n
n' TT n
ty') TT n
scr)
| Bool
otherwise = TT n
t
applyNames [n]
ns TT n
t TT n
l TT n
r = [n] -> TT n -> TT n -> TT n -> TT n
forall {t :: * -> *} {n}.
(Foldable t, Eq n) =>
t n -> TT n -> TT n -> TT n -> TT n
matchTerm [n]
ns TT n
l TT n
r TT n
t
matchTerm :: t n -> TT n -> TT n -> TT n -> TT n
matchTerm t n
ns TT n
l TT n
r TT n
t
| Just [(n, TT n)]
nmap <- t n -> TT n -> TT n -> Maybe [(n, TT n)]
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
t a -> TT a -> TT a -> Maybe [(a, TT a)]
match t n
ns TT n
l TT n
t = [(n, TT n)] -> TT n -> TT n
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(n, TT n)]
nmap TT n
r
matchTerm t n
ns TT n
l TT n
r (App AppStatus n
s TT n
f TT n
a) = let f' :: TT n
f' = t n -> TT n -> TT n -> TT n -> TT n
matchTerm t n
ns TT n
l TT n
r TT n
f
a' :: TT n
a' = t n -> TT n -> TT n -> TT n -> TT n
matchTerm t n
ns TT n
l TT n
r TT n
a in
AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
s TT n
f' TT n
a'
matchTerm t n
ns TT n
l TT n
r (Bind n
n Binder (TT n)
b TT n
sc) = let b' :: Binder (TT n)
b' = (TT n -> TT n) -> Binder (TT n) -> Binder (TT n)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t n -> TT n -> TT n -> TT n -> TT n
matchTerm t n
ns TT n
l TT n
r) Binder (TT n)
b
sc' :: TT n
sc' = t n -> TT n -> TT n -> TT n -> TT n
matchTerm t n
ns TT n
l TT n
r TT n
sc in
n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n Binder (TT n)
b' TT n
sc'
matchTerm t n
ns TT n
l TT n
r TT n
t = TT n
t
match :: t a -> TT a -> TT a -> Maybe [(a, TT a)]
match t a
ns TT a
l TT a
t = do [(a, TT a)]
ms <- t a -> TT a -> TT a -> Maybe [(a, TT a)]
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
t a -> TT a -> TT a -> Maybe [(a, TT a)]
match' t a
ns TT a
l TT a
t
[(a, TT a)] -> Maybe [(a, TT a)]
forall {a} {b}. Eq a => [(a, b)] -> Maybe [(a, b)]
combine ([(a, TT a)] -> [(a, TT a)]
forall a. Eq a => [a] -> [a]
nub [(a, TT a)]
ms)
combine :: [(a, b)] -> Maybe [(a, b)]
combine [] = [(a, b)] -> Maybe [(a, b)]
forall a. a -> Maybe a
Just []
combine ((a
x, b
t) : [(a, b)]
xs)
| Just b
_ <- a -> [(a, b)] -> Maybe b
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
x [(a, b)]
xs = Maybe [(a, b)]
forall a. Maybe a
Nothing
| Bool
otherwise = do [(a, b)]
xs' <- [(a, b)] -> Maybe [(a, b)]
combine [(a, b)]
xs
[(a, b)] -> Maybe [(a, b)]
forall a. a -> Maybe a
Just ((a
x, b
t) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
xs')
match' :: t a -> TT a -> TT a -> Maybe [(a, TT a)]
match' t a
ns (P NameType
Ref a
n TT a
_) TT a
t | a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ns = [(a, TT a)] -> Maybe [(a, TT a)]
forall a. a -> Maybe a
Just [(a
n, TT a
t)]
match' t a
ns (App AppStatus a
_ TT a
f TT a
a) (App AppStatus a
_ TT a
f' TT a
a') = do [(a, TT a)]
fs <- t a -> TT a -> TT a -> Maybe [(a, TT a)]
match' t a
ns TT a
f TT a
f'
[(a, TT a)]
as <- t a -> TT a -> TT a -> Maybe [(a, TT a)]
match' t a
ns TT a
a TT a
a'
[(a, TT a)] -> Maybe [(a, TT a)]
forall a. a -> Maybe a
Just ([(a, TT a)]
fs [(a, TT a)] -> [(a, TT a)] -> [(a, TT a)]
forall a. [a] -> [a] -> [a]
++ [(a, TT a)]
as)
match' t a
ns TT a
x TT a
y = if TT a
x TT a -> TT a -> Bool
forall a. Eq a => a -> a -> Bool
== TT a
y then [(a, TT a)] -> Maybe [(a, TT a)]
forall a. a -> Maybe a
Just [] else Maybe [(a, TT a)]
forall a. Maybe a
Nothing