dde7fc3 · Idris-dev · git.iko.soy

src/Core/TT.hs+2

compare with master

unifiedsplit

@@ -49,6 +49,7 @@ data Err = Msg String

49 -- Bool indicates recoverability, True indicates more info may make

50 -- unification succeed

51 | NoSuchVariable Name

52+ | NoTypeDecl Name

52 | NotInjective Term Term Term

53 | NotInjective Term Term Term

53 | CantResolve Term

54 | CantResolve Term

54 | CantResolveAlts [String]

55 | CantResolveAlts [String]

@@ -64,6 +65,7 @@ instance Sized Err where

64 size (InternalMsg msg) = length msg

65 size (InternalMsg msg) = length msg

65 size (CantUnify _ left right err _ score) = size left + size right + size err

66 size (CantUnify _ left right err _ score) = size left + size right + size err

66 size (NoSuchVariable name) = size name

67 size (NoSuchVariable name) = size name

68+ size (NoTypeDecl name) = size name

67 size (NotInjective l c r) = size l + size c + size r

69 size (NotInjective l c r) = size l + size c + size r

68 size (CantResolve trm) = size trm

70 size (CantResolve trm) = size trm

69 size (CantResolveAlts _) = 1

71 size (CantResolveAlts _) = 1

src/Idris/AbsSyntaxTree.hs+1

@@ -245,6 +245,7 @@ inlinable = elem Inlinable

245data PDecl' t = PFix FC Fixity [String] -- fixity declaration

246 | PTy SyntaxInfo FC FnOpts Name t -- type declaration

247 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

248+ | PCAF FC Name t -- top level constant

248 | PData SyntaxInfo FC (PData' t) -- data declaration

249 | PData SyntaxInfo FC (PData' t) -- data declaration

249 | PParams FC [(Name, t)] [PDecl' t] -- params block

250 | PParams FC [(Name, t)] [PDecl' t] -- params block

250 | PNamespace String [PDecl' t] -- new namespace

251 | PNamespace String [PDecl' t] -- new namespace

src/Idris/Delaborate.hs+1

@@ -94,6 +94,7 @@ pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p

94 show (delab i y)

95pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

96pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

97+pshow i (NoTypeDecl n) = "No type declaration for " ++ show n

97pshow i (NoSuchVariable n) = "No such variable " ++ show n

98pshow i (NoSuchVariable n) = "No such variable " ++ show n

98pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)

99pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)

99pshow i UniverseError = "Universe inconsistency"

100pshow i UniverseError = "Universe inconsistency"

src/Idris/ElabDecls.hs+8−1

@@ -221,7 +221,14 @@ elabCon info syn tn (n, t_in, fc)

221

222elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

223elabClauses info fc opts n_in cs = let n = liftname info n_in in

224+ do ctxt <- getContext

225+ -- Check n actually exists

226+ case lookupTy Nothing n ctxt of

227+ [] -> tclift $ tfail $ (At fc (NoTypeDecl n))

228+ _ -> return ()

224− do pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs

229+ pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs

230+

231+

225 solveDeferred n

232 solveDeferred n

226 let pats = mapMaybe id pats_in

233 let pats = mapMaybe id pats_in

227 logLvl 3 (showSep "\n" (map (\ (l,r) ->

234 logLvl 3 (showSep "\n" (map (\ (l,r) ->

src/Idris/IBC.hs+8

@@ -857,6 +857,10 @@ instance (Binary t) => Binary (PDecl' t) where

857 PDSL x1 x2 -> do putWord8 9

858 put x1

859 put x2

860+ PCAF x1 x2 x3 -> do putWord8 10

861+ put x1

862+ put x2

863+ put x3

860 get

864 get

861 = do i <- getWord8

865 = do i <- getWord8

862 case i of

866 case i of

@@ -912,6 +916,10 @@ instance (Binary t) => Binary (PDecl' t) where

912 9 -> do x1 <- get

916 9 -> do x1 <- get

913 x2 <- get

917 x2 <- get

914 return (PDSL x1 x2)

918 return (PDSL x1 x2)

919+ 10 -> do x1 <- get

920+ x2 <- get

921+ x3 <- get

922+ return (PCAF x1 x2 x3)

915 _ -> error "Corrupted binary data for PDecl'"

923 _ -> error "Corrupted binary data for PDecl'"

916

924

917instance Binary SyntaxInfo where

925instance Binary SyntaxInfo where