85cf83f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow building with base-4.8.0.0

commit85cf83f37f08754214e65f5011187f7aa9569f3d authorRyanGlScott <ryan.gl.scott@ku.edu> dateSat 3 Jan 2015, 21:35 (12 years ago) parentc1cf03f

6 files changed+25−11

compare with master

unifiedsplit

idris.cabal+2−2 src/Idris/Core/Unify.hs+4−4 src/Idris/IdeSlave.hs+3−3 src/Idris/ParseHelpers.hs+8−1 src/Idris/Primitives.hs+1−1 src/Pkg/PParser.hs+7

idris.cabal+2−2

@@ -725,12 +725,12 @@ Library

725725 , bytestring < 0.11

726726 , cheapskate < 0.2

727727 , containers >= 0.5 && < 0.6

728− , deepseq < 1.4

728+ , deepseq < 1.5

729729 , directory >= 1.2 && < 1.3

730730 , filepath < 1.4

731731 , fingertree >= 0.1 && < 0.2

732732 , haskeline >= 0.7 && < 0.8

733− , lens >= 4.1.1 && < 4.7

733+ , lens >= 4.1.1 && < 4.8

734734 , mtl >= 2.2.1 && < 2.3

735735 , network < 2.7

736736 , optparse-applicative >= 0.11 && < 0.12

src/Idris/Core/Unify.hs+4−4

@@ -73,14 +73,14 @@ match_unify ctxt env topx topy inj holes from =

7373 let topxn = renameBindersTm env (normalise ctxt env topx)

7474 topyn = renameBindersTm env (normalise ctxt env topy) in

7575 case runStateT (un [] topxn topyn)

76− (UI 0 []) of

76+ (UI 0 []) of

7777 OK (v, UI _ fails) ->

7878 do v' <- trimSolutions topx topy from env v

7979 return (map (renameBinders env) v')

8080 Error e ->

8181 -- just normalise the term we're matching against

8282 case runStateT (un [] topxn topy)

83− (UI 0 []) of

83+ (UI 0 []) of

8484 OK (v, UI _ fails) ->

8585 do v' <- trimSolutions topx topy from env v

8686 return (map (renameBinders env) v')

@@ -286,12 +286,12 @@ unify ctxt env topx topy inj holes usersupp from =

286286 topyn = renameBindersTm env (normalise ctxt env topy) in

287287-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

288288 case runStateT (un False [] topxn topyn)

289− (UI 0 []) of

289+ (UI 0 []) of

290290 OK (v, UI _ fails) ->

291291 do v' <- trimSolutions topx topy from env v

292292 return (map (renameBinders env) v', reverse fails)

293293-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

294− Error e -> tfail e

294+ Error e -> tfail e

295295 where

296296 headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

297297 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

src/Idris/IdeSlave.hs+3−3

@@ -150,9 +150,9 @@ instance SExpable OutputAnnotation where

150150 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",

151151 StringAtom ("Result type is " ++ descr))]

152152 where descr = case ordr of

153− EQ -> "isomorphic"

154− LT -> "more general than searched type"

155− GT -> "more specific than searched type"

153+ EQ -> "isomorphic"

154+ LT -> "more general than searched type"

155+ GT -> "more specific than searched type"

156156 toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]

157157

158158encodeTerm :: [(Name, Bool)] -> Term -> String

src/Idris/ParseHelpers.hs+8−1

@@ -1,4 +1,7 @@

1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, OverlappingInstances, StandaloneDeriving #-}

1+{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, StandaloneDeriving #-}

2+#if !(MIN_VERSION_base(4,8,0))

3+{-# LANGUAGE OverlappingInstances #-}

4+#endif

25module Idris.ParseHelpers where

47import Prelude hiding (pi)

@@ -47,7 +50,11 @@ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

4750

4851deriving instance Parsing IdrisInnerParser

4952

53+#if MIN_VERSION_base(4,8,0)

54+instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

55+#else

5056instance TokenParsing IdrisParser where

57+#endif

5158 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

5259 token p = do s <- get

5360 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

src/Idris/Primitives.hs+1−1

@@ -20,7 +20,7 @@ data Prim = Prim { p_name :: Name,

2020 p_type :: Type,

2121 p_arity :: Int,

2222 p_def :: [Const] -> Maybe Const,

23− p_lexp :: (Int, PrimFn),

23+ p_lexp :: (Int, PrimFn),

2424 p_total :: Totality

2525 }

2626

src/Pkg/PParser.hs+7

@@ -1,4 +1,7 @@

1+{-# LANGUAGE CPP #-}

2+#if !(MIN_VERSION_base(4,8,0))

13{-# LANGUAGE OverlappingInstances #-}

4+#endif

36module Pkg.PParser where

@@ -31,7 +34,11 @@ data PkgDesc = PkgDesc { pkgname :: String,

3134 }

3235 deriving Show

3336

37+#if MIN_VERSION_base(4,8,0)

38+instance {-# OVERLAPPING #-} TokenParsing PParser where

39+#else

3440instance TokenParsing PParser where

41+#endif

3542 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

3643

3744