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

idris.cabal+2−2

compare with master

unifiedsplit

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

725 , bytestring < 0.11

726 , cheapskate < 0.2

727 , containers >= 0.5 && < 0.6

728− , deepseq < 1.4

728+ , deepseq < 1.5

729 , directory >= 1.2 && < 1.3

730 , filepath < 1.4

731 , fingertree >= 0.1 && < 0.2

732 , haskeline >= 0.7 && < 0.8

733− , lens >= 4.1.1 && < 4.7

733+ , lens >= 4.1.1 && < 4.8

734 , mtl >= 2.2.1 && < 2.3

735 , network < 2.7

736 , 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 =

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

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

75 case runStateT (un [] topxn topyn)

76− (UI 0 []) of

76+ (UI 0 []) of

77 OK (v, UI _ fails) ->

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

79 return (map (renameBinders env) v')

80 Error e ->

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

82 case runStateT (un [] topxn topy)

83− (UI 0 []) of

83+ (UI 0 []) of

84 OK (v, UI _ fails) ->

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

86 return (map (renameBinders env) v')

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

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

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

288 case runStateT (un False [] topxn topyn)

289− (UI 0 []) of

289+ (UI 0 []) of

290 OK (v, UI _ fails) ->

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

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

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

294− Error e -> tfail e

294+ Error e -> tfail e

295 where

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

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

src/Idris/IdeSlave.hs+3−3

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

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

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

152 where descr = case ordr of

153− EQ -> "isomorphic"

153+ EQ -> "isomorphic"

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

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

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

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

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

157

158encodeTerm :: [(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

2module Idris.ParseHelpers where

5module Idris.ParseHelpers where

3

6

4import Prelude hiding (pi)

7import Prelude hiding (pi)

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

47

50

48deriving instance Parsing IdrisInnerParser

51deriving instance Parsing IdrisInnerParser

49

52

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

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

55+#else

50instance TokenParsing IdrisParser where

56instance TokenParsing IdrisParser where

57+#endif

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

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

52 token p = do s <- get

59 token p = do s <- get

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

60 (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,

20 p_type :: Type,

21 p_arity :: Int,

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

23− p_lexp :: (Int, PrimFn),

23+ p_lexp :: (Int, PrimFn),

24 p_total :: Totality

25 }

26

src/Pkg/PParser.hs+7

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

1+{-# LANGUAGE CPP #-}

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

1{-# LANGUAGE OverlappingInstances #-}

3{-# LANGUAGE OverlappingInstances #-}

4+#endif

2

5

3module Pkg.PParser where

6module Pkg.PParser where

4

7

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

31 }

34 }

32 deriving Show

35 deriving Show

33

36

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

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

39+#else

34instance TokenParsing PParser where

40instance TokenParsing PParser where

41+#endif

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

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

36

43

37

44