git.iko.soy/Idris-dev
on master help sign in
Add %used directive for idris_crash
6d8bfbcEdwin Brady
libs/base/Debug/Error.idr+3−5
compare with master
unifiedsplit
@@ -12,8 +12,6 @@ error : {default (%runElab sourceLocation) loc : SourceLocation} ->
12 (message : String) ->
12 (message : String) ->
13 a
13 a
14error {loc = FileLoc filename (line, col) _} message =
14error {loc = FileLoc filename (line, col) _} message =
15− unsafePerformIO $
16− do let place = filename ++ " line " ++ show line ++ " column " ++ show col
15+ let place = filename ++ " line " ++ show line ++ " column " ++ show col
17− let message' = place ++ ": " ++ message
16+ message' = place ++ ": " ++ message in
18− putStrLn message'
17+ idris_crash message'
19− exit 1
libs/prelude/Builtins.idr+3−1
@@ -179,9 +179,11 @@ assert_unreachable : a
179-- compiled as primitive
179-- compiled as primitive
180
180
181||| Abort immediately with an error message
181||| Abort immediately with an error message
182−idris_crash : String -> a
182+idris_crash : (msg : String) -> a
183-- compiled as primitive
183-- compiled as primitive
184
184
185+%used idris_crash msg
186+
185||| Subvert the type checker. This function is abstract, so it will not reduce in
187||| Subvert the type checker. This function is abstract, so it will not reduce in
186||| the type checker. Use it with care - it can result in segfaults or worse!
188||| the type checker. Use it with care - it can result in segfaults or worse!
187export
189export