0e6138f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

added forgotten LStrLen primitive and length function for String

commit0e6138fa95d56dec6884fee8c22f3305d5977214 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateSat 16 Mar 2013, 20:08 (14 years ago) parent2686158

5 files changed+21

compare with master

unifiedsplit

lib/Prelude/Strings.idr+3 src/Idris/Primitives.hs+3 test/reg012/expected+3 test/reg012/reg012.idr+8 test/reg012/run+4

lib/Prelude/Strings.idr+3

@@ -115,3 +115,6 @@ unwords' ws = (foldr1 addSpace ws)

115115unwords : List String -> String

116116unwords = pack . unwords' . map unpack

117117

118+length : String -> Nat

119+length = fromInteger . prim_lenString

120+

src/Idris/Primitives.hs+3

@@ -332,6 +332,8 @@ primitives =

332332 (2, LStrEq) total,

333333 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

334334 (2, LStrLt) total,

335+ Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

336+ (1, LStrLen) total,

335337 -- Conversions

336338 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

337339 (1, LStrInt) total,

@@ -622,6 +624,7 @@ p_floatSqrt = p_fPrim sqrt

622624p_floatFloor = p_fPrim (fromInteger . floor)

623625p_floatCeil = p_fPrim (fromInteger . ceiling)

624626

627+p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

625628p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

626629p_strHead _ = Nothing

627630p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

test/reg012/expectednew file+3

@@ -0,0 +1,3 @@

1+5

2+1

3+0

test/reg012/reg012.idrnew file+8

@@ -0,0 +1,8 @@

1+module Main

3+main : IO ()

4+main = do

5+ print $ prim_lenString "hallo"

6+ print $ prim_lenString "1"

7+ print $ prim_lenString ""

test/reg012/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ reg012.idr -o reg012

3+./reg012

4+rm -f reg012 *.ibc