4a5c677 · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+4

compare with master

unifiedsplit

@@ -178,6 +178,10 @@ assert_total x = x

178assert_unreachable : a

179-- compiled as primitive

180

181+||| Abort immediately with an error message

182+idris_crash : String -> a

183+-- compiled as primitive

184+

181||| Subvert the type checker. This function is abstract, so it will not reduce in

185||| Subvert the type checker. This function is abstract, so it will not reduce in

182||| the type checker. Use it with care - it can result in segfaults or worse!

186||| the type checker. Use it with care - it can result in segfaults or worse!

183export

187export

libs/prelude/Prelude/Strings.idr+19−14

@@ -45,7 +45,8 @@ foldl1 f (x::xs) = foldl f x xs

45||| ```

46partial

47strHead : String -> Char

48+strHead "" = idris_crash "Prelude.Strings: attempt to take the head of an empty string"

48−strHead = prim__strHead

49+strHead x = prim__strHead x

49

50

50||| Returns the characters specified after the head of the string.

51||| Returns the characters specified after the head of the string.

51|||

52|||

@@ -59,7 +60,8 @@ strHead = prim__strHead

59||| ```

60||| ```

60partial

61partial

61strTail : String -> String

62strTail : String -> String

63+strTail "" = idris_crash "Prelude.Strings: attempt to take the tail of an empty string"

62−strTail = prim__strTail

64+strTail xs = prim__strTail xs

63

65

64||| Adds a character to the front of the specified string.

66||| Adds a character to the front of the specified string.

65|||

67|||

@@ -72,6 +74,18 @@ strTail = prim__strTail

72strCons : Char -> String -> String

74strCons : Char -> String -> String

73strCons = prim__strCons

75strCons = prim__strCons

74

76

77+||| Returns the length of the string.

78+|||

79+||| ```idris example

80+||| length ""

81+||| ```

82+||| ```idris example

83+||| length "ABC"

84+||| ```

85+length : String -> Nat

86+length = fromInteger . prim__zextInt_BigInt . prim_lenString

87+

88+

75||| Returns the nth character (starting from 0) of the specified string.

89||| Returns the nth character (starting from 0) of the specified string.

76|||

90|||

77||| Precondition: '0 < i < length s' for 'strIndex s i'.

91||| Precondition: '0 < i < length s' for 'strIndex s i'.

@@ -81,7 +95,9 @@ strCons = prim__strCons

81||| ```

95||| ```

82partial

96partial

83strIndex : String -> Int -> Char

97strIndex : String -> Int -> Char

98+strIndex x i = if (i < 0 || i >= cast (length x))

99+ then idris_crash "Prelude.Strings: String index out of bounds"

84−strIndex = prim__strIndex

100+ else prim__strIndex x i

85

101

86||| Reverses the elements within a String.

102||| Reverses the elements within a String.

87|||

103|||

@@ -297,17 +313,6 @@ unlines' (l::ls) = l ++ '\n' :: unlines' ls

297unlines : List String -> String

313unlines : List String -> String

298unlines = pack . unlines' . map unpack

314unlines = pack . unlines' . map unpack

299

315

300−||| Returns the length of the string.

301−|||

302−||| ```idris example

303−||| length ""

304−||| ```

305−||| ```idris example

306−||| length "ABC"

307−||| ```

308−length : String -> Nat

309−length = fromInteger . prim__zextInt_BigInt . prim_lenString

310−

311||| Returns a substring of a given string

316||| Returns a substring of a given string

312|||

317|||

313||| @ index The (zero based) index of the string to extract. If this is

318||| @ index The (zero based) index of the string to extract. If this is

rts/idris_rts.c+5

@@ -595,6 +595,11 @@ VAL idris_readStr(VM* vm, FILE* h) {

595 return ret;

596}

597

598+void idris_crash(char* msg) {

599+ fprintf(stderr, "%s\n", msg);

600+ exit(1);

601+}

602+

598VAL idris_strHead(VM* vm, VAL str) {

603VAL idris_strHead(VM* vm, VAL str) {

599 return idris_strIndex(vm, str, 0);

604 return idris_strIndex(vm, str, 0);

600}

605}

rts/idris_rts.h+3

@@ -364,6 +364,9 @@ VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data);

364VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset);

365VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data);

366

367+// Crash with a message (used for partial primitives)

368+void idris_crash(char* msg);

369+

367// String primitives

370// String primitives

368VAL idris_concat(VM* vm, VAL l, VAL r);

371VAL idris_concat(VM* vm, VAL l, VAL r);

369VAL idris_strlt(VM* vm, VAL l, VAL r);

372VAL idris_strlt(VM* vm, VAL l, VAL r);

src/IRTS/CodegenC.hs+1

@@ -617,6 +617,7 @@ doOp v (LIntCh ITNative) args = v ++ creg (last args)

617doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

618

619doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

620+doOp v LCrash [x] = "idris_crash(GETSTR(" ++ creg x ++ "))"

620doOp v LNoOp args = v ++ creg (last args)

621doOp v LNoOp args = v ++ creg (last args)

621

622

622-- Pointer primitives (declared as %extern in Builtins.idr)

623-- Pointer primitives (declared as %extern in Builtins.idr)

src/IRTS/Compiler.hs+5

@@ -260,6 +260,11 @@ irTerm top vs env tm@(App _ f a) = do

260 | u == txt "assert_unreachable"

261 -> return $ LError $ "ABORT: Reached an unreachable case in " ++ show top

262

263+ (P _ (UN u) _, [_, msg])

264+ | u == txt "idris_crash"

265+ -> do msg' <- irTerm top vs env msg

266+ return $ LOp LCrash [msg']

267+

263 -- TMP HACK - until we get inlining.

268 -- TMP HACK - until we get inlining.

264 (P _ (UN r) _, [_, _, _, _, _, arg])

269 (P _ (UN r) _, [_, _, _, _, _, arg])

265 | r == txt "replace"

270 | r == txt "replace"

src/IRTS/Lang.hs+2

@@ -92,6 +92,8 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

92 | LPar -- evaluate argument anywhere, possibly on another

93 -- core or another machine. 'id' is a valid implementation

94 | LExternal Name

95+ | LCrash

96+

95 | LNoOp

97 | LNoOp

96 deriving (Show, Eq, Generic)

98 deriving (Show, Eq, Generic)

97

99

src/Idris/AbsSyntaxTree.hs+1

@@ -336,6 +336,7 @@ primDefs = [ sUN "unsafePerformPrimIO"

336 , sUN "mkForeignPrim"

337 , sUN "void"

338 , sUN "assert_unreachable"

339+ , sUN "idris_crash"

339 ]

340 ]

340

341

341-- information that needs writing for the current module's .ibc file

342-- information that needs writing for the current module's .ibc file