dde7fc3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Report error for missing type declaration

commitdde7fc3f22022b3c81a08dff6672f6c0483b08f4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 29 Sep 2012, 14:45 (14 years ago) parent0de6d2d

5 files changed+20−1

compare with master

unifiedsplit

src/Core/TT.hs+2 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+8−1 src/Idris/IBC.hs+8

src/Core/TT.hs+2

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

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

5050 -- unification succeed

5151 | NoSuchVariable Name

52+ | NoTypeDecl Name

5253 | NotInjective Term Term Term

5354 | CantResolve Term

5455 | CantResolveAlts [String]

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

6465 size (InternalMsg msg) = length msg

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

6667 size (NoSuchVariable name) = size name

68+ size (NoTypeDecl name) = size name

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

6870 size (CantResolve trm) = size trm

6971 size (CantResolveAlts _) = 1

src/Idris/AbsSyntaxTree.hs+1

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

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

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

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

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

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

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

250251 | 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

9494 show (delab i y)

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

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

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

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

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

99100pshow i UniverseError = "Universe inconsistency"

src/Idris/ElabDecls.hs+8−1

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

221221

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

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

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

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

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

230+

231+

225232 solveDeferred n

226233 let pats = mapMaybe id pats_in

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

src/Idris/IBC.hs+8

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

857857 PDSL x1 x2 -> do putWord8 9

858858 put x1

859859 put x2

860+ PCAF x1 x2 x3 -> do putWord8 10

861+ put x1

862+ put x2

863+ put x3

860864 get

861865 = do i <- getWord8

862866 case i of

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

912916 9 -> do x1 <- get

913917 x2 <- get

914918 return (PDSL x1 x2)

919+ 10 -> do x1 <- get

920+ x2 <- get

921+ x3 <- get

922+ return (PCAF x1 x2 x3)

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

916924

917925instance Binary SyntaxInfo where