c6ec808 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow programs with holes to be compiled

c6ec808Edwin Brady11 years ago

CHANGELOG+2

compare with master

unifiedsplit

@@ -79,6 +79,8 @@ Minor language changes

79* More flexible holes.

80 Holes can now depend on other holes in a term (such as implicit arguments

81 which may be inferred from the definition of the hole).

82+* Programs with holes can now be compiled.

83+ Attempting to evaluate an expression with a hole results in a run time error.

83New in 0.10:

85New in 0.10:

84============

86============

src/IRTS/Compiler.hs+7−1

@@ -18,6 +18,7 @@ import Idris.AbsSyntaxTree

18import Idris.ASTUtils

19import Idris.Erasure

20import Idris.Error

21+import Idris.Output

22import Debug.Trace

23import Debug.Trace

@@ -112,7 +113,9 @@ compile codegen f mtm

112 where checkMVs = do i <- getIState

113 where checkMVs = do i <- getIState

113 case map fst (idris_metavars i) \\ primDefs of

114 case map fst (idris_metavars i) \\ primDefs of

114 [] -> return ()

115 [] -> return ()

115− ms -> ifail $ "There are undefined holes: " ++ show ms

116+ ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms

117+ iputStrLn "\nEvaluation of any of these will crash at run time."

118+ return ()

116 checkTotality = do i <- getIState

119 checkTotality = do i <- getIState

117 case idris_totcheckfail i of

120 case idris_totcheckfail i of

118 [] -> return ()

121 [] -> return ()

@@ -227,6 +230,9 @@ irTerm :: Vars -> [Name] -> Term -> Idris LExp

227irTerm vs env tm@(App _ f a) = do

230irTerm vs env tm@(App _ f a) = do

228 ist <- getIState

231 ist <- getIState

229 case unApply tm of

232 case unApply tm of

233+ (P _ n _, args)

234+ | n `elem` map fst (idris_metavars ist) \\ primDefs

235+ -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n

230 (P _ (UN m) _, args)

236 (P _ (UN m) _, args)

231 | m == txt "mkForeignPrim"

237 | m == txt "mkForeignPrim"

232 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits

238 -> doForeign vs env (reverse (drop 4 args)) -- drop implicits