8ab1ac6 · Idris-dev · git.iko.soy

src/Idris/Core/Binary.hs+26−2

compare with master

unifiedsplit

@@ -3,6 +3,9 @@

3{-| Binary instances for the core datatypes -}

4module Idris.Core.Binary where

5

6+import Control.Applicative ((<*>), (<$>))

7+import Control.Monad (liftM2)

8+

6import Data.Binary

9import Data.Binary

7import Data.Vector.Binary

10import Data.Vector.Binary

8import qualified Data.Text as T

11import qualified Data.Text as T

@@ -43,6 +46,22 @@ instance Binary Provenance where

43 return (TooManyArgs x1)

46 return (TooManyArgs x1)

44 _ -> error "Corrupted binary data for Provenance"

47 _ -> error "Corrupted binary data for Provenance"

45

48

49+instance Binary UConstraint where

50+ put (ULT x1 x2) = putWord8 0 >> put x1 >> put x2

51+ put (ULE x1 x2) = putWord8 1 >> put x1 >> put x2

52+ get = do i <- getWord8

53+ case i of

54+ 0 -> ULT <$> get <*> get

55+ 1 -> ULE <$> get <*> get

56+ _ -> error "Corrupted binary data for UConstraint"

57+

58+instance Binary ConstraintFC where

59+ put (ConstraintFC x1 x2) = putWord8 0 >> put x1 >> put x2

60+ get = do i <- getWord8

61+ case i of

62+ 0 -> liftM2 ConstraintFC get get

63+ _ -> error "Corrupted binary data for ConstraintFC"

64+

46instance Binary a => Binary (Err' a) where

65instance Binary a => Binary (Err' a) where

47 put (Msg str) = do putWord8 0

66 put (Msg str) = do putWord8 0

48 put str

67 put str

@@ -97,7 +116,12 @@ instance Binary a => Binary (Err' a) where

97 put ns

116 put ns

98 put (IncompleteTerm t) = do putWord8 17

117 put (IncompleteTerm t) = do putWord8 17

99 put t

118 put t

100− put UniverseError = putWord8 18

119+ put (UniverseError x1 x2 x3 x4 x5) = do putWord8 18

120+ put x1

121+ put x2

122+ put x3

123+ put x4

124+ put x5

101 put (UniqueError u n) = do putWord8 19

125 put (UniqueError u n) = do putWord8 19

102 put u

126 put u

103 put n

127 put n

@@ -181,7 +205,7 @@ instance Binary a => Binary (Err' a) where

181 15 -> fmap (CantResolve False) get

205 15 -> fmap (CantResolve False) get

182 16 -> fmap CantResolveAlts get

206 16 -> fmap CantResolveAlts get

183 17 -> fmap IncompleteTerm get

207 17 -> fmap IncompleteTerm get

184− 18 -> return UniverseError

208+ 18 -> UniverseError <$> get <*> get <*> get <*> get <*> get

185 19 -> do x <- get ; y <- get

209 19 -> do x <- get ; y <- get

186 return $ UniqueError x y

210 return $ UniqueError x y

187 20 -> do x <- get ; y <- get

211 20 -> do x <- get ; y <- get

src/Idris/Core/Constraints.hs+8−7

@@ -145,18 +145,19 @@ solve maxUniverseLevel ucs =

145 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)

146 domainOf (UVal val) = return (Domain val val)

147

148+ asPair :: Domain -> (Int, Int)

149+ asPair (Domain x y) = (x, y)

150+

148 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

151 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

149 updateUpperBoundOf suspect (UVar var) upper = do

152 updateUpperBoundOf suspect (UVar var) upper = do

150 doms <- gets domainStore

153 doms <- gets domainStore

151 let (oldDom@(Domain lower _), suspects) = doms M.! Var var

154 let (oldDom@(Domain lower _), suspects) = doms M.! Var var

152 let newDom = Domain lower upper

155 let newDom = Domain lower upper

153− when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines

156+ when (wipeOut newDom) $

154− $ "Universe inconsistency."

157+ lift $ Error $

155− : ("Working on: " ++ show (UVar var))

158+ UniverseError (ufc suspect) (UVar var)

156− : ("Old domain: " ++ show oldDom)

159+ (asPair oldDom) (asPair newDom)

157− : ("New domain: " ++ show newDom)

158− : "Involved constraints: "

159− : map (("\t"++) . show) (suspect : S.toList suspects)

160+ (suspect : S.toList suspects)

160 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

161 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

161 addToQueueRHS (uconstraint suspect) (Var var)

162 addToQueueRHS (uconstraint suspect) (Var var)

162 updateUpperBoundOf _ UVal{} _ = return ()

163 updateUpperBoundOf _ UVal{} _ = return ()

src/Idris/Core/DeepSeq.hs+8−1

@@ -51,6 +51,13 @@ instance NFData Provenance where

51 rnf (SourceTerm x1) = rnf x1 `seq` ()

52 rnf (TooManyArgs x1) = rnf x1 `seq` ()

53

54+instance NFData UConstraint where

55+ rnf (ULT x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

56+ rnf (ULE x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

57+

58+instance NFData ConstraintFC where

59+ rnf (ConstraintFC x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

60+

54instance NFData Err where

61instance NFData Err where

55 rnf (Msg x1) = rnf x1 `seq` ()

62 rnf (Msg x1) = rnf x1 `seq` ()

56 rnf (InternalMsg x1) = rnf x1 `seq` ()

63 rnf (InternalMsg x1) = rnf x1 `seq` ()

@@ -86,7 +93,7 @@ instance NFData Err where

86 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

93 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

87 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

94 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

88 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

95 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

89− rnf UniverseError = ()

96+ rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

90 rnf ProgramLineComment = ()

97 rnf ProgramLineComment = ()

91 rnf (Inaccessible x1) = rnf x1 `seq` ()

98 rnf (Inaccessible x1) = rnf x1 `seq` ()

92 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

99 rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()

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

@@ -162,7 +162,8 @@ data Err' t

162 | CantResolveAlts [Name]

163 | IncompleteTerm t

164 | NoEliminator String t

165− | UniverseError

165+ | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

166+ -- ^ Location, bad universe, old domain, new domain, suspects

166 | UniqueError Universe Name

167 | UniqueError Universe Name

167 | UniqueKindError Universe Name

168 | UniqueKindError Universe Name

168 | ProgramLineComment

169 | ProgramLineComment

@@ -239,7 +240,6 @@ instance Sized Err where

239 size (NoRewriting trm) = size trm

240 size (NoRewriting trm) = size trm

240 size (CantResolveAlts _) = 1

241 size (CantResolveAlts _) = 1

241 size (IncompleteTerm trm) = size trm

242 size (IncompleteTerm trm) = size trm

242− size UniverseError = 1

243 size ProgramLineComment = 1

244 size (At fc err) = size fc + size err

245 size (Elaborating _ n err) = size err

@@ -775,11 +775,11 @@ instance Show UExp where

775-- | Universe constraints

776data UConstraint = ULT UExp UExp -- ^ Strictly less than

777 | ULE UExp UExp -- ^ Less than or equal to

778− deriving (Eq, Ord)

778+ deriving (Eq, Ord, Data, Typeable)

779

780data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,

781 ufc :: FC }

782− deriving Show

782+ deriving (Show, Data, Typeable)

783

784instance Eq ConstraintFC where

785 x == y = uconstraint x == uconstraint y

src/Idris/Delaborate.hs+8−1

@@ -311,7 +311,14 @@ pprintErr' i (NoEliminator s t)

311 text "Please note that 'induction' is experimental." <$>

312 text "Only types declared with '%elim' can be used." <$>

313 text "Consider writing a pattern matching definition instead."

314+pprintErr' i (UniverseError fc uexp old new suspects) =

314−pprintErr' i UniverseError = text "Universe inconsistency"

315+ text "Universe inconsistency." <>

316+ (indented . vsep) [ text "Working on:" <+> text (show uexp)

317+ , text "Old domain:" <+> text (show old)

318+ , text "New domain:" <+> text (show new)

319+ , text "Involved constraints:" <+>

320+ (indented . vsep) (map (text . show) suspects)

321+ ]

315pprintErr' i (UniqueError NullType n)

322pprintErr' i (UniqueError NullType n)

316 = text "Borrowed name" <+> annName' n (showbasic n)

323 = text "Borrowed name" <+> annName' n (showbasic n)

317 <+> text "must not be used on RHS"

324 <+> text "must not be used on RHS"

src/Idris/Error.hs+2

@@ -68,6 +68,7 @@ ierror = throwError

68tclift :: TC a -> Idris a

69tclift (OK v) = return v

70tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

71+tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err

71tclift (Error err) = throwError err

72tclift (Error err) = throwError err

72

73

73tctry :: TC a -> TC a -> Idris a

74tctry :: TC a -> TC a -> Idris a

@@ -78,6 +79,7 @@ tctry tc1 tc2

78

79

79getErrSpan :: Err -> FC

80getErrSpan :: Err -> FC

80getErrSpan (At fc _) = fc

81getErrSpan (At fc _) = fc

82+getErrSpan (UniverseError fc _ _ _ _) = fc

81getErrSpan _ = emptyFC

83getErrSpan _ = emptyFC

82

84

83--------------------------------------------------------------------

85--------------------------------------------------------------------

src/Idris/IBC.hs+1−1

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

41import Util.Zlib (decompressEither)

42

43ibcVersion :: Word16

44−ibcVersion = 106

44+ibcVersion = 107

45

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

src/Idris/Reflection.hs+3−1

@@ -847,7 +847,9 @@ reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [

847reflectErr (NoEliminator str t)

848 = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

849 reflect t]

850+reflectErr (UniverseError fc ue old new tys) =

851+ -- NB: loses information, but OK because this is not likely to be rewritten

850−reflectErr UniverseError = Var $ reflErrName "UniverseError"

852+ Var $ reflErrName "UniverseError"

851reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

853reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

852reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

854reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

853reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

855reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]

test/error001/expected+7−8

@@ -1,9 +1,8 @@

1test002.idr:1:6:Universe inconsistency.

2−Working on: z

2+ Working on: z

3−Old domain: Domain 6 6

3+ Old domain: (6,6)

4−New domain: Domain 6 5

4+ New domain: (6,5)

5−Involved constraints:

5+ Involved constraints:

6− ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

6+ ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

7− ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}

7+ ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}

8− ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

8+ ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

9−

test/error001/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris $@ test002.idr --check --noprelude

2+idris $@ test002.idr --check --noprelude --consolewidth 70

3rm -f *.ibc