bac75d0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'AddMissingStrLen' of https://github.com/JanBessai/Idris-dev into JanBessai-AddMissingStrLen

bac75d0Edwin Brady14 years ago

lib/Prelude/Strings.idr+3

compare with master

unifiedsplit

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

115unwords : List String -> String

116unwords = pack . unwords' . map unpack

117

118+length : String -> Nat

119+length = fromInteger . prim_lenString

120+

src/Idris/Primitives.hs+3

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

332 (2, LStrEq) total,

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

334 (2, LStrLt) total,

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

336+ (1, LStrLen) total,

335 -- Conversions

337 -- Conversions

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

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

337 (1, LStrInt) total,

339 (1, LStrInt) total,

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

622p_floatFloor = p_fPrim (fromInteger . floor)

624p_floatFloor = p_fPrim (fromInteger . floor)

623p_floatCeil = p_fPrim (fromInteger . ceiling)

625p_floatCeil = p_fPrim (fromInteger . ceiling)

624

626

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

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

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

626p_strHead _ = Nothing

629p_strHead _ = Nothing

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

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

test/reg012/run+1−1

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

1#!/bin/bash

2idris $@ reg012.lidr --check

3−rm -f reg012 *.ibc

3+rm -f *.ibc

test/reg013/expectednew file+3

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

1+5

2+1

3+0

test/reg013/reg013.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/reg013/runnew file+4

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

1+#!/bin/bash

2+idris $@ reg013.idr -o reg013

3+./reg013

4+rm -f reg013 *.ibc

tutorial/idris-tutorial.pdf

Binary file not shown.