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

git.iko.soy/Idris-dev

Richer universe error objects

Now, they are reported using the standard infrastructure.

commit8ab1ac6c29d89245bc94dacfffc09f1b560c913d authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 28 Apr 2015, 12:01 (11 years ago) parent66c9c38

10 files changed+68−26

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+26−2 src/Idris/Core/Constraints.hs+8−7 src/Idris/Core/DeepSeq.hs+8−1 src/Idris/Core/TT.hs+4−4 src/Idris/Delaborate.hs+8−1 src/Idris/Error.hs+2 src/Idris/IBC.hs+1−1 src/Idris/Reflection.hs+3−1 test/error001/expected+7−8 test/error001/run+1−1

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

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

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

44module Idris.Core.Binary where

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

7+import Control.Monad (liftM2)

69import Data.Binary

710import Data.Vector.Binary

811import qualified Data.Text as T

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

4346 return (TooManyArgs x1)

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

4548

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+

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

4766 put (Msg str) = do putWord8 0

4867 put str

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

97116 put ns

98117 put (IncompleteTerm t) = do putWord8 17

99118 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

101125 put (UniqueError u n) = do putWord8 19

102126 put u

103127 put n

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

181205 15 -> fmap (CantResolve False) get

182206 16 -> fmap CantResolveAlts get

183207 17 -> fmap IncompleteTerm get

184− 18 -> return UniverseError

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

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

186210 return $ UniqueError x y

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

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

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

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

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

147147

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

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

150+

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

149152 updateUpperBoundOf suspect (UVar var) upper = do

150153 doms <- gets domainStore

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

152155 let newDom = Domain lower upper

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

154− $ "Universe inconsistency."

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

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

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

158− : "Involved constraints: "

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

156+ when (wipeOut newDom) $

157+ lift $ Error $

158+ UniverseError (ufc suspect) (UVar var)

159+ (asPair oldDom) (asPair newDom)

160+ (suspect : S.toList suspects)

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

161162 addToQueueRHS (uconstraint suspect) (Var var)

162163 updateUpperBoundOf _ UVal{} _ = return ()

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

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

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

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

5353

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+

5461instance NFData Err where

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

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

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

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

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

8895 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` ()

9097 rnf ProgramLineComment = ()

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

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

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

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

162162 | CantResolveAlts [Name]

163163 | IncompleteTerm t

164164 | NoEliminator String t

165− | UniverseError

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

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

166167 | UniqueError Universe Name

167168 | UniqueKindError Universe Name

168169 | ProgramLineComment

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

239240 size (NoRewriting trm) = size trm

240241 size (CantResolveAlts _) = 1

241242 size (IncompleteTerm trm) = size trm

242− size UniverseError = 1

243243 size ProgramLineComment = 1

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

245245 size (Elaborating _ n err) = size err

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

775775-- | Universe constraints

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

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

778− deriving (Eq, Ord)

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

779779

780780data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,

781781 ufc :: FC }

782− deriving Show

782+ deriving (Show, Data, Typeable)

783783

784784instance Eq ConstraintFC where

785785 x == y = uconstraint x == uconstraint y

src/Idris/Delaborate.hs+8−1

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

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

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

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

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

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

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+ ]

315322pprintErr' i (UniqueError NullType n)

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

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

src/Idris/Error.hs+2

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

6868tclift :: TC a -> Idris a

6969tclift (OK v) = return v

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

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

7172tclift (Error err) = throwError err

7273

7374tctry :: TC a -> TC a -> Idris a

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

7879

7980getErrSpan :: Err -> FC

8081getErrSpan (At fc _) = fc

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

8183getErrSpan _ = emptyFC

8284

8385--------------------------------------------------------------------

src/Idris/IBC.hs+1−1

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

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 106

44+ibcVersion = 107

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

src/Idris/Reflection.hs+3−1

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

847847reflectErr (NoEliminator str t)

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

849849 reflect t]

850−reflectErr UniverseError = Var $ reflErrName "UniverseError"

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

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

852+ Var $ reflErrName "UniverseError"

851853reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

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

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

test/error001/expected+7−8

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

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

2−Working on: z

3−Old domain: Domain 6 6

4−New domain: Domain 6 5

5−Involved constraints:

6− ConstraintFC {uconstraint = z <= a1, 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}

9−

2+ Working on: z

3+ Old domain: (6,6)

4+ New domain: (6,5)

5+ Involved constraints:

6+ ConstraintFC {uconstraint = z <= a1, 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}

test/error001/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc