@@ -9,6 +9,7 @@ import Core.Evaluate
99import Core.CaseTree
1010
1111import Control.Monad.State
12+import Data.List
1213
1314import Epic.Epic hiding (Term, Type, Name, fn, compile)
1415import qualified Epic.Epic as E
@@ -16,13 +17,18 @@ import qualified Epic.Epic as E
1617primDefs = [UN "mkForeign", UN "FalseElim"]
1718
1819compile :: FilePath -> Idris ()
19−compile f = do ds <- mkDecls
20+compile f = do checkMVs
21+ ds <- mkDecls
2022 objs <- getObjectFiles
2123 libs <- getLibs
2224 hdrs <- getHdrs
2325 let incs = map Include hdrs
2426 lift $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")
2527 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
28+ where checkMVs = do i <- get
29+ case idris_metavars i \\ primDefs of
30+ [] -> return ()
31+ ms -> fail $ "There are undefined metavariables: " ++ show ms
2632
2733mkDecls :: Idris [EpicDecl]
2834mkDecls = do i <- getIState