@@ -22,8 +22,8 @@ TT is the core language of Idris. The language has:
2222 * We have a simple collection of tactics which we use to elaborate source
2323 programs with implicit syntax into fully explicit terms.
2424-}
25−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,
26− DeriveDataTypeable, DeriveGeneric, PatternGuards #-}
25+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,
26+ FunctionalDependencies, MultiParamTypeClasses, PatternGuards #-}
2727{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2828module Idris.Core.TT(
2929 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
@@ -51,40 +51,39 @@ module Idris.Core.TT(
5151 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm
5252 ) where
5353
54+import Util.Pretty hiding (Str)
55+
5456-- Work around AMP without CPP
55−import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,
56− Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),
57− Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, flip,
58− fst, snd, not, mod, read, otherwise)
57+import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,
58+ Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),
59+ Read(..), Show(..), String, div, error, flip, fst, mod, not,
60+ otherwise, read, snd, ($), (&&), (.), (||))
5961
60−import Control.Applicative (Applicative (..), Alternative)
61−import qualified Control.Applicative as A (Alternative (..))
62+import Control.Applicative (Alternative, Applicative(..))
63+import qualified Control.Applicative as A (Alternative(..))
6264import Control.DeepSeq (($!!))
6365import Control.Monad.State.Strict
64−import Control.Monad.Trans.Except (Except (..))
65−import Debug.Trace
66−import qualified Data.Map.Strict as Map
66+import Control.Monad.Trans.Except (Except(..))
67+import Data.Binary hiding (get, put)
68+import qualified Data.Binary as B
6769import Data.Char
6870import Data.Data (Data)
69−import Data.Monoid (mconcat)
70−import Numeric (showIntAtBase)
71−import qualified Data.Text as T
71+import Data.Foldable (Foldable)
7272import Data.List hiding (group, insert)
73−import Data.Set(Set, member, fromList, insert)
73+import qualified Data.Map.Strict as Map
7474import Data.Maybe (listToMaybe)
75−import Data.Foldable (Foldable)
75+import Data.Monoid (mconcat)
76+import Data.Set (Set, fromList, insert, member)
77+import qualified Data.Text as T
7678import Data.Traversable (Traversable)
7779import Data.Typeable (Typeable)
7880import Data.Vector.Unboxed (Vector)
7981import qualified Data.Vector.Unboxed as V
80−import qualified Data.Binary as B
81−import Data.Binary hiding (get, put)
82+import Debug.Trace
8283import Foreign.Storable (sizeOf)
8384import GHC.Generics (Generic)
84−
85−import Numeric.IEEE (IEEE (identicalIEEE))
86−
87−import Util.Pretty hiding (Str)
85+import Numeric (showIntAtBase)
86+import Numeric.IEEE (IEEE(identicalIEEE))
8887
8988data Option = TTypeInTType
9089 | CheckConv
@@ -941,7 +940,7 @@ instance Sized UExp where
941940 size _ = 1
942941
943942instance Show UExp where
944− show (UVar ns x)
943+ show (UVar ns x)
945944 | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]
946945 | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
947946 show (UVal x) = show x
@@ -1289,7 +1288,7 @@ substTerm old new = st where
12891288 st (Bind x b sc) = Bind x (fmap st b) (st sc)
12901289 st t = t
12911290
1292− eqAlpha as (P _ x _) (P _ y _)
1291+ eqAlpha as (P _ x _) (P _ y _)
12931292 = x == y || (x, y) `elem` as || (y, x) `elem` as
12941293 eqAlpha as (V x) (V y) = x == y
12951294 eqAlpha as (Bind x xb xs) (Bind y yb ys)
@@ -1301,7 +1300,7 @@ substTerm old new = st where
13011300 = eqAlpha as xt yt && eqAlpha as xv yv
13021301 eqAlphaB as (Guess xt xv) (Guess yt yv)
13031302 = eqAlpha as xt yt && eqAlpha as xv yv
1304− eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)
1303+ eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)
13051304
13061305-- | Return number of occurrences of V 0 or bound name i the term
13071306occurrences :: Eq n => n -> TT n -> Int