git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/ErrReverse.hs
73 lines 2.7 kB history raw
1{-|
2Module : Idris.ErrReverse
3Description : Utility to make errors readable using transformations.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
10module Idris.ErrReverse(errReverse) where
12import Idris.AbsSyntax
13import Idris.Core.Evaluate (unfold)
14import Idris.Core.TT
16import Data.List
18-- | For display purposes, apply any 'error reversal' transformations
19-- so that errors will be more readable,
20-- and any 'error reduce' transformations
21errReverse :: IState -> Term -> Term
22errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)
23 where
24 do_unfold :: Term -> Term
25 do_unfold t = let ns = idris_errReduce ist in
26 if null ns then t
27 else unfold (tt_ctxt ist) []
28 (map (\x -> (x, 1000)) (idris_errReduce ist))
29 t
31 rewrite 0 t = t
32 rewrite n t = let t' = foldl applyRule t (reverse (idris_errRev ist)) in
33 if t == t' then t
34 else rewrite (n - 1) t'
36 applyRule :: Term -> (Term, Term) -> Term
37 applyRule t (l, r) = applyNames [] t l r
39 -- Assume pattern bindings match in l and r (if they don't just treat
40 -- the rule as invalid and return t)
42 applyNames ns t (Bind n (PVar _ ty) scl) (Bind n' (PVar _ ty') scr)
43 | n == n' = applyNames (n : ns) t (instantiate (P Ref n ty) scl)
44 (instantiate (P Ref n' ty') scr)
45 | otherwise = t
46 applyNames ns t l r = matchTerm ns l r t
48 matchTerm ns l r t
49 | Just nmap <- match ns l t = substNames nmap r
50 matchTerm ns l r (App s f a) = let f' = matchTerm ns l r f
51 a' = matchTerm ns l r a in
52 App s f' a'
53 matchTerm ns l r (Bind n b sc) = let b' = fmap (matchTerm ns l r) b
54 sc' = matchTerm ns l r sc in
55 Bind n b' sc'
56 matchTerm ns l r t = t
58 match ns l t = do ms <- match' ns l t
59 combine (nub ms)
61 -- If any duplicate mappings, it's a failure
62 combine [] = Just []
63 combine ((x, t) : xs)
64 | Just _ <- lookup x xs = Nothing
65 | otherwise = do xs' <- combine xs
66 Just ((x, t) : xs')
68 match' ns (P Ref n _) t | n `elem` ns = Just [(n, t)]
69 match' ns (App _ f a) (App _ f' a') = do fs <- match' ns f f'
70 as <- match' ns a a'
71 Just (fs ++ as)
72 -- no matching Binds, for now...
73 match' ns x y = if x == y then Just [] else Nothing