Add idris_crash function

Because sometimes all you can do is give up (e.g. failing to allocate
memory for some crucial thing).

libs/base/System/File.idr

@@ -26,7 +26,7 @@ prim_fileErrno : PrimIO Int
 
 %foreign support "idris2_readLine"
 prim__readLine : FilePtr -> PrimIO (Ptr String)
-%foreign support "idris2_readLine"
+%foreign support "idris2_readChars"
 prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
 %foreign support "idris2_writeLine"
 prim__writeLine : FilePtr -> String -> PrimIO Int

libs/prelude/Builtin.idr

@@ -140,3 +140,7 @@ trans Refl Refl = Refl
 public export
 believe_me : a -> b
 believe_me = prim__believe_me _ _
+
+export partial
+idris_crash : String -> a
+idris_crash = prim__crash _

src/Compiler/Scheme/Common.idr

@@ -156,6 +156,7 @@ schOp (Cast IntType CharType) [x] = op "integer->char" [x]
 schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"
 
 schOp BelieveMe [_,_,x] = x
+schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"
 
 ||| Extended primitives for the scheme backend, outside the standard set of primFn
 public export

src/Core/Primitives.idr

@@ -287,6 +287,12 @@ believeMeTy
       Bind emptyFC (UN "x") (Pi top Explicit (Local emptyFC Nothing _ (Later First))) $
       Local emptyFC Nothing _ (Later First)
 
+crashTy : ClosedTerm
+crashTy
+    = Bind emptyFC (UN "a") (Pi erased Explicit (TType emptyFC)) $
+      Bind emptyFC (UN "msg") (Pi top Explicit (PrimVal emptyFC StringType)) $
+      Local emptyFC Nothing _ (Later First)
+
 castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars)
 castTo IntType = castInt
 castTo IntegerType = castInteger
@@ -385,6 +391,7 @@ opName DoubleFloor = prim "doubleFloor"
 opName DoubleCeiling = prim "doubleCeiling"
 opName (Cast x y) = prim $ "cast_" ++ show x ++ show y
 opName BelieveMe = prim $ "believe_me"
+opName Crash = prim $ "crash"
 
 export
 allPrimitives : List Prim
@@ -416,7 +423,8 @@ allPrimitives =
      MkPrim StrAppend (arithTy StringType) isTotal,
      MkPrim StrReverse (predTy StringType StringType) isTotal,
      MkPrim StrSubstr (constTy3 IntType IntType StringType StringType) isTotal,
-     MkPrim BelieveMe believeMeTy isTotal] ++
+     MkPrim BelieveMe believeMeTy isTotal,
+     MkPrim Crash crashTy notCovering] ++
 
     [MkPrim DoubleExp doubleTy isTotal,
      MkPrim DoubleLog doubleTy isTotal,

src/Core/TT.idr

@@ -147,6 +147,7 @@ data PrimFn : Nat -> Type where
 
      Cast : Constant -> Constant -> PrimFn 1
      BelieveMe : PrimFn 3
+     Crash : PrimFn 2
 
 export
 Show (PrimFn arity) where
@@ -187,6 +188,7 @@ Show (PrimFn arity) where
   show DoubleCeiling = "op_doubleCeiling"
   show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y
   show BelieveMe = "believe_me"
+  show Crash = "crash"
 
 public export
 data PiInfo t = Implicit | Explicit | AutoImplicit | DefImplicit t

src/Core/TTC.idr

@@ -517,6 +517,7 @@ TTC (PrimFn n) where
 
   toBuf b (Cast x y) = do tag 99; toBuf b x; toBuf b y
   toBuf b BelieveMe = tag 100
+  toBuf b Crash = tag 101
 
   fromBuf {n} b
       = case n of
@@ -571,6 +572,7 @@ TTC (PrimFn n) where
                  37 => do ty <- fromBuf b; pure (BAnd ty)
                  38 => do ty <- fromBuf b; pure (BOr ty)
                  39 => do ty <- fromBuf b; pure (BXOr ty)
+                 101 => pure Crash
                  _ => corrupt "PrimFn 2"
 
       fromBuf3 : Ref Bin Binary ->