content: {-|
  Module      : Idris.ErrReverse
  Description : Utility to make errors readable using transformations.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE PatternGuards #-}
  
  module Idris.ErrReverse(errReverse) where
  
  import Idris.AbsSyntax
  import Idris.Core.Evaluate (unfold)
  import Idris.Core.TT
  
  import Data.List
  
  -- | For display purposes, apply any 'error reversal' transformations
  -- so that errors will be more readable,
  -- and any 'error reduce' transformations
  errReverse :: IState -> Term -> Term
  errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)
    where
      do_unfold :: Term -> Term
      do_unfold t = let ns = idris_errReduce ist in
                        if null ns then t
                           else unfold (tt_ctxt ist) []
                                       (map (\x -> (x, 1000)) (idris_errReduce ist))
                                       t
  
      rewrite 0 t = t
      rewrite n t = let t' = foldl applyRule t (reverse (idris_errRev ist)) in
                        if t == t' then t
                                   else rewrite (n - 1) t'
  
      applyRule :: Term -> (Term, Term) -> Term
      applyRule t (l, r) = applyNames [] t l r
  
      -- Assume pattern bindings match in l and r (if they don't just treat
      -- the rule as invalid and return t)
  
      applyNames ns t (Bind n (PVar _ ty) scl) (Bind n' (PVar _ ty') scr)
         | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)
                                           (instantiate (P Ref n' ty') scr)
         | otherwise = t
      applyNames ns t l r = matchTerm ns l r t
  
      matchTerm ns l r t
         | Just nmap <- match ns l t = substNames nmap r
      matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f
                                         a' = matchTerm ns l r a in
                                         App s f' a'
      matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b
                                           sc' = matchTerm ns l r sc in
                                           Bind n b' sc'
      matchTerm ns l r t = t
  
      match ns l t = do ms <- match' ns l t
                        combine (nub ms)
  
      -- If any duplicate mappings, it's a failure
      combine [] = Just []
      combine ((x, t) : xs)
         | Just _ <- lookup x xs = Nothing
         | otherwise = do xs' <- combine xs
                          Just ((x, t) : xs')
  
      match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]
      match' ns (App _ f a) (App _ f' a') = do fs <- match' ns f f'
                                               as <- match' ns a a'
                                               Just (fs ++ as)
      -- no matching Binds, for now...
      match' ns x y = if x == y then Just [] else Nothing
  