diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 55d6a8d..77f1fe1 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -305,13 +305,17 @@ toCDef tags n (TCon tag arity _ _ _ _) -- We do want to be able to compile these, but also report an error at run time -- (and, TODO: warn at compile time) toCDef tags n (Hole _ _) - = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++ show n) + = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++ + show !(getFullName n)) toCDef tags n (Guess _ _) - = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++ show n) + = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++ + show !(getFullName n)) toCDef tags n (BySearch _ _ _) - = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++ show n) + = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++ + show !(getFullName n)) toCDef tags n def - = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++ show (n, def)) + = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++ + show (!(getFullName n), def)) export compileExp : {auto c : Ref Ctxt Defs} -> diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 2db1160..29a1540 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -548,6 +548,11 @@ calcRefs at fn | Just _ => pure () -- already done let metas = getMetas tree_ct let refs = addRefs at metas tree_ct + traverse_ addToSave (keys metas) + + logC 5 (do fulln <- getFullName fn + refns <- traverse getFullName (keys refs) + pure (show fulln ++ " refers to " ++ show refns)) addDef fn (record { refersToM = Just refs } gdef) traverse_ (calcRefs at) (keys refs) diff --git a/tests/Main.idr b/tests/Main.idr index a5e3c8a..6617436 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -31,12 +31,12 @@ idrisTests "coverage001", "coverage002", "coverage003", "coverage004", "error001", "error002", "error003", "error004", "error005", "error006", + "import001", "import002", "interactive001", "interactive002", "interactive003", "interactive004", "interactive005", "interactive006", "interactive007", "interactive008", "interactive009", "interactive010", "interactive011", "interactive012", "interface001", "interface002", "interface003", "interface004", "interface005", - "import001", "import002", "lazy001", "linear001", "linear002", "linear003", "linear004", "linear005", "perror001", "perror002", "perror003", "perror004", "perror005",