@@ -9,6 +9,7 @@ import Core.Evaluate
9import Core.CaseTree
9import Core.CaseTree
11import Control.Monad.State
11import Control.Monad.State
13import Epic.Epic hiding (Term, Type, Name, fn, compile)
14import Epic.Epic hiding (Term, Type, Name, fn, compile)
14import qualified Epic.Epic as E
15import qualified Epic.Epic as E
@@ -16,13 +17,18 @@ import qualified Epic.Epic as E
16primDefs = [UN "mkForeign", UN "FalseElim"]
17primDefs = [UN "mkForeign", UN "FalseElim"]
18compile :: FilePath -> Idris ()
19compile :: FilePath -> Idris ()
20+compile f = do checkMVs
19−compile f = do ds <- mkDecls
21+ ds <- mkDecls
20 objs <- getObjectFiles
22 objs <- getObjectFiles
21 libs <- getLibs
23 libs <- getLibs
22 hdrs <- getHdrs
24 hdrs <- getHdrs
23 let incs = map Include hdrs
25 let incs = map Include hdrs
24 lift $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")
26 lift $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")
25 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
27 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
28+ where checkMVs = do i <- get
29+ case idris_metavars i \\ primDefs of
31+ ms -> fail $ "There are undefined metavariables: " ++ show ms
27mkDecls :: Idris [EpicDecl]
33mkDecls :: Idris [EpicDecl]
28mkDecls = do i <- getIState
34mkDecls = do i <- getIState